This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mulassnq

Description: Multiplication of positive fractions is associative. (Contributed by NM, 1-Sep-1995) (Revised by Mario Carneiro, 8-May-2013) (New usage is discouraged.)

Ref Expression
Assertion mulassnq 
|- ( ( A .Q B ) .Q C ) = ( A .Q ( B .Q C ) )

Proof

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