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 ) )