Step |
Hyp |
Ref |
Expression |
1 |
|
mulasspi |
|- ( ( ( 1st ` A ) .N ( 1st ` B ) ) .N ( 1st ` C ) ) = ( ( 1st ` A ) .N ( ( 1st ` B ) .N ( 1st ` C ) ) ) |
2 |
|
mulasspi |
|- ( ( ( 2nd ` A ) .N ( 2nd ` B ) ) .N ( 2nd ` C ) ) = ( ( 2nd ` A ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) |
3 |
1 2
|
opeq12i |
|- <. ( ( ( 1st ` A ) .N ( 1st ` B ) ) .N ( 1st ` C ) ) , ( ( ( 2nd ` A ) .N ( 2nd ` B ) ) .N ( 2nd ` C ) ) >. = <. ( ( 1st ` A ) .N ( ( 1st ` B ) .N ( 1st ` C ) ) ) , ( ( 2nd ` A ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) >. |
4 |
|
elpqn |
|- ( A e. Q. -> A e. ( N. X. N. ) ) |
5 |
4
|
3ad2ant1 |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> A e. ( N. X. N. ) ) |
6 |
|
elpqn |
|- ( B e. Q. -> B e. ( N. X. N. ) ) |
7 |
6
|
3ad2ant2 |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> B e. ( N. X. N. ) ) |
8 |
|
mulpipq2 |
|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A .pQ B ) = <. ( ( 1st ` A ) .N ( 1st ` B ) ) , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) |
9 |
5 7 8
|
syl2anc |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( A .pQ B ) = <. ( ( 1st ` A ) .N ( 1st ` B ) ) , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. ) |
10 |
|
relxp |
|- Rel ( N. X. N. ) |
11 |
|
elpqn |
|- ( C e. Q. -> C e. ( N. X. N. ) ) |
12 |
11
|
3ad2ant3 |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> C e. ( N. X. N. ) ) |
13 |
|
1st2nd |
|- ( ( Rel ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> C = <. ( 1st ` C ) , ( 2nd ` C ) >. ) |
14 |
10 12 13
|
sylancr |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> C = <. ( 1st ` C ) , ( 2nd ` C ) >. ) |
15 |
9 14
|
oveq12d |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( A .pQ B ) .pQ C ) = ( <. ( ( 1st ` A ) .N ( 1st ` B ) ) , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. .pQ <. ( 1st ` C ) , ( 2nd ` C ) >. ) ) |
16 |
|
xp1st |
|- ( A e. ( N. X. N. ) -> ( 1st ` A ) e. N. ) |
17 |
5 16
|
syl |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( 1st ` A ) e. N. ) |
18 |
|
xp1st |
|- ( B e. ( N. X. N. ) -> ( 1st ` B ) e. N. ) |
19 |
7 18
|
syl |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( 1st ` B ) e. N. ) |
20 |
|
mulclpi |
|- ( ( ( 1st ` A ) e. N. /\ ( 1st ` B ) e. N. ) -> ( ( 1st ` A ) .N ( 1st ` B ) ) e. N. ) |
21 |
17 19 20
|
syl2anc |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( 1st ` A ) .N ( 1st ` B ) ) e. N. ) |
22 |
|
xp2nd |
|- ( A e. ( N. X. N. ) -> ( 2nd ` A ) e. N. ) |
23 |
5 22
|
syl |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( 2nd ` A ) e. N. ) |
24 |
|
xp2nd |
|- ( B e. ( N. X. N. ) -> ( 2nd ` B ) e. N. ) |
25 |
7 24
|
syl |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( 2nd ` B ) e. N. ) |
26 |
|
mulclpi |
|- ( ( ( 2nd ` A ) e. N. /\ ( 2nd ` B ) e. N. ) -> ( ( 2nd ` A ) .N ( 2nd ` B ) ) e. N. ) |
27 |
23 25 26
|
syl2anc |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( 2nd ` A ) .N ( 2nd ` B ) ) e. N. ) |
28 |
|
xp1st |
|- ( C e. ( N. X. N. ) -> ( 1st ` C ) e. N. ) |
29 |
12 28
|
syl |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( 1st ` C ) e. N. ) |
30 |
|
xp2nd |
|- ( C e. ( N. X. N. ) -> ( 2nd ` C ) e. N. ) |
31 |
12 30
|
syl |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( 2nd ` C ) e. N. ) |
32 |
|
mulpipq |
|- ( ( ( ( ( 1st ` A ) .N ( 1st ` B ) ) e. N. /\ ( ( 2nd ` A ) .N ( 2nd ` B ) ) e. N. ) /\ ( ( 1st ` C ) e. N. /\ ( 2nd ` C ) e. N. ) ) -> ( <. ( ( 1st ` A ) .N ( 1st ` B ) ) , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. .pQ <. ( 1st ` C ) , ( 2nd ` C ) >. ) = <. ( ( ( 1st ` A ) .N ( 1st ` B ) ) .N ( 1st ` C ) ) , ( ( ( 2nd ` A ) .N ( 2nd ` B ) ) .N ( 2nd ` C ) ) >. ) |
33 |
21 27 29 31 32
|
syl22anc |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( <. ( ( 1st ` A ) .N ( 1st ` B ) ) , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. .pQ <. ( 1st ` C ) , ( 2nd ` C ) >. ) = <. ( ( ( 1st ` A ) .N ( 1st ` B ) ) .N ( 1st ` C ) ) , ( ( ( 2nd ` A ) .N ( 2nd ` B ) ) .N ( 2nd ` C ) ) >. ) |
34 |
15 33
|
eqtrd |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( A .pQ B ) .pQ C ) = <. ( ( ( 1st ` A ) .N ( 1st ` B ) ) .N ( 1st ` C ) ) , ( ( ( 2nd ` A ) .N ( 2nd ` B ) ) .N ( 2nd ` C ) ) >. ) |
35 |
|
1st2nd |
|- ( ( Rel ( N. X. N. ) /\ A e. ( N. X. N. ) ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. ) |
36 |
10 5 35
|
sylancr |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. ) |
37 |
|
mulpipq2 |
|- ( ( B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( B .pQ C ) = <. ( ( 1st ` B ) .N ( 1st ` C ) ) , ( ( 2nd ` B ) .N ( 2nd ` C ) ) >. ) |
38 |
7 12 37
|
syl2anc |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( B .pQ C ) = <. ( ( 1st ` B ) .N ( 1st ` C ) ) , ( ( 2nd ` B ) .N ( 2nd ` C ) ) >. ) |
39 |
36 38
|
oveq12d |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( A .pQ ( B .pQ C ) ) = ( <. ( 1st ` A ) , ( 2nd ` A ) >. .pQ <. ( ( 1st ` B ) .N ( 1st ` C ) ) , ( ( 2nd ` B ) .N ( 2nd ` C ) ) >. ) ) |
40 |
|
mulclpi |
|- ( ( ( 1st ` B ) e. N. /\ ( 1st ` C ) e. N. ) -> ( ( 1st ` B ) .N ( 1st ` C ) ) e. N. ) |
41 |
19 29 40
|
syl2anc |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( 1st ` B ) .N ( 1st ` C ) ) e. N. ) |
42 |
|
mulclpi |
|- ( ( ( 2nd ` B ) e. N. /\ ( 2nd ` C ) e. N. ) -> ( ( 2nd ` B ) .N ( 2nd ` C ) ) e. N. ) |
43 |
25 31 42
|
syl2anc |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( 2nd ` B ) .N ( 2nd ` C ) ) e. N. ) |
44 |
|
mulpipq |
|- ( ( ( ( 1st ` A ) e. N. /\ ( 2nd ` A ) e. N. ) /\ ( ( ( 1st ` B ) .N ( 1st ` C ) ) e. N. /\ ( ( 2nd ` B ) .N ( 2nd ` C ) ) e. N. ) ) -> ( <. ( 1st ` A ) , ( 2nd ` A ) >. .pQ <. ( ( 1st ` B ) .N ( 1st ` C ) ) , ( ( 2nd ` B ) .N ( 2nd ` C ) ) >. ) = <. ( ( 1st ` A ) .N ( ( 1st ` B ) .N ( 1st ` C ) ) ) , ( ( 2nd ` A ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) >. ) |
45 |
17 23 41 43 44
|
syl22anc |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( <. ( 1st ` A ) , ( 2nd ` A ) >. .pQ <. ( ( 1st ` B ) .N ( 1st ` C ) ) , ( ( 2nd ` B ) .N ( 2nd ` C ) ) >. ) = <. ( ( 1st ` A ) .N ( ( 1st ` B ) .N ( 1st ` C ) ) ) , ( ( 2nd ` A ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) >. ) |
46 |
39 45
|
eqtrd |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( A .pQ ( B .pQ C ) ) = <. ( ( 1st ` A ) .N ( ( 1st ` B ) .N ( 1st ` C ) ) ) , ( ( 2nd ` A ) .N ( ( 2nd ` B ) .N ( 2nd ` C ) ) ) >. ) |
47 |
3 34 46
|
3eqtr4a |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( A .pQ B ) .pQ C ) = ( A .pQ ( B .pQ C ) ) ) |
48 |
47
|
fveq2d |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( /Q ` ( ( A .pQ B ) .pQ C ) ) = ( /Q ` ( A .pQ ( B .pQ C ) ) ) ) |
49 |
|
mulerpq |
|- ( ( /Q ` ( A .pQ B ) ) .Q ( /Q ` C ) ) = ( /Q ` ( ( A .pQ B ) .pQ C ) ) |
50 |
|
mulerpq |
|- ( ( /Q ` A ) .Q ( /Q ` ( B .pQ C ) ) ) = ( /Q ` ( A .pQ ( B .pQ C ) ) ) |
51 |
48 49 50
|
3eqtr4g |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( /Q ` ( A .pQ B ) ) .Q ( /Q ` C ) ) = ( ( /Q ` A ) .Q ( /Q ` ( B .pQ C ) ) ) ) |
52 |
|
mulpqnq |
|- ( ( A e. Q. /\ B e. Q. ) -> ( A .Q B ) = ( /Q ` ( A .pQ B ) ) ) |
53 |
52
|
3adant3 |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( A .Q B ) = ( /Q ` ( A .pQ B ) ) ) |
54 |
|
nqerid |
|- ( C e. Q. -> ( /Q ` C ) = C ) |
55 |
54
|
eqcomd |
|- ( C e. Q. -> C = ( /Q ` C ) ) |
56 |
55
|
3ad2ant3 |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> C = ( /Q ` C ) ) |
57 |
53 56
|
oveq12d |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( A .Q B ) .Q C ) = ( ( /Q ` ( A .pQ B ) ) .Q ( /Q ` C ) ) ) |
58 |
|
nqerid |
|- ( A e. Q. -> ( /Q ` A ) = A ) |
59 |
58
|
eqcomd |
|- ( A e. Q. -> A = ( /Q ` A ) ) |
60 |
59
|
3ad2ant1 |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> A = ( /Q ` A ) ) |
61 |
|
mulpqnq |
|- ( ( B e. Q. /\ C e. Q. ) -> ( B .Q C ) = ( /Q ` ( B .pQ C ) ) ) |
62 |
61
|
3adant1 |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( B .Q C ) = ( /Q ` ( B .pQ C ) ) ) |
63 |
60 62
|
oveq12d |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( A .Q ( B .Q C ) ) = ( ( /Q ` A ) .Q ( /Q ` ( B .pQ C ) ) ) ) |
64 |
51 57 63
|
3eqtr4d |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( A .Q B ) .Q C ) = ( A .Q ( B .Q C ) ) ) |
65 |
|
mulnqf |
|- .Q : ( Q. X. Q. ) --> Q. |
66 |
65
|
fdmi |
|- dom .Q = ( Q. X. Q. ) |
67 |
|
0nnq |
|- -. (/) e. Q. |
68 |
66 67
|
ndmovass |
|- ( -. ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( A .Q B ) .Q C ) = ( A .Q ( B .Q C ) ) ) |
69 |
64 68
|
pm2.61i |
|- ( ( A .Q B ) .Q C ) = ( A .Q ( B .Q C ) ) |