Proof of Theorem mulerpq
Step | Hyp | Ref
| Expression |
1 | | nqercl 10715 |
. . . 4
⊢ (𝐴 ∈ (N ×
N) → ([Q]‘𝐴) ∈ Q) |
2 | | nqercl 10715 |
. . . 4
⊢ (𝐵 ∈ (N ×
N) → ([Q]‘𝐵) ∈ Q) |
3 | | mulpqnq 10725 |
. . . 4
⊢
((([Q]‘𝐴) ∈ Q ∧
([Q]‘𝐵)
∈ Q) → (([Q]‘𝐴) ·Q
([Q]‘𝐵)) =
([Q]‘(([Q]‘𝐴) ·pQ
([Q]‘𝐵)))) |
4 | 1, 2, 3 | syl2an 595 |
. . 3
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) →
(([Q]‘𝐴) ·Q
([Q]‘𝐵)) =
([Q]‘(([Q]‘𝐴) ·pQ
([Q]‘𝐵)))) |
5 | | enqer 10705 |
. . . . . 6
⊢
~Q Er (N ×
N) |
6 | 5 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) →
~Q Er (N ×
N)) |
7 | | nqerrel 10716 |
. . . . . . 7
⊢ (𝐴 ∈ (N ×
N) → 𝐴
~Q ([Q]‘𝐴)) |
8 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → 𝐴 ~Q
([Q]‘𝐴)) |
9 | | elpqn 10709 |
. . . . . . . . 9
⊢
(([Q]‘𝐴) ∈ Q →
([Q]‘𝐴)
∈ (N × N)) |
10 | 1, 9 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ (N ×
N) → ([Q]‘𝐴) ∈ (N ×
N)) |
11 | | mulerpqlem 10739 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (N ×
N) ∧ ([Q]‘𝐴) ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → (𝐴 ~Q
([Q]‘𝐴)
↔ (𝐴
·pQ 𝐵) ~Q
(([Q]‘𝐴) ·pQ 𝐵))) |
12 | 11 | 3exp 1117 |
. . . . . . . 8
⊢ (𝐴 ∈ (N ×
N) → (([Q]‘𝐴) ∈ (N ×
N) → (𝐵
∈ (N × N) → (𝐴 ~Q
([Q]‘𝐴)
↔ (𝐴
·pQ 𝐵) ~Q
(([Q]‘𝐴) ·pQ 𝐵))))) |
13 | 10, 12 | mpd 15 |
. . . . . . 7
⊢ (𝐴 ∈ (N ×
N) → (𝐵
∈ (N × N) → (𝐴 ~Q
([Q]‘𝐴)
↔ (𝐴
·pQ 𝐵) ~Q
(([Q]‘𝐴) ·pQ 𝐵)))) |
14 | 13 | imp 406 |
. . . . . 6
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → (𝐴 ~Q
([Q]‘𝐴)
↔ (𝐴
·pQ 𝐵) ~Q
(([Q]‘𝐴) ·pQ 𝐵))) |
15 | 8, 14 | mpbid 231 |
. . . . 5
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → (𝐴 ·pQ 𝐵) ~Q
(([Q]‘𝐴) ·pQ 𝐵)) |
16 | | nqerrel 10716 |
. . . . . . . 8
⊢ (𝐵 ∈ (N ×
N) → 𝐵
~Q ([Q]‘𝐵)) |
17 | 16 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → 𝐵 ~Q
([Q]‘𝐵)) |
18 | | elpqn 10709 |
. . . . . . . . . 10
⊢
(([Q]‘𝐵) ∈ Q →
([Q]‘𝐵)
∈ (N × N)) |
19 | 2, 18 | syl 17 |
. . . . . . . . 9
⊢ (𝐵 ∈ (N ×
N) → ([Q]‘𝐵) ∈ (N ×
N)) |
20 | | mulerpqlem 10739 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ (N ×
N) ∧ ([Q]‘𝐵) ∈ (N ×
N) ∧ ([Q]‘𝐴) ∈ (N ×
N)) → (𝐵
~Q ([Q]‘𝐵) ↔ (𝐵 ·pQ
([Q]‘𝐴)) ~Q
(([Q]‘𝐵) ·pQ
([Q]‘𝐴)))) |
21 | 20 | 3exp 1117 |
. . . . . . . . 9
⊢ (𝐵 ∈ (N ×
N) → (([Q]‘𝐵) ∈ (N ×
N) → (([Q]‘𝐴) ∈ (N ×
N) → (𝐵
~Q ([Q]‘𝐵) ↔ (𝐵 ·pQ
([Q]‘𝐴)) ~Q
(([Q]‘𝐵) ·pQ
([Q]‘𝐴)))))) |
22 | 19, 21 | mpd 15 |
. . . . . . . 8
⊢ (𝐵 ∈ (N ×
N) → (([Q]‘𝐴) ∈ (N ×
N) → (𝐵
~Q ([Q]‘𝐵) ↔ (𝐵 ·pQ
([Q]‘𝐴)) ~Q
(([Q]‘𝐵) ·pQ
([Q]‘𝐴))))) |
23 | 10, 22 | mpan9 506 |
. . . . . . 7
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → (𝐵 ~Q
([Q]‘𝐵)
↔ (𝐵
·pQ ([Q]‘𝐴)) ~Q
(([Q]‘𝐵) ·pQ
([Q]‘𝐴)))) |
24 | 17, 23 | mpbid 231 |
. . . . . 6
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → (𝐵 ·pQ
([Q]‘𝐴)) ~Q
(([Q]‘𝐵) ·pQ
([Q]‘𝐴))) |
25 | | mulcompq 10736 |
. . . . . 6
⊢ (𝐵
·pQ ([Q]‘𝐴)) = (([Q]‘𝐴)
·pQ 𝐵) |
26 | | mulcompq 10736 |
. . . . . 6
⊢
(([Q]‘𝐵) ·pQ
([Q]‘𝐴)) = (([Q]‘𝐴)
·pQ ([Q]‘𝐵)) |
27 | 24, 25, 26 | 3brtr3g 5110 |
. . . . 5
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) →
(([Q]‘𝐴) ·pQ 𝐵) ~Q
(([Q]‘𝐴) ·pQ
([Q]‘𝐵))) |
28 | 6, 15, 27 | ertrd 8534 |
. . . 4
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → (𝐴 ·pQ 𝐵) ~Q
(([Q]‘𝐴) ·pQ
([Q]‘𝐵))) |
29 | | mulpqf 10730 |
. . . . . 6
⊢
·pQ :((N × N)
× (N × N))⟶(N
× N) |
30 | 29 | fovcl 7422 |
. . . . 5
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → (𝐴 ·pQ 𝐵) ∈ (N
× N)) |
31 | 29 | fovcl 7422 |
. . . . . 6
⊢
((([Q]‘𝐴) ∈ (N ×
N) ∧ ([Q]‘𝐵) ∈ (N ×
N)) → (([Q]‘𝐴) ·pQ
([Q]‘𝐵)) ∈ (N ×
N)) |
32 | 10, 19, 31 | syl2an 595 |
. . . . 5
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) →
(([Q]‘𝐴) ·pQ
([Q]‘𝐵)) ∈ (N ×
N)) |
33 | | nqereq 10719 |
. . . . 5
⊢ (((𝐴
·pQ 𝐵) ∈ (N ×
N) ∧ (([Q]‘𝐴) ·pQ
([Q]‘𝐵)) ∈ (N ×
N)) → ((𝐴 ·pQ 𝐵) ~Q
(([Q]‘𝐴) ·pQ
([Q]‘𝐵)) ↔ ([Q]‘(𝐴
·pQ 𝐵)) =
([Q]‘(([Q]‘𝐴) ·pQ
([Q]‘𝐵))))) |
34 | 30, 32, 33 | syl2anc 583 |
. . . 4
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → ((𝐴 ·pQ 𝐵) ~Q
(([Q]‘𝐴) ·pQ
([Q]‘𝐵)) ↔ ([Q]‘(𝐴
·pQ 𝐵)) =
([Q]‘(([Q]‘𝐴) ·pQ
([Q]‘𝐵))))) |
35 | 28, 34 | mpbid 231 |
. . 3
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) →
([Q]‘(𝐴
·pQ 𝐵)) =
([Q]‘(([Q]‘𝐴) ·pQ
([Q]‘𝐵)))) |
36 | 4, 35 | eqtr4d 2776 |
. 2
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) →
(([Q]‘𝐴) ·Q
([Q]‘𝐵)) = ([Q]‘(𝐴
·pQ 𝐵))) |
37 | | 0nnq 10708 |
. . . . . . 7
⊢ ¬
∅ ∈ Q |
38 | | nqerf 10714 |
. . . . . . . . . . 11
⊢
[Q]:(N ×
N)⟶Q |
39 | 38 | fdmi 6630 |
. . . . . . . . . 10
⊢ dom
[Q] = (N × N) |
40 | 39 | eleq2i 2825 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom [Q]
↔ 𝐴 ∈
(N × N)) |
41 | | ndmfv 6824 |
. . . . . . . . 9
⊢ (¬
𝐴 ∈ dom
[Q] → ([Q]‘𝐴) = ∅) |
42 | 40, 41 | sylnbir 330 |
. . . . . . . 8
⊢ (¬
𝐴 ∈ (N
× N) → ([Q]‘𝐴) = ∅) |
43 | 42 | eleq1d 2818 |
. . . . . . 7
⊢ (¬
𝐴 ∈ (N
× N) → (([Q]‘𝐴) ∈ Q ↔ ∅
∈ Q)) |
44 | 37, 43 | mtbiri 326 |
. . . . . 6
⊢ (¬
𝐴 ∈ (N
× N) → ¬ ([Q]‘𝐴) ∈
Q) |
45 | 44 | con4i 114 |
. . . . 5
⊢
(([Q]‘𝐴) ∈ Q → 𝐴 ∈ (N ×
N)) |
46 | 39 | eleq2i 2825 |
. . . . . . . . 9
⊢ (𝐵 ∈ dom [Q]
↔ 𝐵 ∈
(N × N)) |
47 | | ndmfv 6824 |
. . . . . . . . 9
⊢ (¬
𝐵 ∈ dom
[Q] → ([Q]‘𝐵) = ∅) |
48 | 46, 47 | sylnbir 330 |
. . . . . . . 8
⊢ (¬
𝐵 ∈ (N
× N) → ([Q]‘𝐵) = ∅) |
49 | 48 | eleq1d 2818 |
. . . . . . 7
⊢ (¬
𝐵 ∈ (N
× N) → (([Q]‘𝐵) ∈ Q ↔ ∅
∈ Q)) |
50 | 37, 49 | mtbiri 326 |
. . . . . 6
⊢ (¬
𝐵 ∈ (N
× N) → ¬ ([Q]‘𝐵) ∈
Q) |
51 | 50 | con4i 114 |
. . . . 5
⊢
(([Q]‘𝐵) ∈ Q → 𝐵 ∈ (N ×
N)) |
52 | 45, 51 | anim12i 612 |
. . . 4
⊢
((([Q]‘𝐴) ∈ Q ∧
([Q]‘𝐵)
∈ Q) → (𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N))) |
53 | | mulnqf 10733 |
. . . . . 6
⊢
·Q :(Q ×
Q)⟶Q |
54 | 53 | fdmi 6630 |
. . . . 5
⊢ dom
·Q = (Q ×
Q) |
55 | 54 | ndmov 7476 |
. . . 4
⊢ (¬
(([Q]‘𝐴) ∈ Q ∧
([Q]‘𝐵)
∈ Q) → (([Q]‘𝐴) ·Q
([Q]‘𝐵)) = ∅) |
56 | 52, 55 | nsyl5 159 |
. . 3
⊢ (¬
(𝐴 ∈ (N
× N) ∧ 𝐵 ∈ (N ×
N)) → (([Q]‘𝐴) ·Q
([Q]‘𝐵)) = ∅) |
57 | | 0nelxp 5625 |
. . . . . 6
⊢ ¬
∅ ∈ (N × N) |
58 | 39 | eleq2i 2825 |
. . . . . 6
⊢ (∅
∈ dom [Q] ↔ ∅ ∈ (N ×
N)) |
59 | 57, 58 | mtbir 322 |
. . . . 5
⊢ ¬
∅ ∈ dom [Q] |
60 | 29 | fdmi 6630 |
. . . . . . 7
⊢ dom
·pQ = ((N ×
N) × (N ×
N)) |
61 | 60 | ndmov 7476 |
. . . . . 6
⊢ (¬
(𝐴 ∈ (N
× N) ∧ 𝐵 ∈ (N ×
N)) → (𝐴
·pQ 𝐵) = ∅) |
62 | 61 | eleq1d 2818 |
. . . . 5
⊢ (¬
(𝐴 ∈ (N
× N) ∧ 𝐵 ∈ (N ×
N)) → ((𝐴 ·pQ 𝐵) ∈ dom [Q]
↔ ∅ ∈ dom [Q])) |
63 | 59, 62 | mtbiri 326 |
. . . 4
⊢ (¬
(𝐴 ∈ (N
× N) ∧ 𝐵 ∈ (N ×
N)) → ¬ (𝐴 ·pQ 𝐵) ∈ dom
[Q]) |
64 | | ndmfv 6824 |
. . . 4
⊢ (¬
(𝐴
·pQ 𝐵) ∈ dom [Q] →
([Q]‘(𝐴
·pQ 𝐵)) = ∅) |
65 | 63, 64 | syl 17 |
. . 3
⊢ (¬
(𝐴 ∈ (N
× N) ∧ 𝐵 ∈ (N ×
N)) → ([Q]‘(𝐴 ·pQ 𝐵)) = ∅) |
66 | 56, 65 | eqtr4d 2776 |
. 2
⊢ (¬
(𝐴 ∈ (N
× N) ∧ 𝐵 ∈ (N ×
N)) → (([Q]‘𝐴) ·Q
([Q]‘𝐵)) = ([Q]‘(𝐴
·pQ 𝐵))) |
67 | 36, 66 | pm2.61i 182 |
1
⊢
(([Q]‘𝐴) ·Q
([Q]‘𝐵)) = ([Q]‘(𝐴
·pQ 𝐵)) |