Metamath Proof Explorer

Theorem tfsconcatfv

Description: The value of the concatenation of two transfinite series. (Contributed by RP, 24-Feb-2025)

Ref Expression
Hypothesis tfsconcat.op 
|- .+ = ( a e. _V , b e. _V |-> ( a u. { <. x , y >. | ( x e. ( ( dom a +o dom b ) \ dom a ) /\ E. z e. dom b ( x = ( dom a +o z ) /\ y = ( b ` z ) ) ) } ) )
Assertion tfsconcatfv 
|- ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. ( C +o D ) ) -> ( ( A .+ B ) ` X ) = if ( X e. C , ( A ` X ) , ( B ` ( iota_ d e. D ( C +o d ) = X ) ) ) )

Proof

Step Hyp Ref Expression
1 tfsconcat.op 
 |-  .+ = ( a e. _V , b e. _V |-> ( a u. { <. x , y >. | ( x e. ( ( dom a +o dom b ) \ dom a ) /\ E. z e. dom b ( x = ( dom a +o z ) /\ y = ( b ` z ) ) ) } ) )
2 1 tfsconcatfv1 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. C ) -> ( ( A .+ B ) ` X ) = ( A ` X ) )
3 2 adantlr 
 |-  ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. ( C +o D ) ) /\ X e. C ) -> ( ( A .+ B ) ` X ) = ( A ` X ) )
4 simpr 
 |-  ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. ( C +o D ) ) /\ X e. C ) -> X e. C )
5 4 iftrued 
 |-  ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. ( C +o D ) ) /\ X e. C ) -> if ( X e. C , ( A ` X ) , ( B ` ( iota_ d e. D ( C +o d ) = X ) ) ) = ( A ` X ) )
6 3 5 eqtr4d 
 |-  ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. ( C +o D ) ) /\ X e. C ) -> ( ( A .+ B ) ` X ) = if ( X e. C , ( A ` X ) , ( B ` ( iota_ d e. D ( C +o d ) = X ) ) ) )
7 simpr 
 |-  ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. ( C +o D ) ) /\ -. X e. C ) -> -. X e. C )
8 7 iffalsed 
 |-  ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. ( C +o D ) ) /\ -. X e. C ) -> if ( X e. C , ( A ` X ) , ( B ` ( iota_ d e. D ( C +o d ) = X ) ) ) = ( B ` ( iota_ d e. D ( C +o d ) = X ) ) )
9 simpll 
 |-  ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. ( C +o D ) ) /\ -. X e. C ) -> ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) )
10 onss 
 |-  ( D e. On -> D C_ On )
11 10 adantl 
 |-  ( ( C e. On /\ D e. On ) -> D C_ On )
12 11 ad3antlr 
 |-  ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. ( C +o D ) ) /\ -. X e. C ) -> D C_ On )
13 simpllr 
 |-  ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. ( C +o D ) ) /\ -. X e. C ) -> ( C e. On /\ D e. On ) )
14 simplrl 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. ( C +o D ) ) -> C e. On )
15 oacl 
 |-  ( ( C e. On /\ D e. On ) -> ( C +o D ) e. On )
16 15 adantl 
 |-  ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( C +o D ) e. On )
17 onelon 
 |-  ( ( ( C +o D ) e. On /\ X e. ( C +o D ) ) -> X e. On )
18 16 17 sylan 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. ( C +o D ) ) -> X e. On )
19 ontri1 
 |-  ( ( C e. On /\ X e. On ) -> ( C C_ X <-> -. X e. C ) )
20 14 18 19 syl2anc 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. ( C +o D ) ) -> ( C C_ X <-> -. X e. C ) )
21 20 biimpar 
 |-  ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. ( C +o D ) ) /\ -. X e. C ) -> C C_ X )
22 simplr 
 |-  ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. ( C +o D ) ) /\ -. X e. C ) -> X e. ( C +o D ) )
23 oawordex2 
 |-  ( ( ( C e. On /\ D e. On ) /\ ( C C_ X /\ X e. ( C +o D ) ) ) -> E. d e. D ( C +o d ) = X )
24 13 21 22 23 syl12anc 
 |-  ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. ( C +o D ) ) /\ -. X e. C ) -> E. d e. D ( C +o d ) = X )
25 14 18 jca 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. ( C +o D ) ) -> ( C e. On /\ X e. On ) )
26 oawordeu 
 |-  ( ( ( C e. On /\ X e. On ) /\ C C_ X ) -> E! d e. On ( C +o d ) = X )
27 25 21 26 syl2an2r 
 |-  ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. ( C +o D ) ) /\ -. X e. C ) -> E! d e. On ( C +o d ) = X )
28 reuss 
 |-  ( ( D C_ On /\ E. d e. D ( C +o d ) = X /\ E! d e. On ( C +o d ) = X ) -> E! d e. D ( C +o d ) = X )
29 12 24 27 28 syl3anc 
 |-  ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. ( C +o D ) ) /\ -. X e. C ) -> E! d e. D ( C +o d ) = X )
30 riotacl 
 |-  ( E! d e. D ( C +o d ) = X -> ( iota_ d e. D ( C +o d ) = X ) e. D )
31 29 30 syl 
 |-  ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. ( C +o D ) ) /\ -. X e. C ) -> ( iota_ d e. D ( C +o d ) = X ) e. D )
32 1 tfsconcatfv2 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ ( iota_ d e. D ( C +o d ) = X ) e. D ) -> ( ( A .+ B ) ` ( C +o ( iota_ d e. D ( C +o d ) = X ) ) ) = ( B ` ( iota_ d e. D ( C +o d ) = X ) ) )
33 9 31 32 syl2anc 
 |-  ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. ( C +o D ) ) /\ -. X e. C ) -> ( ( A .+ B ) ` ( C +o ( iota_ d e. D ( C +o d ) = X ) ) ) = ( B ` ( iota_ d e. D ( C +o d ) = X ) ) )
34 riotasbc 
 |-  ( E! d e. D ( C +o d ) = X -> [. ( iota_ d e. D ( C +o d ) = X ) / d ]. ( C +o d ) = X )
35 29 34 syl 
 |-  ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. ( C +o D ) ) /\ -. X e. C ) -> [. ( iota_ d e. D ( C +o d ) = X ) / d ]. ( C +o d ) = X )
36 sbceq1g 
 |-  ( ( iota_ d e. D ( C +o d ) = X ) e. D -> ( [. ( iota_ d e. D ( C +o d ) = X ) / d ]. ( C +o d ) = X <-> [_ ( iota_ d e. D ( C +o d ) = X ) / d ]_ ( C +o d ) = X ) )
37 csbov2g 
 |-  ( ( iota_ d e. D ( C +o d ) = X ) e. D -> [_ ( iota_ d e. D ( C +o d ) = X ) / d ]_ ( C +o d ) = ( C +o [_ ( iota_ d e. D ( C +o d ) = X ) / d ]_ d ) )
38 csbvarg 
 |-  ( ( iota_ d e. D ( C +o d ) = X ) e. D -> [_ ( iota_ d e. D ( C +o d ) = X ) / d ]_ d = ( iota_ d e. D ( C +o d ) = X ) )
39 38 oveq2d 
 |-  ( ( iota_ d e. D ( C +o d ) = X ) e. D -> ( C +o [_ ( iota_ d e. D ( C +o d ) = X ) / d ]_ d ) = ( C +o ( iota_ d e. D ( C +o d ) = X ) ) )
40 37 39 eqtrd 
 |-  ( ( iota_ d e. D ( C +o d ) = X ) e. D -> [_ ( iota_ d e. D ( C +o d ) = X ) / d ]_ ( C +o d ) = ( C +o ( iota_ d e. D ( C +o d ) = X ) ) )
41 40 eqeq1d 
 |-  ( ( iota_ d e. D ( C +o d ) = X ) e. D -> ( [_ ( iota_ d e. D ( C +o d ) = X ) / d ]_ ( C +o d ) = X <-> ( C +o ( iota_ d e. D ( C +o d ) = X ) ) = X ) )
42 36 41 bitrd 
 |-  ( ( iota_ d e. D ( C +o d ) = X ) e. D -> ( [. ( iota_ d e. D ( C +o d ) = X ) / d ]. ( C +o d ) = X <-> ( C +o ( iota_ d e. D ( C +o d ) = X ) ) = X ) )
43 42 biimpa 
 |-  ( ( ( iota_ d e. D ( C +o d ) = X ) e. D /\ [. ( iota_ d e. D ( C +o d ) = X ) / d ]. ( C +o d ) = X ) -> ( C +o ( iota_ d e. D ( C +o d ) = X ) ) = X )
44 31 35 43 syl2anc 
 |-  ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. ( C +o D ) ) /\ -. X e. C ) -> ( C +o ( iota_ d e. D ( C +o d ) = X ) ) = X )
45 44 fveq2d 
 |-  ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. ( C +o D ) ) /\ -. X e. C ) -> ( ( A .+ B ) ` ( C +o ( iota_ d e. D ( C +o d ) = X ) ) ) = ( ( A .+ B ) ` X ) )
46 8 33 45 3eqtr2rd 
 |-  ( ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. ( C +o D ) ) /\ -. X e. C ) -> ( ( A .+ B ) ` X ) = if ( X e. C , ( A ` X ) , ( B ` ( iota_ d e. D ( C +o d ) = X ) ) ) )
47 6 46 pm2.61dan 
 |-  ( ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) /\ X e. ( C +o D ) ) -> ( ( A .+ B ) ` X ) = if ( X e. C , ( A ` X ) , ( B ` ( iota_ d e. D ( C +o d ) = X ) ) ) )