Metamath Proof Explorer

Theorem adderpq

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

Ref Expression
Assertion adderpq ⊢/𝑸⁡A+𝑸/𝑸⁡B=/𝑸⁡A+𝑝𝑸B

Proof

Step Hyp Ref Expression
1 nqercl ⊢A∈𝑵×𝑵→/𝑸⁡A∈𝑸
2 nqercl ⊢B∈𝑵×𝑵→/𝑸⁡B∈𝑸
3 addpqnq ⊢/𝑸⁡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 adderpqlem ⊢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 adderpqlem ⊢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 addcompq ⊢B+𝑝𝑸/𝑸⁡A=/𝑸⁡A+𝑝𝑸B
26 addcompq ⊢/𝑸⁡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 addpqf ⊢+𝑝𝑸:𝑵×𝑵×𝑵×𝑵⟶𝑵×𝑵
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 addnqf ⊢+𝑸:𝑸×𝑸⟶𝑸
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