| Step | Hyp | Ref
| Expression |
| 1 | | elprnq 11031 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) → 𝑔 ∈ Q) |
| 2 | | elprnq 11031 |
. . . . . 6
⊢ ((𝐵 ∈ P ∧
ℎ ∈ 𝐵) → ℎ ∈ Q) |
| 3 | | recclnq 11006 |
. . . . . . . . 9
⊢ (ℎ ∈ Q →
(*Q‘ℎ) ∈ Q) |
| 4 | 3 | adantl 481 |
. . . . . . . 8
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ (*Q‘ℎ) ∈ Q) |
| 5 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
| 6 | | ovex 7464 |
. . . . . . . . 9
⊢ (𝑔
·Q ℎ) ∈ V |
| 7 | | ltmnq 11012 |
. . . . . . . . 9
⊢ (𝑤 ∈ Q →
(𝑦
<Q 𝑧 ↔ (𝑤 ·Q 𝑦) <Q
(𝑤
·Q 𝑧))) |
| 8 | | fvex 6919 |
. . . . . . . . 9
⊢
(*Q‘ℎ) ∈ V |
| 9 | | mulcomnq 10993 |
. . . . . . . . 9
⊢ (𝑦
·Q 𝑧) = (𝑧 ·Q 𝑦) |
| 10 | 5, 6, 7, 8, 9 | caovord2 7645 |
. . . . . . . 8
⊢
((*Q‘ℎ) ∈ Q → (𝑥 <Q
(𝑔
·Q ℎ) ↔ (𝑥 ·Q
(*Q‘ℎ)) <Q ((𝑔
·Q ℎ) ·Q
(*Q‘ℎ)))) |
| 11 | 4, 10 | syl 17 |
. . . . . . 7
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ (𝑥
<Q (𝑔 ·Q ℎ) ↔ (𝑥 ·Q
(*Q‘ℎ)) <Q ((𝑔
·Q ℎ) ·Q
(*Q‘ℎ)))) |
| 12 | | mulassnq 10999 |
. . . . . . . . . 10
⊢ ((𝑔
·Q ℎ) ·Q
(*Q‘ℎ)) = (𝑔 ·Q (ℎ
·Q (*Q‘ℎ))) |
| 13 | | recidnq 11005 |
. . . . . . . . . . 11
⊢ (ℎ ∈ Q →
(ℎ
·Q (*Q‘ℎ)) =
1Q) |
| 14 | 13 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (ℎ ∈ Q →
(𝑔
·Q (ℎ ·Q
(*Q‘ℎ))) = (𝑔 ·Q
1Q)) |
| 15 | 12, 14 | eqtrid 2789 |
. . . . . . . . 9
⊢ (ℎ ∈ Q →
((𝑔
·Q ℎ) ·Q
(*Q‘ℎ)) = (𝑔 ·Q
1Q)) |
| 16 | | mulidnq 11003 |
. . . . . . . . 9
⊢ (𝑔 ∈ Q →
(𝑔
·Q 1Q) = 𝑔) |
| 17 | 15, 16 | sylan9eqr 2799 |
. . . . . . . 8
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ ((𝑔
·Q ℎ) ·Q
(*Q‘ℎ)) = 𝑔) |
| 18 | 17 | breq2d 5155 |
. . . . . . 7
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ ((𝑥
·Q (*Q‘ℎ)) <Q
((𝑔
·Q ℎ) ·Q
(*Q‘ℎ)) ↔ (𝑥 ·Q
(*Q‘ℎ)) <Q 𝑔)) |
| 19 | 11, 18 | bitrd 279 |
. . . . . 6
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ (𝑥
<Q (𝑔 ·Q ℎ) ↔ (𝑥 ·Q
(*Q‘ℎ)) <Q 𝑔)) |
| 20 | 1, 2, 19 | syl2an 596 |
. . . . 5
⊢ (((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) → (𝑥 <Q (𝑔
·Q ℎ) ↔ (𝑥 ·Q
(*Q‘ℎ)) <Q 𝑔)) |
| 21 | | prcdnq 11033 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) → ((𝑥 ·Q
(*Q‘ℎ)) <Q 𝑔 → (𝑥 ·Q
(*Q‘ℎ)) ∈ 𝐴)) |
| 22 | 21 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) → ((𝑥 ·Q
(*Q‘ℎ)) <Q 𝑔 → (𝑥 ·Q
(*Q‘ℎ)) ∈ 𝐴)) |
| 23 | 20, 22 | sylbid 240 |
. . . 4
⊢ (((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) → (𝑥 <Q (𝑔
·Q ℎ) → (𝑥 ·Q
(*Q‘ℎ)) ∈ 𝐴)) |
| 24 | | df-mp 11024 |
. . . . . . . . 9
⊢
·P = (𝑤 ∈ P, 𝑣 ∈ P ↦ {𝑥 ∣ ∃𝑦 ∈ 𝑤 ∃𝑧 ∈ 𝑣 𝑥 = (𝑦 ·Q 𝑧)}) |
| 25 | | mulclnq 10987 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦
·Q 𝑧) ∈ Q) |
| 26 | 24, 25 | genpprecl 11041 |
. . . . . . . 8
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (((𝑥
·Q (*Q‘ℎ)) ∈ 𝐴 ∧ ℎ ∈ 𝐵) → ((𝑥 ·Q
(*Q‘ℎ)) ·Q ℎ) ∈ (𝐴 ·P 𝐵))) |
| 27 | 26 | exp4b 430 |
. . . . . . 7
⊢ (𝐴 ∈ P →
(𝐵 ∈ P
→ ((𝑥
·Q (*Q‘ℎ)) ∈ 𝐴 → (ℎ ∈ 𝐵 → ((𝑥 ·Q
(*Q‘ℎ)) ·Q ℎ) ∈ (𝐴 ·P 𝐵))))) |
| 28 | 27 | com34 91 |
. . . . . 6
⊢ (𝐴 ∈ P →
(𝐵 ∈ P
→ (ℎ ∈ 𝐵 → ((𝑥 ·Q
(*Q‘ℎ)) ∈ 𝐴 → ((𝑥 ·Q
(*Q‘ℎ)) ·Q ℎ) ∈ (𝐴 ·P 𝐵))))) |
| 29 | 28 | imp32 418 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
(𝐵 ∈ P
∧ ℎ ∈ 𝐵)) → ((𝑥 ·Q
(*Q‘ℎ)) ∈ 𝐴 → ((𝑥 ·Q
(*Q‘ℎ)) ·Q ℎ) ∈ (𝐴 ·P 𝐵))) |
| 30 | 29 | adantlr 715 |
. . . 4
⊢ (((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) → ((𝑥 ·Q
(*Q‘ℎ)) ∈ 𝐴 → ((𝑥 ·Q
(*Q‘ℎ)) ·Q ℎ) ∈ (𝐴 ·P 𝐵))) |
| 31 | 23, 30 | syld 47 |
. . 3
⊢ (((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) → (𝑥 <Q (𝑔
·Q ℎ) → ((𝑥 ·Q
(*Q‘ℎ)) ·Q ℎ) ∈ (𝐴 ·P 𝐵))) |
| 32 | 31 | adantr 480 |
. 2
⊢ ((((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) ∧ 𝑥 ∈ Q) → (𝑥 <Q
(𝑔
·Q ℎ) → ((𝑥 ·Q
(*Q‘ℎ)) ·Q ℎ) ∈ (𝐴 ·P 𝐵))) |
| 33 | 2 | adantl 481 |
. . 3
⊢ (((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) → ℎ ∈ Q) |
| 34 | | mulassnq 10999 |
. . . . . 6
⊢ ((𝑥
·Q (*Q‘ℎ))
·Q ℎ) = (𝑥 ·Q
((*Q‘ℎ) ·Q ℎ)) |
| 35 | | mulcomnq 10993 |
. . . . . . . 8
⊢
((*Q‘ℎ) ·Q ℎ) = (ℎ ·Q
(*Q‘ℎ)) |
| 36 | 35, 13 | eqtrid 2789 |
. . . . . . 7
⊢ (ℎ ∈ Q →
((*Q‘ℎ) ·Q ℎ) =
1Q) |
| 37 | 36 | oveq2d 7447 |
. . . . . 6
⊢ (ℎ ∈ Q →
(𝑥
·Q ((*Q‘ℎ)
·Q ℎ)) = (𝑥 ·Q
1Q)) |
| 38 | 34, 37 | eqtrid 2789 |
. . . . 5
⊢ (ℎ ∈ Q →
((𝑥
·Q (*Q‘ℎ))
·Q ℎ) = (𝑥 ·Q
1Q)) |
| 39 | | mulidnq 11003 |
. . . . 5
⊢ (𝑥 ∈ Q →
(𝑥
·Q 1Q) = 𝑥) |
| 40 | 38, 39 | sylan9eq 2797 |
. . . 4
⊢ ((ℎ ∈ Q ∧
𝑥 ∈ Q)
→ ((𝑥
·Q (*Q‘ℎ))
·Q ℎ) = 𝑥) |
| 41 | 40 | eleq1d 2826 |
. . 3
⊢ ((ℎ ∈ Q ∧
𝑥 ∈ Q)
→ (((𝑥
·Q (*Q‘ℎ))
·Q ℎ) ∈ (𝐴 ·P 𝐵) ↔ 𝑥 ∈ (𝐴 ·P 𝐵))) |
| 42 | 33, 41 | sylan 580 |
. 2
⊢ ((((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) ∧ 𝑥 ∈ Q) → (((𝑥
·Q (*Q‘ℎ))
·Q ℎ) ∈ (𝐴 ·P 𝐵) ↔ 𝑥 ∈ (𝐴 ·P 𝐵))) |
| 43 | 32, 42 | sylibd 239 |
1
⊢ ((((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) ∧ 𝑥 ∈ Q) → (𝑥 <Q
(𝑔
·Q ℎ) → 𝑥 ∈ (𝐴 ·P 𝐵))) |