adderpqlem

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

		Ref	Expression
	Assertion	adderpqlem	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to (A ~_{𝑸} B \leftrightarrow (A +_{𝑝𝑸} C) ~_{𝑸} (B +_{𝑝𝑸} C))$

Proof

Step	Hyp	Ref	Expression
1		xp1st	$⊢ A \in (𝑵 \times 𝑵) \to 1^{st} (A) \in 𝑵$
2	1	3ad2ant1	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to 1^{st} (A) \in 𝑵$
3		xp2nd	$⊢ C \in (𝑵 \times 𝑵) \to 2^{nd} (C) \in 𝑵$
4	3	3ad2ant3	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to 2^{nd} (C) \in 𝑵$
5		mulclpi	$⊢ (1^{st} (A) \in 𝑵 \land 2^{nd} (C) \in 𝑵) \to 1^{st} (A) \cdot_{𝑵} 2^{nd} (C) \in 𝑵$
6	2 4 5	syl2anc	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to 1^{st} (A) \cdot_{𝑵} 2^{nd} (C) \in 𝑵$
7		xp1st	$⊢ C \in (𝑵 \times 𝑵) \to 1^{st} (C) \in 𝑵$
8	7	3ad2ant3	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to 1^{st} (C) \in 𝑵$
9		xp2nd	$⊢ A \in (𝑵 \times 𝑵) \to 2^{nd} (A) \in 𝑵$
10	9	3ad2ant1	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to 2^{nd} (A) \in 𝑵$
11		mulclpi	$⊢ (1^{st} (C) \in 𝑵 \land 2^{nd} (A) \in 𝑵) \to 1^{st} (C) \cdot_{𝑵} 2^{nd} (A) \in 𝑵$
12	8 10 11	syl2anc	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to 1^{st} (C) \cdot_{𝑵} 2^{nd} (A) \in 𝑵$
13		addclpi	$⊢ (1^{st} (A) \cdot_{𝑵} 2^{nd} (C) \in 𝑵 \land 1^{st} (C) \cdot_{𝑵} 2^{nd} (A) \in 𝑵) \to (1^{st} (A) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A)) \in 𝑵$
14	6 12 13	syl2anc	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to (1^{st} (A) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A)) \in 𝑵$
15		mulclpi	$⊢ (2^{nd} (A) \in 𝑵 \land 2^{nd} (C) \in 𝑵) \to 2^{nd} (A) \cdot_{𝑵} 2^{nd} (C) \in 𝑵$
16	10 4 15	syl2anc	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to 2^{nd} (A) \cdot_{𝑵} 2^{nd} (C) \in 𝑵$
17		xp1st	$⊢ B \in (𝑵 \times 𝑵) \to 1^{st} (B) \in 𝑵$
18	17	3ad2ant2	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to 1^{st} (B) \in 𝑵$
19		mulclpi	$⊢ (1^{st} (B) \in 𝑵 \land 2^{nd} (C) \in 𝑵) \to 1^{st} (B) \cdot_{𝑵} 2^{nd} (C) \in 𝑵$
20	18 4 19	syl2anc	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to 1^{st} (B) \cdot_{𝑵} 2^{nd} (C) \in 𝑵$
21		xp2nd	$⊢ B \in (𝑵 \times 𝑵) \to 2^{nd} (B) \in 𝑵$
22	21	3ad2ant2	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to 2^{nd} (B) \in 𝑵$
23		mulclpi	$⊢ (1^{st} (C) \in 𝑵 \land 2^{nd} (B) \in 𝑵) \to 1^{st} (C) \cdot_{𝑵} 2^{nd} (B) \in 𝑵$
24	8 22 23	syl2anc	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to 1^{st} (C) \cdot_{𝑵} 2^{nd} (B) \in 𝑵$
25		addclpi	$⊢ (1^{st} (B) \cdot_{𝑵} 2^{nd} (C) \in 𝑵 \land 1^{st} (C) \cdot_{𝑵} 2^{nd} (B) \in 𝑵) \to (1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)) \in 𝑵$
26	20 24 25	syl2anc	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to (1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)) \in 𝑵$
27		mulclpi	$⊢ (2^{nd} (B) \in 𝑵 \land 2^{nd} (C) \in 𝑵) \to 2^{nd} (B) \cdot_{𝑵} 2^{nd} (C) \in 𝑵$
28	22 4 27	syl2anc	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to 2^{nd} (B) \cdot_{𝑵} 2^{nd} (C) \in 𝑵$
29		enqbreq	$⊢ (((1^{st} (A) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A)) \in 𝑵 \land 2^{nd} (A) \cdot_{𝑵} 2^{nd} (C) \in 𝑵) \land ((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)) \in 𝑵 \land 2^{nd} (B) \cdot_{𝑵} 2^{nd} (C) \in 𝑵)) \to (⟨(1^{st} (A) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A)), 2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)⟩ ~_{𝑸} ⟨(1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)), 2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)⟩ \leftrightarrow ((1^{st} (A) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A))) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)) = (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} ((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))))$
30	14 16 26 28 29	syl22anc	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to (⟨(1^{st} (A) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A)), 2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)⟩ ~_{𝑸} ⟨(1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)), 2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)⟩ \leftrightarrow ((1^{st} (A) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A))) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)) = (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} ((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))))$
31		addpipq2	$⊢ (A \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to A +_{𝑝𝑸} C = ⟨(1^{st} (A) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A)), 2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)⟩$
32	31	3adant2	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to A +_{𝑝𝑸} C = ⟨(1^{st} (A) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A)), 2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)⟩$
33		addpipq2	$⊢ (B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to B +_{𝑝𝑸} C = ⟨(1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)), 2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)⟩$
34	33	3adant1	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to B +_{𝑝𝑸} C = ⟨(1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)), 2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)⟩$
35	32 34	breq12d	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to ((A +_{𝑝𝑸} C) ~_{𝑸} (B +_{𝑝𝑸} C) \leftrightarrow ⟨(1^{st} (A) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A)), 2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)⟩ ~_{𝑸} ⟨(1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)), 2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)⟩)$
36		enqbreq2	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to (A ~_{𝑸} B \leftrightarrow 1^{st} (A) \cdot_{𝑵} 2^{nd} (B) = 1^{st} (B) \cdot_{𝑵} 2^{nd} (A))$
37	36	3adant3	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to (A ~_{𝑸} B \leftrightarrow 1^{st} (A) \cdot_{𝑵} 2^{nd} (B) = 1^{st} (B) \cdot_{𝑵} 2^{nd} (A))$
38		mulclpi	$⊢ (2^{nd} (C) \in 𝑵 \land 2^{nd} (C) \in 𝑵) \to 2^{nd} (C) \cdot_{𝑵} 2^{nd} (C) \in 𝑵$
39	4 4 38	syl2anc	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to 2^{nd} (C) \cdot_{𝑵} 2^{nd} (C) \in 𝑵$
40		mulclpi	$⊢ (1^{st} (A) \in 𝑵 \land 2^{nd} (B) \in 𝑵) \to 1^{st} (A) \cdot_{𝑵} 2^{nd} (B) \in 𝑵$
41	2 22 40	syl2anc	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to 1^{st} (A) \cdot_{𝑵} 2^{nd} (B) \in 𝑵$
42		mulcanpi	$⊢ (2^{nd} (C) \cdot_{𝑵} 2^{nd} (C) \in 𝑵 \land 1^{st} (A) \cdot_{𝑵} 2^{nd} (B) \in 𝑵) \to ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) = (2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \leftrightarrow 1^{st} (A) \cdot_{𝑵} 2^{nd} (B) = 1^{st} (B) \cdot_{𝑵} 2^{nd} (A))$
43	39 41 42	syl2anc	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) = (2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \leftrightarrow 1^{st} (A) \cdot_{𝑵} 2^{nd} (B) = 1^{st} (B) \cdot_{𝑵} 2^{nd} (A))$
44		mulclpi	$⊢ (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C) \in 𝑵 \land 1^{st} (C) \cdot_{𝑵} 2^{nd} (B) \in 𝑵) \to (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)) \in 𝑵$
45	16 24 44	syl2anc	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)) \in 𝑵$
46		mulclpi	$⊢ (2^{nd} (C) \cdot_{𝑵} 2^{nd} (C) \in 𝑵 \land 1^{st} (A) \cdot_{𝑵} 2^{nd} (B) \in 𝑵) \to (2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) \in 𝑵$
47	39 41 46	syl2anc	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to (2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) \in 𝑵$
48		addcanpi	$⊢ ((2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)) \in 𝑵 \land (2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) \in 𝑵) \to (((2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))) +_{𝑵} ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B))) = ((2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))) +_{𝑵} ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A))) \leftrightarrow (2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) = (2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)))$
49	45 47 48	syl2anc	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to (((2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))) +_{𝑵} ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B))) = ((2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))) +_{𝑵} ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A))) \leftrightarrow (2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) = (2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)))$
50		mulcompi	$⊢ (2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) = (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (2^{nd} (C) \cdot_{𝑵} 2^{nd} (C))$
51		fvex	$⊢ 1^{st} (A) \in V$
52		fvex	$⊢ 2^{nd} (B) \in V$
53		fvex	$⊢ 2^{nd} (C) \in V$
54		mulcompi	$⊢ x \cdot_{𝑵} y = y \cdot_{𝑵} x$
55		mulasspi	$⊢ (x \cdot_{𝑵} y) \cdot_{𝑵} z = x \cdot_{𝑵} (y \cdot_{𝑵} z)$
56	51 52 53 54 55 53	caov4	$⊢ (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) = (1^{st} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))$
57	50 56	eqtri	$⊢ (2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) = (1^{st} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))$
58		fvex	$⊢ 2^{nd} (A) \in V$
59		fvex	$⊢ 1^{st} (C) \in V$
60	58 53 59 54 55 52	caov4	$⊢ (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)) = (2^{nd} (A) \cdot_{𝑵} 1^{st} (C)) \cdot_{𝑵} (2^{nd} (C) \cdot_{𝑵} 2^{nd} (B))$
61		mulcompi	$⊢ 2^{nd} (A) \cdot_{𝑵} 1^{st} (C) = 1^{st} (C) \cdot_{𝑵} 2^{nd} (A)$
62		mulcompi	$⊢ 2^{nd} (C) \cdot_{𝑵} 2^{nd} (B) = 2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)$
63	61 62	oveq12i	$⊢ (2^{nd} (A) \cdot_{𝑵} 1^{st} (C)) \cdot_{𝑵} (2^{nd} (C) \cdot_{𝑵} 2^{nd} (B)) = (1^{st} (C) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))$
64	60 63	eqtri	$⊢ (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)) = (1^{st} (C) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))$
65	57 64	oveq12i	$⊢ ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B))) +_{𝑵} ((2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))) = ((1^{st} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))) +_{𝑵} ((1^{st} (C) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)))$
66		addcompi	$⊢ ((2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))) +_{𝑵} ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B))) = ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B))) +_{𝑵} ((2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)))$
67		ovex	$⊢ 1^{st} (A) \cdot_{𝑵} 2^{nd} (C) \in V$
68		ovex	$⊢ 1^{st} (C) \cdot_{𝑵} 2^{nd} (A) \in V$
69		ovex	$⊢ 2^{nd} (B) \cdot_{𝑵} 2^{nd} (C) \in V$
70		distrpi	$⊢ x \cdot_{𝑵} (y +_{𝑵} z) = (x \cdot_{𝑵} y) +_{𝑵} (x \cdot_{𝑵} z)$
71	67 68 69 54 70	caovdir	$⊢ ((1^{st} (A) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A))) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)) = ((1^{st} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))) +_{𝑵} ((1^{st} (C) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)))$
72	65 66 71	3eqtr4i	$⊢ ((2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))) +_{𝑵} ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B))) = ((1^{st} (A) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A))) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))$
73		addcompi	$⊢ ((2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))) +_{𝑵} ((2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (C))) = ((2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (C))) +_{𝑵} ((2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)))$
74		mulasspi	$⊢ (2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) = 2^{nd} (C) \cdot_{𝑵} (2^{nd} (C) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)))$
75		mulcompi	$⊢ 2^{nd} (C) \cdot_{𝑵} (2^{nd} (C) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A))) = (2^{nd} (C) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A))) \cdot_{𝑵} 2^{nd} (C)$
76		mulasspi	$⊢ (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} 1^{st} (B) = 2^{nd} (A) \cdot_{𝑵} (2^{nd} (C) \cdot_{𝑵} 1^{st} (B))$
77		mulcompi	$⊢ 2^{nd} (A) \cdot_{𝑵} (2^{nd} (C) \cdot_{𝑵} 1^{st} (B)) = (2^{nd} (C) \cdot_{𝑵} 1^{st} (B)) \cdot_{𝑵} 2^{nd} (A)$
78		mulasspi	$⊢ (2^{nd} (C) \cdot_{𝑵} 1^{st} (B)) \cdot_{𝑵} 2^{nd} (A) = 2^{nd} (C) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A))$
79	76 77 78	3eqtrri	$⊢ 2^{nd} (C) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) = (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} 1^{st} (B)$
80	79	oveq1i	$⊢ (2^{nd} (C) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A))) \cdot_{𝑵} 2^{nd} (C) = ((2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} 1^{st} (B)) \cdot_{𝑵} 2^{nd} (C)$
81	75 80	eqtri	$⊢ 2^{nd} (C) \cdot_{𝑵} (2^{nd} (C) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A))) = ((2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} 1^{st} (B)) \cdot_{𝑵} 2^{nd} (C)$
82		mulasspi	$⊢ ((2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} 1^{st} (B)) \cdot_{𝑵} 2^{nd} (C) = (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (C))$
83	81 82	eqtri	$⊢ 2^{nd} (C) \cdot_{𝑵} (2^{nd} (C) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A))) = (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (C))$
84	74 83	eqtri	$⊢ (2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) = (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (C))$
85	84	oveq2i	$⊢ ((2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))) +_{𝑵} ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A))) = ((2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))) +_{𝑵} ((2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (C)))$
86		distrpi	$⊢ (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} ((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))) = ((2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (C))) +_{𝑵} ((2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)))$
87	73 85 86	3eqtr4i	$⊢ ((2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))) +_{𝑵} ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A))) = (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} ((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)))$
88	72 87	eqeq12i	$⊢ ((2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))) +_{𝑵} ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B))) = ((2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))) +_{𝑵} ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A))) \leftrightarrow ((1^{st} (A) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A))) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)) = (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} ((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)))$
89	49 88	bitr3di	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to ((2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) = (2^{nd} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \leftrightarrow ((1^{st} (A) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A))) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)) = (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} ((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))))$
90	37 43 89	3bitr2d	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to (A ~_{𝑸} B \leftrightarrow ((1^{st} (A) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (A))) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)) = (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} ((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))))$
91	30 35 90	3bitr4rd	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to (A ~_{𝑸} B \leftrightarrow (A +_{𝑝𝑸} C) ~_{𝑸} (B +_{𝑝𝑸} C))$

Metamath Proof Explorer

Theorem adderpqlem

Proof