Step | Hyp | Ref
| Expression |
1 | | recexpr.1 |
. . . . . 6
⊢ B = 〈{x
∣ ∃y(x
<Q y ∧ (*Q‘y) ∈
(2nd ‘A))}, {x ∣ ∃y(y <Q x ∧
(*Q‘y) ∈ (1st ‘A))}〉 |
2 | 1 | recexprlempr 6604 |
. . . . 5
⊢ (A ∈
P → B ∈ P) |
3 | | df-imp 6452 |
. . . . . 6
⊢
·P = (y
∈ P, w ∈
P ↦ 〈{u ∈ Q ∣ ∃f ∈ Q ∃g ∈ Q (f ∈
(1st ‘y) ∧ g ∈ (1st ‘w) ∧ u = (f
·Q g))},
{u ∈
Q ∣ ∃f ∈
Q ∃g ∈
Q (f ∈ (2nd ‘y) ∧ g ∈
(2nd ‘w) ∧ u = (f ·Q g))}〉) |
4 | | mulclnq 6360 |
. . . . . 6
⊢
((f ∈ Q ∧ g ∈ Q) → (f ·Q g) ∈
Q) |
5 | 3, 4 | genpelvl 6495 |
. . . . 5
⊢
((A ∈ P ∧ B ∈ P) → (w ∈
(1st ‘(A
·P B))
↔ ∃z ∈
(1st ‘A)∃𝑞 ∈
(1st ‘B)w = (z
·Q 𝑞))) |
6 | 2, 5 | mpdan 398 |
. . . 4
⊢ (A ∈
P → (w ∈ (1st ‘(A ·P B)) ↔ ∃z ∈ (1st ‘A)∃𝑞 ∈ (1st ‘B)w = (z ·Q 𝑞))) |
7 | 1 | recexprlemell 6594 |
. . . . . . . 8
⊢ (𝑞 ∈ (1st ‘B) ↔ ∃y(𝑞 <Q
y ∧
(*Q‘y) ∈ (2nd ‘A))) |
8 | | ltrelnq 6349 |
. . . . . . . . . . . . . 14
⊢
<Q ⊆ (Q ×
Q) |
9 | 8 | brel 4335 |
. . . . . . . . . . . . 13
⊢ (𝑞 <Q
y → (𝑞 ∈
Q ∧ y ∈
Q)) |
10 | 9 | simprd 107 |
. . . . . . . . . . . 12
⊢ (𝑞 <Q
y → y ∈
Q) |
11 | | prop 6458 |
. . . . . . . . . . . . . . . . . 18
⊢ (A ∈
P → 〈(1st ‘A), (2nd ‘A)〉 ∈
P) |
12 | | elprnql 6464 |
. . . . . . . . . . . . . . . . . 18
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ z ∈ (1st ‘A)) → z
∈ Q) |
13 | 11, 12 | sylan 267 |
. . . . . . . . . . . . . . . . 17
⊢
((A ∈ P ∧ z ∈ (1st ‘A)) → z
∈ Q) |
14 | | ltmnqi 6387 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑞 <Q
y ∧
z ∈
Q) → (z
·Q 𝑞) <Q (z ·Q y)) |
15 | 14 | expcom 109 |
. . . . . . . . . . . . . . . . 17
⊢ (z ∈
Q → (𝑞
<Q y →
(z ·Q 𝑞) <Q
(z ·Q
y))) |
16 | 13, 15 | syl 14 |
. . . . . . . . . . . . . . . 16
⊢
((A ∈ P ∧ z ∈ (1st ‘A)) → (𝑞 <Q y → (z
·Q 𝑞) <Q (z ·Q y))) |
17 | 16 | adantr 261 |
. . . . . . . . . . . . . . 15
⊢
(((A ∈ P ∧ z ∈ (1st ‘A)) ∧ y ∈
Q) → (𝑞
<Q y →
(z ·Q 𝑞) <Q
(z ·Q
y))) |
18 | | prltlu 6470 |
. . . . . . . . . . . . . . . . . . 19
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ z ∈ (1st ‘A) ∧
(*Q‘y) ∈ (2nd ‘A)) → z
<Q (*Q‘y)) |
19 | 11, 18 | syl3an1 1167 |
. . . . . . . . . . . . . . . . . 18
⊢
((A ∈ P ∧ z ∈ (1st ‘A) ∧
(*Q‘y) ∈ (2nd ‘A)) → z
<Q (*Q‘y)) |
20 | 19 | 3expia 1105 |
. . . . . . . . . . . . . . . . 17
⊢
((A ∈ P ∧ z ∈ (1st ‘A)) →
((*Q‘y)
∈ (2nd ‘A) → z
<Q (*Q‘y))) |
21 | 20 | adantr 261 |
. . . . . . . . . . . . . . . 16
⊢
(((A ∈ P ∧ z ∈ (1st ‘A)) ∧ y ∈
Q) → ((*Q‘y) ∈
(2nd ‘A) → z <Q
(*Q‘y))) |
22 | | ltmnqi 6387 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((z <Q
(*Q‘y) ∧ y ∈ Q) → (y ·Q z) <Q (y ·Q
(*Q‘y))) |
23 | 22 | expcom 109 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (y ∈
Q → (z
<Q (*Q‘y) → (y
·Q z)
<Q (y
·Q (*Q‘y)))) |
24 | 23 | adantr 261 |
. . . . . . . . . . . . . . . . . . 19
⊢
((y ∈ Q ∧ z ∈ Q) → (z <Q
(*Q‘y)
→ (y
·Q z)
<Q (y
·Q (*Q‘y)))) |
25 | | mulcomnqg 6367 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((y ∈ Q ∧ z ∈ Q) → (y ·Q z) = (z
·Q y)) |
26 | | recidnq 6377 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (y ∈
Q → (y
·Q (*Q‘y)) = 1Q) |
27 | 26 | adantr 261 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((y ∈ Q ∧ z ∈ Q) → (y ·Q
(*Q‘y)) =
1Q) |
28 | 25, 27 | breq12d 3768 |
. . . . . . . . . . . . . . . . . . 19
⊢
((y ∈ Q ∧ z ∈ Q) → ((y ·Q z) <Q (y ·Q
(*Q‘y))
↔ (z
·Q y)
<Q 1Q)) |
29 | 24, 28 | sylibd 138 |
. . . . . . . . . . . . . . . . . 18
⊢
((y ∈ Q ∧ z ∈ Q) → (z <Q
(*Q‘y)
→ (z
·Q y)
<Q 1Q)) |
30 | 29 | ancoms 255 |
. . . . . . . . . . . . . . . . 17
⊢
((z ∈ Q ∧ y ∈ Q) → (z <Q
(*Q‘y)
→ (z
·Q y)
<Q 1Q)) |
31 | 13, 30 | sylan 267 |
. . . . . . . . . . . . . . . 16
⊢
(((A ∈ P ∧ z ∈ (1st ‘A)) ∧ y ∈
Q) → (z
<Q (*Q‘y) → (z
·Q y)
<Q 1Q)) |
32 | 21, 31 | syld 40 |
. . . . . . . . . . . . . . 15
⊢
(((A ∈ P ∧ z ∈ (1st ‘A)) ∧ y ∈
Q) → ((*Q‘y) ∈
(2nd ‘A) → (z ·Q y) <Q
1Q)) |
33 | 17, 32 | anim12d 318 |
. . . . . . . . . . . . . 14
⊢
(((A ∈ P ∧ z ∈ (1st ‘A)) ∧ y ∈
Q) → ((𝑞
<Q y ∧ (*Q‘y) ∈
(2nd ‘A)) →
((z ·Q
𝑞)
<Q (z
·Q y) ∧ (z
·Q y)
<Q 1Q))) |
34 | | ltsonq 6382 |
. . . . . . . . . . . . . . 15
⊢
<Q Or Q |
35 | 34, 8 | sotri 4663 |
. . . . . . . . . . . . . 14
⊢
(((z
·Q 𝑞) <Q (z ·Q y) ∧ (z ·Q y) <Q
1Q) → (z
·Q 𝑞) <Q
1Q) |
36 | 33, 35 | syl6 29 |
. . . . . . . . . . . . 13
⊢
(((A ∈ P ∧ z ∈ (1st ‘A)) ∧ y ∈
Q) → ((𝑞
<Q y ∧ (*Q‘y) ∈
(2nd ‘A)) → (z ·Q 𝑞) <Q
1Q)) |
37 | 36 | exp4b 349 |
. . . . . . . . . . . 12
⊢
((A ∈ P ∧ z ∈ (1st ‘A)) → (y
∈ Q → (𝑞 <Q y →
((*Q‘y)
∈ (2nd ‘A) → (z
·Q 𝑞) <Q
1Q)))) |
38 | 10, 37 | syl5 28 |
. . . . . . . . . . 11
⊢
((A ∈ P ∧ z ∈ (1st ‘A)) → (𝑞 <Q y → (𝑞 <Q y →
((*Q‘y)
∈ (2nd ‘A) → (z
·Q 𝑞) <Q
1Q)))) |
39 | 38 | pm2.43d 44 |
. . . . . . . . . 10
⊢
((A ∈ P ∧ z ∈ (1st ‘A)) → (𝑞 <Q y →
((*Q‘y)
∈ (2nd ‘A) → (z
·Q 𝑞) <Q
1Q))) |
40 | 39 | impd 242 |
. . . . . . . . 9
⊢
((A ∈ P ∧ z ∈ (1st ‘A)) → ((𝑞 <Q y ∧
(*Q‘y) ∈ (2nd ‘A)) → (z
·Q 𝑞) <Q
1Q)) |
41 | 40 | exlimdv 1697 |
. . . . . . . 8
⊢
((A ∈ P ∧ z ∈ (1st ‘A)) → (∃y(𝑞 <Q
y ∧
(*Q‘y) ∈ (2nd ‘A)) → (z
·Q 𝑞) <Q
1Q)) |
42 | 7, 41 | syl5bi 141 |
. . . . . . 7
⊢
((A ∈ P ∧ z ∈ (1st ‘A)) → (𝑞 ∈
(1st ‘B) → (z ·Q 𝑞) <Q
1Q)) |
43 | | breq1 3758 |
. . . . . . . 8
⊢ (w = (z
·Q 𝑞) → (w <Q
1Q ↔ (z
·Q 𝑞) <Q
1Q)) |
44 | 43 | biimprcd 149 |
. . . . . . 7
⊢
((z
·Q 𝑞) <Q
1Q → (w =
(z ·Q 𝑞) → w <Q
1Q)) |
45 | 42, 44 | syl6 29 |
. . . . . 6
⊢
((A ∈ P ∧ z ∈ (1st ‘A)) → (𝑞 ∈
(1st ‘B) → (w = (z
·Q 𝑞) → w <Q
1Q))) |
46 | 45 | expimpd 345 |
. . . . 5
⊢ (A ∈
P → ((z ∈ (1st ‘A) ∧ 𝑞 ∈ (1st ‘B)) → (w =
(z ·Q 𝑞) → w <Q
1Q))) |
47 | 46 | rexlimdvv 2433 |
. . . 4
⊢ (A ∈
P → (∃z ∈
(1st ‘A)∃𝑞 ∈
(1st ‘B)w = (z
·Q 𝑞) → w <Q
1Q)) |
48 | 6, 47 | sylbid 139 |
. . 3
⊢ (A ∈
P → (w ∈ (1st ‘(A ·P B)) → w
<Q 1Q)) |
49 | | 1prl 6536 |
. . . 4
⊢
(1st ‘1P) = {w ∣ w
<Q 1Q} |
50 | 49 | abeq2i 2145 |
. . 3
⊢ (w ∈
(1st ‘1P) ↔ w <Q
1Q) |
51 | 48, 50 | syl6ibr 151 |
. 2
⊢ (A ∈
P → (w ∈ (1st ‘(A ·P B)) → w
∈ (1st
‘1P))) |
52 | 51 | ssrdv 2945 |
1
⊢ (A ∈
P → (1st ‘(A ·P B)) ⊆ (1st
‘1P)) |