Step | Hyp | Ref
| Expression |
1 | | fvex 6201 |
. . . 4
⊢
(*Q‘𝐴) ∈ V |
2 | 1 | a1i 11 |
. . 3
⊢ (𝐴 ∈ Q →
(*Q‘𝐴) ∈ V) |
3 | | eleq1 2689 |
. . 3
⊢
((*Q‘𝐴) = 𝐵 →
((*Q‘𝐴) ∈ V ↔ 𝐵 ∈ V)) |
4 | 2, 3 | syl5ibcom 235 |
. 2
⊢ (𝐴 ∈ Q →
((*Q‘𝐴) = 𝐵 → 𝐵 ∈ V)) |
5 | | id 22 |
. . . . . . 7
⊢ ((𝐴
·Q 𝐵) = 1Q →
(𝐴
·Q 𝐵) =
1Q) |
6 | | 1nq 9750 |
. . . . . . 7
⊢
1Q ∈ Q |
7 | 5, 6 | syl6eqel 2709 |
. . . . . 6
⊢ ((𝐴
·Q 𝐵) = 1Q →
(𝐴
·Q 𝐵) ∈ Q) |
8 | | mulnqf 9771 |
. . . . . . . 8
⊢
·Q :(Q ×
Q)⟶Q |
9 | 8 | fdmi 6052 |
. . . . . . 7
⊢ dom
·Q = (Q ×
Q) |
10 | | 0nnq 9746 |
. . . . . . 7
⊢ ¬
∅ ∈ Q |
11 | 9, 10 | ndmovrcl 6820 |
. . . . . 6
⊢ ((𝐴
·Q 𝐵) ∈ Q → (𝐴 ∈ Q ∧
𝐵 ∈
Q)) |
12 | 7, 11 | syl 17 |
. . . . 5
⊢ ((𝐴
·Q 𝐵) = 1Q →
(𝐴 ∈ Q
∧ 𝐵 ∈
Q)) |
13 | 12 | simprd 479 |
. . . 4
⊢ ((𝐴
·Q 𝐵) = 1Q → 𝐵 ∈
Q) |
14 | | elex 3212 |
. . . 4
⊢ (𝐵 ∈ Q →
𝐵 ∈
V) |
15 | 13, 14 | syl 17 |
. . 3
⊢ ((𝐴
·Q 𝐵) = 1Q → 𝐵 ∈ V) |
16 | 15 | a1i 11 |
. 2
⊢ (𝐴 ∈ Q →
((𝐴
·Q 𝐵) = 1Q → 𝐵 ∈ V)) |
17 | | oveq1 6657 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝑥 ·Q 𝑦) = (𝐴 ·Q 𝑦)) |
18 | 17 | eqeq1d 2624 |
. . . 4
⊢ (𝑥 = 𝐴 → ((𝑥 ·Q 𝑦) = 1Q
↔ (𝐴
·Q 𝑦) =
1Q)) |
19 | | oveq2 6658 |
. . . . 5
⊢ (𝑦 = 𝐵 → (𝐴 ·Q 𝑦) = (𝐴 ·Q 𝐵)) |
20 | 19 | eqeq1d 2624 |
. . . 4
⊢ (𝑦 = 𝐵 → ((𝐴 ·Q 𝑦) = 1Q
↔ (𝐴
·Q 𝐵) =
1Q)) |
21 | | nqerid 9755 |
. . . . . . . . . 10
⊢ (𝑥 ∈ Q →
([Q]‘𝑥)
= 𝑥) |
22 | | relxp 5227 |
. . . . . . . . . . . 12
⊢ Rel
(N × N) |
23 | | elpqn 9747 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ Q →
𝑥 ∈ (N
× N)) |
24 | | 1st2nd 7214 |
. . . . . . . . . . . 12
⊢ ((Rel
(N × N) ∧ 𝑥 ∈ (N ×
N)) → 𝑥
= 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
25 | 22, 23, 24 | sylancr 695 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ Q →
𝑥 = 〈(1st
‘𝑥), (2nd
‘𝑥)〉) |
26 | 25 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑥 ∈ Q →
([Q]‘𝑥)
= ([Q]‘〈(1st ‘𝑥), (2nd ‘𝑥)〉)) |
27 | 21, 26 | eqtr3d 2658 |
. . . . . . . . 9
⊢ (𝑥 ∈ Q →
𝑥 =
([Q]‘〈(1st ‘𝑥), (2nd ‘𝑥)〉)) |
28 | 27 | oveq1d 6665 |
. . . . . . . 8
⊢ (𝑥 ∈ Q →
(𝑥
·Q
([Q]‘〈(2nd ‘𝑥), (1st ‘𝑥)〉)) =
(([Q]‘〈(1st ‘𝑥), (2nd ‘𝑥)〉) ·Q
([Q]‘〈(2nd ‘𝑥), (1st ‘𝑥)〉))) |
29 | | mulerpq 9779 |
. . . . . . . 8
⊢
(([Q]‘〈(1st ‘𝑥), (2nd ‘𝑥)〉)
·Q
([Q]‘〈(2nd ‘𝑥), (1st ‘𝑥)〉)) =
([Q]‘(〈(1st ‘𝑥), (2nd ‘𝑥)〉 ·pQ
〈(2nd ‘𝑥), (1st ‘𝑥)〉)) |
30 | 28, 29 | syl6eq 2672 |
. . . . . . 7
⊢ (𝑥 ∈ Q →
(𝑥
·Q
([Q]‘〈(2nd ‘𝑥), (1st ‘𝑥)〉)) =
([Q]‘(〈(1st ‘𝑥), (2nd ‘𝑥)〉 ·pQ
〈(2nd ‘𝑥), (1st ‘𝑥)〉))) |
31 | | xp1st 7198 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (N ×
N) → (1st ‘𝑥) ∈ N) |
32 | 23, 31 | syl 17 |
. . . . . . . . . 10
⊢ (𝑥 ∈ Q →
(1st ‘𝑥)
∈ N) |
33 | | xp2nd 7199 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (N ×
N) → (2nd ‘𝑥) ∈ N) |
34 | 23, 33 | syl 17 |
. . . . . . . . . 10
⊢ (𝑥 ∈ Q →
(2nd ‘𝑥)
∈ N) |
35 | | mulpipq 9762 |
. . . . . . . . . 10
⊢
((((1st ‘𝑥) ∈ N ∧
(2nd ‘𝑥)
∈ N) ∧ ((2nd ‘𝑥) ∈ N ∧
(1st ‘𝑥)
∈ N)) → (〈(1st ‘𝑥), (2nd ‘𝑥)〉
·pQ 〈(2nd ‘𝑥), (1st ‘𝑥)〉) =
〈((1st ‘𝑥) ·N
(2nd ‘𝑥)),
((2nd ‘𝑥)
·N (1st ‘𝑥))〉) |
36 | 32, 34, 34, 32, 35 | syl22anc 1327 |
. . . . . . . . 9
⊢ (𝑥 ∈ Q →
(〈(1st ‘𝑥), (2nd ‘𝑥)〉 ·pQ
〈(2nd ‘𝑥), (1st ‘𝑥)〉) = 〈((1st
‘𝑥)
·N (2nd ‘𝑥)), ((2nd ‘𝑥)
·N (1st ‘𝑥))〉) |
37 | | mulcompi 9718 |
. . . . . . . . . 10
⊢
((2nd ‘𝑥) ·N
(1st ‘𝑥))
= ((1st ‘𝑥) ·N
(2nd ‘𝑥)) |
38 | 37 | opeq2i 4406 |
. . . . . . . . 9
⊢
〈((1st ‘𝑥) ·N
(2nd ‘𝑥)),
((2nd ‘𝑥)
·N (1st ‘𝑥))〉 = 〈((1st
‘𝑥)
·N (2nd ‘𝑥)), ((1st ‘𝑥)
·N (2nd ‘𝑥))〉 |
39 | 36, 38 | syl6eq 2672 |
. . . . . . . 8
⊢ (𝑥 ∈ Q →
(〈(1st ‘𝑥), (2nd ‘𝑥)〉 ·pQ
〈(2nd ‘𝑥), (1st ‘𝑥)〉) = 〈((1st
‘𝑥)
·N (2nd ‘𝑥)), ((1st ‘𝑥)
·N (2nd ‘𝑥))〉) |
40 | 39 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑥 ∈ Q →
([Q]‘(〈(1st ‘𝑥), (2nd ‘𝑥)〉 ·pQ
〈(2nd ‘𝑥), (1st ‘𝑥)〉)) =
([Q]‘〈((1st ‘𝑥) ·N
(2nd ‘𝑥)),
((1st ‘𝑥)
·N (2nd ‘𝑥))〉)) |
41 | | nqerid 9755 |
. . . . . . . . 9
⊢
(1Q ∈ Q →
([Q]‘1Q) =
1Q) |
42 | 6, 41 | ax-mp 5 |
. . . . . . . 8
⊢
([Q]‘1Q) =
1Q |
43 | | mulclpi 9715 |
. . . . . . . . . . 11
⊢
(((1st ‘𝑥) ∈ N ∧
(2nd ‘𝑥)
∈ N) → ((1st ‘𝑥) ·N
(2nd ‘𝑥))
∈ N) |
44 | 32, 34, 43 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝑥 ∈ Q →
((1st ‘𝑥)
·N (2nd ‘𝑥)) ∈ N) |
45 | | 1nqenq 9784 |
. . . . . . . . . 10
⊢
(((1st ‘𝑥) ·N
(2nd ‘𝑥))
∈ N → 1Q
~Q 〈((1st ‘𝑥) ·N
(2nd ‘𝑥)),
((1st ‘𝑥)
·N (2nd ‘𝑥))〉) |
46 | 44, 45 | syl 17 |
. . . . . . . . 9
⊢ (𝑥 ∈ Q →
1Q ~Q 〈((1st
‘𝑥)
·N (2nd ‘𝑥)), ((1st ‘𝑥)
·N (2nd ‘𝑥))〉) |
47 | | elpqn 9747 |
. . . . . . . . . . 11
⊢
(1Q ∈ Q →
1Q ∈ (N ×
N)) |
48 | 6, 47 | ax-mp 5 |
. . . . . . . . . 10
⊢
1Q ∈ (N ×
N) |
49 | | opelxpi 5148 |
. . . . . . . . . . 11
⊢
((((1st ‘𝑥) ·N
(2nd ‘𝑥))
∈ N ∧ ((1st ‘𝑥) ·N
(2nd ‘𝑥))
∈ N) → 〈((1st ‘𝑥) ·N
(2nd ‘𝑥)),
((1st ‘𝑥)
·N (2nd ‘𝑥))〉 ∈ (N ×
N)) |
50 | 44, 44, 49 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝑥 ∈ Q →
〈((1st ‘𝑥) ·N
(2nd ‘𝑥)),
((1st ‘𝑥)
·N (2nd ‘𝑥))〉 ∈ (N ×
N)) |
51 | | nqereq 9757 |
. . . . . . . . . 10
⊢
((1Q ∈ (N ×
N) ∧ 〈((1st ‘𝑥) ·N
(2nd ‘𝑥)),
((1st ‘𝑥)
·N (2nd ‘𝑥))〉 ∈ (N ×
N)) → (1Q
~Q 〈((1st ‘𝑥) ·N
(2nd ‘𝑥)),
((1st ‘𝑥)
·N (2nd ‘𝑥))〉 ↔
([Q]‘1Q) =
([Q]‘〈((1st ‘𝑥) ·N
(2nd ‘𝑥)),
((1st ‘𝑥)
·N (2nd ‘𝑥))〉))) |
52 | 48, 50, 51 | sylancr 695 |
. . . . . . . . 9
⊢ (𝑥 ∈ Q →
(1Q ~Q 〈((1st
‘𝑥)
·N (2nd ‘𝑥)), ((1st ‘𝑥)
·N (2nd ‘𝑥))〉 ↔
([Q]‘1Q) =
([Q]‘〈((1st ‘𝑥) ·N
(2nd ‘𝑥)),
((1st ‘𝑥)
·N (2nd ‘𝑥))〉))) |
53 | 46, 52 | mpbid 222 |
. . . . . . . 8
⊢ (𝑥 ∈ Q →
([Q]‘1Q) =
([Q]‘〈((1st ‘𝑥) ·N
(2nd ‘𝑥)),
((1st ‘𝑥)
·N (2nd ‘𝑥))〉)) |
54 | 42, 53 | syl5reqr 2671 |
. . . . . . 7
⊢ (𝑥 ∈ Q →
([Q]‘〈((1st ‘𝑥) ·N
(2nd ‘𝑥)),
((1st ‘𝑥)
·N (2nd ‘𝑥))〉) =
1Q) |
55 | 30, 40, 54 | 3eqtrd 2660 |
. . . . . 6
⊢ (𝑥 ∈ Q →
(𝑥
·Q
([Q]‘〈(2nd ‘𝑥), (1st ‘𝑥)〉)) =
1Q) |
56 | | fvex 6201 |
. . . . . . 7
⊢
([Q]‘〈(2nd ‘𝑥), (1st ‘𝑥)〉) ∈ V |
57 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑦 =
([Q]‘〈(2nd ‘𝑥), (1st ‘𝑥)〉) → (𝑥 ·Q 𝑦) = (𝑥 ·Q
([Q]‘〈(2nd ‘𝑥), (1st ‘𝑥)〉))) |
58 | 57 | eqeq1d 2624 |
. . . . . . 7
⊢ (𝑦 =
([Q]‘〈(2nd ‘𝑥), (1st ‘𝑥)〉) → ((𝑥 ·Q 𝑦) = 1Q
↔ (𝑥
·Q
([Q]‘〈(2nd ‘𝑥), (1st ‘𝑥)〉)) =
1Q)) |
59 | 56, 58 | spcev 3300 |
. . . . . 6
⊢ ((𝑥
·Q
([Q]‘〈(2nd ‘𝑥), (1st ‘𝑥)〉)) = 1Q
→ ∃𝑦(𝑥
·Q 𝑦) =
1Q) |
60 | 55, 59 | syl 17 |
. . . . 5
⊢ (𝑥 ∈ Q →
∃𝑦(𝑥 ·Q 𝑦) =
1Q) |
61 | | mulcomnq 9775 |
. . . . . . 7
⊢ (𝑟
·Q 𝑠) = (𝑠 ·Q 𝑟) |
62 | | mulassnq 9781 |
. . . . . . 7
⊢ ((𝑟
·Q 𝑠) ·Q 𝑡) = (𝑟 ·Q (𝑠
·Q 𝑡)) |
63 | | mulidnq 9785 |
. . . . . . 7
⊢ (𝑟 ∈ Q →
(𝑟
·Q 1Q) = 𝑟) |
64 | 6, 9, 10, 61, 62, 63 | caovmo 6871 |
. . . . . 6
⊢
∃*𝑦(𝑥
·Q 𝑦) =
1Q |
65 | | eu5 2496 |
. . . . . 6
⊢
(∃!𝑦(𝑥
·Q 𝑦) = 1Q ↔
(∃𝑦(𝑥
·Q 𝑦) = 1Q ∧
∃*𝑦(𝑥
·Q 𝑦) =
1Q)) |
66 | 64, 65 | mpbiran2 954 |
. . . . 5
⊢
(∃!𝑦(𝑥
·Q 𝑦) = 1Q ↔
∃𝑦(𝑥 ·Q 𝑦) =
1Q) |
67 | 60, 66 | sylibr 224 |
. . . 4
⊢ (𝑥 ∈ Q →
∃!𝑦(𝑥
·Q 𝑦) =
1Q) |
68 | | cnvimass 5485 |
. . . . . . . 8
⊢ (◡ ·Q “
{1Q}) ⊆ dom
·Q |
69 | | df-rq 9739 |
. . . . . . . 8
⊢
*Q = (◡
·Q “
{1Q}) |
70 | 9 | eqcomi 2631 |
. . . . . . . 8
⊢
(Q × Q) = dom
·Q |
71 | 68, 69, 70 | 3sstr4i 3644 |
. . . . . . 7
⊢
*Q ⊆ (Q ×
Q) |
72 | | relxp 5227 |
. . . . . . 7
⊢ Rel
(Q × Q) |
73 | | relss 5206 |
. . . . . . 7
⊢
(*Q ⊆ (Q ×
Q) → (Rel (Q × Q) →
Rel *Q)) |
74 | 71, 72, 73 | mp2 9 |
. . . . . 6
⊢ Rel
*Q |
75 | 69 | eleq2i 2693 |
. . . . . . . 8
⊢
(〈𝑥, 𝑦〉 ∈
*Q ↔ 〈𝑥, 𝑦〉 ∈ (◡ ·Q “
{1Q})) |
76 | | ffn 6045 |
. . . . . . . . 9
⊢ (
·Q :(Q ×
Q)⟶Q →
·Q Fn (Q ×
Q)) |
77 | | fniniseg 6338 |
. . . . . . . . 9
⊢ (
·Q Fn (Q × Q)
→ (〈𝑥, 𝑦〉 ∈ (◡ ·Q “
{1Q}) ↔ (〈𝑥, 𝑦〉 ∈ (Q ×
Q) ∧ ( ·Q ‘〈𝑥, 𝑦〉) =
1Q))) |
78 | 8, 76, 77 | mp2b 10 |
. . . . . . . 8
⊢
(〈𝑥, 𝑦〉 ∈ (◡ ·Q “
{1Q}) ↔ (〈𝑥, 𝑦〉 ∈ (Q ×
Q) ∧ ( ·Q ‘〈𝑥, 𝑦〉) =
1Q)) |
79 | | ancom 466 |
. . . . . . . . 9
⊢
((〈𝑥, 𝑦〉 ∈ (Q
× Q) ∧ ( ·Q
‘〈𝑥, 𝑦〉) =
1Q) ↔ (( ·Q
‘〈𝑥, 𝑦〉) =
1Q ∧ 〈𝑥, 𝑦〉 ∈ (Q ×
Q))) |
80 | | ancom 466 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ Q ∧
(𝑥
·Q 𝑦) = 1Q) ↔
((𝑥
·Q 𝑦) = 1Q ∧ 𝑥 ∈
Q)) |
81 | | eleq1 2689 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥
·Q 𝑦) = 1Q →
((𝑥
·Q 𝑦) ∈ Q ↔
1Q ∈ Q)) |
82 | 6, 81 | mpbiri 248 |
. . . . . . . . . . . . . 14
⊢ ((𝑥
·Q 𝑦) = 1Q → (𝑥
·Q 𝑦) ∈ Q) |
83 | 9, 10 | ndmovrcl 6820 |
. . . . . . . . . . . . . 14
⊢ ((𝑥
·Q 𝑦) ∈ Q → (𝑥 ∈ Q ∧
𝑦 ∈
Q)) |
84 | 82, 83 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑥
·Q 𝑦) = 1Q → (𝑥 ∈ Q ∧
𝑦 ∈
Q)) |
85 | | opelxpi 5148 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ 〈𝑥, 𝑦〉 ∈ (Q
× Q)) |
86 | 84, 85 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑥
·Q 𝑦) = 1Q →
〈𝑥, 𝑦〉 ∈ (Q ×
Q)) |
87 | 84 | simpld 475 |
. . . . . . . . . . . 12
⊢ ((𝑥
·Q 𝑦) = 1Q → 𝑥 ∈
Q) |
88 | 86, 87 | 2thd 255 |
. . . . . . . . . . 11
⊢ ((𝑥
·Q 𝑦) = 1Q →
(〈𝑥, 𝑦〉 ∈ (Q
× Q) ↔ 𝑥 ∈ Q)) |
89 | 88 | pm5.32i 669 |
. . . . . . . . . 10
⊢ (((𝑥
·Q 𝑦) = 1Q ∧
〈𝑥, 𝑦〉 ∈ (Q ×
Q)) ↔ ((𝑥 ·Q 𝑦) = 1Q
∧ 𝑥 ∈
Q)) |
90 | | df-ov 6653 |
. . . . . . . . . . . 12
⊢ (𝑥
·Q 𝑦) = ( ·Q
‘〈𝑥, 𝑦〉) |
91 | 90 | eqeq1i 2627 |
. . . . . . . . . . 11
⊢ ((𝑥
·Q 𝑦) = 1Q ↔ (
·Q ‘〈𝑥, 𝑦〉) =
1Q) |
92 | 91 | anbi1i 731 |
. . . . . . . . . 10
⊢ (((𝑥
·Q 𝑦) = 1Q ∧
〈𝑥, 𝑦〉 ∈ (Q ×
Q)) ↔ (( ·Q
‘〈𝑥, 𝑦〉) =
1Q ∧ 〈𝑥, 𝑦〉 ∈ (Q ×
Q))) |
93 | 80, 89, 92 | 3bitr2ri 289 |
. . . . . . . . 9
⊢ (((
·Q ‘〈𝑥, 𝑦〉) = 1Q ∧
〈𝑥, 𝑦〉 ∈ (Q ×
Q)) ↔ (𝑥
∈ Q ∧ (𝑥 ·Q 𝑦) =
1Q)) |
94 | 79, 93 | bitri 264 |
. . . . . . . 8
⊢
((〈𝑥, 𝑦〉 ∈ (Q
× Q) ∧ ( ·Q
‘〈𝑥, 𝑦〉) =
1Q) ↔ (𝑥 ∈ Q ∧ (𝑥
·Q 𝑦) =
1Q)) |
95 | 75, 78, 94 | 3bitri 286 |
. . . . . . 7
⊢
(〈𝑥, 𝑦〉 ∈
*Q ↔ (𝑥 ∈ Q ∧ (𝑥
·Q 𝑦) =
1Q)) |
96 | 95 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (〈𝑥, 𝑦〉 ∈
*Q ↔ (𝑥 ∈ Q ∧ (𝑥
·Q 𝑦) =
1Q))) |
97 | 74, 96 | opabbi2dv 5271 |
. . . . 5
⊢ (⊤
→ *Q = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ Q ∧ (𝑥
·Q 𝑦) =
1Q)}) |
98 | 97 | trud 1493 |
. . . 4
⊢
*Q = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ Q ∧ (𝑥
·Q 𝑦) =
1Q)} |
99 | 18, 20, 67, 98 | fvopab3g 6277 |
. . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ V) →
((*Q‘𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) =
1Q)) |
100 | 99 | ex 450 |
. 2
⊢ (𝐴 ∈ Q →
(𝐵 ∈ V →
((*Q‘𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) =
1Q))) |
101 | 4, 16, 100 | pm5.21ndd 369 |
1
⊢ (𝐴 ∈ Q →
((*Q‘𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) =
1Q)) |