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 ( ( [Q] ‘ 𝐴 ) +Q ( [Q] ‘ 𝐵 ) ) = ( [Q] ‘ ( 𝐴 +pQ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 nqercl ⊢ ( 𝐴 ∈ ( N × N ) → ( [Q] ‘ 𝐴 ) ∈ Q )
2 nqercl ⊢ ( 𝐵 ∈ ( N × N ) → ( [Q] ‘ 𝐵 ) ∈ Q )
3 addpqnq ⊢ ( ( ( [Q] ‘ 𝐴 ) ∈ Q ∧ ( [Q] ‘ 𝐵 ) ∈ Q ) → ( ( [Q] ‘ 𝐴 ) +Q ( [Q] ‘ 𝐵 ) ) = ( [Q] ‘ ( ( [Q] ‘ 𝐴 ) +pQ ( [Q] ‘ 𝐵 ) ) ) )
4 1 2 3 syl2an ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( ( [Q] ‘ 𝐴 ) +Q ( [Q] ‘ 𝐵 ) ) = ( [Q] ‘ ( ( [Q] ‘ 𝐴 ) +pQ ( [Q] ‘ 𝐵 ) ) ) )
5 enqer ⊢ ~Q Er ( N × N )
6 5 a1i ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ~Q Er ( N × N ) )
7 nqerrel ⊢ ( 𝐴 ∈ ( N × N ) → 𝐴 ~Q ( [Q] ‘ 𝐴 ) )
8 7 adantr ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → 𝐴 ~Q ( [Q] ‘ 𝐴 ) )
9 elpqn ⊢ ( ( [Q] ‘ 𝐴 ) ∈ Q → ( [Q] ‘ 𝐴 ) ∈ ( N × N ) )
10 1 9 syl ⊢ ( 𝐴 ∈ ( N × N ) → ( [Q] ‘ 𝐴 ) ∈ ( N × N ) )
11 adderpqlem ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ ( [Q] ‘ 𝐴 ) ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 ~Q ( [Q] ‘ 𝐴 ) ↔ ( 𝐴 +pQ 𝐵 ) ~Q ( ( [Q] ‘ 𝐴 ) +pQ 𝐵 ) ) )
12 11 3exp ⊢ ( 𝐴 ∈ ( N × N ) → ( ( [Q] ‘ 𝐴 ) ∈ ( N × N ) → ( 𝐵 ∈ ( N × N ) → ( 𝐴 ~Q ( [Q] ‘ 𝐴 ) ↔ ( 𝐴 +pQ 𝐵 ) ~Q ( ( [Q] ‘ 𝐴 ) +pQ 𝐵 ) ) ) ) )
13 10 12 mpd ⊢ ( 𝐴 ∈ ( N × N ) → ( 𝐵 ∈ ( N × N ) → ( 𝐴 ~Q ( [Q] ‘ 𝐴 ) ↔ ( 𝐴 +pQ 𝐵 ) ~Q ( ( [Q] ‘ 𝐴 ) +pQ 𝐵 ) ) ) )
14 13 imp ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 ~Q ( [Q] ‘ 𝐴 ) ↔ ( 𝐴 +pQ 𝐵 ) ~Q ( ( [Q] ‘ 𝐴 ) +pQ 𝐵 ) ) )
15 8 14 mpbid ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 +pQ 𝐵 ) ~Q ( ( [Q] ‘ 𝐴 ) +pQ 𝐵 ) )
16 nqerrel ⊢ ( 𝐵 ∈ ( N × N ) → 𝐵 ~Q ( [Q] ‘ 𝐵 ) )
17 16 adantl ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → 𝐵 ~Q ( [Q] ‘ 𝐵 ) )
18 elpqn ⊢ ( ( [Q] ‘ 𝐵 ) ∈ Q → ( [Q] ‘ 𝐵 ) ∈ ( N × N ) )
19 2 18 syl ⊢ ( 𝐵 ∈ ( N × N ) → ( [Q] ‘ 𝐵 ) ∈ ( N × N ) )
20 adderpqlem ⊢ ( ( 𝐵 ∈ ( N × N ) ∧ ( [Q] ‘ 𝐵 ) ∈ ( N × N ) ∧ ( [Q] ‘ 𝐴 ) ∈ ( N × N ) ) → ( 𝐵 ~Q ( [Q] ‘ 𝐵 ) ↔ ( 𝐵 +pQ ( [Q] ‘ 𝐴 ) ) ~Q ( ( [Q] ‘ 𝐵 ) +pQ ( [Q] ‘ 𝐴 ) ) ) )
21 20 3exp ⊢ ( 𝐵 ∈ ( N × N ) → ( ( [Q] ‘ 𝐵 ) ∈ ( N × N ) → ( ( [Q] ‘ 𝐴 ) ∈ ( N × N ) → ( 𝐵 ~Q ( [Q] ‘ 𝐵 ) ↔ ( 𝐵 +pQ ( [Q] ‘ 𝐴 ) ) ~Q ( ( [Q] ‘ 𝐵 ) +pQ ( [Q] ‘ 𝐴 ) ) ) ) ) )
22 19 21 mpd ⊢ ( 𝐵 ∈ ( N × N ) → ( ( [Q] ‘ 𝐴 ) ∈ ( N × N ) → ( 𝐵 ~Q ( [Q] ‘ 𝐵 ) ↔ ( 𝐵 +pQ ( [Q] ‘ 𝐴 ) ) ~Q ( ( [Q] ‘ 𝐵 ) +pQ ( [Q] ‘ 𝐴 ) ) ) ) )
23 10 22 mpan9 ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐵 ~Q ( [Q] ‘ 𝐵 ) ↔ ( 𝐵 +pQ ( [Q] ‘ 𝐴 ) ) ~Q ( ( [Q] ‘ 𝐵 ) +pQ ( [Q] ‘ 𝐴 ) ) ) )
24 17 23 mpbid ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐵 +pQ ( [Q] ‘ 𝐴 ) ) ~Q ( ( [Q] ‘ 𝐵 ) +pQ ( [Q] ‘ 𝐴 ) ) )
25 addcompq ⊢ ( 𝐵 +pQ ( [Q] ‘ 𝐴 ) ) = ( ( [Q] ‘ 𝐴 ) +pQ 𝐵 )
26 addcompq ⊢ ( ( [Q] ‘ 𝐵 ) +pQ ( [Q] ‘ 𝐴 ) ) = ( ( [Q] ‘ 𝐴 ) +pQ ( [Q] ‘ 𝐵 ) )
27 24 25 26 3brtr3g ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( ( [Q] ‘ 𝐴 ) +pQ 𝐵 ) ~Q ( ( [Q] ‘ 𝐴 ) +pQ ( [Q] ‘ 𝐵 ) ) )
28 6 15 27 ertrd ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 +pQ 𝐵 ) ~Q ( ( [Q] ‘ 𝐴 ) +pQ ( [Q] ‘ 𝐵 ) ) )
29 addpqf ⊢ +pQ : ( ( N × N ) × ( N × N ) ) ⟶ ( N × N )
30 29 fovcl ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 +pQ 𝐵 ) ∈ ( N × N ) )
31 29 fovcl ⊢ ( ( ( [Q] ‘ 𝐴 ) ∈ ( N × N ) ∧ ( [Q] ‘ 𝐵 ) ∈ ( N × N ) ) → ( ( [Q] ‘ 𝐴 ) +pQ ( [Q] ‘ 𝐵 ) ) ∈ ( N × N ) )
32 10 19 31 syl2an ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( ( [Q] ‘ 𝐴 ) +pQ ( [Q] ‘ 𝐵 ) ) ∈ ( N × N ) )
33 nqereq ⊢ ( ( ( 𝐴 +pQ 𝐵 ) ∈ ( N × N ) ∧ ( ( [Q] ‘ 𝐴 ) +pQ ( [Q] ‘ 𝐵 ) ) ∈ ( N × N ) ) → ( ( 𝐴 +pQ 𝐵 ) ~Q ( ( [Q] ‘ 𝐴 ) +pQ ( [Q] ‘ 𝐵 ) ) ↔ ( [Q] ‘ ( 𝐴 +pQ 𝐵 ) ) = ( [Q] ‘ ( ( [Q] ‘ 𝐴 ) +pQ ( [Q] ‘ 𝐵 ) ) ) ) )
34 30 32 33 syl2anc ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( ( 𝐴 +pQ 𝐵 ) ~Q ( ( [Q] ‘ 𝐴 ) +pQ ( [Q] ‘ 𝐵 ) ) ↔ ( [Q] ‘ ( 𝐴 +pQ 𝐵 ) ) = ( [Q] ‘ ( ( [Q] ‘ 𝐴 ) +pQ ( [Q] ‘ 𝐵 ) ) ) ) )
35 28 34 mpbid ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( [Q] ‘ ( 𝐴 +pQ 𝐵 ) ) = ( [Q] ‘ ( ( [Q] ‘ 𝐴 ) +pQ ( [Q] ‘ 𝐵 ) ) ) )
36 4 35 eqtr4d ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( ( [Q] ‘ 𝐴 ) +Q ( [Q] ‘ 𝐵 ) ) = ( [Q] ‘ ( 𝐴 +pQ 𝐵 ) ) )
37 0nnq ⊢ ¬ ∅ ∈ Q
38 nqerf ⊢ [Q] : ( N × N ) ⟶ Q
39 38 fdmi ⊢ dom [Q] = ( N × N )
40 39 eleq2i ⊢ ( 𝐴 ∈ dom [Q] ↔ 𝐴 ∈ ( N × N ) )
41 ndmfv ⊢ ( ¬ 𝐴 ∈ dom [Q] → ( [Q] ‘ 𝐴 ) = ∅ )
42 40 41 sylnbir ⊢ ( ¬ 𝐴 ∈ ( N × N ) → ( [Q] ‘ 𝐴 ) = ∅ )
43 42 eleq1d ⊢ ( ¬ 𝐴 ∈ ( N × N ) → ( ( [Q] ‘ 𝐴 ) ∈ Q ↔ ∅ ∈ Q ) )
44 37 43 mtbiri ⊢ ( ¬ 𝐴 ∈ ( N × N ) → ¬ ( [Q] ‘ 𝐴 ) ∈ Q )
45 44 con4i ⊢ ( ( [Q] ‘ 𝐴 ) ∈ Q → 𝐴 ∈ ( N × N ) )
46 39 eleq2i ⊢ ( 𝐵 ∈ dom [Q] ↔ 𝐵 ∈ ( N × N ) )
47 ndmfv ⊢ ( ¬ 𝐵 ∈ dom [Q] → ( [Q] ‘ 𝐵 ) = ∅ )
48 46 47 sylnbir ⊢ ( ¬ 𝐵 ∈ ( N × N ) → ( [Q] ‘ 𝐵 ) = ∅ )
49 48 eleq1d ⊢ ( ¬ 𝐵 ∈ ( N × N ) → ( ( [Q] ‘ 𝐵 ) ∈ Q ↔ ∅ ∈ Q ) )
50 37 49 mtbiri ⊢ ( ¬ 𝐵 ∈ ( N × N ) → ¬ ( [Q] ‘ 𝐵 ) ∈ Q )
51 50 con4i ⊢ ( ( [Q] ‘ 𝐵 ) ∈ Q → 𝐵 ∈ ( N × N ) )
52 45 51 anim12i ⊢ ( ( ( [Q] ‘ 𝐴 ) ∈ Q ∧ ( [Q] ‘ 𝐵 ) ∈ Q ) → ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) )
53 52 con3i ⊢ ( ¬ ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ¬ ( ( [Q] ‘ 𝐴 ) ∈ Q ∧ ( [Q] ‘ 𝐵 ) ∈ Q ) )
54 addnqf ⊢ +Q : ( Q × Q ) ⟶ Q
55 54 fdmi ⊢ dom +Q = ( Q × Q )
56 55 ndmov ⊢ ( ¬ ( ( [Q] ‘ 𝐴 ) ∈ Q ∧ ( [Q] ‘ 𝐵 ) ∈ Q ) → ( ( [Q] ‘ 𝐴 ) +Q ( [Q] ‘ 𝐵 ) ) = ∅ )
57 53 56 syl ⊢ ( ¬ ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( ( [Q] ‘ 𝐴 ) +Q ( [Q] ‘ 𝐵 ) ) = ∅ )
58 0nelxp ⊢ ¬ ∅ ∈ ( N × N )
59 39 eleq2i ⊢ ( ∅ ∈ dom [Q] ↔ ∅ ∈ ( N × N ) )
60 58 59 mtbir ⊢ ¬ ∅ ∈ dom [Q]
61 29 fdmi ⊢ dom +pQ = ( ( N × N ) × ( N × N ) )
62 61 ndmov ⊢ ( ¬ ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 +pQ 𝐵 ) = ∅ )
63 62 eleq1d ⊢ ( ¬ ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( ( 𝐴 +pQ 𝐵 ) ∈ dom [Q] ↔ ∅ ∈ dom [Q] ) )
64 60 63 mtbiri ⊢ ( ¬ ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ¬ ( 𝐴 +pQ 𝐵 ) ∈ dom [Q] )
65 ndmfv ⊢ ( ¬ ( 𝐴 +pQ 𝐵 ) ∈ dom [Q] → ( [Q] ‘ ( 𝐴 +pQ 𝐵 ) ) = ∅ )
66 64 65 syl ⊢ ( ¬ ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( [Q] ‘ ( 𝐴 +pQ 𝐵 ) ) = ∅ )
67 57 66 eqtr4d ⊢ ( ¬ ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( ( [Q] ‘ 𝐴 ) +Q ( [Q] ‘ 𝐵 ) ) = ( [Q] ‘ ( 𝐴 +pQ 𝐵 ) ) )
68 36 67 pm2.61i ⊢ ( ( [Q] ‘ 𝐴 ) +Q ( [Q] ‘ 𝐵 ) ) = ( [Q] ‘ ( 𝐴 +pQ 𝐵 ) )