| Step | Hyp | Ref
| Expression |
| 1 | | fldext2chn.3 |
. . 3
⊢ (𝜑 → 0 <
(♯‘𝑇)) |
| 2 | | fveq2 6906 |
. . . . . 6
⊢ (𝑑 = ∅ →
(♯‘𝑑) =
(♯‘∅)) |
| 3 | 2 | breq2d 5155 |
. . . . 5
⊢ (𝑑 = ∅ → (0 <
(♯‘𝑑) ↔ 0
< (♯‘∅))) |
| 4 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑑 = ∅ →
(lastS‘𝑑) =
(lastS‘∅)) |
| 5 | 4 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑑 = ∅ → (𝑊 ↾s
(lastS‘𝑑)) = (𝑊 ↾s
(lastS‘∅))) |
| 6 | | fveq1 6905 |
. . . . . . . 8
⊢ (𝑑 = ∅ → (𝑑‘0) =
(∅‘0)) |
| 7 | 6 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑑 = ∅ → (𝑊 ↾s (𝑑‘0)) = (𝑊 ↾s
(∅‘0))) |
| 8 | 5, 7 | breq12d 5156 |
. . . . . 6
⊢ (𝑑 = ∅ → ((𝑊 ↾s
(lastS‘𝑑))/FldExt(𝑊 ↾s (𝑑‘0)) ↔ (𝑊 ↾s
(lastS‘∅))/FldExt(𝑊 ↾s
(∅‘0)))) |
| 9 | 5, 7 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝑑 = ∅ → ((𝑊 ↾s
(lastS‘𝑑))[:](𝑊 ↾s (𝑑‘0))) = ((𝑊 ↾s
(lastS‘∅))[:](𝑊
↾s (∅‘0)))) |
| 10 | 9 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑑 = ∅ → (((𝑊 ↾s
(lastS‘𝑑))[:](𝑊 ↾s (𝑑‘0))) = (2↑𝑛) ↔ ((𝑊 ↾s
(lastS‘∅))[:](𝑊
↾s (∅‘0))) = (2↑𝑛))) |
| 11 | 10 | rexbidv 3179 |
. . . . . 6
⊢ (𝑑 = ∅ → (∃𝑛 ∈ ℕ0
((𝑊 ↾s
(lastS‘𝑑))[:](𝑊 ↾s (𝑑‘0))) = (2↑𝑛) ↔ ∃𝑛 ∈ ℕ0
((𝑊 ↾s
(lastS‘∅))[:](𝑊
↾s (∅‘0))) = (2↑𝑛))) |
| 12 | 8, 11 | anbi12d 632 |
. . . . 5
⊢ (𝑑 = ∅ → (((𝑊 ↾s
(lastS‘𝑑))/FldExt(𝑊 ↾s (𝑑‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑑))[:](𝑊 ↾s (𝑑‘0))) = (2↑𝑛)) ↔ ((𝑊 ↾s
(lastS‘∅))/FldExt(𝑊 ↾s (∅‘0))
∧ ∃𝑛 ∈
ℕ0 ((𝑊
↾s (lastS‘∅))[:](𝑊 ↾s (∅‘0))) =
(2↑𝑛)))) |
| 13 | 3, 12 | imbi12d 344 |
. . . 4
⊢ (𝑑 = ∅ → ((0 <
(♯‘𝑑) →
((𝑊 ↾s
(lastS‘𝑑))/FldExt(𝑊 ↾s (𝑑‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑑))[:](𝑊 ↾s (𝑑‘0))) = (2↑𝑛))) ↔ (0 <
(♯‘∅) → ((𝑊 ↾s
(lastS‘∅))/FldExt(𝑊 ↾s (∅‘0))
∧ ∃𝑛 ∈
ℕ0 ((𝑊
↾s (lastS‘∅))[:](𝑊 ↾s (∅‘0))) =
(2↑𝑛))))) |
| 14 | | fveq2 6906 |
. . . . . 6
⊢ (𝑑 = 𝑐 → (♯‘𝑑) = (♯‘𝑐)) |
| 15 | 14 | breq2d 5155 |
. . . . 5
⊢ (𝑑 = 𝑐 → (0 < (♯‘𝑑) ↔ 0 <
(♯‘𝑐))) |
| 16 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑑 = 𝑐 → (lastS‘𝑑) = (lastS‘𝑐)) |
| 17 | 16 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑑 = 𝑐 → (𝑊 ↾s (lastS‘𝑑)) = (𝑊 ↾s (lastS‘𝑐))) |
| 18 | | fveq1 6905 |
. . . . . . . 8
⊢ (𝑑 = 𝑐 → (𝑑‘0) = (𝑐‘0)) |
| 19 | 18 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑑 = 𝑐 → (𝑊 ↾s (𝑑‘0)) = (𝑊 ↾s (𝑐‘0))) |
| 20 | 17, 19 | breq12d 5156 |
. . . . . 6
⊢ (𝑑 = 𝑐 → ((𝑊 ↾s (lastS‘𝑑))/FldExt(𝑊 ↾s (𝑑‘0)) ↔ (𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)))) |
| 21 | 17, 19 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝑑 = 𝑐 → ((𝑊 ↾s (lastS‘𝑑))[:](𝑊 ↾s (𝑑‘0))) = ((𝑊 ↾s (lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0)))) |
| 22 | 21 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑑 = 𝑐 → (((𝑊 ↾s (lastS‘𝑑))[:](𝑊 ↾s (𝑑‘0))) = (2↑𝑛) ↔ ((𝑊 ↾s (lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛))) |
| 23 | 22 | rexbidv 3179 |
. . . . . 6
⊢ (𝑑 = 𝑐 → (∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑑))[:](𝑊 ↾s (𝑑‘0))) = (2↑𝑛) ↔ ∃𝑛 ∈ ℕ0
((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛))) |
| 24 | 20, 23 | anbi12d 632 |
. . . . 5
⊢ (𝑑 = 𝑐 → (((𝑊 ↾s (lastS‘𝑑))/FldExt(𝑊 ↾s (𝑑‘0)) ∧ ∃𝑛 ∈ ℕ0
((𝑊 ↾s
(lastS‘𝑑))[:](𝑊 ↾s (𝑑‘0))) = (2↑𝑛)) ↔ ((𝑊 ↾s (lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0
((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) |
| 25 | 15, 24 | imbi12d 344 |
. . . 4
⊢ (𝑑 = 𝑐 → ((0 < (♯‘𝑑) → ((𝑊 ↾s (lastS‘𝑑))/FldExt(𝑊 ↾s (𝑑‘0)) ∧ ∃𝑛 ∈ ℕ0
((𝑊 ↾s
(lastS‘𝑑))[:](𝑊 ↾s (𝑑‘0))) = (2↑𝑛))) ↔ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛))))) |
| 26 | | fveq2 6906 |
. . . . . 6
⊢ (𝑑 = (𝑐 ++ 〈“𝑔”〉) → (♯‘𝑑) = (♯‘(𝑐 ++ 〈“𝑔”〉))) |
| 27 | 26 | breq2d 5155 |
. . . . 5
⊢ (𝑑 = (𝑐 ++ 〈“𝑔”〉) → (0 <
(♯‘𝑑) ↔ 0
< (♯‘(𝑐 ++
〈“𝑔”〉)))) |
| 28 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑑 = (𝑐 ++ 〈“𝑔”〉) → (lastS‘𝑑) = (lastS‘(𝑐 ++ 〈“𝑔”〉))) |
| 29 | 28 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑑 = (𝑐 ++ 〈“𝑔”〉) → (𝑊 ↾s (lastS‘𝑑)) = (𝑊 ↾s (lastS‘(𝑐 ++ 〈“𝑔”〉)))) |
| 30 | | fveq1 6905 |
. . . . . . . 8
⊢ (𝑑 = (𝑐 ++ 〈“𝑔”〉) → (𝑑‘0) = ((𝑐 ++ 〈“𝑔”〉)‘0)) |
| 31 | 30 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑑 = (𝑐 ++ 〈“𝑔”〉) → (𝑊 ↾s (𝑑‘0)) = (𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0))) |
| 32 | 29, 31 | breq12d 5156 |
. . . . . 6
⊢ (𝑑 = (𝑐 ++ 〈“𝑔”〉) → ((𝑊 ↾s (lastS‘𝑑))/FldExt(𝑊 ↾s (𝑑‘0)) ↔ (𝑊 ↾s
(lastS‘(𝑐 ++
〈“𝑔”〉)))/FldExt(𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0)))) |
| 33 | 29, 31 | oveq12d 7449 |
. . . . . . . . 9
⊢ (𝑑 = (𝑐 ++ 〈“𝑔”〉) → ((𝑊 ↾s (lastS‘𝑑))[:](𝑊 ↾s (𝑑‘0))) = ((𝑊 ↾s (lastS‘(𝑐 ++ 〈“𝑔”〉)))[:](𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0)))) |
| 34 | 33 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑑 = (𝑐 ++ 〈“𝑔”〉) → (((𝑊 ↾s (lastS‘𝑑))[:](𝑊 ↾s (𝑑‘0))) = (2↑𝑛) ↔ ((𝑊 ↾s (lastS‘(𝑐 ++ 〈“𝑔”〉)))[:](𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0))) =
(2↑𝑛))) |
| 35 | 34 | rexbidv 3179 |
. . . . . . 7
⊢ (𝑑 = (𝑐 ++ 〈“𝑔”〉) → (∃𝑛 ∈ ℕ0
((𝑊 ↾s
(lastS‘𝑑))[:](𝑊 ↾s (𝑑‘0))) = (2↑𝑛) ↔ ∃𝑛 ∈ ℕ0
((𝑊 ↾s
(lastS‘(𝑐 ++
〈“𝑔”〉)))[:](𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0))) = (2↑𝑛))) |
| 36 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (2↑𝑛) = (2↑𝑚)) |
| 37 | 36 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → (((𝑊 ↾s (lastS‘(𝑐 ++ 〈“𝑔”〉)))[:](𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0))) =
(2↑𝑛) ↔ ((𝑊 ↾s
(lastS‘(𝑐 ++
〈“𝑔”〉)))[:](𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0))) = (2↑𝑚))) |
| 38 | 37 | cbvrexvw 3238 |
. . . . . . 7
⊢
(∃𝑛 ∈
ℕ0 ((𝑊
↾s (lastS‘(𝑐 ++ 〈“𝑔”〉)))[:](𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0))) = (2↑𝑛) ↔ ∃𝑚 ∈ ℕ0
((𝑊 ↾s
(lastS‘(𝑐 ++
〈“𝑔”〉)))[:](𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0))) = (2↑𝑚)) |
| 39 | 35, 38 | bitrdi 287 |
. . . . . 6
⊢ (𝑑 = (𝑐 ++ 〈“𝑔”〉) → (∃𝑛 ∈ ℕ0
((𝑊 ↾s
(lastS‘𝑑))[:](𝑊 ↾s (𝑑‘0))) = (2↑𝑛) ↔ ∃𝑚 ∈ ℕ0
((𝑊 ↾s
(lastS‘(𝑐 ++
〈“𝑔”〉)))[:](𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0))) = (2↑𝑚))) |
| 40 | 32, 39 | anbi12d 632 |
. . . . 5
⊢ (𝑑 = (𝑐 ++ 〈“𝑔”〉) → (((𝑊 ↾s (lastS‘𝑑))/FldExt(𝑊 ↾s (𝑑‘0)) ∧ ∃𝑛 ∈ ℕ0
((𝑊 ↾s
(lastS‘𝑑))[:](𝑊 ↾s (𝑑‘0))) = (2↑𝑛)) ↔ ((𝑊 ↾s (lastS‘(𝑐 ++ 〈“𝑔”〉)))/FldExt(𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0)) ∧
∃𝑚 ∈
ℕ0 ((𝑊
↾s (lastS‘(𝑐 ++ 〈“𝑔”〉)))[:](𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0))) = (2↑𝑚)))) |
| 41 | 27, 40 | imbi12d 344 |
. . . 4
⊢ (𝑑 = (𝑐 ++ 〈“𝑔”〉) → ((0 <
(♯‘𝑑) →
((𝑊 ↾s
(lastS‘𝑑))/FldExt(𝑊 ↾s (𝑑‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑑))[:](𝑊 ↾s (𝑑‘0))) = (2↑𝑛))) ↔ (0 <
(♯‘(𝑐 ++
〈“𝑔”〉)) → ((𝑊 ↾s (lastS‘(𝑐 ++ 〈“𝑔”〉)))/FldExt(𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0)) ∧
∃𝑚 ∈
ℕ0 ((𝑊
↾s (lastS‘(𝑐 ++ 〈“𝑔”〉)))[:](𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0))) = (2↑𝑚))))) |
| 42 | | fveq2 6906 |
. . . . . 6
⊢ (𝑑 = 𝑇 → (♯‘𝑑) = (♯‘𝑇)) |
| 43 | 42 | breq2d 5155 |
. . . . 5
⊢ (𝑑 = 𝑇 → (0 < (♯‘𝑑) ↔ 0 <
(♯‘𝑇))) |
| 44 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑑 = 𝑇 → (lastS‘𝑑) = (lastS‘𝑇)) |
| 45 | 44 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑑 = 𝑇 → (𝑊 ↾s (lastS‘𝑑)) = (𝑊 ↾s (lastS‘𝑇))) |
| 46 | | fveq1 6905 |
. . . . . . . 8
⊢ (𝑑 = 𝑇 → (𝑑‘0) = (𝑇‘0)) |
| 47 | 46 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑑 = 𝑇 → (𝑊 ↾s (𝑑‘0)) = (𝑊 ↾s (𝑇‘0))) |
| 48 | 45, 47 | breq12d 5156 |
. . . . . 6
⊢ (𝑑 = 𝑇 → ((𝑊 ↾s (lastS‘𝑑))/FldExt(𝑊 ↾s (𝑑‘0)) ↔ (𝑊 ↾s
(lastS‘𝑇))/FldExt(𝑊 ↾s (𝑇‘0)))) |
| 49 | 45, 47 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝑑 = 𝑇 → ((𝑊 ↾s (lastS‘𝑑))[:](𝑊 ↾s (𝑑‘0))) = ((𝑊 ↾s (lastS‘𝑇))[:](𝑊 ↾s (𝑇‘0)))) |
| 50 | 49 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑑 = 𝑇 → (((𝑊 ↾s (lastS‘𝑑))[:](𝑊 ↾s (𝑑‘0))) = (2↑𝑛) ↔ ((𝑊 ↾s (lastS‘𝑇))[:](𝑊 ↾s (𝑇‘0))) = (2↑𝑛))) |
| 51 | 50 | rexbidv 3179 |
. . . . . 6
⊢ (𝑑 = 𝑇 → (∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑑))[:](𝑊 ↾s (𝑑‘0))) = (2↑𝑛) ↔ ∃𝑛 ∈ ℕ0
((𝑊 ↾s
(lastS‘𝑇))[:](𝑊 ↾s (𝑇‘0))) = (2↑𝑛))) |
| 52 | 48, 51 | anbi12d 632 |
. . . . 5
⊢ (𝑑 = 𝑇 → (((𝑊 ↾s (lastS‘𝑑))/FldExt(𝑊 ↾s (𝑑‘0)) ∧ ∃𝑛 ∈ ℕ0
((𝑊 ↾s
(lastS‘𝑑))[:](𝑊 ↾s (𝑑‘0))) = (2↑𝑛)) ↔ ((𝑊 ↾s (lastS‘𝑇))/FldExt(𝑊 ↾s (𝑇‘0)) ∧ ∃𝑛 ∈ ℕ0
((𝑊 ↾s
(lastS‘𝑇))[:](𝑊 ↾s (𝑇‘0))) = (2↑𝑛)))) |
| 53 | 43, 52 | imbi12d 344 |
. . . 4
⊢ (𝑑 = 𝑇 → ((0 < (♯‘𝑑) → ((𝑊 ↾s (lastS‘𝑑))/FldExt(𝑊 ↾s (𝑑‘0)) ∧ ∃𝑛 ∈ ℕ0
((𝑊 ↾s
(lastS‘𝑑))[:](𝑊 ↾s (𝑑‘0))) = (2↑𝑛))) ↔ (0 <
(♯‘𝑇) →
((𝑊 ↾s
(lastS‘𝑇))/FldExt(𝑊 ↾s (𝑇‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑇))[:](𝑊 ↾s (𝑇‘0))) = (2↑𝑛))))) |
| 54 | | fldext2chn.t |
. . . 4
⊢ (𝜑 → 𝑇 ∈ ( <
Chain(SubDRing‘𝑊))) |
| 55 | | 0re 11263 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
| 56 | 55 | ltnri 11370 |
. . . . . . 7
⊢ ¬ 0
< 0 |
| 57 | 56 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ¬ 0 <
0) |
| 58 | | hash0 14406 |
. . . . . . 7
⊢
(♯‘∅) = 0 |
| 59 | 58 | breq2i 5151 |
. . . . . 6
⊢ (0 <
(♯‘∅) ↔ 0 < 0) |
| 60 | 57, 59 | sylnibr 329 |
. . . . 5
⊢ (𝜑 → ¬ 0 <
(♯‘∅)) |
| 61 | 60 | pm2.21d 121 |
. . . 4
⊢ (𝜑 → (0 <
(♯‘∅) → ((𝑊 ↾s
(lastS‘∅))/FldExt(𝑊 ↾s (∅‘0))
∧ ∃𝑛 ∈
ℕ0 ((𝑊
↾s (lastS‘∅))[:](𝑊 ↾s (∅‘0))) =
(2↑𝑛)))) |
| 62 | | fldext2chn.w |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑊 ∈ Field) |
| 63 | 62 | ad6antr 736 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 = ∅) → 𝑊 ∈ Field) |
| 64 | | simp-5r 786 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 = ∅) → 𝑔 ∈ (SubDRing‘𝑊)) |
| 65 | | fldsdrgfld 20799 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Field ∧ 𝑔 ∈ (SubDRing‘𝑊)) → (𝑊 ↾s 𝑔) ∈ Field) |
| 66 | 63, 64, 65 | syl2anc 584 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 = ∅) → (𝑊 ↾s 𝑔) ∈ Field) |
| 67 | | fldextid 33710 |
. . . . . . . . 9
⊢ ((𝑊 ↾s 𝑔) ∈ Field → (𝑊 ↾s 𝑔)/FldExt(𝑊 ↾s 𝑔)) |
| 68 | 66, 67 | syl 17 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 = ∅) → (𝑊 ↾s 𝑔)/FldExt(𝑊 ↾s 𝑔)) |
| 69 | | simp-5r 786 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) → 𝑐 ∈ ( <
Chain(SubDRing‘𝑊))) |
| 70 | 69 | chnwrd 32997 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) → 𝑐 ∈ Word (SubDRing‘𝑊)) |
| 71 | 70 | adantr 480 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 = ∅) → 𝑐 ∈ Word (SubDRing‘𝑊)) |
| 72 | | lswccats1 14672 |
. . . . . . . . . 10
⊢ ((𝑐 ∈ Word
(SubDRing‘𝑊) ∧
𝑔 ∈
(SubDRing‘𝑊)) →
(lastS‘(𝑐 ++
〈“𝑔”〉)) = 𝑔) |
| 73 | 71, 64, 72 | syl2anc 584 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 = ∅) → (lastS‘(𝑐 ++ 〈“𝑔”〉)) = 𝑔) |
| 74 | 73 | oveq2d 7447 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 = ∅) → (𝑊 ↾s (lastS‘(𝑐 ++ 〈“𝑔”〉))) = (𝑊 ↾s 𝑔)) |
| 75 | | simpr 484 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 = ∅) → 𝑐 = ∅) |
| 76 | 75 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 = ∅) → (𝑐 ++ 〈“𝑔”〉) = (∅ ++
〈“𝑔”〉)) |
| 77 | | s0s1 14961 |
. . . . . . . . . . . 12
⊢
〈“𝑔”〉 = (∅ ++
〈“𝑔”〉) |
| 78 | 76, 77 | eqtr4di 2795 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 = ∅) → (𝑐 ++ 〈“𝑔”〉) = 〈“𝑔”〉) |
| 79 | 78 | fveq1d 6908 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 = ∅) → ((𝑐 ++ 〈“𝑔”〉)‘0) = (〈“𝑔”〉‘0)) |
| 80 | | s1fv 14648 |
. . . . . . . . . . 11
⊢ (𝑔 ∈ (SubDRing‘𝑊) → (〈“𝑔”〉‘0) = 𝑔) |
| 81 | 64, 80 | syl 17 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 = ∅) → (〈“𝑔”〉‘0) = 𝑔) |
| 82 | 79, 81 | eqtrd 2777 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 = ∅) → ((𝑐 ++ 〈“𝑔”〉)‘0) = 𝑔) |
| 83 | 82 | oveq2d 7447 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 = ∅) → (𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0)) = (𝑊 ↾s 𝑔)) |
| 84 | 68, 74, 83 | 3brtr4d 5175 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 = ∅) → (𝑊 ↾s (lastS‘(𝑐 ++ 〈“𝑔”〉)))/FldExt(𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0))) |
| 85 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑚 = 0 → (2↑𝑚) = (2↑0)) |
| 86 | | 2cn 12341 |
. . . . . . . . . . 11
⊢ 2 ∈
ℂ |
| 87 | | exp0 14106 |
. . . . . . . . . . 11
⊢ (2 ∈
ℂ → (2↑0) = 1) |
| 88 | 86, 87 | ax-mp 5 |
. . . . . . . . . 10
⊢
(2↑0) = 1 |
| 89 | 85, 88 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (𝑚 = 0 → (2↑𝑚) = 1) |
| 90 | 89 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑚 = 0 → (((𝑊 ↾s (lastS‘(𝑐 ++ 〈“𝑔”〉)))[:](𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0))) =
(2↑𝑚) ↔ ((𝑊 ↾s
(lastS‘(𝑐 ++
〈“𝑔”〉)))[:](𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0))) =
1)) |
| 91 | | 0nn0 12541 |
. . . . . . . . 9
⊢ 0 ∈
ℕ0 |
| 92 | 91 | a1i 11 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 = ∅) → 0 ∈
ℕ0) |
| 93 | 74, 83 | oveq12d 7449 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 = ∅) → ((𝑊 ↾s (lastS‘(𝑐 ++ 〈“𝑔”〉)))[:](𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0))) =
((𝑊 ↾s
𝑔)[:](𝑊 ↾s 𝑔))) |
| 94 | | extdgid 33711 |
. . . . . . . . . 10
⊢ ((𝑊 ↾s 𝑔) ∈ Field → ((𝑊 ↾s 𝑔)[:](𝑊 ↾s 𝑔)) = 1) |
| 95 | 66, 94 | syl 17 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 = ∅) → ((𝑊 ↾s 𝑔)[:](𝑊 ↾s 𝑔)) = 1) |
| 96 | 93, 95 | eqtrd 2777 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 = ∅) → ((𝑊 ↾s (lastS‘(𝑐 ++ 〈“𝑔”〉)))[:](𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0))) =
1) |
| 97 | 90, 92, 96 | rspcedvdw 3625 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 = ∅) → ∃𝑚 ∈ ℕ0 ((𝑊 ↾s
(lastS‘(𝑐 ++
〈“𝑔”〉)))[:](𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0))) = (2↑𝑚)) |
| 98 | 84, 97 | jca 511 |
. . . . . 6
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 = ∅) → ((𝑊 ↾s (lastS‘(𝑐 ++ 〈“𝑔”〉)))/FldExt(𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0)) ∧
∃𝑚 ∈
ℕ0 ((𝑊
↾s (lastS‘(𝑐 ++ 〈“𝑔”〉)))[:](𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0))) = (2↑𝑚))) |
| 99 | | simp-6r 788 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) |
| 100 | | simpllr 776 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → 𝑐 ≠ ∅) |
| 101 | 100 | neneqd 2945 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → ¬ 𝑐 = ∅) |
| 102 | 99, 101 | orcnd 879 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → (lastS‘𝑐) < 𝑔) |
| 103 | 70 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → 𝑐 ∈ Word (SubDRing‘𝑊)) |
| 104 | | lswcl 14606 |
. . . . . . . . . . . . . 14
⊢ ((𝑐 ∈ Word
(SubDRing‘𝑊) ∧
𝑐 ≠ ∅) →
(lastS‘𝑐) ∈
(SubDRing‘𝑊)) |
| 105 | 103, 100,
104 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → (lastS‘𝑐) ∈ (SubDRing‘𝑊)) |
| 106 | | simp-7r 790 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → 𝑔 ∈ (SubDRing‘𝑊)) |
| 107 | | fldext2chn.e |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐸 = (𝑊 ↾s 𝑒) |
| 108 | | fldext2chn.f |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐹 = (𝑊 ↾s 𝑓) |
| 109 | 107, 108 | breq12i 5152 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐸/FldExt𝐹 ↔ (𝑊 ↾s 𝑒)/FldExt(𝑊 ↾s 𝑓)) |
| 110 | 107, 108 | oveq12i 7443 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐸[:]𝐹) = ((𝑊 ↾s 𝑒)[:](𝑊 ↾s 𝑓)) |
| 111 | 110 | eqeq1i 2742 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐸[:]𝐹) = 2 ↔ ((𝑊 ↾s 𝑒)[:](𝑊 ↾s 𝑓)) = 2) |
| 112 | 109, 111 | anbi12i 628 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 2) ↔ ((𝑊 ↾s 𝑒)/FldExt(𝑊 ↾s 𝑓) ∧ ((𝑊 ↾s 𝑒)[:](𝑊 ↾s 𝑓)) = 2)) |
| 113 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑒 = 𝑔 → (𝑊 ↾s 𝑒) = (𝑊 ↾s 𝑔)) |
| 114 | 113 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → (𝑊 ↾s 𝑒) = (𝑊 ↾s 𝑔)) |
| 115 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = (lastS‘𝑐) → (𝑊 ↾s 𝑓) = (𝑊 ↾s (lastS‘𝑐))) |
| 116 | 115 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → (𝑊 ↾s 𝑓) = (𝑊 ↾s (lastS‘𝑐))) |
| 117 | 114, 116 | breq12d 5156 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → ((𝑊 ↾s 𝑒)/FldExt(𝑊 ↾s 𝑓) ↔ (𝑊 ↾s 𝑔)/FldExt(𝑊 ↾s (lastS‘𝑐)))) |
| 118 | 114, 116 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → ((𝑊 ↾s 𝑒)[:](𝑊 ↾s 𝑓)) = ((𝑊 ↾s 𝑔)[:](𝑊 ↾s (lastS‘𝑐)))) |
| 119 | 118 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → (((𝑊 ↾s 𝑒)[:](𝑊 ↾s 𝑓)) = 2 ↔ ((𝑊 ↾s 𝑔)[:](𝑊 ↾s (lastS‘𝑐))) = 2)) |
| 120 | 117, 119 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → (((𝑊 ↾s 𝑒)/FldExt(𝑊 ↾s 𝑓) ∧ ((𝑊 ↾s 𝑒)[:](𝑊 ↾s 𝑓)) = 2) ↔ ((𝑊 ↾s 𝑔)/FldExt(𝑊 ↾s (lastS‘𝑐)) ∧ ((𝑊 ↾s 𝑔)[:](𝑊 ↾s (lastS‘𝑐))) = 2))) |
| 121 | 112, 120 | bitrid 283 |
. . . . . . . . . . . . . . 15
⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 2) ↔ ((𝑊 ↾s 𝑔)/FldExt(𝑊 ↾s (lastS‘𝑐)) ∧ ((𝑊 ↾s 𝑔)[:](𝑊 ↾s (lastS‘𝑐))) = 2))) |
| 122 | 121 | ancoms 458 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 = (lastS‘𝑐) ∧ 𝑒 = 𝑔) → ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 2) ↔ ((𝑊 ↾s 𝑔)/FldExt(𝑊 ↾s (lastS‘𝑐)) ∧ ((𝑊 ↾s 𝑔)[:](𝑊 ↾s (lastS‘𝑐))) = 2))) |
| 123 | | fldext2chn.l |
. . . . . . . . . . . . . 14
⊢ < =
{〈𝑓, 𝑒〉 ∣ (𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 2)} |
| 124 | 122, 123 | brabga 5539 |
. . . . . . . . . . . . 13
⊢
(((lastS‘𝑐)
∈ (SubDRing‘𝑊)
∧ 𝑔 ∈
(SubDRing‘𝑊)) →
((lastS‘𝑐) < 𝑔 ↔ ((𝑊 ↾s 𝑔)/FldExt(𝑊 ↾s (lastS‘𝑐)) ∧ ((𝑊 ↾s 𝑔)[:](𝑊 ↾s (lastS‘𝑐))) = 2))) |
| 125 | 105, 106,
124 | syl2anc 584 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → ((lastS‘𝑐) < 𝑔 ↔ ((𝑊 ↾s 𝑔)/FldExt(𝑊 ↾s (lastS‘𝑐)) ∧ ((𝑊 ↾s 𝑔)[:](𝑊 ↾s (lastS‘𝑐))) = 2))) |
| 126 | 102, 125 | mpbid 232 |
. . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → ((𝑊 ↾s 𝑔)/FldExt(𝑊 ↾s (lastS‘𝑐)) ∧ ((𝑊 ↾s 𝑔)[:](𝑊 ↾s (lastS‘𝑐))) = 2)) |
| 127 | 126 | simpld 494 |
. . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → (𝑊 ↾s 𝑔)/FldExt(𝑊 ↾s (lastS‘𝑐))) |
| 128 | | hashgt0 14427 |
. . . . . . . . . . . . . 14
⊢ ((𝑐 ∈ ( <
Chain(SubDRing‘𝑊))
∧ 𝑐 ≠ ∅)
→ 0 < (♯‘𝑐)) |
| 129 | 69, 128 | sylan 580 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) → 0 <
(♯‘𝑐)) |
| 130 | | simpllr 776 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) → (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) |
| 131 | 129, 130 | mpd 15 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) → ((𝑊 ↾s (lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0
((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛))) |
| 132 | 131 | simprd 495 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) → ∃𝑛 ∈ ℕ0
((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)) |
| 133 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑜 → (2↑𝑛) = (2↑𝑜)) |
| 134 | 133 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑜 → (((𝑊 ↾s (lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛) ↔ ((𝑊 ↾s (lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜))) |
| 135 | 134 | cbvrexvw 3238 |
. . . . . . . . . . 11
⊢
(∃𝑛 ∈
ℕ0 ((𝑊
↾s (lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛) ↔ ∃𝑜 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) |
| 136 | 132, 135 | sylib 218 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) → ∃𝑜 ∈ ℕ0
((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) |
| 137 | 127, 136 | r19.29a 3162 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) → (𝑊 ↾s 𝑔)/FldExt(𝑊 ↾s (lastS‘𝑐))) |
| 138 | 131 | simpld 494 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) → (𝑊 ↾s (lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0))) |
| 139 | | fldexttr 33709 |
. . . . . . . . 9
⊢ (((𝑊 ↾s 𝑔)/FldExt(𝑊 ↾s
(lastS‘𝑐)) ∧
(𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0))) → (𝑊 ↾s 𝑔)/FldExt(𝑊 ↾s (𝑐‘0))) |
| 140 | 137, 138,
139 | syl2anc 584 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) → (𝑊 ↾s 𝑔)/FldExt(𝑊 ↾s (𝑐‘0))) |
| 141 | 103, 106,
72 | syl2anc 584 |
. . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → (lastS‘(𝑐 ++ 〈“𝑔”〉)) = 𝑔) |
| 142 | 141 | oveq2d 7447 |
. . . . . . . . 9
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → (𝑊 ↾s (lastS‘(𝑐 ++ 〈“𝑔”〉))) = (𝑊 ↾s 𝑔)) |
| 143 | 142, 136 | r19.29a 3162 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) → (𝑊 ↾s (lastS‘(𝑐 ++ 〈“𝑔”〉))) = (𝑊 ↾s 𝑔)) |
| 144 | 106 | s1cld 14641 |
. . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → 〈“𝑔”〉 ∈ Word
(SubDRing‘𝑊)) |
| 145 | 129 | ad2antrr 726 |
. . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → 0 <
(♯‘𝑐)) |
| 146 | | ccatfv0 14621 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ Word
(SubDRing‘𝑊) ∧
〈“𝑔”〉
∈ Word (SubDRing‘𝑊) ∧ 0 < (♯‘𝑐)) → ((𝑐 ++ 〈“𝑔”〉)‘0) = (𝑐‘0)) |
| 147 | 103, 144,
145, 146 | syl3anc 1373 |
. . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → ((𝑐 ++ 〈“𝑔”〉)‘0) = (𝑐‘0)) |
| 148 | 147 | oveq2d 7447 |
. . . . . . . . 9
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → (𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0)) = (𝑊 ↾s (𝑐‘0))) |
| 149 | 148, 136 | r19.29a 3162 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) → (𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0)) = (𝑊 ↾s (𝑐‘0))) |
| 150 | 140, 143,
149 | 3brtr4d 5175 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) → (𝑊 ↾s (lastS‘(𝑐 ++ 〈“𝑔”〉)))/FldExt(𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0))) |
| 151 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑜 + 1) → (2↑𝑚) = (2↑(𝑜 + 1))) |
| 152 | 151 | eqeq2d 2748 |
. . . . . . . . 9
⊢ (𝑚 = (𝑜 + 1) → (((𝑊 ↾s (lastS‘(𝑐 ++ 〈“𝑔”〉)))[:](𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0))) =
(2↑𝑚) ↔ ((𝑊 ↾s
(lastS‘(𝑐 ++
〈“𝑔”〉)))[:](𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0))) = (2↑(𝑜 + 1)))) |
| 153 | | simplr 769 |
. . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → 𝑜 ∈ ℕ0) |
| 154 | | 1nn0 12542 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ0 |
| 155 | 154 | a1i 11 |
. . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → 1 ∈
ℕ0) |
| 156 | 153, 155 | nn0addcld 12591 |
. . . . . . . . 9
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → (𝑜 + 1) ∈
ℕ0) |
| 157 | 142, 148 | oveq12d 7449 |
. . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → ((𝑊 ↾s (lastS‘(𝑐 ++ 〈“𝑔”〉)))[:](𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0))) =
((𝑊 ↾s
𝑔)[:](𝑊 ↾s (𝑐‘0)))) |
| 158 | 138 | ad2antrr 726 |
. . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → (𝑊 ↾s (lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0))) |
| 159 | | extdgmul 33714 |
. . . . . . . . . . 11
⊢ (((𝑊 ↾s 𝑔)/FldExt(𝑊 ↾s
(lastS‘𝑐)) ∧
(𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0))) → ((𝑊 ↾s 𝑔)[:](𝑊 ↾s (𝑐‘0))) = (((𝑊 ↾s 𝑔)[:](𝑊 ↾s (lastS‘𝑐))) ·e ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))))) |
| 160 | 127, 158,
159 | syl2anc 584 |
. . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → ((𝑊 ↾s 𝑔)[:](𝑊 ↾s (𝑐‘0))) = (((𝑊 ↾s 𝑔)[:](𝑊 ↾s (lastS‘𝑐))) ·e ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))))) |
| 161 | 86 | a1i 11 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → 2 ∈
ℂ) |
| 162 | 161, 153 | expcld 14186 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → (2↑𝑜) ∈
ℂ) |
| 163 | 161, 162 | mulcomd 11282 |
. . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → (2 ·
(2↑𝑜)) =
((2↑𝑜) ·
2)) |
| 164 | 126 | simprd 495 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → ((𝑊 ↾s 𝑔)[:](𝑊 ↾s (lastS‘𝑐))) = 2) |
| 165 | | simpr 484 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → ((𝑊 ↾s (lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) |
| 166 | 164, 165 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → (((𝑊 ↾s 𝑔)[:](𝑊 ↾s (lastS‘𝑐))) ·e ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0)))) = (2
·e (2↑𝑜))) |
| 167 | | 2re 12340 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℝ |
| 168 | 167 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → 2 ∈
ℝ) |
| 169 | 168, 153 | reexpcld 14203 |
. . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → (2↑𝑜) ∈
ℝ) |
| 170 | | rexmul 13313 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℝ ∧ (2↑𝑜) ∈ ℝ) → (2
·e (2↑𝑜)) = (2 · (2↑𝑜))) |
| 171 | 168, 169,
170 | syl2anc 584 |
. . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → (2
·e (2↑𝑜)) = (2 · (2↑𝑜))) |
| 172 | 166, 171 | eqtrd 2777 |
. . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → (((𝑊 ↾s 𝑔)[:](𝑊 ↾s (lastS‘𝑐))) ·e ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0)))) = (2 ·
(2↑𝑜))) |
| 173 | 161, 153 | expp1d 14187 |
. . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → (2↑(𝑜 + 1)) = ((2↑𝑜) · 2)) |
| 174 | 163, 172,
173 | 3eqtr4d 2787 |
. . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → (((𝑊 ↾s 𝑔)[:](𝑊 ↾s (lastS‘𝑐))) ·e ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0)))) = (2↑(𝑜 + 1))) |
| 175 | 157, 160,
174 | 3eqtrd 2781 |
. . . . . . . . 9
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → ((𝑊 ↾s (lastS‘(𝑐 ++ 〈“𝑔”〉)))[:](𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0))) =
(2↑(𝑜 +
1))) |
| 176 | 152, 156,
175 | rspcedvdw 3625 |
. . . . . . . 8
⊢
(((((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ0) ∧ ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑜)) → ∃𝑚 ∈ ℕ0
((𝑊 ↾s
(lastS‘(𝑐 ++
〈“𝑔”〉)))[:](𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0))) = (2↑𝑚)) |
| 177 | 176, 136 | r19.29a 3162 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) → ∃𝑚 ∈ ℕ0
((𝑊 ↾s
(lastS‘(𝑐 ++
〈“𝑔”〉)))[:](𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0))) = (2↑𝑚)) |
| 178 | 150, 177 | jca 511 |
. . . . . 6
⊢
(((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) ∧ 𝑐 ≠ ∅) → ((𝑊 ↾s (lastS‘(𝑐 ++ 〈“𝑔”〉)))/FldExt(𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0)) ∧
∃𝑚 ∈
ℕ0 ((𝑊
↾s (lastS‘(𝑐 ++ 〈“𝑔”〉)))[:](𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0))) = (2↑𝑚))) |
| 179 | 98, 178 | pm2.61dane 3029 |
. . . . 5
⊢
((((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 <
(♯‘(𝑐 ++
〈“𝑔”〉))) → ((𝑊 ↾s (lastS‘(𝑐 ++ 〈“𝑔”〉)))/FldExt(𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0)) ∧
∃𝑚 ∈
ℕ0 ((𝑊
↾s (lastS‘(𝑐 ++ 〈“𝑔”〉)))[:](𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0))) = (2↑𝑚))) |
| 180 | 179 | ex 412 |
. . . 4
⊢
(((((𝜑 ∧ 𝑐 ∈ ( <
Chain(SubDRing‘𝑊)))
∧ 𝑔 ∈
(SubDRing‘𝑊)) ∧
(𝑐 = ∅ ∨
(lastS‘𝑐) < 𝑔)) ∧ (0 <
(♯‘𝑐) →
((𝑊 ↾s
(lastS‘𝑐))/FldExt(𝑊 ↾s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑐))[:](𝑊 ↾s (𝑐‘0))) = (2↑𝑛)))) → (0 <
(♯‘(𝑐 ++
〈“𝑔”〉)) → ((𝑊 ↾s (lastS‘(𝑐 ++ 〈“𝑔”〉)))/FldExt(𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0)) ∧
∃𝑚 ∈
ℕ0 ((𝑊
↾s (lastS‘(𝑐 ++ 〈“𝑔”〉)))[:](𝑊 ↾s ((𝑐 ++ 〈“𝑔”〉)‘0))) = (2↑𝑚)))) |
| 181 | 13, 25, 41, 53, 54, 61, 180 | chnind 33001 |
. . 3
⊢ (𝜑 → (0 <
(♯‘𝑇) →
((𝑊 ↾s
(lastS‘𝑇))/FldExt(𝑊 ↾s (𝑇‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑇))[:](𝑊 ↾s (𝑇‘0))) = (2↑𝑛)))) |
| 182 | 1, 181 | mpd 15 |
. 2
⊢ (𝜑 → ((𝑊 ↾s (lastS‘𝑇))/FldExt(𝑊 ↾s (𝑇‘0)) ∧ ∃𝑛 ∈ ℕ0
((𝑊 ↾s
(lastS‘𝑇))[:](𝑊 ↾s (𝑇‘0))) = (2↑𝑛))) |
| 183 | | fldext2chn.2 |
. . . 4
⊢ (𝜑 → (𝑊 ↾s (lastS‘𝑇)) = 𝐿) |
| 184 | | fldext2chn.1 |
. . . 4
⊢ (𝜑 → (𝑊 ↾s (𝑇‘0)) = 𝑄) |
| 185 | 183, 184 | breq12d 5156 |
. . 3
⊢ (𝜑 → ((𝑊 ↾s (lastS‘𝑇))/FldExt(𝑊 ↾s (𝑇‘0)) ↔ 𝐿/FldExt𝑄)) |
| 186 | 183, 184 | oveq12d 7449 |
. . . . 5
⊢ (𝜑 → ((𝑊 ↾s (lastS‘𝑇))[:](𝑊 ↾s (𝑇‘0))) = (𝐿[:]𝑄)) |
| 187 | 186 | eqeq1d 2739 |
. . . 4
⊢ (𝜑 → (((𝑊 ↾s (lastS‘𝑇))[:](𝑊 ↾s (𝑇‘0))) = (2↑𝑛) ↔ (𝐿[:]𝑄) = (2↑𝑛))) |
| 188 | 187 | rexbidv 3179 |
. . 3
⊢ (𝜑 → (∃𝑛 ∈ ℕ0 ((𝑊 ↾s
(lastS‘𝑇))[:](𝑊 ↾s (𝑇‘0))) = (2↑𝑛) ↔ ∃𝑛 ∈ ℕ0
(𝐿[:]𝑄) = (2↑𝑛))) |
| 189 | 185, 188 | anbi12d 632 |
. 2
⊢ (𝜑 → (((𝑊 ↾s (lastS‘𝑇))/FldExt(𝑊 ↾s (𝑇‘0)) ∧ ∃𝑛 ∈ ℕ0
((𝑊 ↾s
(lastS‘𝑇))[:](𝑊 ↾s (𝑇‘0))) = (2↑𝑛)) ↔ (𝐿/FldExt𝑄 ∧ ∃𝑛 ∈ ℕ0 (𝐿[:]𝑄) = (2↑𝑛)))) |
| 190 | 182, 189 | mpbid 232 |
1
⊢ (𝜑 → (𝐿/FldExt𝑄 ∧ ∃𝑛 ∈ ℕ0 (𝐿[:]𝑄) = (2↑𝑛))) |