mulerpqlem

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

		Ref	Expression
	Assertion	mulerpqlem	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to (A ~_{𝑸} B \leftrightarrow (A \cdot_{𝑝𝑸} C) ~_{𝑸} (B \cdot_{𝑝𝑸} 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		xp1st	$⊢ C \in (𝑵 \times 𝑵) \to 1^{st} (C) \in 𝑵$
4	3	3ad2ant3	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to 1^{st} (C) \in 𝑵$
5		mulclpi	$⊢ (1^{st} (A) \in 𝑵 \land 1^{st} (C) \in 𝑵) \to 1^{st} (A) \cdot_{𝑵} 1^{st} (C) \in 𝑵$
6	2 4 5	syl2anc	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to 1^{st} (A) \cdot_{𝑵} 1^{st} (C) \in 𝑵$
7		xp2nd	$⊢ A \in (𝑵 \times 𝑵) \to 2^{nd} (A) \in 𝑵$
8	7	3ad2ant1	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to 2^{nd} (A) \in 𝑵$
9		xp2nd	$⊢ C \in (𝑵 \times 𝑵) \to 2^{nd} (C) \in 𝑵$
10	9	3ad2ant3	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to 2^{nd} (C) \in 𝑵$
11		mulclpi	$⊢ (2^{nd} (A) \in 𝑵 \land 2^{nd} (C) \in 𝑵) \to 2^{nd} (A) \cdot_{𝑵} 2^{nd} (C) \in 𝑵$
12	8 10 11	syl2anc	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to 2^{nd} (A) \cdot_{𝑵} 2^{nd} (C) \in 𝑵$
13		xp1st	$⊢ B \in (𝑵 \times 𝑵) \to 1^{st} (B) \in 𝑵$
14	13	3ad2ant2	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to 1^{st} (B) \in 𝑵$
15		mulclpi	$⊢ (1^{st} (B) \in 𝑵 \land 1^{st} (C) \in 𝑵) \to 1^{st} (B) \cdot_{𝑵} 1^{st} (C) \in 𝑵$
16	14 4 15	syl2anc	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to 1^{st} (B) \cdot_{𝑵} 1^{st} (C) \in 𝑵$
17		xp2nd	$⊢ B \in (𝑵 \times 𝑵) \to 2^{nd} (B) \in 𝑵$
18	17	3ad2ant2	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to 2^{nd} (B) \in 𝑵$
19		mulclpi	$⊢ (2^{nd} (B) \in 𝑵 \land 2^{nd} (C) \in 𝑵) \to 2^{nd} (B) \cdot_{𝑵} 2^{nd} (C) \in 𝑵$
20	18 10 19	syl2anc	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to 2^{nd} (B) \cdot_{𝑵} 2^{nd} (C) \in 𝑵$
21		enqbreq	$⊢ ((1^{st} (A) \cdot_{𝑵} 1^{st} (C) \in 𝑵 \land 2^{nd} (A) \cdot_{𝑵} 2^{nd} (C) \in 𝑵) \land (1^{st} (B) \cdot_{𝑵} 1^{st} (C) \in 𝑵 \land 2^{nd} (B) \cdot_{𝑵} 2^{nd} (C) \in 𝑵)) \to (⟨1^{st} (A) \cdot_{𝑵} 1^{st} (C), 2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)⟩ ~_{𝑸} ⟨1^{st} (B) \cdot_{𝑵} 1^{st} (C), 2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)⟩ \leftrightarrow (1^{st} (A) \cdot_{𝑵} 1^{st} (C)) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)) = (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 1^{st} (C)))$
22	6 12 16 20 21	syl22anc	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to (⟨1^{st} (A) \cdot_{𝑵} 1^{st} (C), 2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)⟩ ~_{𝑸} ⟨1^{st} (B) \cdot_{𝑵} 1^{st} (C), 2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)⟩ \leftrightarrow (1^{st} (A) \cdot_{𝑵} 1^{st} (C)) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)) = (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 1^{st} (C)))$
23		mulpipq2	$⊢ (A \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to A \cdot_{𝑝𝑸} C = ⟨1^{st} (A) \cdot_{𝑵} 1^{st} (C), 2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)⟩$
24	23	3adant2	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to A \cdot_{𝑝𝑸} C = ⟨1^{st} (A) \cdot_{𝑵} 1^{st} (C), 2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)⟩$
25		mulpipq2	$⊢ (B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to B \cdot_{𝑝𝑸} C = ⟨1^{st} (B) \cdot_{𝑵} 1^{st} (C), 2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)⟩$
26	25	3adant1	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to B \cdot_{𝑝𝑸} C = ⟨1^{st} (B) \cdot_{𝑵} 1^{st} (C), 2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)⟩$
27	24 26	breq12d	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to ((A \cdot_{𝑝𝑸} C) ~_{𝑸} (B \cdot_{𝑝𝑸} C) \leftrightarrow ⟨1^{st} (A) \cdot_{𝑵} 1^{st} (C), 2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)⟩ ~_{𝑸} ⟨1^{st} (B) \cdot_{𝑵} 1^{st} (C), 2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)⟩)$
28		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))$
29	28	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))$
30		mulclpi	$⊢ (1^{st} (C) \in 𝑵 \land 2^{nd} (C) \in 𝑵) \to 1^{st} (C) \cdot_{𝑵} 2^{nd} (C) \in 𝑵$
31	4 10 30	syl2anc	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to 1^{st} (C) \cdot_{𝑵} 2^{nd} (C) \in 𝑵$
32		mulclpi	$⊢ (1^{st} (A) \in 𝑵 \land 2^{nd} (B) \in 𝑵) \to 1^{st} (A) \cdot_{𝑵} 2^{nd} (B) \in 𝑵$
33	2 18 32	syl2anc	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to 1^{st} (A) \cdot_{𝑵} 2^{nd} (B) \in 𝑵$
34		mulcanpi	$⊢ (1^{st} (C) \cdot_{𝑵} 2^{nd} (C) \in 𝑵 \land 1^{st} (A) \cdot_{𝑵} 2^{nd} (B) \in 𝑵) \to ((1^{st} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) = (1^{st} (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))$
35	31 33 34	syl2anc	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to ((1^{st} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) = (1^{st} (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))$
36		mulcompi	$⊢ (1^{st} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) = (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (C))$
37		fvex	$⊢ 1^{st} (A) \in V$
38		fvex	$⊢ 2^{nd} (B) \in V$
39		fvex	$⊢ 1^{st} (C) \in V$
40		mulcompi	$⊢ x \cdot_{𝑵} y = y \cdot_{𝑵} x$
41		mulasspi	$⊢ (x \cdot_{𝑵} y) \cdot_{𝑵} z = x \cdot_{𝑵} (y \cdot_{𝑵} z)$
42		fvex	$⊢ 2^{nd} (C) \in V$
43	37 38 39 40 41 42	caov4	$⊢ (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (C)) = (1^{st} (A) \cdot_{𝑵} 1^{st} (C)) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))$
44	36 43	eqtri	$⊢ (1^{st} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) = (1^{st} (A) \cdot_{𝑵} 1^{st} (C)) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))$
45		mulcompi	$⊢ (1^{st} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) = (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (C))$
46		fvex	$⊢ 1^{st} (B) \in V$
47		fvex	$⊢ 2^{nd} (A) \in V$
48	46 47 39 40 41 42	caov4	$⊢ (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (C)) = (1^{st} (B) \cdot_{𝑵} 1^{st} (C)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C))$
49		mulcompi	$⊢ (1^{st} (B) \cdot_{𝑵} 1^{st} (C)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) = (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 1^{st} (C))$
50	45 48 49	3eqtri	$⊢ (1^{st} (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_{𝑵} 1^{st} (C))$
51	44 50	eqeq12i	$⊢ (1^{st} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) = (1^{st} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \leftrightarrow (1^{st} (A) \cdot_{𝑵} 1^{st} (C)) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)) = (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 1^{st} (C))$
52	51	a1i	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to ((1^{st} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) = (1^{st} (C) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \leftrightarrow (1^{st} (A) \cdot_{𝑵} 1^{st} (C)) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)) = (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 1^{st} (C)))$
53	29 35 52	3bitr2d	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to (A ~_{𝑸} B \leftrightarrow (1^{st} (A) \cdot_{𝑵} 1^{st} (C)) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)) = (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 1^{st} (C)))$
54	22 27 53	3bitr4rd	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to (A ~_{𝑸} B \leftrightarrow (A \cdot_{𝑝𝑸} C) ~_{𝑸} (B \cdot_{𝑝𝑸} C))$

Metamath Proof Explorer

Theorem mulerpqlem

Proof