Metamath Proof Explorer

Theorem 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 ⋅ 𝑸 / 𝑸 ⁡ B = / 𝑸 ⁡ A ⋅ 𝑝𝑸 B

Proof

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