mulerpq

Description: Multiplication is compatible with the equivalence relation. (Contributed by Mario Carneiro, 8-May-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	mulerpq	$⊢ /_{𝑸} (A) \cdot_{𝑸} /_{𝑸} (B) = /_{𝑸} (A \cdot_{𝑝𝑸} B)$

Proof

Step	Hyp	Ref	Expression
1		nqercl	$⊢ A \in (𝑵 \times 𝑵) \to /_{𝑸} (A) \in 𝑸$
2		nqercl	$⊢ B \in (𝑵 \times 𝑵) \to /_{𝑸} (B) \in 𝑸$
3		mulpqnq	$⊢ (/_{𝑸} (A) \in 𝑸 \land /_{𝑸} (B) \in 𝑸) \to /_{𝑸} (A) \cdot_{𝑸} /_{𝑸} (B) = /_{𝑸} (/_{𝑸} (A) \cdot_{𝑝𝑸} /_{𝑸} (B))$
4	1 2 3	syl2an	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to /_{𝑸} (A) \cdot_{𝑸} /_{𝑸} (B) = /_{𝑸} (/_{𝑸} (A) \cdot_{𝑝𝑸} /_{𝑸} (B))$
5		enqer	$⊢ ~_{𝑸} Er (𝑵 \times 𝑵)$
6	5	a1i	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to ~_{𝑸} Er (𝑵 \times 𝑵)$
7		nqerrel	$⊢ A \in (𝑵 \times 𝑵) \to A ~_{𝑸} /_{𝑸} (A)$
8	7	adantr	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to A ~_{𝑸} /_{𝑸} (A)$
9		elpqn	$⊢ /_{𝑸} (A) \in 𝑸 \to /_{𝑸} (A) \in (𝑵 \times 𝑵)$
10	1 9	syl	$⊢ A \in (𝑵 \times 𝑵) \to /_{𝑸} (A) \in (𝑵 \times 𝑵)$
11		mulerpqlem	$⊢ (A \in (𝑵 \times 𝑵) \land /_{𝑸} (A) \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to (A ~_{𝑸} /_{𝑸} (A) \leftrightarrow (A \cdot_{𝑝𝑸} B) ~_{𝑸} (/_{𝑸} (A) \cdot_{𝑝𝑸} B))$
12	11	3exp	$⊢ A \in (𝑵 \times 𝑵) \to (/_{𝑸} (A) \in (𝑵 \times 𝑵) \to (B \in (𝑵 \times 𝑵) \to (A ~_{𝑸} /_{𝑸} (A) \leftrightarrow (A \cdot_{𝑝𝑸} B) ~_{𝑸} (/_{𝑸} (A) \cdot_{𝑝𝑸} B))))$
13	10 12	mpd	$⊢ A \in (𝑵 \times 𝑵) \to (B \in (𝑵 \times 𝑵) \to (A ~_{𝑸} /_{𝑸} (A) \leftrightarrow (A \cdot_{𝑝𝑸} B) ~_{𝑸} (/_{𝑸} (A) \cdot_{𝑝𝑸} B)))$
14	13	imp	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to (A ~_{𝑸} /_{𝑸} (A) \leftrightarrow (A \cdot_{𝑝𝑸} B) ~_{𝑸} (/_{𝑸} (A) \cdot_{𝑝𝑸} B))$
15	8 14	mpbid	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to (A \cdot_{𝑝𝑸} B) ~_{𝑸} (/_{𝑸} (A) \cdot_{𝑝𝑸} B)$
16		nqerrel	$⊢ B \in (𝑵 \times 𝑵) \to B ~_{𝑸} /_{𝑸} (B)$
17	16	adantl	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to B ~_{𝑸} /_{𝑸} (B)$
18		elpqn	$⊢ /_{𝑸} (B) \in 𝑸 \to /_{𝑸} (B) \in (𝑵 \times 𝑵)$
19	2 18	syl	$⊢ B \in (𝑵 \times 𝑵) \to /_{𝑸} (B) \in (𝑵 \times 𝑵)$
20		mulerpqlem	$⊢ (B \in (𝑵 \times 𝑵) \land /_{𝑸} (B) \in (𝑵 \times 𝑵) \land /_{𝑸} (A) \in (𝑵 \times 𝑵)) \to (B ~_{𝑸} /_{𝑸} (B) \leftrightarrow (B \cdot_{𝑝𝑸} /_{𝑸} (A)) ~_{𝑸} (/_{𝑸} (B) \cdot_{𝑝𝑸} /_{𝑸} (A)))$
21	20	3exp	$⊢ B \in (𝑵 \times 𝑵) \to (/_{𝑸} (B) \in (𝑵 \times 𝑵) \to (/_{𝑸} (A) \in (𝑵 \times 𝑵) \to (B ~_{𝑸} /_{𝑸} (B) \leftrightarrow (B \cdot_{𝑝𝑸} /_{𝑸} (A)) ~_{𝑸} (/_{𝑸} (B) \cdot_{𝑝𝑸} /_{𝑸} (A)))))$
22	19 21	mpd	$⊢ B \in (𝑵 \times 𝑵) \to (/_{𝑸} (A) \in (𝑵 \times 𝑵) \to (B ~_{𝑸} /_{𝑸} (B) \leftrightarrow (B \cdot_{𝑝𝑸} /_{𝑸} (A)) ~_{𝑸} (/_{𝑸} (B) \cdot_{𝑝𝑸} /_{𝑸} (A))))$
23	10 22	mpan9	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to (B ~_{𝑸} /_{𝑸} (B) \leftrightarrow (B \cdot_{𝑝𝑸} /_{𝑸} (A)) ~_{𝑸} (/_{𝑸} (B) \cdot_{𝑝𝑸} /_{𝑸} (A)))$
24	17 23	mpbid	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to (B \cdot_{𝑝𝑸} /_{𝑸} (A)) ~_{𝑸} (/_{𝑸} (B) \cdot_{𝑝𝑸} /_{𝑸} (A))$
25		mulcompq	$⊢ B \cdot_{𝑝𝑸} /_{𝑸} (A) = /_{𝑸} (A) \cdot_{𝑝𝑸} B$
26		mulcompq	$⊢ /_{𝑸} (B) \cdot_{𝑝𝑸} /_{𝑸} (A) = /_{𝑸} (A) \cdot_{𝑝𝑸} /_{𝑸} (B)$
27	24 25 26	3brtr3g	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to (/_{𝑸} (A) \cdot_{𝑝𝑸} B) ~_{𝑸} (/_{𝑸} (A) \cdot_{𝑝𝑸} /_{𝑸} (B))$
28	6 15 27	ertrd	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to (A \cdot_{𝑝𝑸} B) ~_{𝑸} (/_{𝑸} (A) \cdot_{𝑝𝑸} /_{𝑸} (B))$
29		mulpqf	$⊢ \cdot_{𝑝𝑸} : (𝑵 \times 𝑵) \times (𝑵 \times 𝑵) ⟶ 𝑵 \times 𝑵$
30	29	fovcl	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to A \cdot_{𝑝𝑸} B \in (𝑵 \times 𝑵)$
31	29	fovcl	$⊢ (/_{𝑸} (A) \in (𝑵 \times 𝑵) \land /_{𝑸} (B) \in (𝑵 \times 𝑵)) \to /_{𝑸} (A) \cdot_{𝑝𝑸} /_{𝑸} (B) \in (𝑵 \times 𝑵)$
32	10 19 31	syl2an	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to /_{𝑸} (A) \cdot_{𝑝𝑸} /_{𝑸} (B) \in (𝑵 \times 𝑵)$
33		nqereq	$⊢ (A \cdot_{𝑝𝑸} B \in (𝑵 \times 𝑵) \land /_{𝑸} (A) \cdot_{𝑝𝑸} /_{𝑸} (B) \in (𝑵 \times 𝑵)) \to ((A \cdot_{𝑝𝑸} B) ~_{𝑸} (/_{𝑸} (A) \cdot_{𝑝𝑸} /_{𝑸} (B)) \leftrightarrow /_{𝑸} (A \cdot_{𝑝𝑸} B) = /_{𝑸} (/_{𝑸} (A) \cdot_{𝑝𝑸} /_{𝑸} (B)))$
34	30 32 33	syl2anc	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to ((A \cdot_{𝑝𝑸} B) ~_{𝑸} (/_{𝑸} (A) \cdot_{𝑝𝑸} /_{𝑸} (B)) \leftrightarrow /_{𝑸} (A \cdot_{𝑝𝑸} B) = /_{𝑸} (/_{𝑸} (A) \cdot_{𝑝𝑸} /_{𝑸} (B)))$
35	28 34	mpbid	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to /_{𝑸} (A \cdot_{𝑝𝑸} B) = /_{𝑸} (/_{𝑸} (A) \cdot_{𝑝𝑸} /_{𝑸} (B))$
36	4 35	eqtr4d	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to /_{𝑸} (A) \cdot_{𝑸} /_{𝑸} (B) = /_{𝑸} (A \cdot_{𝑝𝑸} B)$
37		0nnq	$⊢ \neg \emptyset \in 𝑸$
38		nqerf	$⊢ /_{𝑸} : 𝑵 \times 𝑵 ⟶ 𝑸$
39	38	fdmi	$⊢ dom /_{𝑸} = 𝑵 \times 𝑵$
40	39	eleq2i	$⊢ A \in dom /_{𝑸} \leftrightarrow A \in (𝑵 \times 𝑵)$
41		ndmfv	$⊢ \neg A \in dom /_{𝑸} \to /_{𝑸} (A) = \emptyset$
42	40 41	sylnbir	$⊢ \neg A \in (𝑵 \times 𝑵) \to /_{𝑸} (A) = \emptyset$
43	42	eleq1d	$⊢ \neg A \in (𝑵 \times 𝑵) \to (/_{𝑸} (A) \in 𝑸 \leftrightarrow \emptyset \in 𝑸)$
44	37 43	mtbiri	$⊢ \neg A \in (𝑵 \times 𝑵) \to \neg /_{𝑸} (A) \in 𝑸$
45	44	con4i	$⊢ /_{𝑸} (A) \in 𝑸 \to A \in (𝑵 \times 𝑵)$
46	39	eleq2i	$⊢ B \in dom /_{𝑸} \leftrightarrow B \in (𝑵 \times 𝑵)$
47		ndmfv	$⊢ \neg B \in dom /_{𝑸} \to /_{𝑸} (B) = \emptyset$
48	46 47	sylnbir	$⊢ \neg B \in (𝑵 \times 𝑵) \to /_{𝑸} (B) = \emptyset$
49	48	eleq1d	$⊢ \neg B \in (𝑵 \times 𝑵) \to (/_{𝑸} (B) \in 𝑸 \leftrightarrow \emptyset \in 𝑸)$
50	37 49	mtbiri	$⊢ \neg B \in (𝑵 \times 𝑵) \to \neg /_{𝑸} (B) \in 𝑸$
51	50	con4i	$⊢ /_{𝑸} (B) \in 𝑸 \to B \in (𝑵 \times 𝑵)$
52	45 51	anim12i	$⊢ (/_{𝑸} (A) \in 𝑸 \land /_{𝑸} (B) \in 𝑸) \to (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵))$
53		mulnqf	$⊢ \cdot_{𝑸} : 𝑸 \times 𝑸 ⟶ 𝑸$
54	53	fdmi	$⊢ dom \cdot_{𝑸} = 𝑸 \times 𝑸$
55	54	ndmov	$⊢ \neg (/_{𝑸} (A) \in 𝑸 \land /_{𝑸} (B) \in 𝑸) \to /_{𝑸} (A) \cdot_{𝑸} /_{𝑸} (B) = \emptyset$
56	52 55	nsyl5	$⊢ \neg (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to /_{𝑸} (A) \cdot_{𝑸} /_{𝑸} (B) = \emptyset$
57		0nelxp	$⊢ \neg \emptyset \in (𝑵 \times 𝑵)$
58	39	eleq2i	$⊢ \emptyset \in dom /_{𝑸} \leftrightarrow \emptyset \in (𝑵 \times 𝑵)$
59	57 58	mtbir	$⊢ \neg \emptyset \in dom /_{𝑸}$
60	29	fdmi	$⊢ dom \cdot_{𝑝𝑸} = (𝑵 \times 𝑵) \times (𝑵 \times 𝑵)$
61	60	ndmov	$⊢ \neg (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to A \cdot_{𝑝𝑸} B = \emptyset$
62	61	eleq1d	$⊢ \neg (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to (A \cdot_{𝑝𝑸} B \in dom /_{𝑸} \leftrightarrow \emptyset \in dom /_{𝑸})$
63	59 62	mtbiri	$⊢ \neg (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to \neg A \cdot_{𝑝𝑸} B \in dom /_{𝑸}$
64		ndmfv	$⊢ \neg A \cdot_{𝑝𝑸} B \in dom /_{𝑸} \to /_{𝑸} (A \cdot_{𝑝𝑸} B) = \emptyset$
65	63 64	syl	$⊢ \neg (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to /_{𝑸} (A \cdot_{𝑝𝑸} B) = \emptyset$
66	56 65	eqtr4d	$⊢ \neg (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to /_{𝑸} (A) \cdot_{𝑸} /_{𝑸} (B) = /_{𝑸} (A \cdot_{𝑝𝑸} B)$
67	36 66	pm2.61i	$⊢ /_{𝑸} (A) \cdot_{𝑸} /_{𝑸} (B) = /_{𝑸} (A \cdot_{𝑝𝑸} B)$

Metamath Proof Explorer

Theorem mulerpq

Proof