Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fldext2chn Structured version   Visualization version   GIF version

Theorem fldext2chn 33769
Description: In a non-empty chain 𝑇 of quadratic field extensions, the degree of the final extension is always a power of two. (Contributed by Thierry Arnoux, 19-Oct-2025.)
Hypotheses
Ref Expression
fldext2chn.e 𝐸 = (𝑊s 𝑒)
fldext2chn.f 𝐹 = (𝑊s 𝑓)
fldext2chn.l < = {⟨𝑓, 𝑒⟩ ∣ (𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 2)}
fldext2chn.t (𝜑𝑇 ∈ ( < Chain(SubDRing‘𝑊)))
fldext2chn.w (𝜑𝑊 ∈ Field)
fldext2chn.1 (𝜑 → (𝑊s (𝑇‘0)) = 𝑄)
fldext2chn.2 (𝜑 → (𝑊s (lastS‘𝑇)) = 𝐿)
fldext2chn.3 (𝜑 → 0 < (♯‘𝑇))
Assertion
Ref Expression
fldext2chn (𝜑 → (𝐿/FldExt𝑄 ∧ ∃𝑛 ∈ ℕ0 (𝐿[:]𝑄) = (2↑𝑛)))
Distinct variable groups:   𝑇,𝑛   𝑛,𝑊   𝑒,𝑊,𝑓   𝜑,𝑛
Allowed substitution hints:   𝜑(𝑒,𝑓)   𝑄(𝑒,𝑓,𝑛)   < (𝑒,𝑓,𝑛)   𝑇(𝑒,𝑓)   𝐸(𝑒,𝑓,𝑛)   𝐹(𝑒,𝑓,𝑛)   𝐿(𝑒,𝑓,𝑛)

Proof of Theorem fldext2chn
Dummy variables 𝑐 𝑑 𝑔 𝑚 𝑜 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fldext2chn.3 . . 3 (𝜑 → 0 < (♯‘𝑇))
2 fveq2 6906 . . . . . 6 (𝑑 = ∅ → (♯‘𝑑) = (♯‘∅))
32breq2d 5155 . . . . 5 (𝑑 = ∅ → (0 < (♯‘𝑑) ↔ 0 < (♯‘∅)))
4 fveq2 6906 . . . . . . . 8 (𝑑 = ∅ → (lastS‘𝑑) = (lastS‘∅))
54oveq2d 7447 . . . . . . 7 (𝑑 = ∅ → (𝑊s (lastS‘𝑑)) = (𝑊s (lastS‘∅)))
6 fveq1 6905 . . . . . . . 8 (𝑑 = ∅ → (𝑑‘0) = (∅‘0))
76oveq2d 7447 . . . . . . 7 (𝑑 = ∅ → (𝑊s (𝑑‘0)) = (𝑊s (∅‘0)))
85, 7breq12d 5156 . . . . . 6 (𝑑 = ∅ → ((𝑊s (lastS‘𝑑))/FldExt(𝑊s (𝑑‘0)) ↔ (𝑊s (lastS‘∅))/FldExt(𝑊s (∅‘0))))
95, 7oveq12d 7449 . . . . . . . 8 (𝑑 = ∅ → ((𝑊s (lastS‘𝑑))[:](𝑊s (𝑑‘0))) = ((𝑊s (lastS‘∅))[:](𝑊s (∅‘0))))
109eqeq1d 2739 . . . . . . 7 (𝑑 = ∅ → (((𝑊s (lastS‘𝑑))[:](𝑊s (𝑑‘0))) = (2↑𝑛) ↔ ((𝑊s (lastS‘∅))[:](𝑊s (∅‘0))) = (2↑𝑛)))
1110rexbidv 3179 . . . . . 6 (𝑑 = ∅ → (∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑑))[:](𝑊s (𝑑‘0))) = (2↑𝑛) ↔ ∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘∅))[:](𝑊s (∅‘0))) = (2↑𝑛)))
128, 11anbi12d 632 . . . . 5 (𝑑 = ∅ → (((𝑊s (lastS‘𝑑))/FldExt(𝑊s (𝑑‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑑))[:](𝑊s (𝑑‘0))) = (2↑𝑛)) ↔ ((𝑊s (lastS‘∅))/FldExt(𝑊s (∅‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘∅))[:](𝑊s (∅‘0))) = (2↑𝑛))))
133, 12imbi12d 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 (𝑑 = 𝑐 → (♯‘𝑑) = (♯‘𝑐))
1514breq2d 5155 . . . . 5 (𝑑 = 𝑐 → (0 < (♯‘𝑑) ↔ 0 < (♯‘𝑐)))
16 fveq2 6906 . . . . . . . 8 (𝑑 = 𝑐 → (lastS‘𝑑) = (lastS‘𝑐))
1716oveq2d 7447 . . . . . . 7 (𝑑 = 𝑐 → (𝑊s (lastS‘𝑑)) = (𝑊s (lastS‘𝑐)))
18 fveq1 6905 . . . . . . . 8 (𝑑 = 𝑐 → (𝑑‘0) = (𝑐‘0))
1918oveq2d 7447 . . . . . . 7 (𝑑 = 𝑐 → (𝑊s (𝑑‘0)) = (𝑊s (𝑐‘0)))
2017, 19breq12d 5156 . . . . . 6 (𝑑 = 𝑐 → ((𝑊s (lastS‘𝑑))/FldExt(𝑊s (𝑑‘0)) ↔ (𝑊s (lastS‘𝑐))/FldExt(𝑊s (𝑐‘0))))
2117, 19oveq12d 7449 . . . . . . . 8 (𝑑 = 𝑐 → ((𝑊s (lastS‘𝑑))[:](𝑊s (𝑑‘0))) = ((𝑊s (lastS‘𝑐))[:](𝑊s (𝑐‘0))))
2221eqeq1d 2739 . . . . . . 7 (𝑑 = 𝑐 → (((𝑊s (lastS‘𝑑))[:](𝑊s (𝑑‘0))) = (2↑𝑛) ↔ ((𝑊s (lastS‘𝑐))[:](𝑊s (𝑐‘0))) = (2↑𝑛)))
2322rexbidv 3179 . . . . . 6 (𝑑 = 𝑐 → (∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑑))[:](𝑊s (𝑑‘0))) = (2↑𝑛) ↔ ∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑐))[:](𝑊s (𝑐‘0))) = (2↑𝑛)))
2420, 23anbi12d 632 . . . . 5 (𝑑 = 𝑐 → (((𝑊s (lastS‘𝑑))/FldExt(𝑊s (𝑑‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑑))[:](𝑊s (𝑑‘0))) = (2↑𝑛)) ↔ ((𝑊s (lastS‘𝑐))/FldExt(𝑊s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑐))[:](𝑊s (𝑐‘0))) = (2↑𝑛))))
2515, 24imbi12d 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 (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (♯‘𝑑) = (♯‘(𝑐 ++ ⟨“𝑔”⟩)))
2726breq2d 5155 . . . . 5 (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (0 < (♯‘𝑑) ↔ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))))
28 fveq2 6906 . . . . . . . 8 (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (lastS‘𝑑) = (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))
2928oveq2d 7447 . . . . . . 7 (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (𝑊s (lastS‘𝑑)) = (𝑊s (lastS‘(𝑐 ++ ⟨“𝑔”⟩))))
30 fveq1 6905 . . . . . . . 8 (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (𝑑‘0) = ((𝑐 ++ ⟨“𝑔”⟩)‘0))
3130oveq2d 7447 . . . . . . 7 (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (𝑊s (𝑑‘0)) = (𝑊s ((𝑐 ++ ⟨“𝑔”⟩)‘0)))
3229, 31breq12d 5156 . . . . . 6 (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → ((𝑊s (lastS‘𝑑))/FldExt(𝑊s (𝑑‘0)) ↔ (𝑊s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))/FldExt(𝑊s ((𝑐 ++ ⟨“𝑔”⟩)‘0))))
3329, 31oveq12d 7449 . . . . . . . . 9 (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → ((𝑊s (lastS‘𝑑))[:](𝑊s (𝑑‘0))) = ((𝑊s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊s ((𝑐 ++ ⟨“𝑔”⟩)‘0))))
3433eqeq1d 2739 . . . . . . . 8 (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (((𝑊s (lastS‘𝑑))[:](𝑊s (𝑑‘0))) = (2↑𝑛) ↔ ((𝑊s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑛)))
3534rexbidv 3179 . . . . . . 7 (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑑))[:](𝑊s (𝑑‘0))) = (2↑𝑛) ↔ ∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑛)))
36 oveq2 7439 . . . . . . . . 9 (𝑛 = 𝑚 → (2↑𝑛) = (2↑𝑚))
3736eqeq2d 2748 . . . . . . . 8 (𝑛 = 𝑚 → (((𝑊s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑛) ↔ ((𝑊s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚)))
3837cbvrexvw 3238 . . . . . . 7 (∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑛) ↔ ∃𝑚 ∈ ℕ0 ((𝑊s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚))
3935, 38bitrdi 287 . . . . . 6 (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑑))[:](𝑊s (𝑑‘0))) = (2↑𝑛) ↔ ∃𝑚 ∈ ℕ0 ((𝑊s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚)))
4032, 39anbi12d 632 . . . . 5 (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (((𝑊s (lastS‘𝑑))/FldExt(𝑊s (𝑑‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑑))[:](𝑊s (𝑑‘0))) = (2↑𝑛)) ↔ ((𝑊s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))/FldExt(𝑊s ((𝑐 ++ ⟨“𝑔”⟩)‘0)) ∧ ∃𝑚 ∈ ℕ0 ((𝑊s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚))))
4127, 40imbi12d 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 (𝑑 = 𝑇 → (♯‘𝑑) = (♯‘𝑇))
4342breq2d 5155 . . . . 5 (𝑑 = 𝑇 → (0 < (♯‘𝑑) ↔ 0 < (♯‘𝑇)))
44 fveq2 6906 . . . . . . . 8 (𝑑 = 𝑇 → (lastS‘𝑑) = (lastS‘𝑇))
4544oveq2d 7447 . . . . . . 7 (𝑑 = 𝑇 → (𝑊s (lastS‘𝑑)) = (𝑊s (lastS‘𝑇)))
46 fveq1 6905 . . . . . . . 8 (𝑑 = 𝑇 → (𝑑‘0) = (𝑇‘0))
4746oveq2d 7447 . . . . . . 7 (𝑑 = 𝑇 → (𝑊s (𝑑‘0)) = (𝑊s (𝑇‘0)))
4845, 47breq12d 5156 . . . . . 6 (𝑑 = 𝑇 → ((𝑊s (lastS‘𝑑))/FldExt(𝑊s (𝑑‘0)) ↔ (𝑊s (lastS‘𝑇))/FldExt(𝑊s (𝑇‘0))))
4945, 47oveq12d 7449 . . . . . . . 8 (𝑑 = 𝑇 → ((𝑊s (lastS‘𝑑))[:](𝑊s (𝑑‘0))) = ((𝑊s (lastS‘𝑇))[:](𝑊s (𝑇‘0))))
5049eqeq1d 2739 . . . . . . 7 (𝑑 = 𝑇 → (((𝑊s (lastS‘𝑑))[:](𝑊s (𝑑‘0))) = (2↑𝑛) ↔ ((𝑊s (lastS‘𝑇))[:](𝑊s (𝑇‘0))) = (2↑𝑛)))
5150rexbidv 3179 . . . . . 6 (𝑑 = 𝑇 → (∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑑))[:](𝑊s (𝑑‘0))) = (2↑𝑛) ↔ ∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑇))[:](𝑊s (𝑇‘0))) = (2↑𝑛)))
5248, 51anbi12d 632 . . . . 5 (𝑑 = 𝑇 → (((𝑊s (lastS‘𝑑))/FldExt(𝑊s (𝑑‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑑))[:](𝑊s (𝑑‘0))) = (2↑𝑛)) ↔ ((𝑊s (lastS‘𝑇))/FldExt(𝑊s (𝑇‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑇))[:](𝑊s (𝑇‘0))) = (2↑𝑛))))
5343, 52imbi12d 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 ∈ ℝ
5655ltnri 11370 . . . . . . 7 ¬ 0 < 0
5756a1i 11 . . . . . 6 (𝜑 → ¬ 0 < 0)
58 hash0 14406 . . . . . . 7 (♯‘∅) = 0
5958breq2i 5151 . . . . . 6 (0 < (♯‘∅) ↔ 0 < 0)
6057, 59sylnibr 329 . . . . 5 (𝜑 → ¬ 0 < (♯‘∅))
6160pm2.21d 121 . . . 4 (𝜑 → (0 < (♯‘∅) → ((𝑊s (lastS‘∅))/FldExt(𝑊s (∅‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘∅))[:](𝑊s (∅‘0))) = (2↑𝑛))))
62 fldext2chn.w . . . . . . . . . . 11 (𝜑𝑊 ∈ Field)
6362ad6antr 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)
6663, 64, 65syl2anc 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 𝑔))
6866, 67syl 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‘𝑊)))
7069chnwrd 32997 . . . . . . . . . . 11 ((((((𝜑𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊s (lastS‘𝑐))/FldExt(𝑊s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑐))[:](𝑊s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) → 𝑐 ∈ Word (SubDRing‘𝑊))
7170adantr 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‘(𝑐 ++ ⟨“𝑔”⟩)) = 𝑔)
7371, 64, 72syl2anc 584 . . . . . . . . 9 (((((((𝜑𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊s (lastS‘𝑐))/FldExt(𝑊s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑐))[:](𝑊s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (lastS‘(𝑐 ++ ⟨“𝑔”⟩)) = 𝑔)
7473oveq2d 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 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → 𝑐 = ∅)
7675oveq1d 7446 . . . . . . . . . . . 12 (((((((𝜑𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊s (lastS‘𝑐))/FldExt(𝑊s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑐))[:](𝑊s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (𝑐 ++ ⟨“𝑔”⟩) = (∅ ++ ⟨“𝑔”⟩))
77 s0s1 14961 . . . . . . . . . . . 12 ⟨“𝑔”⟩ = (∅ ++ ⟨“𝑔”⟩)
7876, 77eqtr4di 2795 . . . . . . . . . . 11 (((((((𝜑𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊s (lastS‘𝑐))/FldExt(𝑊s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑐))[:](𝑊s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (𝑐 ++ ⟨“𝑔”⟩) = ⟨“𝑔”⟩)
7978fveq1d 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) = 𝑔)
8164, 80syl 17 . . . . . . . . . 10 (((((((𝜑𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊s (lastS‘𝑐))/FldExt(𝑊s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑐))[:](𝑊s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (⟨“𝑔”⟩‘0) = 𝑔)
8279, 81eqtrd 2777 . . . . . . . . 9 (((((((𝜑𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊s (lastS‘𝑐))/FldExt(𝑊s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑐))[:](𝑊s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → ((𝑐 ++ ⟨“𝑔”⟩)‘0) = 𝑔)
8382oveq2d 7447 . . . . . . . 8 (((((((𝜑𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊s (lastS‘𝑐))/FldExt(𝑊s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑐))[:](𝑊s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (𝑊s ((𝑐 ++ ⟨“𝑔”⟩)‘0)) = (𝑊s 𝑔))
8468, 74, 833brtr4d 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)
8886, 87ax-mp 5 . . . . . . . . . 10 (2↑0) = 1
8985, 88eqtrdi 2793 . . . . . . . . 9 (𝑚 = 0 → (2↑𝑚) = 1)
9089eqeq2d 2748 . . . . . . . 8 (𝑚 = 0 → (((𝑊s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚) ↔ ((𝑊s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = 1))
91 0nn0 12541 . . . . . . . . 9 0 ∈ ℕ0
9291a1i 11 . . . . . . . 8 (((((((𝜑𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊s (lastS‘𝑐))/FldExt(𝑊s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑐))[:](𝑊s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → 0 ∈ ℕ0)
9374, 83oveq12d 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)
9566, 94syl 17 . . . . . . . . 9 (((((((𝜑𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊s (lastS‘𝑐))/FldExt(𝑊s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑐))[:](𝑊s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → ((𝑊s 𝑔)[:](𝑊s 𝑔)) = 1)
9693, 95eqtrd 2777 . . . . . . . 8 (((((((𝜑𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊s (lastS‘𝑐))/FldExt(𝑊s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑐))[:](𝑊s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → ((𝑊s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = 1)
9790, 92, 96rspcedvdw 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↑𝑚))
9884, 97jca 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↑𝑜)) → 𝑐 ≠ ∅)
101100neneqd 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↑𝑜)) → ¬ 𝑐 = ∅)
10299, 101orcnd 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‘𝑐) < 𝑔)
10370ad3antrrr 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‘𝑊))
105103, 100, 104syl2anc 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 𝑓)
109107, 108breq12i 5152 . . . . . . . . . . . . . . . . 17 (𝐸/FldExt𝐹 ↔ (𝑊s 𝑒)/FldExt(𝑊s 𝑓))
110107, 108oveq12i 7443 . . . . . . . . . . . . . . . . . 18 (𝐸[:]𝐹) = ((𝑊s 𝑒)[:](𝑊s 𝑓))
111110eqeq1i 2742 . . . . . . . . . . . . . . . . 17 ((𝐸[:]𝐹) = 2 ↔ ((𝑊s 𝑒)[:](𝑊s 𝑓)) = 2)
112109, 111anbi12i 628 . . . . . . . . . . . . . . . 16 ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 2) ↔ ((𝑊s 𝑒)/FldExt(𝑊s 𝑓) ∧ ((𝑊s 𝑒)[:](𝑊s 𝑓)) = 2))
113 oveq2 7439 . . . . . . . . . . . . . . . . . . 19 (𝑒 = 𝑔 → (𝑊s 𝑒) = (𝑊s 𝑔))
114113adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝑒 = 𝑔𝑓 = (lastS‘𝑐)) → (𝑊s 𝑒) = (𝑊s 𝑔))
115 oveq2 7439 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (lastS‘𝑐) → (𝑊s 𝑓) = (𝑊s (lastS‘𝑐)))
116115adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝑒 = 𝑔𝑓 = (lastS‘𝑐)) → (𝑊s 𝑓) = (𝑊s (lastS‘𝑐)))
117114, 116breq12d 5156 . . . . . . . . . . . . . . . . 17 ((𝑒 = 𝑔𝑓 = (lastS‘𝑐)) → ((𝑊s 𝑒)/FldExt(𝑊s 𝑓) ↔ (𝑊s 𝑔)/FldExt(𝑊s (lastS‘𝑐))))
118114, 116oveq12d 7449 . . . . . . . . . . . . . . . . . 18 ((𝑒 = 𝑔𝑓 = (lastS‘𝑐)) → ((𝑊s 𝑒)[:](𝑊s 𝑓)) = ((𝑊s 𝑔)[:](𝑊s (lastS‘𝑐))))
119118eqeq1d 2739 . . . . . . . . . . . . . . . . 17 ((𝑒 = 𝑔𝑓 = (lastS‘𝑐)) → (((𝑊s 𝑒)[:](𝑊s 𝑓)) = 2 ↔ ((𝑊s 𝑔)[:](𝑊s (lastS‘𝑐))) = 2))
120117, 119anbi12d 632 . . . . . . . . . . . . . . . 16 ((𝑒 = 𝑔𝑓 = (lastS‘𝑐)) → (((𝑊s 𝑒)/FldExt(𝑊s 𝑓) ∧ ((𝑊s 𝑒)[:](𝑊s 𝑓)) = 2) ↔ ((𝑊s 𝑔)/FldExt(𝑊s (lastS‘𝑐)) ∧ ((𝑊s 𝑔)[:](𝑊s (lastS‘𝑐))) = 2)))
121112, 120bitrid 283 . . . . . . . . . . . . . . 15 ((𝑒 = 𝑔𝑓 = (lastS‘𝑐)) → ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 2) ↔ ((𝑊s 𝑔)/FldExt(𝑊s (lastS‘𝑐)) ∧ ((𝑊s 𝑔)[:](𝑊s (lastS‘𝑐))) = 2)))
122121ancoms 458 . . . . . . . . . . . . . 14 ((𝑓 = (lastS‘𝑐) ∧ 𝑒 = 𝑔) → ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 2) ↔ ((𝑊s 𝑔)/FldExt(𝑊s (lastS‘𝑐)) ∧ ((𝑊s 𝑔)[:](𝑊s (lastS‘𝑐))) = 2)))
123 fldext2chn.l . . . . . . . . . . . . . 14 < = {⟨𝑓, 𝑒⟩ ∣ (𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 2)}
124122, 123brabga 5539 . . . . . . . . . . . . 13 (((lastS‘𝑐) ∈ (SubDRing‘𝑊) ∧ 𝑔 ∈ (SubDRing‘𝑊)) → ((lastS‘𝑐) < 𝑔 ↔ ((𝑊s 𝑔)/FldExt(𝑊s (lastS‘𝑐)) ∧ ((𝑊s 𝑔)[:](𝑊s (lastS‘𝑐))) = 2)))
125105, 106, 124syl2anc 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)))
126102, 125mpbid 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))
127126simpld 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 < (♯‘𝑐))
12969, 128sylan 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↑𝑛))))
131129, 130mpd 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↑𝑛)))
132131simprd 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↑𝑜))
134133eqeq2d 2748 . . . . . . . . . . . 12 (𝑛 = 𝑜 → (((𝑊s (lastS‘𝑐))[:](𝑊s (𝑐‘0))) = (2↑𝑛) ↔ ((𝑊s (lastS‘𝑐))[:](𝑊s (𝑐‘0))) = (2↑𝑜)))
135134cbvrexvw 3238 . . . . . . . . . . 11 (∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑐))[:](𝑊s (𝑐‘0))) = (2↑𝑛) ↔ ∃𝑜 ∈ ℕ0 ((𝑊s (lastS‘𝑐))[:](𝑊s (𝑐‘0))) = (2↑𝑜))
136132, 135sylib 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↑𝑜))
137127, 136r19.29a 3162 . . . . . . . . 9 (((((((𝜑𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊s (lastS‘𝑐))/FldExt(𝑊s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑐))[:](𝑊s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → (𝑊s 𝑔)/FldExt(𝑊s (lastS‘𝑐)))
138131simpld 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)))
140137, 138, 139syl2anc 584 . . . . . . . 8 (((((((𝜑𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊s (lastS‘𝑐))/FldExt(𝑊s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑐))[:](𝑊s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → (𝑊s 𝑔)/FldExt(𝑊s (𝑐‘0)))
141103, 106, 72syl2anc 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‘(𝑐 ++ ⟨“𝑔”⟩)) = 𝑔)
142141oveq2d 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 𝑔))
143142, 136r19.29a 3162 . . . . . . . 8 (((((((𝜑𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊s (lastS‘𝑐))/FldExt(𝑊s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑐))[:](𝑊s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → (𝑊s (lastS‘(𝑐 ++ ⟨“𝑔”⟩))) = (𝑊s 𝑔))
144106s1cld 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‘𝑊))
145129ad2antrr 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))
147103, 144, 145, 146syl3anc 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))
148147oveq2d 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)))
149148, 136r19.29a 3162 . . . . . . . 8 (((((((𝜑𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊s (lastS‘𝑐))/FldExt(𝑊s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑐))[:](𝑊s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → (𝑊s ((𝑐 ++ ⟨“𝑔”⟩)‘0)) = (𝑊s (𝑐‘0)))
150140, 143, 1493brtr4d 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)))
152151eqeq2d 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
155154a1i 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)
156153, 155nn0addcld 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)
157142, 148oveq12d 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))))
158138ad2antrr 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)))))
160127, 158, 159syl2anc 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)))))
16186a1i 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 ∈ ℂ)
162161, 153expcld 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↑𝑜) ∈ ℂ)
163161, 162mulcomd 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))
164126simprd 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↑𝑜))
166164, 165oveq12d 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 ∈ ℝ
168167a1i 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 ∈ ℝ)
169168, 153reexpcld 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↑𝑜)))
171168, 169, 170syl2anc 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↑𝑜)))
172166, 171eqtrd 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↑𝑜)))
173161, 153expp1d 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))
174163, 172, 1733eqtr4d 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)))
175157, 160, 1743eqtrd 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)))
176152, 156, 175rspcedvdw 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↑𝑚))
177176, 136r19.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↑𝑚))
178150, 177jca 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↑𝑚)))
17998, 178pm2.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↑𝑚)))
180179ex 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↑𝑚))))
18113, 25, 41, 53, 54, 61, 180chnind 33001 . . 3 (𝜑 → (0 < (♯‘𝑇) → ((𝑊s (lastS‘𝑇))/FldExt(𝑊s (𝑇‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑇))[:](𝑊s (𝑇‘0))) = (2↑𝑛))))
1821, 181mpd 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)) = 𝑄)
185183, 184breq12d 5156 . . 3 (𝜑 → ((𝑊s (lastS‘𝑇))/FldExt(𝑊s (𝑇‘0)) ↔ 𝐿/FldExt𝑄))
186183, 184oveq12d 7449 . . . . 5 (𝜑 → ((𝑊s (lastS‘𝑇))[:](𝑊s (𝑇‘0))) = (𝐿[:]𝑄))
187186eqeq1d 2739 . . . 4 (𝜑 → (((𝑊s (lastS‘𝑇))[:](𝑊s (𝑇‘0))) = (2↑𝑛) ↔ (𝐿[:]𝑄) = (2↑𝑛)))
188187rexbidv 3179 . . 3 (𝜑 → (∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑇))[:](𝑊s (𝑇‘0))) = (2↑𝑛) ↔ ∃𝑛 ∈ ℕ0 (𝐿[:]𝑄) = (2↑𝑛)))
189185, 188anbi12d 632 . 2 (𝜑 → (((𝑊s (lastS‘𝑇))/FldExt(𝑊s (𝑇‘0)) ∧ ∃𝑛 ∈ ℕ0 ((𝑊s (lastS‘𝑇))[:](𝑊s (𝑇‘0))) = (2↑𝑛)) ↔ (𝐿/FldExt𝑄 ∧ ∃𝑛 ∈ ℕ0 (𝐿[:]𝑄) = (2↑𝑛))))
190182, 189mpbid 232 1 (𝜑 → (𝐿/FldExt𝑄 ∧ ∃𝑛 ∈ ℕ0 (𝐿[:]𝑄) = (2↑𝑛)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 848   = wceq 1540  wcel 2108  wne 2940  wrex 3070  c0 4333   class class class wbr 5143  {copab 5205  cfv 6561  (class class class)co 7431  cc 11153  cr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160   < clt 11295  2c2 12321  0cn0 12526   ·e cxmu 13153  cexp 14102  chash 14369  Word cword 14552  lastSclsw 14600   ++ cconcat 14608  ⟨“cs1 14633  s cress 17274  Fieldcfield 20730  SubDRingcsdrg 20787  Chaincchn 32994  /FldExtcfldext 33689  [:]cextdg 33692
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-reg 9632  ax-inf2 9681  ax-ac2 10503  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-rpss 7743  df-om 7888  df-1st 8014  df-2nd 8015  df-supp 8186  df-tpos 8251  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-oadd 8510  df-er 8745  df-map 8868  df-ixp 8938  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fsupp 9402  df-sup 9482  df-oi 9550  df-r1 9804  df-rank 9805  df-dju 9941  df-card 9979  df-acn 9982  df-ac 10156  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-xnn0 12600  df-z 12614  df-dec 12734  df-uz 12879  df-rp 13035  df-xmul 13156  df-fz 13548  df-fzo 13695  df-seq 14043  df-exp 14103  df-hash 14370  df-word 14553  df-lsw 14601  df-concat 14609  df-s1 14634  df-substr 14679  df-pfx 14709  df-struct 17184  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-mulr 17311  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ocomp 17318  df-ds 17319  df-hom 17321  df-cco 17322  df-0g 17486  df-gsum 17487  df-prds 17492  df-pws 17494  df-mre 17629  df-mrc 17630  df-mri 17631  df-acs 17632  df-proset 18340  df-drs 18341  df-poset 18359  df-ipo 18573  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-mhm 18796  df-submnd 18797  df-grp 18954  df-minusg 18955  df-sbg 18956  df-mulg 19086  df-subg 19141  df-ghm 19231  df-cntz 19335  df-cmn 19800  df-abl 19801  df-mgp 20138  df-rng 20150  df-ur 20179  df-ring 20232  df-cring 20233  df-oppr 20334  df-dvdsr 20357  df-unit 20358  df-invr 20388  df-nzr 20513  df-subrng 20546  df-subrg 20570  df-drng 20731  df-field 20732  df-sdrg 20788  df-lmod 20860  df-lss 20930  df-lsp 20970  df-lmhm 21021  df-lbs 21074  df-lvec 21102  df-sra 21172  df-rgmod 21173  df-lidl 21218  df-rsp 21219  df-dsmm 21752  df-frlm 21767  df-uvc 21803  df-lindf 21826  df-linds 21827  df-chn 32995  df-dim 33650  df-fldext 33693  df-extdg 33694
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator