| Step | Hyp | Ref
| Expression |
| 1 | | reclempr.1 |
. . . . . . 7
⊢ 𝐵 = {𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴)} |
| 2 | 1 | reclem2pr 11088 |
. . . . . 6
⊢ (𝐴 ∈ P →
𝐵 ∈
P) |
| 3 | | df-mp 11024 |
. . . . . . 7
⊢
·P = (𝑦 ∈ P, 𝑤 ∈ P ↦ {𝑢 ∣ ∃𝑓 ∈ 𝑦 ∃𝑔 ∈ 𝑤 𝑢 = (𝑓 ·Q 𝑔)}) |
| 4 | | mulclnq 10987 |
. . . . . . 7
⊢ ((𝑓 ∈ Q ∧
𝑔 ∈ Q)
→ (𝑓
·Q 𝑔) ∈ Q) |
| 5 | 3, 4 | genpelv 11040 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝑤 ∈ (𝐴
·P 𝐵) ↔ ∃𝑧 ∈ 𝐴 ∃𝑥 ∈ 𝐵 𝑤 = (𝑧 ·Q 𝑥))) |
| 6 | 2, 5 | mpdan 687 |
. . . . 5
⊢ (𝐴 ∈ P →
(𝑤 ∈ (𝐴
·P 𝐵) ↔ ∃𝑧 ∈ 𝐴 ∃𝑥 ∈ 𝐵 𝑤 = (𝑧 ·Q 𝑥))) |
| 7 | 1 | eqabri 2885 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 ↔ ∃𝑦(𝑥 <Q 𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴)) |
| 8 | | ltrelnq 10966 |
. . . . . . . . . . . . . . 15
⊢
<Q ⊆ (Q ×
Q) |
| 9 | 8 | brel 5750 |
. . . . . . . . . . . . . 14
⊢ (𝑥 <Q
𝑦 → (𝑥 ∈ Q ∧
𝑦 ∈
Q)) |
| 10 | 9 | simprd 495 |
. . . . . . . . . . . . 13
⊢ (𝑥 <Q
𝑦 → 𝑦 ∈ Q) |
| 11 | | elprnq 11031 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ P ∧
𝑧 ∈ 𝐴) → 𝑧 ∈ Q) |
| 12 | | ltmnq 11012 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ Q →
(𝑥
<Q 𝑦 ↔ (𝑧 ·Q 𝑥) <Q
(𝑧
·Q 𝑦))) |
| 13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ P ∧
𝑧 ∈ 𝐴) → (𝑥 <Q 𝑦 ↔ (𝑧 ·Q 𝑥) <Q
(𝑧
·Q 𝑦))) |
| 14 | 13 | biimpd 229 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ P ∧
𝑧 ∈ 𝐴) → (𝑥 <Q 𝑦 → (𝑧 ·Q 𝑥) <Q
(𝑧
·Q 𝑦))) |
| 15 | 14 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ P ∧
𝑧 ∈ 𝐴) ∧ 𝑦 ∈ Q) → (𝑥 <Q
𝑦 → (𝑧
·Q 𝑥) <Q (𝑧
·Q 𝑦))) |
| 16 | | recclnq 11006 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ Q →
(*Q‘𝑦) ∈ Q) |
| 17 | | prub 11034 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ P ∧
𝑧 ∈ 𝐴) ∧
(*Q‘𝑦) ∈ Q) → (¬
(*Q‘𝑦) ∈ 𝐴 → 𝑧 <Q
(*Q‘𝑦))) |
| 18 | 16, 17 | sylan2 593 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ P ∧
𝑧 ∈ 𝐴) ∧ 𝑦 ∈ Q) → (¬
(*Q‘𝑦) ∈ 𝐴 → 𝑧 <Q
(*Q‘𝑦))) |
| 19 | | ltmnq 11012 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ Q →
(𝑧
<Q (*Q‘𝑦) ↔ (𝑦 ·Q 𝑧) <Q
(𝑦
·Q (*Q‘𝑦)))) |
| 20 | | mulcomnq 10993 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦
·Q 𝑧) = (𝑧 ·Q 𝑦) |
| 21 | 20 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ Q →
(𝑦
·Q 𝑧) = (𝑧 ·Q 𝑦)) |
| 22 | | recidnq 11005 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ Q →
(𝑦
·Q (*Q‘𝑦)) =
1Q) |
| 23 | 21, 22 | breq12d 5156 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ Q →
((𝑦
·Q 𝑧) <Q (𝑦
·Q (*Q‘𝑦)) ↔ (𝑧 ·Q 𝑦) <Q
1Q)) |
| 24 | 19, 23 | bitrd 279 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ Q →
(𝑧
<Q (*Q‘𝑦) ↔ (𝑧 ·Q 𝑦) <Q
1Q)) |
| 25 | 24 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ P ∧
𝑧 ∈ 𝐴) ∧ 𝑦 ∈ Q) → (𝑧 <Q
(*Q‘𝑦) ↔ (𝑧 ·Q 𝑦) <Q
1Q)) |
| 26 | 18, 25 | sylibd 239 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ P ∧
𝑧 ∈ 𝐴) ∧ 𝑦 ∈ Q) → (¬
(*Q‘𝑦) ∈ 𝐴 → (𝑧 ·Q 𝑦) <Q
1Q)) |
| 27 | 15, 26 | anim12d 609 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ P ∧
𝑧 ∈ 𝐴) ∧ 𝑦 ∈ Q) → ((𝑥 <Q
𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴) → ((𝑧 ·Q 𝑥) <Q
(𝑧
·Q 𝑦) ∧ (𝑧 ·Q 𝑦) <Q
1Q))) |
| 28 | | ltsonq 11009 |
. . . . . . . . . . . . . . . 16
⊢
<Q Or Q |
| 29 | 28, 8 | sotri 6147 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧
·Q 𝑥) <Q (𝑧
·Q 𝑦) ∧ (𝑧 ·Q 𝑦) <Q
1Q) → (𝑧 ·Q 𝑥) <Q
1Q) |
| 30 | 27, 29 | syl6 35 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ P ∧
𝑧 ∈ 𝐴) ∧ 𝑦 ∈ Q) → ((𝑥 <Q
𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴) → (𝑧 ·Q 𝑥) <Q
1Q)) |
| 31 | 30 | exp4b 430 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ P ∧
𝑧 ∈ 𝐴) → (𝑦 ∈ Q → (𝑥 <Q
𝑦 → (¬
(*Q‘𝑦) ∈ 𝐴 → (𝑧 ·Q 𝑥) <Q
1Q)))) |
| 32 | 10, 31 | syl5 34 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ P ∧
𝑧 ∈ 𝐴) → (𝑥 <Q 𝑦 → (𝑥 <Q 𝑦 → (¬
(*Q‘𝑦) ∈ 𝐴 → (𝑧 ·Q 𝑥) <Q
1Q)))) |
| 33 | 32 | pm2.43d 53 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ P ∧
𝑧 ∈ 𝐴) → (𝑥 <Q 𝑦 → (¬
(*Q‘𝑦) ∈ 𝐴 → (𝑧 ·Q 𝑥) <Q
1Q))) |
| 34 | 33 | impd 410 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ P ∧
𝑧 ∈ 𝐴) → ((𝑥 <Q 𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴) → (𝑧 ·Q 𝑥) <Q
1Q)) |
| 35 | 34 | exlimdv 1933 |
. . . . . . . . 9
⊢ ((𝐴 ∈ P ∧
𝑧 ∈ 𝐴) → (∃𝑦(𝑥 <Q 𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴) → (𝑧 ·Q 𝑥) <Q
1Q)) |
| 36 | 7, 35 | biimtrid 242 |
. . . . . . . 8
⊢ ((𝐴 ∈ P ∧
𝑧 ∈ 𝐴) → (𝑥 ∈ 𝐵 → (𝑧 ·Q 𝑥) <Q
1Q)) |
| 37 | | breq1 5146 |
. . . . . . . . 9
⊢ (𝑤 = (𝑧 ·Q 𝑥) → (𝑤 <Q
1Q ↔ (𝑧 ·Q 𝑥) <Q
1Q)) |
| 38 | 37 | biimprcd 250 |
. . . . . . . 8
⊢ ((𝑧
·Q 𝑥) <Q
1Q → (𝑤 = (𝑧 ·Q 𝑥) → 𝑤 <Q
1Q)) |
| 39 | 36, 38 | syl6 35 |
. . . . . . 7
⊢ ((𝐴 ∈ P ∧
𝑧 ∈ 𝐴) → (𝑥 ∈ 𝐵 → (𝑤 = (𝑧 ·Q 𝑥) → 𝑤 <Q
1Q))) |
| 40 | 39 | expimpd 453 |
. . . . . 6
⊢ (𝐴 ∈ P →
((𝑧 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → (𝑤 = (𝑧 ·Q 𝑥) → 𝑤 <Q
1Q))) |
| 41 | 40 | rexlimdvv 3212 |
. . . . 5
⊢ (𝐴 ∈ P →
(∃𝑧 ∈ 𝐴 ∃𝑥 ∈ 𝐵 𝑤 = (𝑧 ·Q 𝑥) → 𝑤 <Q
1Q)) |
| 42 | 6, 41 | sylbid 240 |
. . . 4
⊢ (𝐴 ∈ P →
(𝑤 ∈ (𝐴
·P 𝐵) → 𝑤 <Q
1Q)) |
| 43 | | df-1p 11022 |
. . . . 5
⊢
1P = {𝑤 ∣ 𝑤 <Q
1Q} |
| 44 | 43 | eqabri 2885 |
. . . 4
⊢ (𝑤 ∈
1P ↔ 𝑤 <Q
1Q) |
| 45 | 42, 44 | imbitrrdi 252 |
. . 3
⊢ (𝐴 ∈ P →
(𝑤 ∈ (𝐴
·P 𝐵) → 𝑤 ∈
1P)) |
| 46 | 45 | ssrdv 3989 |
. 2
⊢ (𝐴 ∈ P →
(𝐴
·P 𝐵) ⊆
1P) |
| 47 | 1 | reclem3pr 11089 |
. 2
⊢ (𝐴 ∈ P →
1P ⊆ (𝐴 ·P 𝐵)) |
| 48 | 46, 47 | eqssd 4001 |
1
⊢ (𝐴 ∈ P →
(𝐴
·P 𝐵) =
1P) |