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 |
|
fsplit |
|- `' ( 1st |` _I ) = ( x e. _V |-> <. x , x >. ) |
4 |
3
|
reseq1i |
|- ( `' ( 1st |` _I ) |` A ) = ( ( x e. _V |-> <. x , x >. ) |` A ) |
5 |
2 4
|
eqtri |
|- S = ( ( x e. _V |-> <. x , x >. ) |` A ) |
6 |
5
|
fveq1i |
|- ( S ` a ) = ( ( ( x e. _V |-> <. x , x >. ) |` A ) ` a ) |
7 |
6
|
a1i |
|- ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> ( S ` a ) = ( ( ( x e. _V |-> <. x , x >. ) |` A ) ` a ) ) |
8 |
|
fvres |
|- ( a e. A -> ( ( ( x e. _V |-> <. x , x >. ) |` A ) ` a ) = ( ( x e. _V |-> <. x , x >. ) ` a ) ) |
9 |
|
eqidd |
|- ( a e. A -> ( x e. _V |-> <. x , x >. ) = ( x e. _V |-> <. x , x >. ) ) |
10 |
|
id |
|- ( x = a -> x = a ) |
11 |
10 10
|
opeq12d |
|- ( x = a -> <. x , x >. = <. a , a >. ) |
12 |
11
|
adantl |
|- ( ( a e. A /\ x = a ) -> <. x , x >. = <. a , a >. ) |
13 |
|
elex |
|- ( a e. A -> a e. _V ) |
14 |
|
opex |
|- <. a , a >. e. _V |
15 |
14
|
a1i |
|- ( a e. A -> <. a , a >. e. _V ) |
16 |
9 12 13 15
|
fvmptd |
|- ( a e. A -> ( ( x e. _V |-> <. x , x >. ) ` a ) = <. a , a >. ) |
17 |
8 16
|
eqtrd |
|- ( a e. A -> ( ( ( x e. _V |-> <. x , x >. ) |` A ) ` a ) = <. a , a >. ) |
18 |
17
|
adantl |
|- ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> ( ( ( x e. _V |-> <. x , x >. ) |` A ) ` a ) = <. a , a >. ) |
19 |
7 18
|
eqtrd |
|- ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> ( S ` a ) = <. a , a >. ) |
20 |
19
|
fveq2d |
|- ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> ( H ` ( S ` a ) ) = ( H ` <. a , a >. ) ) |
21 |
|
df-ov |
|- ( a H a ) = ( H ` <. a , a >. ) |
22 |
1
|
fpar |
|- ( ( F Fn A /\ G Fn A ) -> H = ( x e. A , y e. A |-> <. ( F ` x ) , ( G ` y ) >. ) ) |
23 |
22
|
adantr |
|- ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> H = ( x e. A , y e. A |-> <. ( F ` x ) , ( G ` y ) >. ) ) |
24 |
|
fveq2 |
|- ( x = a -> ( F ` x ) = ( F ` a ) ) |
25 |
24
|
adantr |
|- ( ( x = a /\ y = a ) -> ( F ` x ) = ( F ` a ) ) |
26 |
|
fveq2 |
|- ( y = a -> ( G ` y ) = ( G ` a ) ) |
27 |
26
|
adantl |
|- ( ( x = a /\ y = a ) -> ( G ` y ) = ( G ` a ) ) |
28 |
25 27
|
opeq12d |
|- ( ( x = a /\ y = a ) -> <. ( F ` x ) , ( G ` y ) >. = <. ( F ` a ) , ( G ` a ) >. ) |
29 |
28
|
adantl |
|- ( ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) /\ ( x = a /\ y = a ) ) -> <. ( F ` x ) , ( G ` y ) >. = <. ( F ` a ) , ( G ` a ) >. ) |
30 |
|
simpr |
|- ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> a e. A ) |
31 |
|
opex |
|- <. ( F ` a ) , ( G ` a ) >. e. _V |
32 |
31
|
a1i |
|- ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> <. ( F ` a ) , ( G ` a ) >. e. _V ) |
33 |
23 29 30 30 32
|
ovmpod |
|- ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> ( a H a ) = <. ( F ` a ) , ( G ` a ) >. ) |
34 |
21 33
|
syl5eqr |
|- ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> ( H ` <. a , a >. ) = <. ( F ` a ) , ( G ` a ) >. ) |
35 |
20 34
|
eqtrd |
|- ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> ( H ` ( S ` a ) ) = <. ( F ` a ) , ( G ` a ) >. ) |
36 |
|
eqid |
|- ( a e. _V |-> <. a , a >. ) = ( a e. _V |-> <. a , a >. ) |
37 |
36
|
fnmpt |
|- ( A. a e. _V <. a , a >. e. _V -> ( a e. _V |-> <. a , a >. ) Fn _V ) |
38 |
14
|
a1i |
|- ( a e. _V -> <. a , a >. e. _V ) |
39 |
37 38
|
mprg |
|- ( a e. _V |-> <. a , a >. ) Fn _V |
40 |
|
ssv |
|- A C_ _V |
41 |
|
fnssres |
|- ( ( ( a e. _V |-> <. a , a >. ) Fn _V /\ A C_ _V ) -> ( ( a e. _V |-> <. a , a >. ) |` A ) Fn A ) |
42 |
39 40 41
|
mp2an |
|- ( ( a e. _V |-> <. a , a >. ) |` A ) Fn A |
43 |
|
fsplit |
|- `' ( 1st |` _I ) = ( a e. _V |-> <. a , a >. ) |
44 |
43
|
reseq1i |
|- ( `' ( 1st |` _I ) |` A ) = ( ( a e. _V |-> <. a , a >. ) |` A ) |
45 |
2 44
|
eqtri |
|- S = ( ( a e. _V |-> <. a , a >. ) |` A ) |
46 |
45
|
fneq1i |
|- ( S Fn A <-> ( ( a e. _V |-> <. a , a >. ) |` A ) Fn A ) |
47 |
42 46
|
mpbir |
|- S Fn A |
48 |
47
|
a1i |
|- ( ( F Fn A /\ G Fn A ) -> S Fn A ) |
49 |
|
fvco2 |
|- ( ( S Fn A /\ a e. A ) -> ( ( H o. S ) ` a ) = ( H ` ( S ` a ) ) ) |
50 |
48 49
|
sylan |
|- ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> ( ( H o. S ) ` a ) = ( H ` ( S ` a ) ) ) |
51 |
|
fveq2 |
|- ( x = a -> ( G ` x ) = ( G ` a ) ) |
52 |
24 51
|
opeq12d |
|- ( x = a -> <. ( F ` x ) , ( G ` x ) >. = <. ( F ` a ) , ( G ` a ) >. ) |
53 |
|
eqid |
|- ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. ) = ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. ) |
54 |
52 53 31
|
fvmpt |
|- ( a e. A -> ( ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. ) ` a ) = <. ( F ` a ) , ( G ` a ) >. ) |
55 |
54
|
adantl |
|- ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> ( ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. ) ` a ) = <. ( F ` a ) , ( G ` a ) >. ) |
56 |
35 50 55
|
3eqtr4d |
|- ( ( ( F Fn A /\ G Fn A ) /\ a e. A ) -> ( ( H o. S ) ` a ) = ( ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. ) ` a ) ) |
57 |
56
|
ralrimiva |
|- ( ( F Fn A /\ G Fn A ) -> A. a e. A ( ( H o. S ) ` a ) = ( ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. ) ` a ) ) |
58 |
|
opex |
|- <. ( F ` x ) , ( G ` y ) >. e. _V |
59 |
58
|
a1i |
|- ( ( ( F Fn A /\ G Fn A ) /\ ( x e. A /\ y e. A ) ) -> <. ( F ` x ) , ( G ` y ) >. e. _V ) |
60 |
59
|
ralrimivva |
|- ( ( F Fn A /\ G Fn A ) -> A. x e. A A. y e. A <. ( F ` x ) , ( G ` y ) >. e. _V ) |
61 |
|
eqid |
|- ( x e. A , y e. A |-> <. ( F ` x ) , ( G ` y ) >. ) = ( x e. A , y e. A |-> <. ( F ` x ) , ( G ` y ) >. ) |
62 |
61
|
fnmpo |
|- ( A. x e. A A. y e. A <. ( F ` x ) , ( G ` y ) >. e. _V -> ( x e. A , y e. A |-> <. ( F ` x ) , ( G ` y ) >. ) Fn ( A X. A ) ) |
63 |
60 62
|
syl |
|- ( ( F Fn A /\ G Fn A ) -> ( x e. A , y e. A |-> <. ( F ` x ) , ( G ` y ) >. ) Fn ( A X. A ) ) |
64 |
22
|
fneq1d |
|- ( ( F Fn A /\ G Fn A ) -> ( H Fn ( A X. A ) <-> ( x e. A , y e. A |-> <. ( F ` x ) , ( G ` y ) >. ) Fn ( A X. A ) ) ) |
65 |
63 64
|
mpbird |
|- ( ( F Fn A /\ G Fn A ) -> H Fn ( A X. A ) ) |
66 |
14
|
a1i |
|- ( ( ( F Fn A /\ G Fn A ) /\ a e. _V ) -> <. a , a >. e. _V ) |
67 |
66
|
ralrimiva |
|- ( ( F Fn A /\ G Fn A ) -> A. a e. _V <. a , a >. e. _V ) |
68 |
67 37
|
syl |
|- ( ( F Fn A /\ G Fn A ) -> ( a e. _V |-> <. a , a >. ) Fn _V ) |
69 |
68 40 41
|
sylancl |
|- ( ( F Fn A /\ G Fn A ) -> ( ( a e. _V |-> <. a , a >. ) |` A ) Fn A ) |
70 |
69 46
|
sylibr |
|- ( ( F Fn A /\ G Fn A ) -> S Fn A ) |
71 |
45
|
rneqi |
|- ran S = ran ( ( a e. _V |-> <. a , a >. ) |` A ) |
72 |
|
mptima |
|- ( ( a e. _V |-> <. a , a >. ) " A ) = ran ( a e. ( _V i^i A ) |-> <. a , a >. ) |
73 |
|
df-ima |
|- ( ( a e. _V |-> <. a , a >. ) " A ) = ran ( ( a e. _V |-> <. a , a >. ) |` A ) |
74 |
|
eqid |
|- ( a e. ( _V i^i A ) |-> <. a , a >. ) = ( a e. ( _V i^i A ) |-> <. a , a >. ) |
75 |
74
|
rnmpt |
|- ran ( a e. ( _V i^i A ) |-> <. a , a >. ) = { p | E. a e. ( _V i^i A ) p = <. a , a >. } |
76 |
72 73 75
|
3eqtr3i |
|- ran ( ( a e. _V |-> <. a , a >. ) |` A ) = { p | E. a e. ( _V i^i A ) p = <. a , a >. } |
77 |
71 76
|
eqtri |
|- ran S = { p | E. a e. ( _V i^i A ) p = <. a , a >. } |
78 |
|
elinel2 |
|- ( a e. ( _V i^i A ) -> a e. A ) |
79 |
|
simpl |
|- ( ( a e. A /\ p = <. a , a >. ) -> a e. A ) |
80 |
79 79
|
opelxpd |
|- ( ( a e. A /\ p = <. a , a >. ) -> <. a , a >. e. ( A X. A ) ) |
81 |
|
eleq1 |
|- ( p = <. a , a >. -> ( p e. ( A X. A ) <-> <. a , a >. e. ( A X. A ) ) ) |
82 |
81
|
adantl |
|- ( ( a e. A /\ p = <. a , a >. ) -> ( p e. ( A X. A ) <-> <. a , a >. e. ( A X. A ) ) ) |
83 |
80 82
|
mpbird |
|- ( ( a e. A /\ p = <. a , a >. ) -> p e. ( A X. A ) ) |
84 |
83
|
ex |
|- ( a e. A -> ( p = <. a , a >. -> p e. ( A X. A ) ) ) |
85 |
78 84
|
syl |
|- ( a e. ( _V i^i A ) -> ( p = <. a , a >. -> p e. ( A X. A ) ) ) |
86 |
85
|
rexlimiv |
|- ( E. a e. ( _V i^i A ) p = <. a , a >. -> p e. ( A X. A ) ) |
87 |
86
|
abssi |
|- { p | E. a e. ( _V i^i A ) p = <. a , a >. } C_ ( A X. A ) |
88 |
87
|
a1i |
|- ( ( F Fn A /\ G Fn A ) -> { p | E. a e. ( _V i^i A ) p = <. a , a >. } C_ ( A X. A ) ) |
89 |
77 88
|
eqsstrid |
|- ( ( F Fn A /\ G Fn A ) -> ran S C_ ( A X. A ) ) |
90 |
|
fnco |
|- ( ( H Fn ( A X. A ) /\ S Fn A /\ ran S C_ ( A X. A ) ) -> ( H o. S ) Fn A ) |
91 |
65 70 89 90
|
syl3anc |
|- ( ( F Fn A /\ G Fn A ) -> ( H o. S ) Fn A ) |
92 |
|
opex |
|- <. ( F ` x ) , ( G ` x ) >. e. _V |
93 |
92
|
a1i |
|- ( ( ( F Fn A /\ G Fn A ) /\ x e. A ) -> <. ( F ` x ) , ( G ` x ) >. e. _V ) |
94 |
93
|
ralrimiva |
|- ( ( F Fn A /\ G Fn A ) -> A. x e. A <. ( F ` x ) , ( G ` x ) >. e. _V ) |
95 |
53
|
fnmpt |
|- ( A. x e. A <. ( F ` x ) , ( G ` x ) >. e. _V -> ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. ) Fn A ) |
96 |
94 95
|
syl |
|- ( ( F Fn A /\ G Fn A ) -> ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. ) Fn A ) |
97 |
|
eqfnfv |
|- ( ( ( H o. S ) Fn A /\ ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. ) Fn A ) -> ( ( H o. S ) = ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. ) <-> A. a e. A ( ( H o. S ) ` a ) = ( ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. ) ` a ) ) ) |
98 |
91 96 97
|
syl2anc |
|- ( ( F Fn A /\ G Fn A ) -> ( ( H o. S ) = ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. ) <-> A. a e. A ( ( H o. S ) ` a ) = ( ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. ) ` a ) ) ) |
99 |
57 98
|
mpbird |
|- ( ( F Fn A /\ G Fn A ) -> ( H o. S ) = ( x e. A |-> <. ( F ` x ) , ( G ` x ) >. ) ) |