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	⊢ ( ( 𝐴 ·Q 𝐵 ) ·Q 𝐶 ) = ( 𝐴 ·Q ( 𝐵 ·Q 𝐶 ) )

Proof

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