Step | Hyp | Ref
| Expression |
1 | | simpr 109 |
. . . . 5
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈ Q) ∧ 𝑋 <Q
𝑆) → 𝑋 <Q 𝑆) |
2 | | ltrnqi 7342 |
. . . . . 6
⊢ (𝑋 <Q
𝑆 →
(*Q‘𝑆) <Q
(*Q‘𝑋)) |
3 | | ltrelnq 7286 |
. . . . . . . . . . . 12
⊢
<Q ⊆ (Q ×
Q) |
4 | 3 | brel 4639 |
. . . . . . . . . . 11
⊢ (𝑋 <Q
𝑆 → (𝑋 ∈ Q ∧ 𝑆 ∈
Q)) |
5 | 4 | adantl 275 |
. . . . . . . . . 10
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈ Q) ∧ 𝑋 <Q
𝑆) → (𝑋 ∈ Q ∧
𝑆 ∈
Q)) |
6 | 5 | simprd 113 |
. . . . . . . . 9
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈ Q) ∧ 𝑋 <Q
𝑆) → 𝑆 ∈ Q) |
7 | | recclnq 7313 |
. . . . . . . . 9
⊢ (𝑆 ∈ Q →
(*Q‘𝑆) ∈ Q) |
8 | 6, 7 | syl 14 |
. . . . . . . 8
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈ Q) ∧ 𝑋 <Q
𝑆) →
(*Q‘𝑆) ∈ Q) |
9 | | simplr 520 |
. . . . . . . . 9
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈ Q) ∧ 𝑋 <Q
𝑆) → 𝑋 ∈ Q) |
10 | | recclnq 7313 |
. . . . . . . . 9
⊢ (𝑋 ∈ Q →
(*Q‘𝑋) ∈ Q) |
11 | 9, 10 | syl 14 |
. . . . . . . 8
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈ Q) ∧ 𝑋 <Q
𝑆) →
(*Q‘𝑋) ∈ Q) |
12 | | ltmnqg 7322 |
. . . . . . . 8
⊢
(((*Q‘𝑆) ∈ Q ∧
(*Q‘𝑋) ∈ Q ∧ 𝑋 ∈ Q) →
((*Q‘𝑆) <Q
(*Q‘𝑋) ↔ (𝑋 ·Q
(*Q‘𝑆)) <Q (𝑋
·Q (*Q‘𝑋)))) |
13 | 8, 11, 9, 12 | syl3anc 1220 |
. . . . . . 7
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈ Q) ∧ 𝑋 <Q
𝑆) →
((*Q‘𝑆) <Q
(*Q‘𝑋) ↔ (𝑋 ·Q
(*Q‘𝑆)) <Q (𝑋
·Q (*Q‘𝑋)))) |
14 | | ltmnqg 7322 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q
∧ 𝑤 ∈
Q) → (𝑦
<Q 𝑧 ↔ (𝑤 ·Q 𝑦) <Q
(𝑤
·Q 𝑧))) |
15 | 14 | adantl 275 |
. . . . . . . 8
⊢
(((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈ Q) ∧ 𝑋 <Q
𝑆) ∧ (𝑦 ∈ Q ∧
𝑧 ∈ Q
∧ 𝑤 ∈
Q)) → (𝑦
<Q 𝑧 ↔ (𝑤 ·Q 𝑦) <Q
(𝑤
·Q 𝑧))) |
16 | | mulclnq 7297 |
. . . . . . . . 9
⊢ ((𝑋 ∈ Q ∧
(*Q‘𝑆) ∈ Q) → (𝑋
·Q (*Q‘𝑆)) ∈
Q) |
17 | 9, 8, 16 | syl2anc 409 |
. . . . . . . 8
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈ Q) ∧ 𝑋 <Q
𝑆) → (𝑋
·Q (*Q‘𝑆)) ∈
Q) |
18 | | mulclnq 7297 |
. . . . . . . . 9
⊢ ((𝑋 ∈ Q ∧
(*Q‘𝑋) ∈ Q) → (𝑋
·Q (*Q‘𝑋)) ∈
Q) |
19 | 9, 11, 18 | syl2anc 409 |
. . . . . . . 8
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈ Q) ∧ 𝑋 <Q
𝑆) → (𝑋
·Q (*Q‘𝑋)) ∈
Q) |
20 | | elprnql 7402 |
. . . . . . . . 9
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝐿) → 𝐺 ∈ Q) |
21 | 20 | ad2antrr 480 |
. . . . . . . 8
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈ Q) ∧ 𝑋 <Q
𝑆) → 𝐺 ∈ Q) |
22 | | mulcomnqg 7304 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦
·Q 𝑧) = (𝑧 ·Q 𝑦)) |
23 | 22 | adantl 275 |
. . . . . . . 8
⊢
(((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈ Q) ∧ 𝑋 <Q
𝑆) ∧ (𝑦 ∈ Q ∧
𝑧 ∈ Q))
→ (𝑦
·Q 𝑧) = (𝑧 ·Q 𝑦)) |
24 | 15, 17, 19, 21, 23 | caovord2d 5991 |
. . . . . . 7
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈ Q) ∧ 𝑋 <Q
𝑆) → ((𝑋
·Q (*Q‘𝑆))
<Q (𝑋 ·Q
(*Q‘𝑋)) ↔ ((𝑋 ·Q
(*Q‘𝑆)) ·Q 𝐺) <Q
((𝑋
·Q (*Q‘𝑋))
·Q 𝐺))) |
25 | 13, 24 | bitrd 187 |
. . . . . 6
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈ Q) ∧ 𝑋 <Q
𝑆) →
((*Q‘𝑆) <Q
(*Q‘𝑋) ↔ ((𝑋 ·Q
(*Q‘𝑆)) ·Q 𝐺) <Q
((𝑋
·Q (*Q‘𝑋))
·Q 𝐺))) |
26 | 2, 25 | syl5ib 153 |
. . . . 5
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈ Q) ∧ 𝑋 <Q
𝑆) → (𝑋 <Q
𝑆 → ((𝑋
·Q (*Q‘𝑆))
·Q 𝐺) <Q ((𝑋
·Q (*Q‘𝑋))
·Q 𝐺))) |
27 | 1, 26 | mpd 13 |
. . . 4
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈ Q) ∧ 𝑋 <Q
𝑆) → ((𝑋
·Q (*Q‘𝑆))
·Q 𝐺) <Q ((𝑋
·Q (*Q‘𝑋))
·Q 𝐺)) |
28 | | recidnq 7314 |
. . . . . . . 8
⊢ (𝑋 ∈ Q →
(𝑋
·Q (*Q‘𝑋)) =
1Q) |
29 | 28 | oveq1d 5840 |
. . . . . . 7
⊢ (𝑋 ∈ Q →
((𝑋
·Q (*Q‘𝑋))
·Q 𝐺) = (1Q
·Q 𝐺)) |
30 | | 1nq 7287 |
. . . . . . . . 9
⊢
1Q ∈ Q |
31 | | mulcomnqg 7304 |
. . . . . . . . 9
⊢
((1Q ∈ Q ∧ 𝐺 ∈ Q) →
(1Q ·Q 𝐺) = (𝐺 ·Q
1Q)) |
32 | 30, 31 | mpan 421 |
. . . . . . . 8
⊢ (𝐺 ∈ Q →
(1Q ·Q 𝐺) = (𝐺 ·Q
1Q)) |
33 | | mulidnq 7310 |
. . . . . . . 8
⊢ (𝐺 ∈ Q →
(𝐺
·Q 1Q) = 𝐺) |
34 | 32, 33 | eqtrd 2190 |
. . . . . . 7
⊢ (𝐺 ∈ Q →
(1Q ·Q 𝐺) = 𝐺) |
35 | 29, 34 | sylan9eqr 2212 |
. . . . . 6
⊢ ((𝐺 ∈ Q ∧
𝑋 ∈ Q)
→ ((𝑋
·Q (*Q‘𝑋))
·Q 𝐺) = 𝐺) |
36 | 35 | breq2d 3978 |
. . . . 5
⊢ ((𝐺 ∈ Q ∧
𝑋 ∈ Q)
→ (((𝑋
·Q (*Q‘𝑆))
·Q 𝐺) <Q ((𝑋
·Q (*Q‘𝑋))
·Q 𝐺) ↔ ((𝑋 ·Q
(*Q‘𝑆)) ·Q 𝐺) <Q
𝐺)) |
37 | 21, 9, 36 | syl2anc 409 |
. . . 4
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈ Q) ∧ 𝑋 <Q
𝑆) → (((𝑋
·Q (*Q‘𝑆))
·Q 𝐺) <Q ((𝑋
·Q (*Q‘𝑋))
·Q 𝐺) ↔ ((𝑋 ·Q
(*Q‘𝑆)) ·Q 𝐺) <Q
𝐺)) |
38 | 27, 37 | mpbid 146 |
. . 3
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈ Q) ∧ 𝑋 <Q
𝑆) → ((𝑋
·Q (*Q‘𝑆))
·Q 𝐺) <Q 𝐺) |
39 | | prcdnql 7405 |
. . . 4
⊢
((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝐿) → (((𝑋 ·Q
(*Q‘𝑆)) ·Q 𝐺) <Q
𝐺 → ((𝑋
·Q (*Q‘𝑆))
·Q 𝐺) ∈ 𝐿)) |
40 | 39 | ad2antrr 480 |
. . 3
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈ Q) ∧ 𝑋 <Q
𝑆) → (((𝑋
·Q (*Q‘𝑆))
·Q 𝐺) <Q 𝐺 → ((𝑋 ·Q
(*Q‘𝑆)) ·Q 𝐺) ∈ 𝐿)) |
41 | 38, 40 | mpd 13 |
. 2
⊢
((((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈ Q) ∧ 𝑋 <Q
𝑆) → ((𝑋
·Q (*Q‘𝑆))
·Q 𝐺) ∈ 𝐿) |
42 | 41 | ex 114 |
1
⊢
(((〈𝐿, 𝑈〉 ∈ P
∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈ Q) → (𝑋 <Q
𝑆 → ((𝑋
·Q (*Q‘𝑆))
·Q 𝐺) ∈ 𝐿)) |