areasplit

54::  |- A e. dom area
55::  |- Q e. RR
56::  |- B = { <. x , y >. | ( <. x , y >. e. A /\ x <_ Q ) }
57::  |- C = { <. x , y >. | ( <. x , y >. e. A /\ Q <_ x ) }

*extract facts about A
58::dmarea         |- ( A e. dom area
	<-> ( A C_ ( RR X. RR ) /\ A. x e. RR ( A " { x } ) e. ( `' vol " RR )
	/\ ( x e. RR |-> ( vol ` ( A " { x } ) ) ) e. L^1 ) )
59:58:simp1bi   |- ( A e. dom area -> A C_ ( RR X. RR ) )
60:58:simp2bi    |- ( A e. dom area -> A. x e. RR ( A " { x } ) e. ( `' vol " RR ) )
61:54,59:ax-mp    |- A C_ ( RR X. RR )
62:54,60:ax-mp      |- A. x e. RR ( A " { x } ) e. ( `' vol " RR )
63:61:sseli   |- ( <. x , y >. e. A -> <. x , y >. e. ( RR X. RR ) )
*show A = B u. C
*first A C_ B u. C
64::elun1  |- ( <. x , y >. e. B -> <. x , y >. e. ( B u. C ) )
65::elun2  |- ( <. x , y >. e. C -> <. x , y >. e. ( B u. C ) )
66::letric         |- ( ( x e. RR /\ Q e. RR ) -> ( x <_ Q \/ Q <_ x ) )
67:55,66:mpan2   |- ( x e. RR -> ( x <_ Q \/ Q <_ x ) )
68::  |- ( ( <. x , y >. e. A /\ x <_ Q ) -> <. x , y >. e. B )
69:68,64:syl    |- ( ( <. x , y >. e. A /\ x <_ Q ) -> <. x , y >. e. ( B u. C ) )
70::  |- ( ( <. x , y >. e. A /\ Q <_ x ) -> <. x , y >. e. C )
71:70,65:syl    |- ( ( <. x , y >. e. A /\ Q <_ x ) -> <. x , y >. e. ( B u. C ) )
72:69,71:jaodan    |- ( ( <. x , y >. e. A /\ ( x <_ Q \/ Q <_ x ) ) -> <. x , y >. e. ( B u. C ) )
73:67,72:sylan2    |- ( ( <. x , y >. e. A /\ x e. RR ) -> <. x , y >. e. ( B u. C ) )
74::opelxp1  |- ( <. x , y >. e. ( RR X. RR ) -> x e. RR )
75:63,74:syl   |- ( <. x , y >. e. A -> x e. RR )
76:75:ancli   |- ( <. x , y >. e. A -> ( <. x , y >. e. A /\ x e. RR ) )
77:76,73:syl   |- ( <. x , y >. e. A ->  <. x , y >. e. ( B u. C ) )
78::ssel           |- ( &C1 C_ &C2 -> ( &C3 e. &C1 -> &C3 e. &C2 ) )
!79::  |- A C_ ( B u. C )
*second show B u. C C_ A
80::  |- ( B u. C ) C_ A
81:79,80:eqssi   |- A = ( B u. C )
*prove B e. dom area, C e. dom area
* B C_ ( RR X. RR )
82::simpl          |- ( ( <. x , y >. e. A /\ x <_ Q ) -> <. x , y >. e. A )
83:82:ssopab2i     |- { <. x , y >. | ( <. x , y >. e. A /\ x <_ Q ) } C_ { <. x , y >. | <. x , y >. e. A }
84:63:ssopab2i     |- { <. x , y >. | <. x , y >. e. A } C_ { <. x , y >. | <. x , y >. e. ( RR X. RR ) }
85:83,84:sstri    |- { <. x , y >. | ( <. x , y >. e. A /\ x <_ Q ) } C_ { <. x , y >. | <. x , y >. e. ( RR X. RR ) }
86:56,85:eqsstri    |- B C_ { <. x , y >. | <. x , y >. e. ( RR X. RR ) }
87::opelxp         |- ( <. x , y >. e. ( RR X. RR ) <-> ( x e. RR /\ y e. RR ) )
88:87:opabbii  |- { <. x , y >. | <. x , y >. e. ( RR X. RR ) } = { <. x , y >. | ( x e. RR /\ y e. RR ) }
89::df-xp          |- ( RR X. RR ) = { <. x , y >. | ( x e. RR /\ y e. RR ) }
90:89,88:eqtr4i    |- ( RR X. RR ) = { <. x , y >. | <. x , y >. e. ( RR X. RR ) }
91:86,90:sseqtr4i    |- B C_ ( RR X. RR )
* A. x e. RR ( B " { x } ) e. ( `' vol " RR )
92::  |- x <_ Q

*show area A = area B + area C

!93::              |- ( T. -> ( vol* ` ( R i^i S ) ) = 0 )
!94::              |- ( T. -> RR = ( R u. S ) )
!95::              |- ( ( T. /\ t e. RR ) -> A e. &C8 )
!96::              |- ( T. -> ( t e. R |-> A ) e. L^1 )
!97::              |- ( T. -> ( t e. S |-> A ) e. L^1 )
98:93,94,95,96,97:itgsplit
                   |- ( T. -> S. RR A _d t = ( S. R A _d t + S. S A _d t ) )