Step |
Hyp |
Ref |
Expression |
1 |
|
moeq |
|- E* z z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. |
2 |
1
|
mosubop |
|- E* z E. u E. f ( y = <. u , f >. /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) |
3 |
2
|
mosubop |
|- E* z E. w E. v ( x = <. w , v >. /\ E. u E. f ( y = <. u , f >. /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) ) |
4 |
|
anass |
|- ( ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) <-> ( x = <. w , v >. /\ ( y = <. u , f >. /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) ) ) |
5 |
4
|
2exbii |
|- ( E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) <-> E. u E. f ( x = <. w , v >. /\ ( y = <. u , f >. /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) ) ) |
6 |
|
19.42vv |
|- ( E. u E. f ( x = <. w , v >. /\ ( y = <. u , f >. /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) ) <-> ( x = <. w , v >. /\ E. u E. f ( y = <. u , f >. /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) ) ) |
7 |
5 6
|
bitri |
|- ( E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) <-> ( x = <. w , v >. /\ E. u E. f ( y = <. u , f >. /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) ) ) |
8 |
7
|
2exbii |
|- ( E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) <-> E. w E. v ( x = <. w , v >. /\ E. u E. f ( y = <. u , f >. /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) ) ) |
9 |
8
|
mobii |
|- ( E* z E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) <-> E* z E. w E. v ( x = <. w , v >. /\ E. u E. f ( y = <. u , f >. /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) ) ) |
10 |
3 9
|
mpbir |
|- E* z E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) |
11 |
10
|
moani |
|- E* z ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) ) |
12 |
11
|
funoprab |
|- Fun { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) ) } |
13 |
|
df-mul |
|- x. = { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) ) } |
14 |
13
|
funeqi |
|- ( Fun x. <-> Fun { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) ) } ) |
15 |
12 14
|
mpbir |
|- Fun x. |
16 |
13
|
dmeqi |
|- dom x. = dom { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) ) } |
17 |
|
dmoprabss |
|- dom { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) ) } C_ ( CC X. CC ) |
18 |
16 17
|
eqsstri |
|- dom x. C_ ( CC X. CC ) |
19 |
|
0ncn |
|- -. (/) e. CC |
20 |
|
df-c |
|- CC = ( R. X. R. ) |
21 |
|
oveq1 |
|- ( <. z , w >. = x -> ( <. z , w >. x. <. v , u >. ) = ( x x. <. v , u >. ) ) |
22 |
21
|
eleq1d |
|- ( <. z , w >. = x -> ( ( <. z , w >. x. <. v , u >. ) e. ( R. X. R. ) <-> ( x x. <. v , u >. ) e. ( R. X. R. ) ) ) |
23 |
|
oveq2 |
|- ( <. v , u >. = y -> ( x x. <. v , u >. ) = ( x x. y ) ) |
24 |
23
|
eleq1d |
|- ( <. v , u >. = y -> ( ( x x. <. v , u >. ) e. ( R. X. R. ) <-> ( x x. y ) e. ( R. X. R. ) ) ) |
25 |
|
mulcnsr |
|- ( ( ( z e. R. /\ w e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> ( <. z , w >. x. <. v , u >. ) = <. ( ( z .R v ) +R ( -1R .R ( w .R u ) ) ) , ( ( w .R v ) +R ( z .R u ) ) >. ) |
26 |
|
mulclsr |
|- ( ( z e. R. /\ v e. R. ) -> ( z .R v ) e. R. ) |
27 |
|
m1r |
|- -1R e. R. |
28 |
|
mulclsr |
|- ( ( w e. R. /\ u e. R. ) -> ( w .R u ) e. R. ) |
29 |
|
mulclsr |
|- ( ( -1R e. R. /\ ( w .R u ) e. R. ) -> ( -1R .R ( w .R u ) ) e. R. ) |
30 |
27 28 29
|
sylancr |
|- ( ( w e. R. /\ u e. R. ) -> ( -1R .R ( w .R u ) ) e. R. ) |
31 |
|
addclsr |
|- ( ( ( z .R v ) e. R. /\ ( -1R .R ( w .R u ) ) e. R. ) -> ( ( z .R v ) +R ( -1R .R ( w .R u ) ) ) e. R. ) |
32 |
26 30 31
|
syl2an |
|- ( ( ( z e. R. /\ v e. R. ) /\ ( w e. R. /\ u e. R. ) ) -> ( ( z .R v ) +R ( -1R .R ( w .R u ) ) ) e. R. ) |
33 |
32
|
an4s |
|- ( ( ( z e. R. /\ w e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> ( ( z .R v ) +R ( -1R .R ( w .R u ) ) ) e. R. ) |
34 |
|
mulclsr |
|- ( ( w e. R. /\ v e. R. ) -> ( w .R v ) e. R. ) |
35 |
|
mulclsr |
|- ( ( z e. R. /\ u e. R. ) -> ( z .R u ) e. R. ) |
36 |
|
addclsr |
|- ( ( ( w .R v ) e. R. /\ ( z .R u ) e. R. ) -> ( ( w .R v ) +R ( z .R u ) ) e. R. ) |
37 |
34 35 36
|
syl2anr |
|- ( ( ( z e. R. /\ u e. R. ) /\ ( w e. R. /\ v e. R. ) ) -> ( ( w .R v ) +R ( z .R u ) ) e. R. ) |
38 |
37
|
an42s |
|- ( ( ( z e. R. /\ w e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> ( ( w .R v ) +R ( z .R u ) ) e. R. ) |
39 |
33 38
|
opelxpd |
|- ( ( ( z e. R. /\ w e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> <. ( ( z .R v ) +R ( -1R .R ( w .R u ) ) ) , ( ( w .R v ) +R ( z .R u ) ) >. e. ( R. X. R. ) ) |
40 |
25 39
|
eqeltrd |
|- ( ( ( z e. R. /\ w e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> ( <. z , w >. x. <. v , u >. ) e. ( R. X. R. ) ) |
41 |
20 22 24 40
|
2optocl |
|- ( ( x e. CC /\ y e. CC ) -> ( x x. y ) e. ( R. X. R. ) ) |
42 |
41 20
|
eleqtrrdi |
|- ( ( x e. CC /\ y e. CC ) -> ( x x. y ) e. CC ) |
43 |
19 42
|
oprssdm |
|- ( CC X. CC ) C_ dom x. |
44 |
18 43
|
eqssi |
|- dom x. = ( CC X. CC ) |
45 |
|
df-fn |
|- ( x. Fn ( CC X. CC ) <-> ( Fun x. /\ dom x. = ( CC X. CC ) ) ) |
46 |
15 44 45
|
mpbir2an |
|- x. Fn ( CC X. CC ) |
47 |
42
|
rgen2 |
|- A. x e. CC A. y e. CC ( x x. y ) e. CC |
48 |
|
ffnov |
|- ( x. : ( CC X. CC ) --> CC <-> ( x. Fn ( CC X. CC ) /\ A. x e. CC A. y e. CC ( x x. y ) e. CC ) ) |
49 |
46 47 48
|
mpbir2an |
|- x. : ( CC X. CC ) --> CC |