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