mulerpqlem

Description: Lemma for mulerpq . (Contributed by Mario Carneiro, 8-May-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	mulerpqlem	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 𝐴 ~_Q 𝐵 ↔ ( 𝐴 ·_pQ 𝐶 ) ~_Q ( 𝐵 ·_pQ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		xp1st	⊢ ( 𝐴 ∈ ( N × N ) → ( 1^st ‘ 𝐴 ) ∈ N )
2	1	3ad2ant1	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 1^st ‘ 𝐴 ) ∈ N )
3		xp1st	⊢ ( 𝐶 ∈ ( N × N ) → ( 1^st ‘ 𝐶 ) ∈ N )
4	3	3ad2ant3	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 1^st ‘ 𝐶 ) ∈ N )
5		mulclpi	⊢ ( ( ( 1^st ‘ 𝐴 ) ∈ N ∧ ( 1^st ‘ 𝐶 ) ∈ N ) → ( ( 1^st ‘ 𝐴 ) ·_N ( 1^st ‘ 𝐶 ) ) ∈ N )
6	2 4 5	syl2anc	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( ( 1^st ‘ 𝐴 ) ·_N ( 1^st ‘ 𝐶 ) ) ∈ N )
7		xp2nd	⊢ ( 𝐴 ∈ ( N × N ) → ( 2^nd ‘ 𝐴 ) ∈ N )
8	7	3ad2ant1	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 2^nd ‘ 𝐴 ) ∈ N )
9		xp2nd	⊢ ( 𝐶 ∈ ( N × N ) → ( 2^nd ‘ 𝐶 ) ∈ N )
10	9	3ad2ant3	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 2^nd ‘ 𝐶 ) ∈ N )
11		mulclpi	⊢ ( ( ( 2^nd ‘ 𝐴 ) ∈ N ∧ ( 2^nd ‘ 𝐶 ) ∈ N ) → ( ( 2^nd ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐶 ) ) ∈ N )
12	8 10 11	syl2anc	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( ( 2^nd ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐶 ) ) ∈ N )
13		xp1st	⊢ ( 𝐵 ∈ ( N × N ) → ( 1^st ‘ 𝐵 ) ∈ N )
14	13	3ad2ant2	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 1^st ‘ 𝐵 ) ∈ N )
15		mulclpi	⊢ ( ( ( 1^st ‘ 𝐵 ) ∈ N ∧ ( 1^st ‘ 𝐶 ) ∈ N ) → ( ( 1^st ‘ 𝐵 ) ·_N ( 1^st ‘ 𝐶 ) ) ∈ N )
16	14 4 15	syl2anc	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( ( 1^st ‘ 𝐵 ) ·_N ( 1^st ‘ 𝐶 ) ) ∈ N )
17		xp2nd	⊢ ( 𝐵 ∈ ( N × N ) → ( 2^nd ‘ 𝐵 ) ∈ N )
18	17	3ad2ant2	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 2^nd ‘ 𝐵 ) ∈ N )
19		mulclpi	⊢ ( ( ( 2^nd ‘ 𝐵 ) ∈ N ∧ ( 2^nd ‘ 𝐶 ) ∈ N ) → ( ( 2^nd ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐶 ) ) ∈ N )
20	18 10 19	syl2anc	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( ( 2^nd ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐶 ) ) ∈ N )
21		enqbreq	⊢ ( ( ( ( ( 1^st ‘ 𝐴 ) ·_N ( 1^st ‘ 𝐶 ) ) ∈ N ∧ ( ( 2^nd ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐶 ) ) ∈ N ) ∧ ( ( ( 1^st ‘ 𝐵 ) ·_N ( 1^st ‘ 𝐶 ) ) ∈ N ∧ ( ( 2^nd ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐶 ) ) ∈ N ) ) → ( ⟨ ( ( 1^st ‘ 𝐴 ) ·_N ( 1^st ‘ 𝐶 ) ) , ( ( 2^nd ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐶 ) ) ⟩ ~_Q ⟨ ( ( 1^st ‘ 𝐵 ) ·_N ( 1^st ‘ 𝐶 ) ) , ( ( 2^nd ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐶 ) ) ⟩ ↔ ( ( ( 1^st ‘ 𝐴 ) ·_N ( 1^st ‘ 𝐶 ) ) ·_N ( ( 2^nd ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐶 ) ) ) = ( ( ( 2^nd ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐶 ) ) ·_N ( ( 1^st ‘ 𝐵 ) ·_N ( 1^st ‘ 𝐶 ) ) ) ) )
22	6 12 16 20 21	syl22anc	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( ⟨ ( ( 1^st ‘ 𝐴 ) ·_N ( 1^st ‘ 𝐶 ) ) , ( ( 2^nd ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐶 ) ) ⟩ ~_Q ⟨ ( ( 1^st ‘ 𝐵 ) ·_N ( 1^st ‘ 𝐶 ) ) , ( ( 2^nd ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐶 ) ) ⟩ ↔ ( ( ( 1^st ‘ 𝐴 ) ·_N ( 1^st ‘ 𝐶 ) ) ·_N ( ( 2^nd ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐶 ) ) ) = ( ( ( 2^nd ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐶 ) ) ·_N ( ( 1^st ‘ 𝐵 ) ·_N ( 1^st ‘ 𝐶 ) ) ) ) )
23		mulpipq2	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 𝐴 ·_pQ 𝐶 ) = ⟨ ( ( 1^st ‘ 𝐴 ) ·_N ( 1^st ‘ 𝐶 ) ) , ( ( 2^nd ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐶 ) ) ⟩ )
24	23	3adant2	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 𝐴 ·_pQ 𝐶 ) = ⟨ ( ( 1^st ‘ 𝐴 ) ·_N ( 1^st ‘ 𝐶 ) ) , ( ( 2^nd ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐶 ) ) ⟩ )
25		mulpipq2	⊢ ( ( 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 𝐵 ·_pQ 𝐶 ) = ⟨ ( ( 1^st ‘ 𝐵 ) ·_N ( 1^st ‘ 𝐶 ) ) , ( ( 2^nd ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐶 ) ) ⟩ )
26	25	3adant1	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 𝐵 ·_pQ 𝐶 ) = ⟨ ( ( 1^st ‘ 𝐵 ) ·_N ( 1^st ‘ 𝐶 ) ) , ( ( 2^nd ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐶 ) ) ⟩ )
27	24 26	breq12d	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( ( 𝐴 ·_pQ 𝐶 ) ~_Q ( 𝐵 ·_pQ 𝐶 ) ↔ ⟨ ( ( 1^st ‘ 𝐴 ) ·_N ( 1^st ‘ 𝐶 ) ) , ( ( 2^nd ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐶 ) ) ⟩ ~_Q ⟨ ( ( 1^st ‘ 𝐵 ) ·_N ( 1^st ‘ 𝐶 ) ) , ( ( 2^nd ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐶 ) ) ⟩ ) )
28		enqbreq2	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 ~_Q 𝐵 ↔ ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) = ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) )
29	28	3adant3	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 𝐴 ~_Q 𝐵 ↔ ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) = ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) )
30		mulclpi	⊢ ( ( ( 1^st ‘ 𝐶 ) ∈ N ∧ ( 2^nd ‘ 𝐶 ) ∈ N ) → ( ( 1^st ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐶 ) ) ∈ N )
31	4 10 30	syl2anc	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( ( 1^st ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐶 ) ) ∈ N )
32		mulclpi	⊢ ( ( ( 1^st ‘ 𝐴 ) ∈ N ∧ ( 2^nd ‘ 𝐵 ) ∈ N ) → ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ∈ N )
33	2 18 32	syl2anc	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ∈ N )
34		mulcanpi	⊢ ( ( ( ( 1^st ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐶 ) ) ∈ N ∧ ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ∈ N ) → ( ( ( ( 1^st ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐶 ) ) ·_N ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ) = ( ( ( 1^st ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐶 ) ) ·_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) ↔ ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) = ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) )
35	31 33 34	syl2anc	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( ( ( ( 1^st ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐶 ) ) ·_N ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ) = ( ( ( 1^st ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐶 ) ) ·_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) ↔ ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) = ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) )
36		mulcompi	⊢ ( ( ( 1^st ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐶 ) ) ·_N ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ) = ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ·_N ( ( 1^st ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐶 ) ) )
37		fvex	⊢ ( 1^st ‘ 𝐴 ) ∈ V
38		fvex	⊢ ( 2^nd ‘ 𝐵 ) ∈ V
39		fvex	⊢ ( 1^st ‘ 𝐶 ) ∈ V
40		mulcompi	⊢ ( 𝑥 ·_N 𝑦 ) = ( 𝑦 ·_N 𝑥 )
41		mulasspi	⊢ ( ( 𝑥 ·_N 𝑦 ) ·_N 𝑧 ) = ( 𝑥 ·_N ( 𝑦 ·_N 𝑧 ) )
42		fvex	⊢ ( 2^nd ‘ 𝐶 ) ∈ V
43	37 38 39 40 41 42	caov4	⊢ ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ·_N ( ( 1^st ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐶 ) ) ) = ( ( ( 1^st ‘ 𝐴 ) ·_N ( 1^st ‘ 𝐶 ) ) ·_N ( ( 2^nd ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐶 ) ) )
44	36 43	eqtri	⊢ ( ( ( 1^st ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐶 ) ) ·_N ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ) = ( ( ( 1^st ‘ 𝐴 ) ·_N ( 1^st ‘ 𝐶 ) ) ·_N ( ( 2^nd ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐶 ) ) )
45		mulcompi	⊢ ( ( ( 1^st ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐶 ) ) ·_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) = ( ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ·_N ( ( 1^st ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐶 ) ) )
46		fvex	⊢ ( 1^st ‘ 𝐵 ) ∈ V
47		fvex	⊢ ( 2^nd ‘ 𝐴 ) ∈ V
48	46 47 39 40 41 42	caov4	⊢ ( ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ·_N ( ( 1^st ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐶 ) ) ) = ( ( ( 1^st ‘ 𝐵 ) ·_N ( 1^st ‘ 𝐶 ) ) ·_N ( ( 2^nd ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐶 ) ) )
49		mulcompi	⊢ ( ( ( 1^st ‘ 𝐵 ) ·_N ( 1^st ‘ 𝐶 ) ) ·_N ( ( 2^nd ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐶 ) ) ) = ( ( ( 2^nd ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐶 ) ) ·_N ( ( 1^st ‘ 𝐵 ) ·_N ( 1^st ‘ 𝐶 ) ) )
50	45 48 49	3eqtri	⊢ ( ( ( 1^st ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐶 ) ) ·_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) = ( ( ( 2^nd ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐶 ) ) ·_N ( ( 1^st ‘ 𝐵 ) ·_N ( 1^st ‘ 𝐶 ) ) )
51	44 50	eqeq12i	⊢ ( ( ( ( 1^st ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐶 ) ) ·_N ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ) = ( ( ( 1^st ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐶 ) ) ·_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) ↔ ( ( ( 1^st ‘ 𝐴 ) ·_N ( 1^st ‘ 𝐶 ) ) ·_N ( ( 2^nd ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐶 ) ) ) = ( ( ( 2^nd ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐶 ) ) ·_N ( ( 1^st ‘ 𝐵 ) ·_N ( 1^st ‘ 𝐶 ) ) ) )
52	51	a1i	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( ( ( ( 1^st ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐶 ) ) ·_N ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) ) = ( ( ( 1^st ‘ 𝐶 ) ·_N ( 2^nd ‘ 𝐶 ) ) ·_N ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) ↔ ( ( ( 1^st ‘ 𝐴 ) ·_N ( 1^st ‘ 𝐶 ) ) ·_N ( ( 2^nd ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐶 ) ) ) = ( ( ( 2^nd ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐶 ) ) ·_N ( ( 1^st ‘ 𝐵 ) ·_N ( 1^st ‘ 𝐶 ) ) ) ) )
53	29 35 52	3bitr2d	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 𝐴 ~_Q 𝐵 ↔ ( ( ( 1^st ‘ 𝐴 ) ·_N ( 1^st ‘ 𝐶 ) ) ·_N ( ( 2^nd ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐶 ) ) ) = ( ( ( 2^nd ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐶 ) ) ·_N ( ( 1^st ‘ 𝐵 ) ·_N ( 1^st ‘ 𝐶 ) ) ) ) )
54	22 27 53	3bitr4rd	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 𝐴 ~_Q 𝐵 ↔ ( 𝐴 ·_pQ 𝐶 ) ~_Q ( 𝐵 ·_pQ 𝐶 ) ) )

Metamath Proof Explorer

Theorem mulerpqlem

Proof