Metamath Proof Explorer

Theorem offsplitfpar

Description: Express the function operation map oF by the functions defined in fsplit and fpar . (Contributed by AV, 4-Jan-2024)

Ref Expression
Hypotheses fsplitfpar.h 
|- H = ( ( `' ( 1st |` ( _V X. _V ) ) o. ( F o. ( 1st |` ( _V X. _V ) ) ) ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. ( G o. ( 2nd |` ( _V X. _V ) ) ) ) )
fsplitfpar.s 
|- S = ( `' ( 1st |` _I ) |` A )
Assertion offsplitfpar 
|- ( ( ( F Fn A /\ G Fn A ) /\ ( F e. V /\ G e. W ) /\ ( .+ Fn C /\ ( ran F X. ran G ) C_ C ) ) -> ( .+ o. ( H o. S ) ) = ( F oF .+ G ) )

Proof

Step Hyp Ref Expression
1 fsplitfpar.h 
 |-  H = ( ( `' ( 1st |` ( _V X. _V ) ) o. ( F o. ( 1st |` ( _V X. _V ) ) ) ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. ( G o. ( 2nd |` ( _V X. _V ) ) ) ) )
2 fsplitfpar.s 
 |-  S = ( `' ( 1st |` _I ) |` A )
3 1 2 fsplitfpar 
 |-  ( ( F Fn A /\ G Fn A ) -> ( H o. S ) = ( a e. A |-> <. ( F ` a ) , ( G ` a ) >. ) )
4 3 coeq2d 
 |-  ( ( F Fn A /\ G Fn A ) -> ( .+ o. ( H o. S ) ) = ( .+ o. ( a e. A |-> <. ( F ` a ) , ( G ` a ) >. ) ) )
5 4 3ad2ant1 
 |-  ( ( ( F Fn A /\ G Fn A ) /\ ( F e. V /\ G e. W ) /\ ( .+ Fn C /\ ( ran F X. ran G ) C_ C ) ) -> ( .+ o. ( H o. S ) ) = ( .+ o. ( a e. A |-> <. ( F ` a ) , ( G ` a ) >. ) ) )
6 dffn3 
 |-  ( .+ Fn C <-> .+ : C --> ran .+ )
7 6 biimpi 
 |-  ( .+ Fn C -> .+ : C --> ran .+ )
8 7 adantr 
 |-  ( ( .+ Fn C /\ ( ran F X. ran G ) C_ C ) -> .+ : C --> ran .+ )
9 8 3ad2ant3 
 |-  ( ( ( F Fn A /\ G Fn A ) /\ ( F e. V /\ G e. W ) /\ ( .+ Fn C /\ ( ran F X. ran G ) C_ C ) ) -> .+ : C --> ran .+ )
10 simpl3r 
 |-  ( ( ( ( F Fn A /\ G Fn A ) /\ ( F e. V /\ G e. W ) /\ ( .+ Fn C /\ ( ran F X. ran G ) C_ C ) ) /\ a e. A ) -> ( ran F X. ran G ) C_ C )
11 simp1l 
 |-  ( ( ( F Fn A /\ G Fn A ) /\ ( F e. V /\ G e. W ) /\ ( .+ Fn C /\ ( ran F X. ran G ) C_ C ) ) -> F Fn A )
12 fnfvelrn 
 |-  ( ( F Fn A /\ a e. A ) -> ( F ` a ) e. ran F )
13 11 12 sylan 
 |-  ( ( ( ( F Fn A /\ G Fn A ) /\ ( F e. V /\ G e. W ) /\ ( .+ Fn C /\ ( ran F X. ran G ) C_ C ) ) /\ a e. A ) -> ( F ` a ) e. ran F )
14 simp1r 
 |-  ( ( ( F Fn A /\ G Fn A ) /\ ( F e. V /\ G e. W ) /\ ( .+ Fn C /\ ( ran F X. ran G ) C_ C ) ) -> G Fn A )
15 fnfvelrn 
 |-  ( ( G Fn A /\ a e. A ) -> ( G ` a ) e. ran G )
16 14 15 sylan 
 |-  ( ( ( ( F Fn A /\ G Fn A ) /\ ( F e. V /\ G e. W ) /\ ( .+ Fn C /\ ( ran F X. ran G ) C_ C ) ) /\ a e. A ) -> ( G ` a ) e. ran G )
17 13 16 opelxpd 
 |-  ( ( ( ( F Fn A /\ G Fn A ) /\ ( F e. V /\ G e. W ) /\ ( .+ Fn C /\ ( ran F X. ran G ) C_ C ) ) /\ a e. A ) -> <. ( F ` a ) , ( G ` a ) >. e. ( ran F X. ran G ) )
18 10 17 sseldd 
 |-  ( ( ( ( F Fn A /\ G Fn A ) /\ ( F e. V /\ G e. W ) /\ ( .+ Fn C /\ ( ran F X. ran G ) C_ C ) ) /\ a e. A ) -> <. ( F ` a ) , ( G ` a ) >. e. C )
19 9 18 cofmpt 
 |-  ( ( ( F Fn A /\ G Fn A ) /\ ( F e. V /\ G e. W ) /\ ( .+ Fn C /\ ( ran F X. ran G ) C_ C ) ) -> ( .+ o. ( a e. A |-> <. ( F ` a ) , ( G ` a ) >. ) ) = ( a e. A |-> ( .+ ` <. ( F ` a ) , ( G ` a ) >. ) ) )
20 df-ov 
 |-  ( ( F ` a ) .+ ( G ` a ) ) = ( .+ ` <. ( F ` a ) , ( G ` a ) >. )
21 20 eqcomi 
 |-  ( .+ ` <. ( F ` a ) , ( G ` a ) >. ) = ( ( F ` a ) .+ ( G ` a ) )
22 21 mpteq2i 
 |-  ( a e. A |-> ( .+ ` <. ( F ` a ) , ( G ` a ) >. ) ) = ( a e. A |-> ( ( F ` a ) .+ ( G ` a ) ) )
23 19 22 eqtrdi 
 |-  ( ( ( F Fn A /\ G Fn A ) /\ ( F e. V /\ G e. W ) /\ ( .+ Fn C /\ ( ran F X. ran G ) C_ C ) ) -> ( .+ o. ( a e. A |-> <. ( F ` a ) , ( G ` a ) >. ) ) = ( a e. A |-> ( ( F ` a ) .+ ( G ` a ) ) ) )
24 offval3 
 |-  ( ( F e. V /\ G e. W ) -> ( F oF .+ G ) = ( a e. ( dom F i^i dom G ) |-> ( ( F ` a ) .+ ( G ` a ) ) ) )
25 fndm 
 |-  ( F Fn A -> dom F = A )
26 fndm 
 |-  ( G Fn A -> dom G = A )
27 25 26 ineqan12d 
 |-  ( ( F Fn A /\ G Fn A ) -> ( dom F i^i dom G ) = ( A i^i A ) )
28 inidm 
 |-  ( A i^i A ) = A
29 27 28 eqtrdi 
 |-  ( ( F Fn A /\ G Fn A ) -> ( dom F i^i dom G ) = A )
30 29 mpteq1d 
 |-  ( ( F Fn A /\ G Fn A ) -> ( a e. ( dom F i^i dom G ) |-> ( ( F ` a ) .+ ( G ` a ) ) ) = ( a e. A |-> ( ( F ` a ) .+ ( G ` a ) ) ) )
31 24 30 sylan9eqr 
 |-  ( ( ( F Fn A /\ G Fn A ) /\ ( F e. V /\ G e. W ) ) -> ( F oF .+ G ) = ( a e. A |-> ( ( F ` a ) .+ ( G ` a ) ) ) )
32 31 eqcomd 
 |-  ( ( ( F Fn A /\ G Fn A ) /\ ( F e. V /\ G e. W ) ) -> ( a e. A |-> ( ( F ` a ) .+ ( G ` a ) ) ) = ( F oF .+ G ) )
33 32 3adant3 
 |-  ( ( ( F Fn A /\ G Fn A ) /\ ( F e. V /\ G e. W ) /\ ( .+ Fn C /\ ( ran F X. ran G ) C_ C ) ) -> ( a e. A |-> ( ( F ` a ) .+ ( G ` a ) ) ) = ( F oF .+ G ) )
34 5 23 33 3eqtrd 
 |-  ( ( ( F Fn A /\ G Fn A ) /\ ( F e. V /\ G e. W ) /\ ( .+ Fn C /\ ( ran F X. ran G ) C_ C ) ) -> ( .+ o. ( H o. S ) ) = ( F oF .+ G ) )