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