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