Step |
Hyp |
Ref |
Expression |
1 |
|
ltrelnq |
|- |
2 |
1
|
brel |
|- ( A ( A e. Q. /\ B e. Q. ) ) |
3 |
1
|
brel |
|- ( ( *Q ` B ) ( ( *Q ` B ) e. Q. /\ ( *Q ` A ) e. Q. ) ) |
4 |
|
dmrecnq |
|- dom *Q = Q. |
5 |
|
0nnq |
|- -. (/) e. Q. |
6 |
4 5
|
ndmfvrcl |
|- ( ( *Q ` B ) e. Q. -> B e. Q. ) |
7 |
4 5
|
ndmfvrcl |
|- ( ( *Q ` A ) e. Q. -> A e. Q. ) |
8 |
6 7
|
anim12ci |
|- ( ( ( *Q ` B ) e. Q. /\ ( *Q ` A ) e. Q. ) -> ( A e. Q. /\ B e. Q. ) ) |
9 |
3 8
|
syl |
|- ( ( *Q ` B ) ( A e. Q. /\ B e. Q. ) ) |
10 |
|
breq1 |
|- ( x = A -> ( x A |
11 |
|
fveq2 |
|- ( x = A -> ( *Q ` x ) = ( *Q ` A ) ) |
12 |
11
|
breq2d |
|- ( x = A -> ( ( *Q ` y ) ( *Q ` y ) |
13 |
10 12
|
bibi12d |
|- ( x = A -> ( ( x ( *Q ` y ) ( A ( *Q ` y ) |
14 |
|
breq2 |
|- ( y = B -> ( A A |
15 |
|
fveq2 |
|- ( y = B -> ( *Q ` y ) = ( *Q ` B ) ) |
16 |
15
|
breq1d |
|- ( y = B -> ( ( *Q ` y ) ( *Q ` B ) |
17 |
14 16
|
bibi12d |
|- ( y = B -> ( ( A ( *Q ` y ) ( A ( *Q ` B ) |
18 |
|
recclnq |
|- ( x e. Q. -> ( *Q ` x ) e. Q. ) |
19 |
|
recclnq |
|- ( y e. Q. -> ( *Q ` y ) e. Q. ) |
20 |
|
mulclnq |
|- ( ( ( *Q ` x ) e. Q. /\ ( *Q ` y ) e. Q. ) -> ( ( *Q ` x ) .Q ( *Q ` y ) ) e. Q. ) |
21 |
18 19 20
|
syl2an |
|- ( ( x e. Q. /\ y e. Q. ) -> ( ( *Q ` x ) .Q ( *Q ` y ) ) e. Q. ) |
22 |
|
ltmnq |
|- ( ( ( *Q ` x ) .Q ( *Q ` y ) ) e. Q. -> ( x ( ( ( *Q ` x ) .Q ( *Q ` y ) ) .Q x ) |
23 |
21 22
|
syl |
|- ( ( x e. Q. /\ y e. Q. ) -> ( x ( ( ( *Q ` x ) .Q ( *Q ` y ) ) .Q x ) |
24 |
|
mulcomnq |
|- ( ( ( *Q ` x ) .Q ( *Q ` y ) ) .Q x ) = ( x .Q ( ( *Q ` x ) .Q ( *Q ` y ) ) ) |
25 |
|
mulassnq |
|- ( ( x .Q ( *Q ` x ) ) .Q ( *Q ` y ) ) = ( x .Q ( ( *Q ` x ) .Q ( *Q ` y ) ) ) |
26 |
|
mulcomnq |
|- ( ( x .Q ( *Q ` x ) ) .Q ( *Q ` y ) ) = ( ( *Q ` y ) .Q ( x .Q ( *Q ` x ) ) ) |
27 |
24 25 26
|
3eqtr2i |
|- ( ( ( *Q ` x ) .Q ( *Q ` y ) ) .Q x ) = ( ( *Q ` y ) .Q ( x .Q ( *Q ` x ) ) ) |
28 |
|
recidnq |
|- ( x e. Q. -> ( x .Q ( *Q ` x ) ) = 1Q ) |
29 |
28
|
oveq2d |
|- ( x e. Q. -> ( ( *Q ` y ) .Q ( x .Q ( *Q ` x ) ) ) = ( ( *Q ` y ) .Q 1Q ) ) |
30 |
|
mulidnq |
|- ( ( *Q ` y ) e. Q. -> ( ( *Q ` y ) .Q 1Q ) = ( *Q ` y ) ) |
31 |
19 30
|
syl |
|- ( y e. Q. -> ( ( *Q ` y ) .Q 1Q ) = ( *Q ` y ) ) |
32 |
29 31
|
sylan9eq |
|- ( ( x e. Q. /\ y e. Q. ) -> ( ( *Q ` y ) .Q ( x .Q ( *Q ` x ) ) ) = ( *Q ` y ) ) |
33 |
27 32
|
eqtrid |
|- ( ( x e. Q. /\ y e. Q. ) -> ( ( ( *Q ` x ) .Q ( *Q ` y ) ) .Q x ) = ( *Q ` y ) ) |
34 |
|
mulassnq |
|- ( ( ( *Q ` x ) .Q ( *Q ` y ) ) .Q y ) = ( ( *Q ` x ) .Q ( ( *Q ` y ) .Q y ) ) |
35 |
|
mulcomnq |
|- ( ( *Q ` y ) .Q y ) = ( y .Q ( *Q ` y ) ) |
36 |
35
|
oveq2i |
|- ( ( *Q ` x ) .Q ( ( *Q ` y ) .Q y ) ) = ( ( *Q ` x ) .Q ( y .Q ( *Q ` y ) ) ) |
37 |
34 36
|
eqtri |
|- ( ( ( *Q ` x ) .Q ( *Q ` y ) ) .Q y ) = ( ( *Q ` x ) .Q ( y .Q ( *Q ` y ) ) ) |
38 |
|
recidnq |
|- ( y e. Q. -> ( y .Q ( *Q ` y ) ) = 1Q ) |
39 |
38
|
oveq2d |
|- ( y e. Q. -> ( ( *Q ` x ) .Q ( y .Q ( *Q ` y ) ) ) = ( ( *Q ` x ) .Q 1Q ) ) |
40 |
|
mulidnq |
|- ( ( *Q ` x ) e. Q. -> ( ( *Q ` x ) .Q 1Q ) = ( *Q ` x ) ) |
41 |
18 40
|
syl |
|- ( x e. Q. -> ( ( *Q ` x ) .Q 1Q ) = ( *Q ` x ) ) |
42 |
39 41
|
sylan9eqr |
|- ( ( x e. Q. /\ y e. Q. ) -> ( ( *Q ` x ) .Q ( y .Q ( *Q ` y ) ) ) = ( *Q ` x ) ) |
43 |
37 42
|
eqtrid |
|- ( ( x e. Q. /\ y e. Q. ) -> ( ( ( *Q ` x ) .Q ( *Q ` y ) ) .Q y ) = ( *Q ` x ) ) |
44 |
33 43
|
breq12d |
|- ( ( x e. Q. /\ y e. Q. ) -> ( ( ( ( *Q ` x ) .Q ( *Q ` y ) ) .Q x ) ( *Q ` y ) |
45 |
23 44
|
bitrd |
|- ( ( x e. Q. /\ y e. Q. ) -> ( x ( *Q ` y ) |
46 |
13 17 45
|
vtocl2ga |
|- ( ( A e. Q. /\ B e. Q. ) -> ( A ( *Q ` B ) |
47 |
2 9 46
|
pm5.21nii |
|- ( A ( *Q ` B ) |