Step | Hyp | Ref
| Expression |
1 | | df-rex 3141 |
. . . . 5
⊢
(∃𝑔 ∈
1P 𝑥 = (𝑓 ·Q 𝑔) ↔ ∃𝑔(𝑔 ∈ 1P ∧
𝑥 = (𝑓 ·Q 𝑔))) |
2 | | 19.42v 1945 |
. . . . . 6
⊢
(∃𝑔(𝑥 <Q
𝑓 ∧ 𝑥 = (𝑓 ·Q 𝑔)) ↔ (𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔))) |
3 | | elprnq 10401 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) → 𝑓 ∈ Q) |
4 | | breq1 5060 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑓 ·Q 𝑔) → (𝑥 <Q 𝑓 ↔ (𝑓 ·Q 𝑔) <Q
𝑓)) |
5 | | df-1p 10392 |
. . . . . . . . . . . . 13
⊢
1P = {𝑔 ∣ 𝑔 <Q
1Q} |
6 | 5 | abeq2i 2945 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈
1P ↔ 𝑔 <Q
1Q) |
7 | | ltmnq 10382 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ Q →
(𝑔
<Q 1Q ↔ (𝑓
·Q 𝑔) <Q (𝑓
·Q
1Q))) |
8 | | mulidnq 10373 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ Q →
(𝑓
·Q 1Q) = 𝑓) |
9 | 8 | breq2d 5069 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ Q →
((𝑓
·Q 𝑔) <Q (𝑓
·Q 1Q) ↔ (𝑓
·Q 𝑔) <Q 𝑓)) |
10 | 7, 9 | bitrd 280 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ Q →
(𝑔
<Q 1Q ↔ (𝑓
·Q 𝑔) <Q 𝑓)) |
11 | 6, 10 | syl5rbb 285 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ Q →
((𝑓
·Q 𝑔) <Q 𝑓 ↔ 𝑔 ∈
1P)) |
12 | 4, 11 | sylan9bbr 511 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ Q ∧
𝑥 = (𝑓 ·Q 𝑔)) → (𝑥 <Q 𝑓 ↔ 𝑔 ∈
1P)) |
13 | 3, 12 | sylan 580 |
. . . . . . . . 9
⊢ (((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) ∧ 𝑥 = (𝑓 ·Q 𝑔)) → (𝑥 <Q 𝑓 ↔ 𝑔 ∈
1P)) |
14 | 13 | ex 413 |
. . . . . . . 8
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) → (𝑥 = (𝑓 ·Q 𝑔) → (𝑥 <Q 𝑓 ↔ 𝑔 ∈
1P))) |
15 | 14 | pm5.32rd 578 |
. . . . . . 7
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) → ((𝑥 <Q 𝑓 ∧ 𝑥 = (𝑓 ·Q 𝑔)) ↔ (𝑔 ∈ 1P ∧
𝑥 = (𝑓 ·Q 𝑔)))) |
16 | 15 | exbidv 1913 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) → (∃𝑔(𝑥 <Q 𝑓 ∧ 𝑥 = (𝑓 ·Q 𝑔)) ↔ ∃𝑔(𝑔 ∈ 1P ∧
𝑥 = (𝑓 ·Q 𝑔)))) |
17 | 2, 16 | syl5rbbr 287 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) → (∃𝑔(𝑔 ∈ 1P ∧
𝑥 = (𝑓 ·Q 𝑔)) ↔ (𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔)))) |
18 | 1, 17 | syl5bb 284 |
. . . 4
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) → (∃𝑔 ∈ 1P 𝑥 = (𝑓 ·Q 𝑔) ↔ (𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔)))) |
19 | 18 | rexbidva 3293 |
. . 3
⊢ (𝐴 ∈ P →
(∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 1P 𝑥 = (𝑓 ·Q 𝑔) ↔ ∃𝑓 ∈ 𝐴 (𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔)))) |
20 | | 1pr 10425 |
. . . 4
⊢
1P ∈ P |
21 | | df-mp 10394 |
. . . . 5
⊢
·P = (𝑦 ∈ P, 𝑧 ∈ P ↦ {𝑤 ∣ ∃𝑢 ∈ 𝑦 ∃𝑣 ∈ 𝑧 𝑤 = (𝑢 ·Q 𝑣)}) |
22 | | mulclnq 10357 |
. . . . 5
⊢ ((𝑢 ∈ Q ∧
𝑣 ∈ Q)
→ (𝑢
·Q 𝑣) ∈ Q) |
23 | 21, 22 | genpelv 10410 |
. . . 4
⊢ ((𝐴 ∈ P ∧
1P ∈ P) → (𝑥 ∈ (𝐴 ·P
1P) ↔ ∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 1P 𝑥 = (𝑓 ·Q 𝑔))) |
24 | 20, 23 | mpan2 687 |
. . 3
⊢ (𝐴 ∈ P →
(𝑥 ∈ (𝐴
·P 1P) ↔
∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 1P 𝑥 = (𝑓 ·Q 𝑔))) |
25 | | prnmax 10405 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
𝑥 ∈ 𝐴) → ∃𝑓 ∈ 𝐴 𝑥 <Q 𝑓) |
26 | | ltrelnq 10336 |
. . . . . . . . . . 11
⊢
<Q ⊆ (Q ×
Q) |
27 | 26 | brel 5610 |
. . . . . . . . . 10
⊢ (𝑥 <Q
𝑓 → (𝑥 ∈ Q ∧
𝑓 ∈
Q)) |
28 | | vex 3495 |
. . . . . . . . . . . . . 14
⊢ 𝑓 ∈ V |
29 | | vex 3495 |
. . . . . . . . . . . . . 14
⊢ 𝑥 ∈ V |
30 | | fvex 6676 |
. . . . . . . . . . . . . 14
⊢
(*Q‘𝑓) ∈ V |
31 | | mulcomnq 10363 |
. . . . . . . . . . . . . 14
⊢ (𝑦
·Q 𝑧) = (𝑧 ·Q 𝑦) |
32 | | mulassnq 10369 |
. . . . . . . . . . . . . 14
⊢ ((𝑦
·Q 𝑧) ·Q 𝑤) = (𝑦 ·Q (𝑧
·Q 𝑤)) |
33 | 28, 29, 30, 31, 32 | caov12 7365 |
. . . . . . . . . . . . 13
⊢ (𝑓
·Q (𝑥 ·Q
(*Q‘𝑓))) = (𝑥 ·Q (𝑓
·Q (*Q‘𝑓))) |
34 | | recidnq 10375 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ Q →
(𝑓
·Q (*Q‘𝑓)) =
1Q) |
35 | 34 | oveq2d 7161 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ Q →
(𝑥
·Q (𝑓 ·Q
(*Q‘𝑓))) = (𝑥 ·Q
1Q)) |
36 | 33, 35 | syl5eq 2865 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ Q →
(𝑓
·Q (𝑥 ·Q
(*Q‘𝑓))) = (𝑥 ·Q
1Q)) |
37 | | mulidnq 10373 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ Q →
(𝑥
·Q 1Q) = 𝑥) |
38 | 36, 37 | sylan9eqr 2875 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ Q ∧
𝑓 ∈ Q)
→ (𝑓
·Q (𝑥 ·Q
(*Q‘𝑓))) = 𝑥) |
39 | 38 | eqcomd 2824 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ Q ∧
𝑓 ∈ Q)
→ 𝑥 = (𝑓
·Q (𝑥 ·Q
(*Q‘𝑓)))) |
40 | | ovex 7178 |
. . . . . . . . . . 11
⊢ (𝑥
·Q (*Q‘𝑓)) ∈ V |
41 | | oveq2 7153 |
. . . . . . . . . . . 12
⊢ (𝑔 = (𝑥 ·Q
(*Q‘𝑓)) → (𝑓 ·Q 𝑔) = (𝑓 ·Q (𝑥
·Q (*Q‘𝑓)))) |
42 | 41 | eqeq2d 2829 |
. . . . . . . . . . 11
⊢ (𝑔 = (𝑥 ·Q
(*Q‘𝑓)) → (𝑥 = (𝑓 ·Q 𝑔) ↔ 𝑥 = (𝑓 ·Q (𝑥
·Q (*Q‘𝑓))))) |
43 | 40, 42 | spcev 3604 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑓 ·Q (𝑥
·Q (*Q‘𝑓))) → ∃𝑔 𝑥 = (𝑓 ·Q 𝑔)) |
44 | 27, 39, 43 | 3syl 18 |
. . . . . . . . 9
⊢ (𝑥 <Q
𝑓 → ∃𝑔 𝑥 = (𝑓 ·Q 𝑔)) |
45 | 44 | a1i 11 |
. . . . . . . 8
⊢ (𝑓 ∈ 𝐴 → (𝑥 <Q 𝑓 → ∃𝑔 𝑥 = (𝑓 ·Q 𝑔))) |
46 | 45 | ancld 551 |
. . . . . . 7
⊢ (𝑓 ∈ 𝐴 → (𝑥 <Q 𝑓 → (𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔)))) |
47 | 46 | reximia 3239 |
. . . . . 6
⊢
(∃𝑓 ∈
𝐴 𝑥 <Q 𝑓 → ∃𝑓 ∈ 𝐴 (𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔))) |
48 | 25, 47 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝑥 ∈ 𝐴) → ∃𝑓 ∈ 𝐴 (𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔))) |
49 | 48 | ex 413 |
. . . 4
⊢ (𝐴 ∈ P →
(𝑥 ∈ 𝐴 → ∃𝑓 ∈ 𝐴 (𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔)))) |
50 | | prcdnq 10403 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) → (𝑥 <Q 𝑓 → 𝑥 ∈ 𝐴)) |
51 | 50 | adantrd 492 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) → ((𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔)) → 𝑥 ∈ 𝐴)) |
52 | 51 | rexlimdva 3281 |
. . . 4
⊢ (𝐴 ∈ P →
(∃𝑓 ∈ 𝐴 (𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔)) → 𝑥 ∈ 𝐴)) |
53 | 49, 52 | impbid 213 |
. . 3
⊢ (𝐴 ∈ P →
(𝑥 ∈ 𝐴 ↔ ∃𝑓 ∈ 𝐴 (𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔)))) |
54 | 19, 24, 53 | 3bitr4d 312 |
. 2
⊢ (𝐴 ∈ P →
(𝑥 ∈ (𝐴
·P 1P) ↔ 𝑥 ∈ 𝐴)) |
55 | 54 | eqrdv 2816 |
1
⊢ (𝐴 ∈ P →
(𝐴
·P 1P) = 𝐴) |