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

Metamath Proof Explorer

Theorem adderpqlem

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

Ref Expression
Assertion adderpqlem ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 𝐴 ~Q 𝐵 ↔ ( 𝐴 +pQ 𝐶 ) ~Q ( 𝐵 +pQ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 xp1st ⊢ ( 𝐴 ∈ ( N × N ) → ( 1st ‘ 𝐴 ) ∈ N )
2 1 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 1st ‘ 𝐴 ) ∈ N )
3 xp2nd ⊢ ( 𝐶 ∈ ( N × N ) → ( 2nd ‘ 𝐶 ) ∈ N )
4 3 3ad2ant3 ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 2nd ‘ 𝐶 ) ∈ N )
5 mulclpi ⊢ ( ( ( 1st ‘ 𝐴 ) ∈ N ∧ ( 2nd ‘ 𝐶 ) ∈ N ) → ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ∈ N )
6 2 4 5 syl2anc ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ∈ N )
7 xp1st ⊢ ( 𝐶 ∈ ( N × N ) → ( 1st ‘ 𝐶 ) ∈ N )
8 7 3ad2ant3 ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 1st ‘ 𝐶 ) ∈ N )
9 xp2nd ⊢ ( 𝐴 ∈ ( N × N ) → ( 2nd ‘ 𝐴 ) ∈ N )
10 9 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 2nd ‘ 𝐴 ) ∈ N )
11 mulclpi ⊢ ( ( ( 1st ‘ 𝐶 ) ∈ N ∧ ( 2nd ‘ 𝐴 ) ∈ N ) → ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐴 ) ) ∈ N )
12 8 10 11 syl2anc ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐴 ) ) ∈ N )
13 addclpi ⊢ ( ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ∈ N ∧ ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐴 ) ) ∈ N ) → ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐴 ) ) ) ∈ N )
14 6 12 13 syl2anc ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐴 ) ) ) ∈ N )
15 mulclpi ⊢ ( ( ( 2nd ‘ 𝐴 ) ∈ N ∧ ( 2nd ‘ 𝐶 ) ∈ N ) → ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ∈ N )
16 10 4 15 syl2anc ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ∈ N )
17 xp1st ⊢ ( 𝐵 ∈ ( N × N ) → ( 1st ‘ 𝐵 ) ∈ N )
18 17 3ad2ant2 ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 1st ‘ 𝐵 ) ∈ N )
19 mulclpi ⊢ ( ( ( 1st ‘ 𝐵 ) ∈ N ∧ ( 2nd ‘ 𝐶 ) ∈ N ) → ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ∈ N )
20 18 4 19 syl2anc ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ∈ N )
21 xp2nd ⊢ ( 𝐵 ∈ ( N × N ) → ( 2nd ‘ 𝐵 ) ∈ N )
22 21 3ad2ant2 ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 2nd ‘ 𝐵 ) ∈ N )
23 mulclpi ⊢ ( ( ( 1st ‘ 𝐶 ) ∈ N ∧ ( 2nd ‘ 𝐵 ) ∈ N ) → ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ∈ N )
24 8 22 23 syl2anc ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ∈ N )
25 addclpi ⊢ ( ( ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ∈ N ∧ ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ∈ N ) → ( ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) ∈ N )
26 20 24 25 syl2anc ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) ∈ N )
27 mulclpi ⊢ ( ( ( 2nd ‘ 𝐵 ) ∈ N ∧ ( 2nd ‘ 𝐶 ) ∈ N ) → ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ∈ N )
28 22 4 27 syl2anc ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ∈ N )
29 enqbreq ⊢ ( ( ( ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐴 ) ) ) ∈ N ∧ ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ∈ N ) ∧ ( ( ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) ∈ N ∧ ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ∈ N ) ) → ( ⟨ ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐴 ) ) ) , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ⟩ ~Q ⟨ ( ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) , ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ⟩ ↔ ( ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐴 ) ) ) ·N ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ) = ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) ) ) )
30 14 16 26 28 29 syl22anc ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( ⟨ ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐴 ) ) ) , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ⟩ ~Q ⟨ ( ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) , ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ⟩ ↔ ( ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐴 ) ) ) ·N ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ) = ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) ) ) )
31 addpipq2 ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 𝐴 +pQ 𝐶 ) = ⟨ ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐴 ) ) ) , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ⟩ )
32 31 3adant2 ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 𝐴 +pQ 𝐶 ) = ⟨ ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐴 ) ) ) , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ⟩ )
33 addpipq2 ⊢ ( ( 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 𝐵 +pQ 𝐶 ) = ⟨ ( ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) , ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ⟩ )
34 33 3adant1 ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 𝐵 +pQ 𝐶 ) = ⟨ ( ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) , ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ⟩ )
35 32 34 breq12d ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( ( 𝐴 +pQ 𝐶 ) ~Q ( 𝐵 +pQ 𝐶 ) ↔ ⟨ ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐴 ) ) ) , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ⟩ ~Q ⟨ ( ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) , ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ⟩ ) )
36 enqbreq2 ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 ~Q 𝐵 ↔ ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) = ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ) )
37 36 3adant3 ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 𝐴 ~Q 𝐵 ↔ ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) = ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ) )
38 mulclpi ⊢ ( ( ( 2nd ‘ 𝐶 ) ∈ N ∧ ( 2nd ‘ 𝐶 ) ∈ N ) → ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ∈ N )
39 4 4 38 syl2anc ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ∈ N )
40 mulclpi ⊢ ( ( ( 1st ‘ 𝐴 ) ∈ N ∧ ( 2nd ‘ 𝐵 ) ∈ N ) → ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ∈ N )
41 2 22 40 syl2anc ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ∈ N )
42 mulcanpi ⊢ ( ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ∈ N ∧ ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ∈ N ) → ( ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) = ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ) ↔ ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) = ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ) )
43 39 41 42 syl2anc ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) = ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ) ↔ ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) = ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ) )
44 mulclpi ⊢ ( ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ∈ N ∧ ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ∈ N ) → ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) ∈ N )
45 16 24 44 syl2anc ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) ∈ N )
46 mulclpi ⊢ ( ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ∈ N ∧ ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ∈ N ) → ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) ∈ N )
47 39 41 46 syl2anc ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) ∈ N )
48 addcanpi ⊢ ( ( ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) ∈ N ∧ ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) ∈ N ) → ( ( ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) +N ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) ) = ( ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) +N ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ) ) ↔ ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) = ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ) ) )
49 45 47 48 syl2anc ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( ( ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) +N ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) ) = ( ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) +N ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ) ) ↔ ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) = ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ) ) )
50 mulcompi ⊢ ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) = ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ·N ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) )
51 fvex ⊢ ( 1st ‘ 𝐴 ) ∈ V
52 fvex ⊢ ( 2nd ‘ 𝐵 ) ∈ V
53 fvex ⊢ ( 2nd ‘ 𝐶 ) ∈ V
54 mulcompi ⊢ ( 𝑥 ·N 𝑦 ) = ( 𝑦 ·N 𝑥 )
55 mulasspi ⊢ ( ( 𝑥 ·N 𝑦 ) ·N 𝑧 ) = ( 𝑥 ·N ( 𝑦 ·N 𝑧 ) )
56 51 52 53 54 55 53 caov4 ⊢ ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ·N ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ) = ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) )
57 50 56 eqtri ⊢ ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) = ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) )
58 fvex ⊢ ( 2nd ‘ 𝐴 ) ∈ V
59 fvex ⊢ ( 1st ‘ 𝐶 ) ∈ V
60 58 53 59 54 55 52 caov4 ⊢ ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) = ( ( ( 2nd ‘ 𝐴 ) ·N ( 1st ‘ 𝐶 ) ) ·N ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) )
61 mulcompi ⊢ ( ( 2nd ‘ 𝐴 ) ·N ( 1st ‘ 𝐶 ) ) = ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐴 ) )
62 mulcompi ⊢ ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) = ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) )
63 61 62 oveq12i ⊢ ( ( ( 2nd ‘ 𝐴 ) ·N ( 1st ‘ 𝐶 ) ) ·N ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) = ( ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) )
64 60 63 eqtri ⊢ ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) = ( ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) )
65 57 64 oveq12i ⊢ ( ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) +N ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) ) = ( ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ) +N ( ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ) )
66 addcompi ⊢ ( ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) +N ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) ) = ( ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) +N ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) )
67 ovex ⊢ ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ∈ V
68 ovex ⊢ ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐴 ) ) ∈ V
69 ovex ⊢ ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ∈ V
70 distrpi ⊢ ( 𝑥 ·N ( 𝑦 +N 𝑧 ) ) = ( ( 𝑥 ·N 𝑦 ) +N ( 𝑥 ·N 𝑧 ) )
71 67 68 69 54 70 caovdir ⊢ ( ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐴 ) ) ) ·N ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ) = ( ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ) +N ( ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ) )
72 65 66 71 3eqtr4i ⊢ ( ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) +N ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) ) = ( ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐴 ) ) ) ·N ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) )
73 addcompi ⊢ ( ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) +N ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ) ) = ( ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ) +N ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) )
74 mulasspi ⊢ ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ) = ( ( 2nd ‘ 𝐶 ) ·N ( ( 2nd ‘ 𝐶 ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ) )
75 mulcompi ⊢ ( ( 2nd ‘ 𝐶 ) ·N ( ( 2nd ‘ 𝐶 ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ) ) = ( ( ( 2nd ‘ 𝐶 ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ) ·N ( 2nd ‘ 𝐶 ) )
76 mulasspi ⊢ ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( 1st ‘ 𝐵 ) ) = ( ( 2nd ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐶 ) ·N ( 1st ‘ 𝐵 ) ) )
77 mulcompi ⊢ ( ( 2nd ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐶 ) ·N ( 1st ‘ 𝐵 ) ) ) = ( ( ( 2nd ‘ 𝐶 ) ·N ( 1st ‘ 𝐵 ) ) ·N ( 2nd ‘ 𝐴 ) )
78 mulasspi ⊢ ( ( ( 2nd ‘ 𝐶 ) ·N ( 1st ‘ 𝐵 ) ) ·N ( 2nd ‘ 𝐴 ) ) = ( ( 2nd ‘ 𝐶 ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) )
79 76 77 78 3eqtrri ⊢ ( ( 2nd ‘ 𝐶 ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ) = ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( 1st ‘ 𝐵 ) )
80 79 oveq1i ⊢ ( ( ( 2nd ‘ 𝐶 ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ) ·N ( 2nd ‘ 𝐶 ) ) = ( ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( 1st ‘ 𝐵 ) ) ·N ( 2nd ‘ 𝐶 ) )
81 75 80 eqtri ⊢ ( ( 2nd ‘ 𝐶 ) ·N ( ( 2nd ‘ 𝐶 ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ) ) = ( ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( 1st ‘ 𝐵 ) ) ·N ( 2nd ‘ 𝐶 ) )
82 mulasspi ⊢ ( ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( 1st ‘ 𝐵 ) ) ·N ( 2nd ‘ 𝐶 ) ) = ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) )
83 81 82 eqtri ⊢ ( ( 2nd ‘ 𝐶 ) ·N ( ( 2nd ‘ 𝐶 ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ) ) = ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) )
84 74 83 eqtri ⊢ ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ) = ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) )
85 84 oveq2i ⊢ ( ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) +N ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ) ) = ( ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) +N ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ) )
86 distrpi ⊢ ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) ) = ( ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ) +N ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) )
87 73 85 86 3eqtr4i ⊢ ( ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) +N ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ) ) = ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) )
88 72 87 eqeq12i ⊢ ( ( ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) +N ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) ) = ( ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) +N ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ) ) ↔ ( ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐴 ) ) ) ·N ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ) = ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) ) )
89 49 88 bitr3di ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) = ( ( ( 2nd ‘ 𝐶 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ) ↔ ( ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐴 ) ) ) ·N ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ) = ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) ) ) )
90 37 43 89 3bitr2d ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 𝐴 ~Q 𝐵 ↔ ( ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐴 ) ) ) ·N ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ) = ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ·N ( ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) ) ) )
91 30 35 90 3bitr4rd ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 𝐴 ~Q 𝐵 ↔ ( 𝐴 +pQ 𝐶 ) ~Q ( 𝐵 +pQ 𝐶 ) ) )