Step | Hyp | Ref
| Expression |
1 | | nqprlu 7467 |
. . . . . 6
⊢ (𝐴 ∈ Q →
〈{𝑙 ∣ 𝑙 <Q
𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉 ∈
P) |
2 | | nqprlu 7467 |
. . . . . 6
⊢ (𝐵 ∈ Q →
〈{𝑙 ∣ 𝑙 <Q
𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉 ∈
P) |
3 | | df-imp 7389 |
. . . . . . 7
⊢
·P = (𝑥 ∈ P, 𝑦 ∈ P ↦ 〈{𝑓 ∈ Q ∣
∃𝑔 ∈
Q ∃ℎ
∈ Q (𝑔
∈ (1st ‘𝑥) ∧ ℎ ∈ (1st ‘𝑦) ∧ 𝑓 = (𝑔 ·Q ℎ))}, {𝑓 ∈ Q ∣ ∃𝑔 ∈ Q
∃ℎ ∈
Q (𝑔 ∈
(2nd ‘𝑥)
∧ ℎ ∈
(2nd ‘𝑦)
∧ 𝑓 = (𝑔
·Q ℎ))}〉) |
4 | | mulclnq 7296 |
. . . . . . 7
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ (𝑔
·Q ℎ) ∈ Q) |
5 | 3, 4 | genpelvu 7433 |
. . . . . 6
⊢
((〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉 ∈ P
∧ 〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉 ∈ P)
→ (𝑟 ∈
(2nd ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)) ↔ ∃𝑠 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉)∃𝑡 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)𝑟 = (𝑠 ·Q 𝑡))) |
6 | 1, 2, 5 | syl2an 287 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝑟 ∈
(2nd ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)) ↔ ∃𝑠 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉)∃𝑡 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)𝑟 = (𝑠 ·Q 𝑡))) |
7 | 6 | biimpa 294 |
. . . 4
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑟 ∈
(2nd ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) → ∃𝑠 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉)∃𝑡 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)𝑟 = (𝑠 ·Q 𝑡)) |
8 | | vex 2715 |
. . . . . . . . . . . . 13
⊢ 𝑠 ∈ V |
9 | | breq2 3969 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑠 → (𝐴 <Q 𝑢 ↔ 𝐴 <Q 𝑠)) |
10 | | ltnqex 7469 |
. . . . . . . . . . . . . 14
⊢ {𝑙 ∣ 𝑙 <Q 𝐴} ∈ V |
11 | | gtnqex 7470 |
. . . . . . . . . . . . . 14
⊢ {𝑢 ∣ 𝐴 <Q 𝑢} ∈ V |
12 | 10, 11 | op2nd 6095 |
. . . . . . . . . . . . 13
⊢
(2nd ‘〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) = {𝑢 ∣ 𝐴 <Q 𝑢} |
13 | 8, 9, 12 | elab2 2860 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ↔ 𝐴 <Q
𝑠) |
14 | 13 | biimpi 119 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) → 𝐴 <Q
𝑠) |
15 | 14 | ad2antrl 482 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑟 ∈
(2nd ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ (𝑠 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ∧ 𝑡 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) → 𝐴 <Q
𝑠) |
16 | 15 | adantr 274 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
Q ∧ 𝐵
∈ Q) ∧ 𝑟 ∈ (2nd ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ (𝑠 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ∧ 𝑡 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ 𝑟 = (𝑠 ·Q 𝑡)) → 𝐴 <Q 𝑠) |
17 | | vex 2715 |
. . . . . . . . . . . . 13
⊢ 𝑡 ∈ V |
18 | | breq2 3969 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑡 → (𝐵 <Q 𝑢 ↔ 𝐵 <Q 𝑡)) |
19 | | ltnqex 7469 |
. . . . . . . . . . . . . 14
⊢ {𝑙 ∣ 𝑙 <Q 𝐵} ∈ V |
20 | | gtnqex 7470 |
. . . . . . . . . . . . . 14
⊢ {𝑢 ∣ 𝐵 <Q 𝑢} ∈ V |
21 | 19, 20 | op2nd 6095 |
. . . . . . . . . . . . 13
⊢
(2nd ‘〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉) = {𝑢 ∣ 𝐵 <Q 𝑢} |
22 | 17, 18, 21 | elab2 2860 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉) ↔ 𝐵 <Q
𝑡) |
23 | 22 | biimpi 119 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉) → 𝐵 <Q
𝑡) |
24 | 23 | ad2antll 483 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑟 ∈
(2nd ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ (𝑠 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ∧ 𝑡 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) → 𝐵 <Q
𝑡) |
25 | 24 | adantr 274 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
Q ∧ 𝐵
∈ Q) ∧ 𝑟 ∈ (2nd ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ (𝑠 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ∧ 𝑡 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ 𝑟 = (𝑠 ·Q 𝑡)) → 𝐵 <Q 𝑡) |
26 | | ltrelnq 7285 |
. . . . . . . . . . . 12
⊢
<Q ⊆ (Q ×
Q) |
27 | 26 | brel 4638 |
. . . . . . . . . . 11
⊢ (𝐴 <Q
𝑠 → (𝐴 ∈ Q ∧ 𝑠 ∈
Q)) |
28 | 16, 27 | syl 14 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
Q ∧ 𝐵
∈ Q) ∧ 𝑟 ∈ (2nd ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ (𝑠 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ∧ 𝑡 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ 𝑟 = (𝑠 ·Q 𝑡)) → (𝐴 ∈ Q ∧ 𝑠 ∈
Q)) |
29 | 26 | brel 4638 |
. . . . . . . . . . 11
⊢ (𝐵 <Q
𝑡 → (𝐵 ∈ Q ∧ 𝑡 ∈
Q)) |
30 | 25, 29 | syl 14 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
Q ∧ 𝐵
∈ Q) ∧ 𝑟 ∈ (2nd ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ (𝑠 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ∧ 𝑡 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ 𝑟 = (𝑠 ·Q 𝑡)) → (𝐵 ∈ Q ∧ 𝑡 ∈
Q)) |
31 | | lt2mulnq 7325 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Q ∧
𝑠 ∈ Q)
∧ (𝐵 ∈
Q ∧ 𝑡
∈ Q)) → ((𝐴 <Q 𝑠 ∧ 𝐵 <Q 𝑡) → (𝐴 ·Q 𝐵) <Q
(𝑠
·Q 𝑡))) |
32 | 28, 30, 31 | syl2anc 409 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
Q ∧ 𝐵
∈ Q) ∧ 𝑟 ∈ (2nd ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ (𝑠 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ∧ 𝑡 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ 𝑟 = (𝑠 ·Q 𝑡)) → ((𝐴 <Q 𝑠 ∧ 𝐵 <Q 𝑡) → (𝐴 ·Q 𝐵) <Q
(𝑠
·Q 𝑡))) |
33 | 16, 25, 32 | mp2and 430 |
. . . . . . . 8
⊢
(((((𝐴 ∈
Q ∧ 𝐵
∈ Q) ∧ 𝑟 ∈ (2nd ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ (𝑠 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ∧ 𝑡 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ 𝑟 = (𝑠 ·Q 𝑡)) → (𝐴 ·Q 𝐵) <Q
(𝑠
·Q 𝑡)) |
34 | | breq2 3969 |
. . . . . . . . 9
⊢ (𝑟 = (𝑠 ·Q 𝑡) → ((𝐴 ·Q 𝐵) <Q
𝑟 ↔ (𝐴 ·Q 𝐵) <Q
(𝑠
·Q 𝑡))) |
35 | 34 | adantl 275 |
. . . . . . . 8
⊢
(((((𝐴 ∈
Q ∧ 𝐵
∈ Q) ∧ 𝑟 ∈ (2nd ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ (𝑠 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ∧ 𝑡 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ 𝑟 = (𝑠 ·Q 𝑡)) → ((𝐴 ·Q 𝐵) <Q
𝑟 ↔ (𝐴 ·Q 𝐵) <Q
(𝑠
·Q 𝑡))) |
36 | 33, 35 | mpbird 166 |
. . . . . . 7
⊢
(((((𝐴 ∈
Q ∧ 𝐵
∈ Q) ∧ 𝑟 ∈ (2nd ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ (𝑠 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ∧ 𝑡 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ 𝑟 = (𝑠 ·Q 𝑡)) → (𝐴 ·Q 𝐵) <Q
𝑟) |
37 | | vex 2715 |
. . . . . . . 8
⊢ 𝑟 ∈ V |
38 | | breq2 3969 |
. . . . . . . 8
⊢ (𝑢 = 𝑟 → ((𝐴 ·Q 𝐵) <Q
𝑢 ↔ (𝐴 ·Q 𝐵) <Q
𝑟)) |
39 | | ltnqex 7469 |
. . . . . . . . 9
⊢ {𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)} ∈ V |
40 | | gtnqex 7470 |
. . . . . . . . 9
⊢ {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢} ∈
V |
41 | 39, 40 | op2nd 6095 |
. . . . . . . 8
⊢
(2nd ‘〈{𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉) = {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢} |
42 | 37, 38, 41 | elab2 2860 |
. . . . . . 7
⊢ (𝑟 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q (𝐴 ·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉) ↔ (𝐴
·Q 𝐵) <Q 𝑟) |
43 | 36, 42 | sylibr 133 |
. . . . . 6
⊢
(((((𝐴 ∈
Q ∧ 𝐵
∈ Q) ∧ 𝑟 ∈ (2nd ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ (𝑠 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ∧ 𝑡 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ 𝑟 = (𝑠 ·Q 𝑡)) → 𝑟 ∈ (2nd ‘〈{𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉)) |
44 | 43 | ex 114 |
. . . . 5
⊢ ((((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑟 ∈
(2nd ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) ∧ (𝑠 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ∧ 𝑡 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) → (𝑟 = (𝑠 ·Q 𝑡) → 𝑟 ∈ (2nd ‘〈{𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉))) |
45 | 44 | rexlimdvva 2582 |
. . . 4
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑟 ∈
(2nd ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) → (∃𝑠 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉)∃𝑡 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)𝑟 = (𝑠 ·Q 𝑡) → 𝑟 ∈ (2nd ‘〈{𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉))) |
46 | 7, 45 | mpd 13 |
. . 3
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ Q)
∧ 𝑟 ∈
(2nd ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉))) → 𝑟 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q (𝐴 ·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉)) |
47 | 46 | ex 114 |
. 2
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝑟 ∈
(2nd ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)) → 𝑟 ∈ (2nd
‘〈{𝑙 ∣
𝑙
<Q (𝐴 ·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉))) |
48 | 47 | ssrdv 3134 |
1
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (2nd ‘(〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉
·P 〈{𝑙 ∣ 𝑙 <Q 𝐵}, {𝑢 ∣ 𝐵 <Q 𝑢}〉)) ⊆
(2nd ‘〈{𝑙 ∣ 𝑙 <Q (𝐴
·Q 𝐵)}, {𝑢 ∣ (𝐴 ·Q 𝐵) <Q
𝑢}〉)) |