Step | Hyp | Ref
| Expression |
1 | | df-1p 10202 |
. . . 4
⊢
1P = {𝑤 ∣ 𝑤 <Q
1Q} |
2 | 1 | abeq2i 2900 |
. . 3
⊢ (𝑤 ∈
1P ↔ 𝑤 <Q
1Q) |
3 | | ltrnq 10199 |
. . . . . . 7
⊢ (𝑤 <Q
1Q ↔
(*Q‘1Q)
<Q (*Q‘𝑤)) |
4 | | mulcomnq 10173 |
. . . . . . . . 9
⊢
((*Q‘1Q)
·Q 1Q) =
(1Q ·Q
(*Q‘1Q)) |
5 | | 1nq 10148 |
. . . . . . . . . 10
⊢
1Q ∈ Q |
6 | | recclnq 10186 |
. . . . . . . . . 10
⊢
(1Q ∈ Q →
(*Q‘1Q) ∈
Q) |
7 | | mulidnq 10183 |
. . . . . . . . . 10
⊢
((*Q‘1Q) ∈
Q →
((*Q‘1Q)
·Q 1Q) =
(*Q‘1Q)) |
8 | 5, 6, 7 | mp2b 10 |
. . . . . . . . 9
⊢
((*Q‘1Q)
·Q 1Q) =
(*Q‘1Q) |
9 | | recidnq 10185 |
. . . . . . . . . 10
⊢
(1Q ∈ Q →
(1Q ·Q
(*Q‘1Q)) =
1Q) |
10 | 5, 9 | ax-mp 5 |
. . . . . . . . 9
⊢
(1Q ·Q
(*Q‘1Q)) =
1Q |
11 | 4, 8, 10 | 3eqtr3i 2810 |
. . . . . . . 8
⊢
(*Q‘1Q) =
1Q |
12 | 11 | breq1i 4936 |
. . . . . . 7
⊢
((*Q‘1Q)
<Q (*Q‘𝑤) ↔
1Q <Q
(*Q‘𝑤)) |
13 | 3, 12 | bitri 267 |
. . . . . 6
⊢ (𝑤 <Q
1Q ↔ 1Q
<Q (*Q‘𝑤)) |
14 | | prlem936 10267 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
1Q <Q
(*Q‘𝑤)) → ∃𝑣 ∈ 𝐴 ¬ (𝑣 ·Q
(*Q‘𝑤)) ∈ 𝐴) |
15 | 13, 14 | sylan2b 584 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝑤
<Q 1Q) → ∃𝑣 ∈ 𝐴 ¬ (𝑣 ·Q
(*Q‘𝑤)) ∈ 𝐴) |
16 | | prnmax 10215 |
. . . . . . 7
⊢ ((𝐴 ∈ P ∧
𝑣 ∈ 𝐴) → ∃𝑧 ∈ 𝐴 𝑣 <Q 𝑧) |
17 | 16 | ad2ant2r 734 |
. . . . . 6
⊢ (((𝐴 ∈ P ∧
𝑤
<Q 1Q) ∧ (𝑣 ∈ 𝐴 ∧ ¬ (𝑣 ·Q
(*Q‘𝑤)) ∈ 𝐴)) → ∃𝑧 ∈ 𝐴 𝑣 <Q 𝑧) |
18 | | elprnq 10211 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ P ∧
𝑣 ∈ 𝐴) → 𝑣 ∈ Q) |
19 | 18 | ad2ant2r 734 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ P ∧
𝑤
<Q 1Q) ∧ (𝑣 ∈ 𝐴 ∧ ¬ (𝑣 ·Q
(*Q‘𝑤)) ∈ 𝐴)) → 𝑣 ∈ Q) |
20 | 19 | 3adant3 1112 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ P ∧
𝑤
<Q 1Q) ∧ (𝑣 ∈ 𝐴 ∧ ¬ (𝑣 ·Q
(*Q‘𝑤)) ∈ 𝐴) ∧ 𝑣 <Q 𝑧) → 𝑣 ∈ Q) |
21 | | simp1r 1178 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ P ∧
𝑤
<Q 1Q) ∧ (𝑣 ∈ 𝐴 ∧ ¬ (𝑣 ·Q
(*Q‘𝑤)) ∈ 𝐴) ∧ 𝑣 <Q 𝑧) → 𝑤 <Q
1Q) |
22 | | ltrelnq 10146 |
. . . . . . . . . . . . . 14
⊢
<Q ⊆ (Q ×
Q) |
23 | 22 | brel 5467 |
. . . . . . . . . . . . 13
⊢ (𝑤 <Q
1Q → (𝑤 ∈ Q ∧
1Q ∈ Q)) |
24 | 23 | simpld 487 |
. . . . . . . . . . . 12
⊢ (𝑤 <Q
1Q → 𝑤 ∈ Q) |
25 | 21, 24 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ P ∧
𝑤
<Q 1Q) ∧ (𝑣 ∈ 𝐴 ∧ ¬ (𝑣 ·Q
(*Q‘𝑤)) ∈ 𝐴) ∧ 𝑣 <Q 𝑧) → 𝑤 ∈ Q) |
26 | | simp3 1118 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ P ∧
𝑤
<Q 1Q) ∧ (𝑣 ∈ 𝐴 ∧ ¬ (𝑣 ·Q
(*Q‘𝑤)) ∈ 𝐴) ∧ 𝑣 <Q 𝑧) → 𝑣 <Q 𝑧) |
27 | | simp2r 1180 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ P ∧
𝑤
<Q 1Q) ∧ (𝑣 ∈ 𝐴 ∧ ¬ (𝑣 ·Q
(*Q‘𝑤)) ∈ 𝐴) ∧ 𝑣 <Q 𝑧) → ¬ (𝑣
·Q (*Q‘𝑤)) ∈ 𝐴) |
28 | | ltrnq 10199 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 <Q
𝑧 ↔
(*Q‘𝑧) <Q
(*Q‘𝑣)) |
29 | | fvex 6512 |
. . . . . . . . . . . . . . . . . 18
⊢
(*Q‘𝑧) ∈ V |
30 | | fvex 6512 |
. . . . . . . . . . . . . . . . . 18
⊢
(*Q‘𝑣) ∈ V |
31 | | ltmnq 10192 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ Q →
(𝑥
<Q 𝑦 ↔ (𝑢 ·Q 𝑥) <Q
(𝑢
·Q 𝑦))) |
32 | | vex 3418 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑤 ∈ V |
33 | | mulcomnq 10173 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥
·Q 𝑦) = (𝑦 ·Q 𝑥) |
34 | 29, 30, 31, 32, 33 | caovord2 7176 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ Q →
((*Q‘𝑧) <Q
(*Q‘𝑣) ↔
((*Q‘𝑧) ·Q 𝑤) <Q
((*Q‘𝑣) ·Q 𝑤))) |
35 | 28, 34 | syl5bb 275 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ Q →
(𝑣
<Q 𝑧 ↔
((*Q‘𝑧) ·Q 𝑤) <Q
((*Q‘𝑣) ·Q 𝑤))) |
36 | 35 | adantl 474 |
. . . . . . . . . . . . . . 15
⊢ ((𝑣 ∈ Q ∧
𝑤 ∈ Q)
→ (𝑣
<Q 𝑧 ↔
((*Q‘𝑧) ·Q 𝑤) <Q
((*Q‘𝑣) ·Q 𝑤))) |
37 | 36 | biimpd 221 |
. . . . . . . . . . . . . 14
⊢ ((𝑣 ∈ Q ∧
𝑤 ∈ Q)
→ (𝑣
<Q 𝑧 →
((*Q‘𝑧) ·Q 𝑤) <Q
((*Q‘𝑣) ·Q 𝑤))) |
38 | | mulcomnq 10173 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣
·Q (*Q‘𝑣)) =
((*Q‘𝑣) ·Q 𝑣) |
39 | | recidnq 10185 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 ∈ Q →
(𝑣
·Q (*Q‘𝑣)) =
1Q) |
40 | 38, 39 | syl5eqr 2828 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 ∈ Q →
((*Q‘𝑣) ·Q 𝑣) =
1Q) |
41 | | recidnq 10185 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ Q →
(𝑤
·Q (*Q‘𝑤)) =
1Q) |
42 | 40, 41 | oveqan12d 6995 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑣 ∈ Q ∧
𝑤 ∈ Q)
→ (((*Q‘𝑣) ·Q 𝑣)
·Q (𝑤 ·Q
(*Q‘𝑤))) = (1Q
·Q
1Q)) |
43 | | vex 3418 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑣 ∈ V |
44 | | mulassnq 10179 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥
·Q 𝑦) ·Q 𝑢) = (𝑥 ·Q (𝑦
·Q 𝑢)) |
45 | | fvex 6512 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(*Q‘𝑤) ∈ V |
46 | 30, 43, 32, 33, 44, 45 | caov4 7195 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((*Q‘𝑣) ·Q 𝑣)
·Q (𝑤 ·Q
(*Q‘𝑤))) =
(((*Q‘𝑣) ·Q 𝑤)
·Q (𝑣 ·Q
(*Q‘𝑤))) |
47 | | mulidnq 10183 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(1Q ∈ Q →
(1Q ·Q
1Q) = 1Q) |
48 | 5, 47 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
(1Q ·Q
1Q) = 1Q |
49 | 42, 46, 48 | 3eqtr3g 2837 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑣 ∈ Q ∧
𝑤 ∈ Q)
→ (((*Q‘𝑣) ·Q 𝑤)
·Q (𝑣 ·Q
(*Q‘𝑤))) =
1Q) |
50 | | recclnq 10186 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 ∈ Q →
(*Q‘𝑣) ∈ Q) |
51 | | mulclnq 10167 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((*Q‘𝑣) ∈ Q ∧ 𝑤 ∈ Q) →
((*Q‘𝑣) ·Q 𝑤) ∈
Q) |
52 | 50, 51 | sylan 572 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑣 ∈ Q ∧
𝑤 ∈ Q)
→ ((*Q‘𝑣) ·Q 𝑤) ∈
Q) |
53 | | recmulnq 10184 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((*Q‘𝑣) ·Q 𝑤) ∈ Q →
((*Q‘((*Q‘𝑣)
·Q 𝑤)) = (𝑣 ·Q
(*Q‘𝑤)) ↔
(((*Q‘𝑣) ·Q 𝑤)
·Q (𝑣 ·Q
(*Q‘𝑤))) =
1Q)) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑣 ∈ Q ∧
𝑤 ∈ Q)
→
((*Q‘((*Q‘𝑣)
·Q 𝑤)) = (𝑣 ·Q
(*Q‘𝑤)) ↔
(((*Q‘𝑣) ·Q 𝑤)
·Q (𝑣 ·Q
(*Q‘𝑤))) =
1Q)) |
55 | 49, 54 | mpbird 249 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ Q ∧
𝑤 ∈ Q)
→
(*Q‘((*Q‘𝑣)
·Q 𝑤)) = (𝑣 ·Q
(*Q‘𝑤))) |
56 | 55 | eleq1d 2850 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ Q ∧
𝑤 ∈ Q)
→
((*Q‘((*Q‘𝑣)
·Q 𝑤)) ∈ 𝐴 ↔ (𝑣 ·Q
(*Q‘𝑤)) ∈ 𝐴)) |
57 | 56 | notbid 310 |
. . . . . . . . . . . . . . 15
⊢ ((𝑣 ∈ Q ∧
𝑤 ∈ Q)
→ (¬
(*Q‘((*Q‘𝑣)
·Q 𝑤)) ∈ 𝐴 ↔ ¬ (𝑣 ·Q
(*Q‘𝑤)) ∈ 𝐴)) |
58 | 57 | biimprd 240 |
. . . . . . . . . . . . . 14
⊢ ((𝑣 ∈ Q ∧
𝑤 ∈ Q)
→ (¬ (𝑣
·Q (*Q‘𝑤)) ∈ 𝐴 → ¬
(*Q‘((*Q‘𝑣)
·Q 𝑤)) ∈ 𝐴)) |
59 | 37, 58 | anim12d 599 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∈ Q ∧
𝑤 ∈ Q)
→ ((𝑣
<Q 𝑧 ∧ ¬ (𝑣 ·Q
(*Q‘𝑤)) ∈ 𝐴) →
(((*Q‘𝑧) ·Q 𝑤) <Q
((*Q‘𝑣) ·Q 𝑤) ∧ ¬
(*Q‘((*Q‘𝑣)
·Q 𝑤)) ∈ 𝐴))) |
60 | | ovex 7008 |
. . . . . . . . . . . . . . 15
⊢
((*Q‘𝑣) ·Q 𝑤) ∈ V |
61 | | breq2 4933 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 =
((*Q‘𝑣) ·Q 𝑤) →
(((*Q‘𝑧) ·Q 𝑤) <Q
𝑦 ↔
((*Q‘𝑧) ·Q 𝑤) <Q
((*Q‘𝑣) ·Q 𝑤))) |
62 | | fveq2 6499 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 =
((*Q‘𝑣) ·Q 𝑤) →
(*Q‘𝑦) =
(*Q‘((*Q‘𝑣)
·Q 𝑤))) |
63 | 62 | eleq1d 2850 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 =
((*Q‘𝑣) ·Q 𝑤) →
((*Q‘𝑦) ∈ 𝐴 ↔
(*Q‘((*Q‘𝑣)
·Q 𝑤)) ∈ 𝐴)) |
64 | 63 | notbid 310 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 =
((*Q‘𝑣) ·Q 𝑤) → (¬
(*Q‘𝑦) ∈ 𝐴 ↔ ¬
(*Q‘((*Q‘𝑣)
·Q 𝑤)) ∈ 𝐴)) |
65 | 61, 64 | anbi12d 621 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 =
((*Q‘𝑣) ·Q 𝑤) →
((((*Q‘𝑧) ·Q 𝑤) <Q
𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴) ↔
(((*Q‘𝑧) ·Q 𝑤) <Q
((*Q‘𝑣) ·Q 𝑤) ∧ ¬
(*Q‘((*Q‘𝑣)
·Q 𝑤)) ∈ 𝐴))) |
66 | 60, 65 | spcev 3525 |
. . . . . . . . . . . . . 14
⊢
((((*Q‘𝑧) ·Q 𝑤) <Q
((*Q‘𝑣) ·Q 𝑤) ∧ ¬
(*Q‘((*Q‘𝑣)
·Q 𝑤)) ∈ 𝐴) → ∃𝑦(((*Q‘𝑧)
·Q 𝑤) <Q 𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴)) |
67 | | ovex 7008 |
. . . . . . . . . . . . . . 15
⊢
((*Q‘𝑧) ·Q 𝑤) ∈ V |
68 | | breq1 4932 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 =
((*Q‘𝑧) ·Q 𝑤) → (𝑥 <Q 𝑦 ↔
((*Q‘𝑧) ·Q 𝑤) <Q
𝑦)) |
69 | 68 | anbi1d 620 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 =
((*Q‘𝑧) ·Q 𝑤) → ((𝑥 <Q 𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴) ↔
(((*Q‘𝑧) ·Q 𝑤) <Q
𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴))) |
70 | 69 | exbidv 1880 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 =
((*Q‘𝑧) ·Q 𝑤) → (∃𝑦(𝑥 <Q 𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴) ↔ ∃𝑦(((*Q‘𝑧)
·Q 𝑤) <Q 𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴))) |
71 | | reclempr.1 |
. . . . . . . . . . . . . . 15
⊢ 𝐵 = {𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴)} |
72 | 67, 70, 71 | elab2 3585 |
. . . . . . . . . . . . . 14
⊢
(((*Q‘𝑧) ·Q 𝑤) ∈ 𝐵 ↔ ∃𝑦(((*Q‘𝑧)
·Q 𝑤) <Q 𝑦 ∧ ¬
(*Q‘𝑦) ∈ 𝐴)) |
73 | 66, 72 | sylibr 226 |
. . . . . . . . . . . . 13
⊢
((((*Q‘𝑧) ·Q 𝑤) <Q
((*Q‘𝑣) ·Q 𝑤) ∧ ¬
(*Q‘((*Q‘𝑣)
·Q 𝑤)) ∈ 𝐴) →
((*Q‘𝑧) ·Q 𝑤) ∈ 𝐵) |
74 | 59, 73 | syl6 35 |
. . . . . . . . . . . 12
⊢ ((𝑣 ∈ Q ∧
𝑤 ∈ Q)
→ ((𝑣
<Q 𝑧 ∧ ¬ (𝑣 ·Q
(*Q‘𝑤)) ∈ 𝐴) →
((*Q‘𝑧) ·Q 𝑤) ∈ 𝐵)) |
75 | 74 | imp 398 |
. . . . . . . . . . 11
⊢ (((𝑣 ∈ Q ∧
𝑤 ∈ Q)
∧ (𝑣
<Q 𝑧 ∧ ¬ (𝑣 ·Q
(*Q‘𝑤)) ∈ 𝐴)) →
((*Q‘𝑧) ·Q 𝑤) ∈ 𝐵) |
76 | 20, 25, 26, 27, 75 | syl22anc 826 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ P ∧
𝑤
<Q 1Q) ∧ (𝑣 ∈ 𝐴 ∧ ¬ (𝑣 ·Q
(*Q‘𝑤)) ∈ 𝐴) ∧ 𝑣 <Q 𝑧) →
((*Q‘𝑧) ·Q 𝑤) ∈ 𝐵) |
77 | 22 | brel 5467 |
. . . . . . . . . . . . 13
⊢ (𝑣 <Q
𝑧 → (𝑣 ∈ Q ∧
𝑧 ∈
Q)) |
78 | 77 | simprd 488 |
. . . . . . . . . . . 12
⊢ (𝑣 <Q
𝑧 → 𝑧 ∈ Q) |
79 | 78 | 3ad2ant3 1115 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ P ∧
𝑤
<Q 1Q) ∧ (𝑣 ∈ 𝐴 ∧ ¬ (𝑣 ·Q
(*Q‘𝑤)) ∈ 𝐴) ∧ 𝑣 <Q 𝑧) → 𝑧 ∈ Q) |
80 | | mulcomnq 10173 |
. . . . . . . . . . . . 13
⊢ (𝑤
·Q 1Q) =
(1Q ·Q 𝑤) |
81 | | mulidnq 10183 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ Q →
(𝑤
·Q 1Q) = 𝑤) |
82 | 80, 81 | syl5reqr 2829 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ Q →
𝑤 =
(1Q ·Q 𝑤)) |
83 | | mulassnq 10179 |
. . . . . . . . . . . . 13
⊢ ((𝑧
·Q (*Q‘𝑧))
·Q 𝑤) = (𝑧 ·Q
((*Q‘𝑧) ·Q 𝑤)) |
84 | | recidnq 10185 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ Q →
(𝑧
·Q (*Q‘𝑧)) =
1Q) |
85 | 84 | oveq1d 6991 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ Q →
((𝑧
·Q (*Q‘𝑧))
·Q 𝑤) = (1Q
·Q 𝑤)) |
86 | 83, 85 | syl5reqr 2829 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ Q →
(1Q ·Q 𝑤) = (𝑧 ·Q
((*Q‘𝑧) ·Q 𝑤))) |
87 | 82, 86 | sylan9eqr 2836 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ Q ∧
𝑤 ∈ Q)
→ 𝑤 = (𝑧
·Q ((*Q‘𝑧)
·Q 𝑤))) |
88 | 79, 25, 87 | syl2anc 576 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ P ∧
𝑤
<Q 1Q) ∧ (𝑣 ∈ 𝐴 ∧ ¬ (𝑣 ·Q
(*Q‘𝑤)) ∈ 𝐴) ∧ 𝑣 <Q 𝑧) → 𝑤 = (𝑧 ·Q
((*Q‘𝑧) ·Q 𝑤))) |
89 | | oveq2 6984 |
. . . . . . . . . . 11
⊢ (𝑥 =
((*Q‘𝑧) ·Q 𝑤) → (𝑧 ·Q 𝑥) = (𝑧 ·Q
((*Q‘𝑧) ·Q 𝑤))) |
90 | 89 | rspceeqv 3553 |
. . . . . . . . . 10
⊢
((((*Q‘𝑧) ·Q 𝑤) ∈ 𝐵 ∧ 𝑤 = (𝑧 ·Q
((*Q‘𝑧) ·Q 𝑤))) → ∃𝑥 ∈ 𝐵 𝑤 = (𝑧 ·Q 𝑥)) |
91 | 76, 88, 90 | syl2anc 576 |
. . . . . . . . 9
⊢ (((𝐴 ∈ P ∧
𝑤
<Q 1Q) ∧ (𝑣 ∈ 𝐴 ∧ ¬ (𝑣 ·Q
(*Q‘𝑤)) ∈ 𝐴) ∧ 𝑣 <Q 𝑧) → ∃𝑥 ∈ 𝐵 𝑤 = (𝑧 ·Q 𝑥)) |
92 | 91 | 3expia 1101 |
. . . . . . . 8
⊢ (((𝐴 ∈ P ∧
𝑤
<Q 1Q) ∧ (𝑣 ∈ 𝐴 ∧ ¬ (𝑣 ·Q
(*Q‘𝑤)) ∈ 𝐴)) → (𝑣 <Q 𝑧 → ∃𝑥 ∈ 𝐵 𝑤 = (𝑧 ·Q 𝑥))) |
93 | 92 | reximdv 3218 |
. . . . . . 7
⊢ (((𝐴 ∈ P ∧
𝑤
<Q 1Q) ∧ (𝑣 ∈ 𝐴 ∧ ¬ (𝑣 ·Q
(*Q‘𝑤)) ∈ 𝐴)) → (∃𝑧 ∈ 𝐴 𝑣 <Q 𝑧 → ∃𝑧 ∈ 𝐴 ∃𝑥 ∈ 𝐵 𝑤 = (𝑧 ·Q 𝑥))) |
94 | 71 | reclem2pr 10268 |
. . . . . . . . 9
⊢ (𝐴 ∈ P →
𝐵 ∈
P) |
95 | | df-mp 10204 |
. . . . . . . . . 10
⊢
·P = (𝑦 ∈ P, 𝑤 ∈ P ↦ {𝑢 ∣ ∃𝑓 ∈ 𝑦 ∃𝑔 ∈ 𝑤 𝑢 = (𝑓 ·Q 𝑔)}) |
96 | | mulclnq 10167 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ Q ∧
𝑔 ∈ Q)
→ (𝑓
·Q 𝑔) ∈ Q) |
97 | 95, 96 | genpelv 10220 |
. . . . . . . . 9
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝑤 ∈ (𝐴
·P 𝐵) ↔ ∃𝑧 ∈ 𝐴 ∃𝑥 ∈ 𝐵 𝑤 = (𝑧 ·Q 𝑥))) |
98 | 94, 97 | mpdan 674 |
. . . . . . . 8
⊢ (𝐴 ∈ P →
(𝑤 ∈ (𝐴
·P 𝐵) ↔ ∃𝑧 ∈ 𝐴 ∃𝑥 ∈ 𝐵 𝑤 = (𝑧 ·Q 𝑥))) |
99 | 98 | ad2antrr 713 |
. . . . . . 7
⊢ (((𝐴 ∈ P ∧
𝑤
<Q 1Q) ∧ (𝑣 ∈ 𝐴 ∧ ¬ (𝑣 ·Q
(*Q‘𝑤)) ∈ 𝐴)) → (𝑤 ∈ (𝐴 ·P 𝐵) ↔ ∃𝑧 ∈ 𝐴 ∃𝑥 ∈ 𝐵 𝑤 = (𝑧 ·Q 𝑥))) |
100 | 93, 99 | sylibrd 251 |
. . . . . 6
⊢ (((𝐴 ∈ P ∧
𝑤
<Q 1Q) ∧ (𝑣 ∈ 𝐴 ∧ ¬ (𝑣 ·Q
(*Q‘𝑤)) ∈ 𝐴)) → (∃𝑧 ∈ 𝐴 𝑣 <Q 𝑧 → 𝑤 ∈ (𝐴 ·P 𝐵))) |
101 | 17, 100 | mpd 15 |
. . . . 5
⊢ (((𝐴 ∈ P ∧
𝑤
<Q 1Q) ∧ (𝑣 ∈ 𝐴 ∧ ¬ (𝑣 ·Q
(*Q‘𝑤)) ∈ 𝐴)) → 𝑤 ∈ (𝐴 ·P 𝐵)) |
102 | 15, 101 | rexlimddv 3236 |
. . . 4
⊢ ((𝐴 ∈ P ∧
𝑤
<Q 1Q) → 𝑤 ∈ (𝐴 ·P 𝐵)) |
103 | 102 | ex 405 |
. . 3
⊢ (𝐴 ∈ P →
(𝑤
<Q 1Q → 𝑤 ∈ (𝐴 ·P 𝐵))) |
104 | 2, 103 | syl5bi 234 |
. 2
⊢ (𝐴 ∈ P →
(𝑤 ∈
1P → 𝑤 ∈ (𝐴 ·P 𝐵))) |
105 | 104 | ssrdv 3864 |
1
⊢ (𝐴 ∈ P →
1P ⊆ (𝐴 ·P 𝐵)) |