| Step | Hyp | Ref
| Expression |
| 1 | | df-rex 3071 |
. . . . 5
⊢
(∃𝑔 ∈
1P 𝑥 = (𝑓 ·Q 𝑔) ↔ ∃𝑔(𝑔 ∈ 1P ∧
𝑥 = (𝑓 ·Q 𝑔))) |
| 2 | | elprnq 11031 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) → 𝑓 ∈ Q) |
| 3 | | breq1 5146 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑓 ·Q 𝑔) → (𝑥 <Q 𝑓 ↔ (𝑓 ·Q 𝑔) <Q
𝑓)) |
| 4 | | df-1p 11022 |
. . . . . . . . . . . . 13
⊢
1P = {𝑔 ∣ 𝑔 <Q
1Q} |
| 5 | 4 | eqabri 2885 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈
1P ↔ 𝑔 <Q
1Q) |
| 6 | | ltmnq 11012 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ Q →
(𝑔
<Q 1Q ↔ (𝑓
·Q 𝑔) <Q (𝑓
·Q
1Q))) |
| 7 | | mulidnq 11003 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ Q →
(𝑓
·Q 1Q) = 𝑓) |
| 8 | 7 | breq2d 5155 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ Q →
((𝑓
·Q 𝑔) <Q (𝑓
·Q 1Q) ↔ (𝑓
·Q 𝑔) <Q 𝑓)) |
| 9 | 6, 8 | bitrd 279 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ Q →
(𝑔
<Q 1Q ↔ (𝑓
·Q 𝑔) <Q 𝑓)) |
| 10 | 5, 9 | bitr2id 284 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ Q →
((𝑓
·Q 𝑔) <Q 𝑓 ↔ 𝑔 ∈
1P)) |
| 11 | 3, 10 | sylan9bbr 510 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ Q ∧
𝑥 = (𝑓 ·Q 𝑔)) → (𝑥 <Q 𝑓 ↔ 𝑔 ∈
1P)) |
| 12 | 2, 11 | sylan 580 |
. . . . . . . . 9
⊢ (((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) ∧ 𝑥 = (𝑓 ·Q 𝑔)) → (𝑥 <Q 𝑓 ↔ 𝑔 ∈
1P)) |
| 13 | 12 | ex 412 |
. . . . . . . 8
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) → (𝑥 = (𝑓 ·Q 𝑔) → (𝑥 <Q 𝑓 ↔ 𝑔 ∈
1P))) |
| 14 | 13 | pm5.32rd 578 |
. . . . . . 7
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) → ((𝑥 <Q 𝑓 ∧ 𝑥 = (𝑓 ·Q 𝑔)) ↔ (𝑔 ∈ 1P ∧
𝑥 = (𝑓 ·Q 𝑔)))) |
| 15 | 14 | exbidv 1921 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) → (∃𝑔(𝑥 <Q 𝑓 ∧ 𝑥 = (𝑓 ·Q 𝑔)) ↔ ∃𝑔(𝑔 ∈ 1P ∧
𝑥 = (𝑓 ·Q 𝑔)))) |
| 16 | | 19.42v 1953 |
. . . . . 6
⊢
(∃𝑔(𝑥 <Q
𝑓 ∧ 𝑥 = (𝑓 ·Q 𝑔)) ↔ (𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔))) |
| 17 | 15, 16 | bitr3di 286 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) → (∃𝑔(𝑔 ∈ 1P ∧
𝑥 = (𝑓 ·Q 𝑔)) ↔ (𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔)))) |
| 18 | 1, 17 | bitrid 283 |
. . . 4
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) → (∃𝑔 ∈ 1P 𝑥 = (𝑓 ·Q 𝑔) ↔ (𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔)))) |
| 19 | 18 | rexbidva 3177 |
. . 3
⊢ (𝐴 ∈ P →
(∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 1P 𝑥 = (𝑓 ·Q 𝑔) ↔ ∃𝑓 ∈ 𝐴 (𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔)))) |
| 20 | | 1pr 11055 |
. . . 4
⊢
1P ∈ P |
| 21 | | df-mp 11024 |
. . . . 5
⊢
·P = (𝑦 ∈ P, 𝑧 ∈ P ↦ {𝑤 ∣ ∃𝑢 ∈ 𝑦 ∃𝑣 ∈ 𝑧 𝑤 = (𝑢 ·Q 𝑣)}) |
| 22 | | mulclnq 10987 |
. . . . 5
⊢ ((𝑢 ∈ Q ∧
𝑣 ∈ Q)
→ (𝑢
·Q 𝑣) ∈ Q) |
| 23 | 21, 22 | genpelv 11040 |
. . . 4
⊢ ((𝐴 ∈ P ∧
1P ∈ P) → (𝑥 ∈ (𝐴 ·P
1P) ↔ ∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 1P 𝑥 = (𝑓 ·Q 𝑔))) |
| 24 | 20, 23 | mpan2 691 |
. . 3
⊢ (𝐴 ∈ P →
(𝑥 ∈ (𝐴
·P 1P) ↔
∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 1P 𝑥 = (𝑓 ·Q 𝑔))) |
| 25 | | prnmax 11035 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
𝑥 ∈ 𝐴) → ∃𝑓 ∈ 𝐴 𝑥 <Q 𝑓) |
| 26 | | ltrelnq 10966 |
. . . . . . . . . . 11
⊢
<Q ⊆ (Q ×
Q) |
| 27 | 26 | brel 5750 |
. . . . . . . . . 10
⊢ (𝑥 <Q
𝑓 → (𝑥 ∈ Q ∧
𝑓 ∈
Q)) |
| 28 | | vex 3484 |
. . . . . . . . . . . . . 14
⊢ 𝑓 ∈ V |
| 29 | | vex 3484 |
. . . . . . . . . . . . . 14
⊢ 𝑥 ∈ V |
| 30 | | fvex 6919 |
. . . . . . . . . . . . . 14
⊢
(*Q‘𝑓) ∈ V |
| 31 | | mulcomnq 10993 |
. . . . . . . . . . . . . 14
⊢ (𝑦
·Q 𝑧) = (𝑧 ·Q 𝑦) |
| 32 | | mulassnq 10999 |
. . . . . . . . . . . . . 14
⊢ ((𝑦
·Q 𝑧) ·Q 𝑤) = (𝑦 ·Q (𝑧
·Q 𝑤)) |
| 33 | 28, 29, 30, 31, 32 | caov12 7661 |
. . . . . . . . . . . . 13
⊢ (𝑓
·Q (𝑥 ·Q
(*Q‘𝑓))) = (𝑥 ·Q (𝑓
·Q (*Q‘𝑓))) |
| 34 | | recidnq 11005 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ Q →
(𝑓
·Q (*Q‘𝑓)) =
1Q) |
| 35 | 34 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ Q →
(𝑥
·Q (𝑓 ·Q
(*Q‘𝑓))) = (𝑥 ·Q
1Q)) |
| 36 | 33, 35 | eqtrid 2789 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ Q →
(𝑓
·Q (𝑥 ·Q
(*Q‘𝑓))) = (𝑥 ·Q
1Q)) |
| 37 | | mulidnq 11003 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ Q →
(𝑥
·Q 1Q) = 𝑥) |
| 38 | 36, 37 | sylan9eqr 2799 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ Q ∧
𝑓 ∈ Q)
→ (𝑓
·Q (𝑥 ·Q
(*Q‘𝑓))) = 𝑥) |
| 39 | 38 | eqcomd 2743 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ Q ∧
𝑓 ∈ Q)
→ 𝑥 = (𝑓
·Q (𝑥 ·Q
(*Q‘𝑓)))) |
| 40 | | ovex 7464 |
. . . . . . . . . . 11
⊢ (𝑥
·Q (*Q‘𝑓)) ∈ V |
| 41 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑔 = (𝑥 ·Q
(*Q‘𝑓)) → (𝑓 ·Q 𝑔) = (𝑓 ·Q (𝑥
·Q (*Q‘𝑓)))) |
| 42 | 41 | eqeq2d 2748 |
. . . . . . . . . . 11
⊢ (𝑔 = (𝑥 ·Q
(*Q‘𝑓)) → (𝑥 = (𝑓 ·Q 𝑔) ↔ 𝑥 = (𝑓 ·Q (𝑥
·Q (*Q‘𝑓))))) |
| 43 | 40, 42 | spcev 3606 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑓 ·Q (𝑥
·Q (*Q‘𝑓))) → ∃𝑔 𝑥 = (𝑓 ·Q 𝑔)) |
| 44 | 27, 39, 43 | 3syl 18 |
. . . . . . . . 9
⊢ (𝑥 <Q
𝑓 → ∃𝑔 𝑥 = (𝑓 ·Q 𝑔)) |
| 45 | 44 | a1i 11 |
. . . . . . . 8
⊢ (𝑓 ∈ 𝐴 → (𝑥 <Q 𝑓 → ∃𝑔 𝑥 = (𝑓 ·Q 𝑔))) |
| 46 | 45 | ancld 550 |
. . . . . . 7
⊢ (𝑓 ∈ 𝐴 → (𝑥 <Q 𝑓 → (𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔)))) |
| 47 | 46 | reximia 3081 |
. . . . . 6
⊢
(∃𝑓 ∈
𝐴 𝑥 <Q 𝑓 → ∃𝑓 ∈ 𝐴 (𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔))) |
| 48 | 25, 47 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝑥 ∈ 𝐴) → ∃𝑓 ∈ 𝐴 (𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔))) |
| 49 | 48 | ex 412 |
. . . 4
⊢ (𝐴 ∈ P →
(𝑥 ∈ 𝐴 → ∃𝑓 ∈ 𝐴 (𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔)))) |
| 50 | | prcdnq 11033 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) → (𝑥 <Q 𝑓 → 𝑥 ∈ 𝐴)) |
| 51 | 50 | adantrd 491 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) → ((𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔)) → 𝑥 ∈ 𝐴)) |
| 52 | 51 | rexlimdva 3155 |
. . . 4
⊢ (𝐴 ∈ P →
(∃𝑓 ∈ 𝐴 (𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔)) → 𝑥 ∈ 𝐴)) |
| 53 | 49, 52 | impbid 212 |
. . 3
⊢ (𝐴 ∈ P →
(𝑥 ∈ 𝐴 ↔ ∃𝑓 ∈ 𝐴 (𝑥 <Q 𝑓 ∧ ∃𝑔 𝑥 = (𝑓 ·Q 𝑔)))) |
| 54 | 19, 24, 53 | 3bitr4d 311 |
. 2
⊢ (𝐴 ∈ P →
(𝑥 ∈ (𝐴
·P 1P) ↔ 𝑥 ∈ 𝐴)) |
| 55 | 54 | eqrdv 2735 |
1
⊢ (𝐴 ∈ P →
(𝐴
·P 1P) = 𝐴) |