Step | Hyp | Ref
| Expression |
1 | | recexpr.1 |
. . . . . 6
⊢ 𝐵 = 〈{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧
(*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧
(*Q‘𝑦) ∈ (1st ‘𝐴))}〉 |
2 | 1 | recexprlempr 7581 |
. . . . 5
⊢ (𝐴 ∈ P →
𝐵 ∈
P) |
3 | | df-imp 7418 |
. . . . . 6
⊢
·P = (𝑦 ∈ P, 𝑤 ∈ P ↦ 〈{𝑢 ∈ Q ∣
∃𝑓 ∈
Q ∃𝑔
∈ Q (𝑓
∈ (1st ‘𝑦) ∧ 𝑔 ∈ (1st ‘𝑤) ∧ 𝑢 = (𝑓 ·Q 𝑔))}, {𝑢 ∈ Q ∣ ∃𝑓 ∈ Q
∃𝑔 ∈
Q (𝑓 ∈
(2nd ‘𝑦)
∧ 𝑔 ∈
(2nd ‘𝑤)
∧ 𝑢 = (𝑓
·Q 𝑔))}〉) |
4 | | mulclnq 7325 |
. . . . . 6
⊢ ((𝑓 ∈ Q ∧
𝑔 ∈ Q)
→ (𝑓
·Q 𝑔) ∈ Q) |
5 | 3, 4 | genpelvu 7462 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝑤 ∈
(2nd ‘(𝐴
·P 𝐵)) ↔ ∃𝑧 ∈ (2nd ‘𝐴)∃𝑞 ∈ (2nd ‘𝐵)𝑤 = (𝑧 ·Q 𝑞))) |
6 | 2, 5 | mpdan 419 |
. . . 4
⊢ (𝐴 ∈ P →
(𝑤 ∈ (2nd
‘(𝐴
·P 𝐵)) ↔ ∃𝑧 ∈ (2nd ‘𝐴)∃𝑞 ∈ (2nd ‘𝐵)𝑤 = (𝑧 ·Q 𝑞))) |
7 | 1 | recexprlemelu 7572 |
. . . . . . . 8
⊢ (𝑞 ∈ (2nd
‘𝐵) ↔
∃𝑦(𝑦 <Q 𝑞 ∧
(*Q‘𝑦) ∈ (1st ‘𝐴))) |
8 | | ltrelnq 7314 |
. . . . . . . . . . . . . 14
⊢
<Q ⊆ (Q ×
Q) |
9 | 8 | brel 4661 |
. . . . . . . . . . . . 13
⊢ (𝑦 <Q
𝑞 → (𝑦 ∈ Q ∧
𝑞 ∈
Q)) |
10 | 9 | simpld 111 |
. . . . . . . . . . . 12
⊢ (𝑦 <Q
𝑞 → 𝑦 ∈ Q) |
11 | | prop 7424 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ P →
〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈
P) |
12 | | elprnqu 7431 |
. . . . . . . . . . . . . . . . . 18
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝑧 ∈ (2nd
‘𝐴)) → 𝑧 ∈
Q) |
13 | 11, 12 | sylan 281 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ P ∧
𝑧 ∈ (2nd
‘𝐴)) → 𝑧 ∈
Q) |
14 | | ltmnqi 7352 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 <Q
𝑞 ∧ 𝑧 ∈ Q) → (𝑧
·Q 𝑦) <Q (𝑧
·Q 𝑞)) |
15 | 14 | expcom 115 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ Q →
(𝑦
<Q 𝑞 → (𝑧 ·Q 𝑦) <Q
(𝑧
·Q 𝑞))) |
16 | 13, 15 | syl 14 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ P ∧
𝑧 ∈ (2nd
‘𝐴)) → (𝑦 <Q
𝑞 → (𝑧
·Q 𝑦) <Q (𝑧
·Q 𝑞))) |
17 | 16 | adantr 274 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ P ∧
𝑧 ∈ (2nd
‘𝐴)) ∧ 𝑦 ∈ Q) →
(𝑦
<Q 𝑞 → (𝑧 ·Q 𝑦) <Q
(𝑧
·Q 𝑞))) |
18 | | prltlu 7436 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧
(*Q‘𝑦) ∈ (1st ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐴)) →
(*Q‘𝑦) <Q 𝑧) |
19 | 11, 18 | syl3an1 1266 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ P ∧
(*Q‘𝑦) ∈ (1st ‘𝐴) ∧ 𝑧 ∈ (2nd ‘𝐴)) →
(*Q‘𝑦) <Q 𝑧) |
20 | 19 | 3com23 1204 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ P ∧
𝑧 ∈ (2nd
‘𝐴) ∧
(*Q‘𝑦) ∈ (1st ‘𝐴)) →
(*Q‘𝑦) <Q 𝑧) |
21 | 20 | 3expia 1200 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ P ∧
𝑧 ∈ (2nd
‘𝐴)) →
((*Q‘𝑦) ∈ (1st ‘𝐴) →
(*Q‘𝑦) <Q 𝑧)) |
22 | 21 | adantr 274 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ P ∧
𝑧 ∈ (2nd
‘𝐴)) ∧ 𝑦 ∈ Q) →
((*Q‘𝑦) ∈ (1st ‘𝐴) →
(*Q‘𝑦) <Q 𝑧)) |
23 | | ltmnqi 7352 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((*Q‘𝑦) <Q 𝑧 ∧ 𝑦 ∈ Q) → (𝑦
·Q (*Q‘𝑦))
<Q (𝑦 ·Q 𝑧)) |
24 | 23 | expcom 115 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ Q →
((*Q‘𝑦) <Q 𝑧 → (𝑦 ·Q
(*Q‘𝑦)) <Q (𝑦
·Q 𝑧))) |
25 | 24 | adantr 274 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ ((*Q‘𝑦) <Q 𝑧 → (𝑦 ·Q
(*Q‘𝑦)) <Q (𝑦
·Q 𝑧))) |
26 | | recidnq 7342 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ Q →
(𝑦
·Q (*Q‘𝑦)) =
1Q) |
27 | 26 | adantr 274 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦
·Q (*Q‘𝑦)) =
1Q) |
28 | | mulcomnqg 7332 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦
·Q 𝑧) = (𝑧 ·Q 𝑦)) |
29 | 27, 28 | breq12d 4000 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ ((𝑦
·Q (*Q‘𝑦))
<Q (𝑦 ·Q 𝑧) ↔
1Q <Q (𝑧 ·Q 𝑦))) |
30 | 25, 29 | sylibd 148 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ ((*Q‘𝑦) <Q 𝑧 →
1Q <Q (𝑧 ·Q 𝑦))) |
31 | 30 | ancoms 266 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ Q ∧
𝑦 ∈ Q)
→ ((*Q‘𝑦) <Q 𝑧 →
1Q <Q (𝑧 ·Q 𝑦))) |
32 | 13, 31 | sylan 281 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ P ∧
𝑧 ∈ (2nd
‘𝐴)) ∧ 𝑦 ∈ Q) →
((*Q‘𝑦) <Q 𝑧 →
1Q <Q (𝑧 ·Q 𝑦))) |
33 | 22, 32 | syld 45 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ P ∧
𝑧 ∈ (2nd
‘𝐴)) ∧ 𝑦 ∈ Q) →
((*Q‘𝑦) ∈ (1st ‘𝐴) →
1Q <Q (𝑧 ·Q 𝑦))) |
34 | 17, 33 | anim12d 333 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ P ∧
𝑧 ∈ (2nd
‘𝐴)) ∧ 𝑦 ∈ Q) →
((𝑦
<Q 𝑞 ∧
(*Q‘𝑦) ∈ (1st ‘𝐴)) → ((𝑧 ·Q 𝑦) <Q
(𝑧
·Q 𝑞) ∧ 1Q
<Q (𝑧 ·Q 𝑦)))) |
35 | | ltsonq 7347 |
. . . . . . . . . . . . . . . 16
⊢
<Q Or Q |
36 | 35, 8 | sotri 5004 |
. . . . . . . . . . . . . . 15
⊢
((1Q <Q (𝑧
·Q 𝑦) ∧ (𝑧 ·Q 𝑦) <Q
(𝑧
·Q 𝑞)) → 1Q
<Q (𝑧 ·Q 𝑞)) |
37 | 36 | ancoms 266 |
. . . . . . . . . . . . . 14
⊢ (((𝑧
·Q 𝑦) <Q (𝑧
·Q 𝑞) ∧ 1Q
<Q (𝑧 ·Q 𝑦)) →
1Q <Q (𝑧 ·Q 𝑞)) |
38 | 34, 37 | syl6 33 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ P ∧
𝑧 ∈ (2nd
‘𝐴)) ∧ 𝑦 ∈ Q) →
((𝑦
<Q 𝑞 ∧
(*Q‘𝑦) ∈ (1st ‘𝐴)) →
1Q <Q (𝑧 ·Q 𝑞))) |
39 | 38 | exp4b 365 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ P ∧
𝑧 ∈ (2nd
‘𝐴)) → (𝑦 ∈ Q →
(𝑦
<Q 𝑞 →
((*Q‘𝑦) ∈ (1st ‘𝐴) →
1Q <Q (𝑧 ·Q 𝑞))))) |
40 | 10, 39 | syl5 32 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ P ∧
𝑧 ∈ (2nd
‘𝐴)) → (𝑦 <Q
𝑞 → (𝑦 <Q
𝑞 →
((*Q‘𝑦) ∈ (1st ‘𝐴) →
1Q <Q (𝑧 ·Q 𝑞))))) |
41 | 40 | pm2.43d 50 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ P ∧
𝑧 ∈ (2nd
‘𝐴)) → (𝑦 <Q
𝑞 →
((*Q‘𝑦) ∈ (1st ‘𝐴) →
1Q <Q (𝑧 ·Q 𝑞)))) |
42 | 41 | impd 252 |
. . . . . . . . 9
⊢ ((𝐴 ∈ P ∧
𝑧 ∈ (2nd
‘𝐴)) → ((𝑦 <Q
𝑞 ∧
(*Q‘𝑦) ∈ (1st ‘𝐴)) →
1Q <Q (𝑧 ·Q 𝑞))) |
43 | 42 | exlimdv 1812 |
. . . . . . . 8
⊢ ((𝐴 ∈ P ∧
𝑧 ∈ (2nd
‘𝐴)) →
(∃𝑦(𝑦 <Q
𝑞 ∧
(*Q‘𝑦) ∈ (1st ‘𝐴)) →
1Q <Q (𝑧 ·Q 𝑞))) |
44 | 7, 43 | syl5bi 151 |
. . . . . . 7
⊢ ((𝐴 ∈ P ∧
𝑧 ∈ (2nd
‘𝐴)) → (𝑞 ∈ (2nd
‘𝐵) →
1Q <Q (𝑧 ·Q 𝑞))) |
45 | | breq2 3991 |
. . . . . . . 8
⊢ (𝑤 = (𝑧 ·Q 𝑞) →
(1Q <Q 𝑤 ↔ 1Q
<Q (𝑧 ·Q 𝑞))) |
46 | 45 | biimprcd 159 |
. . . . . . 7
⊢
(1Q <Q (𝑧
·Q 𝑞) → (𝑤 = (𝑧 ·Q 𝑞) →
1Q <Q 𝑤)) |
47 | 44, 46 | syl6 33 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
𝑧 ∈ (2nd
‘𝐴)) → (𝑞 ∈ (2nd
‘𝐵) → (𝑤 = (𝑧 ·Q 𝑞) →
1Q <Q 𝑤))) |
48 | 47 | expimpd 361 |
. . . . 5
⊢ (𝐴 ∈ P →
((𝑧 ∈ (2nd
‘𝐴) ∧ 𝑞 ∈ (2nd
‘𝐵)) → (𝑤 = (𝑧 ·Q 𝑞) →
1Q <Q 𝑤))) |
49 | 48 | rexlimdvv 2594 |
. . . 4
⊢ (𝐴 ∈ P →
(∃𝑧 ∈
(2nd ‘𝐴)∃𝑞 ∈ (2nd ‘𝐵)𝑤 = (𝑧 ·Q 𝑞) →
1Q <Q 𝑤)) |
50 | 6, 49 | sylbid 149 |
. . 3
⊢ (𝐴 ∈ P →
(𝑤 ∈ (2nd
‘(𝐴
·P 𝐵)) → 1Q
<Q 𝑤)) |
51 | | 1pru 7505 |
. . . 4
⊢
(2nd ‘1P) = {𝑤 ∣
1Q <Q 𝑤} |
52 | 51 | abeq2i 2281 |
. . 3
⊢ (𝑤 ∈ (2nd
‘1P) ↔ 1Q
<Q 𝑤) |
53 | 50, 52 | syl6ibr 161 |
. 2
⊢ (𝐴 ∈ P →
(𝑤 ∈ (2nd
‘(𝐴
·P 𝐵)) → 𝑤 ∈ (2nd
‘1P))) |
54 | 53 | ssrdv 3153 |
1
⊢ (𝐴 ∈ P →
(2nd ‘(𝐴
·P 𝐵)) ⊆ (2nd
‘1P)) |