fldext2chn - Mathbox for Thierry Arnoux

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

Theorem fldext2chn 33866

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𝑄 ∧ ∃𝑛 ∈ ℕ₀ (𝐿[:]𝑄) = (2↑𝑛)))

Distinct variable groups: 𝑇,𝑛 𝑛,𝑊 𝑒,𝑊,𝑓 𝜑,𝑛 Allowed substitution hints: 𝜑(𝑒,𝑓) 𝑄(𝑒,𝑓,𝑛) < (𝑒,𝑓,𝑛) 𝑇(𝑒,𝑓) 𝐸(𝑒,𝑓,𝑛) 𝐹(𝑒,𝑓,𝑛) 𝐿(𝑒,𝑓,𝑛)

Proof of Theorem fldext2chn Dummy variables 𝑐 𝑑 𝑔 𝑚 𝑜 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fldext2chn.3	. . 3 ⊢ (𝜑 → 0 < (♯‘𝑇))
2		fveq2 6835	. . . . . 6 ⊢ (𝑑 = ∅ → (♯‘𝑑) = (♯‘∅))
3	2	breq2d 5111	. . . . 5 ⊢ (𝑑 = ∅ → (0 < (♯‘𝑑) ↔ 0 < (♯‘∅)))
4		fveq2 6835	. . . . . . . 8 ⊢ (𝑑 = ∅ → (lastS‘𝑑) = (lastS‘∅))
5	4	oveq2d 7376	. . . . . . 7 ⊢ (𝑑 = ∅ → (𝑊 ↾_s (lastS‘𝑑)) = (𝑊 ↾_s (lastS‘∅)))
6		fveq1 6834	. . . . . . . 8 ⊢ (𝑑 = ∅ → (𝑑‘0) = (∅‘0))
7	6	oveq2d 7376	. . . . . . 7 ⊢ (𝑑 = ∅ → (𝑊 ↾_s (𝑑‘0)) = (𝑊 ↾_s (∅‘0)))
8	5, 7	breq12d 5112	. . . . . 6 ⊢ (𝑑 = ∅ → ((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ↔ (𝑊 ↾_s (lastS‘∅))/_FldExt(𝑊 ↾_s (∅‘0))))
9	5, 7	oveq12d 7378	. . . . . . . 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 3161	. . . . . 6 ⊢ (𝑑 = ∅ → (∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘∅))[:](𝑊 ↾_s (∅‘0))) = (2↑𝑛)))
12	8, 11	anbi12d 633	. . . . 5 ⊢ (𝑑 = ∅ → (((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛)) ↔ ((𝑊 ↾_s (lastS‘∅))/_FldExt(𝑊 ↾_s (∅‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘∅))[:](𝑊 ↾_s (∅‘0))) = (2↑𝑛))))
13	3, 12	imbi12d 344	. . . 4 ⊢ (𝑑 = ∅ → ((0 < (♯‘𝑑) → ((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛))) ↔ (0 < (♯‘∅) → ((𝑊 ↾_s (lastS‘∅))/_FldExt(𝑊 ↾_s (∅‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘∅))[:](𝑊 ↾_s (∅‘0))) = (2↑𝑛)))))
14		fveq2 6835	. . . . . 6 ⊢ (𝑑 = 𝑐 → (♯‘𝑑) = (♯‘𝑐))
15	14	breq2d 5111	. . . . 5 ⊢ (𝑑 = 𝑐 → (0 < (♯‘𝑑) ↔ 0 < (♯‘𝑐)))
16		fveq2 6835	. . . . . . . 8 ⊢ (𝑑 = 𝑐 → (lastS‘𝑑) = (lastS‘𝑐))
17	16	oveq2d 7376	. . . . . . 7 ⊢ (𝑑 = 𝑐 → (𝑊 ↾_s (lastS‘𝑑)) = (𝑊 ↾_s (lastS‘𝑐)))
18		fveq1 6834	. . . . . . . 8 ⊢ (𝑑 = 𝑐 → (𝑑‘0) = (𝑐‘0))
19	18	oveq2d 7376	. . . . . . 7 ⊢ (𝑑 = 𝑐 → (𝑊 ↾_s (𝑑‘0)) = (𝑊 ↾_s (𝑐‘0)))
20	17, 19	breq12d 5112	. . . . . 6 ⊢ (𝑑 = 𝑐 → ((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ↔ (𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0))))
21	17, 19	oveq12d 7378	. . . . . . . 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 3161	. . . . . 6 ⊢ (𝑑 = 𝑐 → (∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))
24	20, 23	anbi12d 633	. . . . 5 ⊢ (𝑑 = 𝑐 → (((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛)) ↔ ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛))))
25	15, 24	imbi12d 344	. . . 4 ⊢ (𝑑 = 𝑐 → ((0 < (♯‘𝑑) → ((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛))) ↔ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))))
26		fveq2 6835	. . . . . 6 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (♯‘𝑑) = (♯‘(𝑐 ++ ⟨“𝑔”⟩)))
27	26	breq2d 5111	. . . . 5 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (0 < (♯‘𝑑) ↔ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))))
28		fveq2 6835	. . . . . . . 8 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (lastS‘𝑑) = (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))
29	28	oveq2d 7376	. . . . . . 7 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (𝑊 ↾_s (lastS‘𝑑)) = (𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩))))
30		fveq1 6834	. . . . . . . 8 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (𝑑‘0) = ((𝑐 ++ ⟨“𝑔”⟩)‘0))
31	30	oveq2d 7376	. . . . . . 7 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (𝑊 ↾_s (𝑑‘0)) = (𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0)))
32	29, 31	breq12d 5112	. . . . . 6 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → ((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ↔ (𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))/_FldExt(𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))))
33	29, 31	oveq12d 7378	. . . . . . . . 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 3161	. . . . . . 7 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑛)))
36		oveq2 7368	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → (2↑𝑛) = (2↑𝑚))
37	36	eqeq2d 2748	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → (((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑛) ↔ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚)))
38	37	cbvrexvw 3216	. . . . . . 7 ⊢ (∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑛) ↔ ∃𝑚 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚))
39	35, 38	bitrdi 287	. . . . . 6 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ∃𝑚 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚)))
40	32, 39	anbi12d 633	. . . . 5 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛)) ↔ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))/_FldExt(𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0)) ∧ ∃𝑚 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚))))
41	27, 40	imbi12d 344	. . . 4 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → ((0 < (♯‘𝑑) → ((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛))) ↔ (0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩)) → ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))/_FldExt(𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0)) ∧ ∃𝑚 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚)))))
42		fveq2 6835	. . . . . 6 ⊢ (𝑑 = 𝑇 → (♯‘𝑑) = (♯‘𝑇))
43	42	breq2d 5111	. . . . 5 ⊢ (𝑑 = 𝑇 → (0 < (♯‘𝑑) ↔ 0 < (♯‘𝑇)))
44		fveq2 6835	. . . . . . . 8 ⊢ (𝑑 = 𝑇 → (lastS‘𝑑) = (lastS‘𝑇))
45	44	oveq2d 7376	. . . . . . 7 ⊢ (𝑑 = 𝑇 → (𝑊 ↾_s (lastS‘𝑑)) = (𝑊 ↾_s (lastS‘𝑇)))
46		fveq1 6834	. . . . . . . 8 ⊢ (𝑑 = 𝑇 → (𝑑‘0) = (𝑇‘0))
47	46	oveq2d 7376	. . . . . . 7 ⊢ (𝑑 = 𝑇 → (𝑊 ↾_s (𝑑‘0)) = (𝑊 ↾_s (𝑇‘0)))
48	45, 47	breq12d 5112	. . . . . 6 ⊢ (𝑑 = 𝑇 → ((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ↔ (𝑊 ↾_s (lastS‘𝑇))/_FldExt(𝑊 ↾_s (𝑇‘0))))
49	45, 47	oveq12d 7378	. . . . . . . 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 3161	. . . . . 6 ⊢ (𝑑 = 𝑇 → (∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (2↑𝑛)))
52	48, 51	anbi12d 633	. . . . 5 ⊢ (𝑑 = 𝑇 → (((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛)) ↔ ((𝑊 ↾_s (lastS‘𝑇))/_FldExt(𝑊 ↾_s (𝑇‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (2↑𝑛))))
53	43, 52	imbi12d 344	. . . 4 ⊢ (𝑑 = 𝑇 → ((0 < (♯‘𝑑) → ((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛))) ↔ (0 < (♯‘𝑇) → ((𝑊 ↾_s (lastS‘𝑇))/_FldExt(𝑊 ↾_s (𝑇‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (2↑𝑛)))))
54		fldext2chn.t	. . . 4 ⊢ (𝜑 → 𝑇 ∈ ( < Chain (SubDRing‘𝑊)))
55		0re 11138	. . . . . . . 8 ⊢ 0 ∈ ℝ
56	55	ltnri 11246	. . . . . . 7 ⊢ ¬ 0 < 0
57	56	a1i 11	. . . . . 6 ⊢ (𝜑 → ¬ 0 < 0)
58		hash0 14294	. . . . . . 7 ⊢ (♯‘∅) = 0
59	58	breq2i 5107	. . . . . 6 ⊢ (0 < (♯‘∅) ↔ 0 < 0)
60	57, 59	sylnibr 329	. . . . 5 ⊢ (𝜑 → ¬ 0 < (♯‘∅))
61	60	pm2.21d 121	. . . 4 ⊢ (𝜑 → (0 < (♯‘∅) → ((𝑊 ↾_s (lastS‘∅))/_FldExt(𝑊 ↾_s (∅‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘∅))[:](𝑊 ↾_s (∅‘0))) = (2↑𝑛))))
62		fldext2chn.w	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 ∈ Field)
63	62	ad6antr 737	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → 𝑊 ∈ Field)
64		simp-5r 786	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → 𝑔 ∈ (SubDRing‘𝑊))
65		fldsdrgfld 20735	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Field ∧ 𝑔 ∈ (SubDRing‘𝑊)) → (𝑊 ↾_s 𝑔) ∈ Field)
66	63, 64, 65	syl2anc 585	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (𝑊 ↾_s 𝑔) ∈ Field)
67		fldextid 33797	. . . . . . . . 9 ⊢ ((𝑊 ↾_s 𝑔) ∈ Field → (𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s 𝑔))
68	66, 67	syl 17	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘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)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) → 𝑐 ∈ ( < Chain (SubDRing‘𝑊)))
70	69	chnwrd 18535	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) → 𝑐 ∈ Word (SubDRing‘𝑊))
71	70	adantr 480	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → 𝑐 ∈ Word (SubDRing‘𝑊))
72		lswccats1 14562	. . . . . . . . . 10 ⊢ ((𝑐 ∈ Word (SubDRing‘𝑊) ∧ 𝑔 ∈ (SubDRing‘𝑊)) → (lastS‘(𝑐 ++ ⟨“𝑔”⟩)) = 𝑔)
73	71, 64, 72	syl2anc 585	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (lastS‘(𝑐 ++ ⟨“𝑔”⟩)) = 𝑔)
74	73	oveq2d 7376	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩))) = (𝑊 ↾_s 𝑔))
75		simpr 484	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → 𝑐 = ∅)
76	75	oveq1d 7375	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (𝑐 ++ ⟨“𝑔”⟩) = (∅ ++ ⟨“𝑔”⟩))
77		s0s1 14849	. . . . . . . . . . . 12 ⊢ ⟨“𝑔”⟩ = (∅ ++ ⟨“𝑔”⟩)
78	76, 77	eqtr4di 2790	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (𝑐 ++ ⟨“𝑔”⟩) = ⟨“𝑔”⟩)
79	78	fveq1d 6837	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → ((𝑐 ++ ⟨“𝑔”⟩)‘0) = (⟨“𝑔”⟩‘0))
80		s1fv 14538	. . . . . . . . . . 11 ⊢ (𝑔 ∈ (SubDRing‘𝑊) → (⟨“𝑔”⟩‘0) = 𝑔)
81	64, 80	syl 17	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (⟨“𝑔”⟩‘0) = 𝑔)
82	79, 81	eqtrd 2772	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → ((𝑐 ++ ⟨“𝑔”⟩)‘0) = 𝑔)
83	82	oveq2d 7376	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0)) = (𝑊 ↾_s 𝑔))
84	68, 74, 83	3brtr4d 5131	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))/_FldExt(𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0)))
85		oveq2 7368	. . . . . . . . . 10 ⊢ (𝑚 = 0 → (2↑𝑚) = (2↑0))
86		2cn 12224	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
87		exp0 13992	. . . . . . . . . . 11 ⊢ (2 ∈ ℂ → (2↑0) = 1)
88	86, 87	ax-mp 5	. . . . . . . . . 10 ⊢ (2↑0) = 1
89	85, 88	eqtrdi 2788	. . . . . . . . 9 ⊢ (𝑚 = 0 → (2↑𝑚) = 1)
90	89	eqeq2d 2748	. . . . . . . 8 ⊢ (𝑚 = 0 → (((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚) ↔ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = 1))
91		0nn0 12420	. . . . . . . . 9 ⊢ 0 ∈ ℕ₀
92	91	a1i 11	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → 0 ∈ ℕ₀)
93	74, 83	oveq12d 7378	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s 𝑔)))
94		extdgid 33798	. . . . . . . . . 10 ⊢ ((𝑊 ↾_s 𝑔) ∈ Field → ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s 𝑔)) = 1)
95	66, 94	syl 17	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s 𝑔)) = 1)
96	93, 95	eqtrd 2772	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = 1)
97	90, 92, 96	rspcedvdw 3580	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → ∃𝑚 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚))
98	84, 97	jca 511	. . . . . 6 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))/_FldExt(𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0)) ∧ ∃𝑚 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚)))
99		simp-6r 788	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔))
100		simpllr 776	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → 𝑐 ≠ ∅)
101	100	neneqd 2938	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → ¬ 𝑐 = ∅)
102	99, 101	orcnd 879	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → (lastS‘𝑐) < 𝑔)
103	70	ad3antrrr 731	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → 𝑐 ∈ Word (SubDRing‘𝑊))
104		lswcl 14495	. . . . . . . . . . . . . 14 ⊢ ((𝑐 ∈ Word (SubDRing‘𝑊) ∧ 𝑐 ≠ ∅) → (lastS‘𝑐) ∈ (SubDRing‘𝑊))
105	103, 100, 104	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → (lastS‘𝑐) ∈ (SubDRing‘𝑊))
106		simp-7r 790	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → 𝑔 ∈ (SubDRing‘𝑊))
107		fldext2chn.e	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐸 = (𝑊 ↾_s 𝑒)
108		fldext2chn.f	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐹 = (𝑊 ↾_s 𝑓)
109	107, 108	breq12i 5108	. . . . . . . . . . . . . . . . 17 ⊢ (𝐸/_FldExt𝐹 ↔ (𝑊 ↾_s 𝑒)/_FldExt(𝑊 ↾_s 𝑓))
110	107, 108	oveq12i 7372	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐸[:]𝐹) = ((𝑊 ↾_s 𝑒)[:](𝑊 ↾_s 𝑓))
111	110	eqeq1i 2742	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐸[:]𝐹) = 2 ↔ ((𝑊 ↾_s 𝑒)[:](𝑊 ↾_s 𝑓)) = 2)
112	109, 111	anbi12i 629	. . . . . . . . . . . . . . . 16 ⊢ ((𝐸/_FldExt𝐹 ∧ (𝐸[:]𝐹) = 2) ↔ ((𝑊 ↾_s 𝑒)/_FldExt(𝑊 ↾_s 𝑓) ∧ ((𝑊 ↾_s 𝑒)[:](𝑊 ↾_s 𝑓)) = 2))
113		oveq2 7368	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑔 → (𝑊 ↾_s 𝑒) = (𝑊 ↾_s 𝑔))
114	113	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → (𝑊 ↾_s 𝑒) = (𝑊 ↾_s 𝑔))
115		oveq2 7368	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (lastS‘𝑐) → (𝑊 ↾_s 𝑓) = (𝑊 ↾_s (lastS‘𝑐)))
116	115	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → (𝑊 ↾_s 𝑓) = (𝑊 ↾_s (lastS‘𝑐)))
117	114, 116	breq12d 5112	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → ((𝑊 ↾_s 𝑒)/_FldExt(𝑊 ↾_s 𝑓) ↔ (𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (lastS‘𝑐))))
118	114, 116	oveq12d 7378	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → ((𝑊 ↾_s 𝑒)[:](𝑊 ↾_s 𝑓)) = ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s (lastS‘𝑐))))
119	118	eqeq1d 2739	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → (((𝑊 ↾_s 𝑒)[:](𝑊 ↾_s 𝑓)) = 2 ↔ ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s (lastS‘𝑐))) = 2))
120	117, 119	anbi12d 633	. . . . . . . . . . . . . . . 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 5483	. . . . . . . . . . . . 13 ⊢ (((lastS‘𝑐) ∈ (SubDRing‘𝑊) ∧ 𝑔 ∈ (SubDRing‘𝑊)) → ((lastS‘𝑐) < 𝑔 ↔ ((𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (lastS‘𝑐)) ∧ ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s (lastS‘𝑐))) = 2)))
125	105, 106, 124	syl2anc 585	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 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)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 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)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → (𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (lastS‘𝑐)))
128		hashgt0 14315	. . . . . . . . . . . . . 14 ⊢ ((𝑐 ∈ ( < Chain (SubDRing‘𝑊)) ∧ 𝑐 ≠ ∅) → 0 < (♯‘𝑐))
129	69, 128	sylan 581	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → 0 < (♯‘𝑐))
130		simpllr 776	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛))))
131	129, 130	mpd 15	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))
132	131	simprd 495	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛))
133		oveq2 7368	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑜 → (2↑𝑛) = (2↑𝑜))
134	133	eqeq2d 2748	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑜 → (((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛) ↔ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)))
135	134	cbvrexvw 3216	. . . . . . . . . . 11 ⊢ (∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛) ↔ ∃𝑜 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜))
136	132, 135	sylib 218	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → ∃𝑜 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜))
137	127, 136	r19.29a 3145	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘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)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → (𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)))
139		fldexttr 33796	. . . . . . . . 9 ⊢ (((𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (lastS‘𝑐)) ∧ (𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0))) → (𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (𝑐‘0)))
140	137, 138, 139	syl2anc 585	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → (𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (𝑐‘0)))
141	103, 106, 72	syl2anc 585	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → (lastS‘(𝑐 ++ ⟨“𝑔”⟩)) = 𝑔)
142	141	oveq2d 7376	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → (𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩))) = (𝑊 ↾_s 𝑔))
143	142, 136	r19.29a 3145	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → (𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩))) = (𝑊 ↾_s 𝑔))
144	106	s1cld 14531	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → ⟨“𝑔”⟩ ∈ Word (SubDRing‘𝑊))
145	129	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → 0 < (♯‘𝑐))
146		ccatfv0 14511	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ Word (SubDRing‘𝑊) ∧ ⟨“𝑔”⟩ ∈ Word (SubDRing‘𝑊) ∧ 0 < (♯‘𝑐)) → ((𝑐 ++ ⟨“𝑔”⟩)‘0) = (𝑐‘0))
147	103, 144, 145, 146	syl3anc 1374	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → ((𝑐 ++ ⟨“𝑔”⟩)‘0) = (𝑐‘0))
148	147	oveq2d 7376	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → (𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0)) = (𝑊 ↾_s (𝑐‘0)))
149	148, 136	r19.29a 3145	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → (𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0)) = (𝑊 ↾_s (𝑐‘0)))
150	140, 143, 149	3brtr4d 5131	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → (𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))/_FldExt(𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0)))
151		oveq2 7368	. . . . . . . . . 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)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → 𝑜 ∈ ℕ₀)
154		1nn0 12421	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ₀
155	154	a1i 11	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → 1 ∈ ℕ₀)
156	153, 155	nn0addcld 12470	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → (𝑜 + 1) ∈ ℕ₀)
157	142, 148	oveq12d 7378	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s (𝑐‘0))))
158	138	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → (𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)))
159		extdgmul 33801	. . . . . . . . . . 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 585	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 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)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → 2 ∈ ℂ)
162	161, 153	expcld 14073	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → (2↑𝑜) ∈ ℂ)
163	161, 162	mulcomd 11157	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 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)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s (lastS‘𝑐))) = 2)
165		simpr 484	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜))
166	164, 165	oveq12d 7378	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → (((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s (lastS‘𝑐))) ·_e ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0)))) = (2 ·_e (2↑𝑜)))
167		2re 12223	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℝ
168	167	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → 2 ∈ ℝ)
169	168, 153	reexpcld 14090	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → (2↑𝑜) ∈ ℝ)
170		rexmul 13190	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ ∧ (2↑𝑜) ∈ ℝ) → (2 ·_e (2↑𝑜)) = (2 · (2↑𝑜)))
171	168, 169, 170	syl2anc 585	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → (2 ·_e (2↑𝑜)) = (2 · (2↑𝑜)))
172	166, 171	eqtrd 2772	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → (((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s (lastS‘𝑐))) ·_e ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0)))) = (2 · (2↑𝑜)))
173	161, 153	expp1d 14074	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → (2↑(𝑜 + 1)) = ((2↑𝑜) · 2))
174	163, 172, 173	3eqtr4d 2782	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → (((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s (lastS‘𝑐))) ·_e ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0)))) = (2↑(𝑜 + 1)))
175	157, 160, 174	3eqtrd 2776	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑(𝑜 + 1)))
176	152, 156, 175	rspcedvdw 3580	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → ∃𝑚 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚))
177	176, 136	r19.29a 3145	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → ∃𝑚 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚))
178	150, 177	jca 511	. . . . . 6 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))/_FldExt(𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0)) ∧ ∃𝑚 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚)))
179	98, 178	pm2.61dane 3020	. . . . 5 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) → ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))/_FldExt(𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0)) ∧ ∃𝑚 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚)))
180	179	ex 412	. . . 4 ⊢ (((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) → (0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩)) → ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))/_FldExt(𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0)) ∧ ∃𝑚 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚))))
181	13, 25, 41, 53, 54, 61, 180	chnind 18548	. . 3 ⊢ (𝜑 → (0 < (♯‘𝑇) → ((𝑊 ↾_s (lastS‘𝑇))/_FldExt(𝑊 ↾_s (𝑇‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (2↑𝑛))))
182	1, 181	mpd 15	. 2 ⊢ (𝜑 → ((𝑊 ↾_s (lastS‘𝑇))/_FldExt(𝑊 ↾_s (𝑇‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (2↑𝑛)))
183		fldext2chn.2	. . . 4 ⊢ (𝜑 → (𝑊 ↾_s (lastS‘𝑇)) = 𝐿)
184		fldext2chn.1	. . . 4 ⊢ (𝜑 → (𝑊 ↾_s (𝑇‘0)) = 𝑄)
185	183, 184	breq12d 5112	. . 3 ⊢ (𝜑 → ((𝑊 ↾_s (lastS‘𝑇))/_FldExt(𝑊 ↾_s (𝑇‘0)) ↔ 𝐿/_FldExt𝑄))
186	183, 184	oveq12d 7378	. . . . 5 ⊢ (𝜑 → ((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (𝐿[:]𝑄))
187	186	eqeq1d 2739	. . . 4 ⊢ (𝜑 → (((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (2↑𝑛) ↔ (𝐿[:]𝑄) = (2↑𝑛)))
188	187	rexbidv 3161	. . 3 ⊢ (𝜑 → (∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (2↑𝑛) ↔ ∃𝑛 ∈ ℕ₀ (𝐿[:]𝑄) = (2↑𝑛)))
189	185, 188	anbi12d 633	. 2 ⊢ (𝜑 → (((𝑊 ↾_s (lastS‘𝑇))/_FldExt(𝑊 ↾_s (𝑇‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (2↑𝑛)) ↔ (𝐿/_FldExt𝑄 ∧ ∃𝑛 ∈ ℕ₀ (𝐿[:]𝑄) = (2↑𝑛))))
190	182, 189	mpbid 232	1 ⊢ (𝜑 → (𝐿/_FldExt𝑄 ∧ ∃𝑛 ∈ ℕ₀ (𝐿[:]𝑄) = (2↑𝑛)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∃wrex 3061 ∅c0 4286 class class class wbr 5099 {copab 5161 ‘cfv 6493 (class class class)co 7360 ℂcc 11028 ℝcr 11029 0cc0 11030 1c1 11031 + caddc 11033 · cmul 11035 < clt 11170 2c2 12204 ℕ₀cn0 12405 ·_e cxmu 13029 ↑cexp 13988 ♯chash 14257 Word cword 14440 lastSclsw 14489 ++ cconcat 14497 ⟨“cs1 14523 ↾_s cress 17161 Chain cchn 18532 Fieldcfield 20667 SubDRingcsdrg 20723 /_FldExtcfldext 33776 [:]cextdg 33778

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5225 ax-sep 5242 ax-nul 5252 ax-pow 5311 ax-pr 5378 ax-un 7682 ax-reg 9501 ax-inf2 9554 ax-ac2 10377 ax-cnex 11086 ax-resscn 11087 ax-1cn 11088 ax-icn 11089 ax-addcl 11090 ax-addrcl 11091 ax-mulcl 11092 ax-mulrcl 11093 ax-mulcom 11094 ax-addass 11095 ax-mulass 11096 ax-distr 11097 ax-i2m1 11098 ax-1ne0 11099 ax-1rid 11100 ax-rnegex 11101 ax-rrecex 11102 ax-cnre 11103 ax-pre-lttri 11104 ax-pre-lttrn 11105 ax-pre-ltadd 11106 ax-pre-mulgt0 11107

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3351 df-reu 3352 df-rab 3401 df-v 3443 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4287 df-if 4481 df-pw 4557 df-sn 4582 df-pr 4584 df-tp 4586 df-op 4588 df-uni 4865 df-int 4904 df-iun 4949 df-iin 4950 df-br 5100 df-opab 5162 df-mpt 5181 df-tr 5207 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-se 5579 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6260 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-isom 6502 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-of 7624 df-rpss 7670 df-om 7811 df-1st 7935 df-2nd 7936 df-supp 8105 df-tpos 8170 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-1o 8399 df-2o 8400 df-oadd 8403 df-er 8637 df-map 8769 df-ixp 8840 df-en 8888 df-dom 8889 df-sdom 8890 df-fin 8891 df-fsupp 9269 df-sup 9349 df-oi 9419 df-r1 9680 df-rank 9681 df-dju 9817 df-card 9855 df-acn 9858 df-ac 10030 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-nn 12150 df-2 12212 df-3 12213 df-4 12214 df-5 12215 df-6 12216 df-7 12217 df-8 12218 df-9 12219 df-n0 12406 df-xnn0 12479 df-z 12493 df-dec 12612 df-uz 12756 df-rp 12910 df-xmul 13032 df-fz 13428 df-fzo 13575 df-seq 13929 df-exp 13989 df-hash 14258 df-word 14441 df-lsw 14490 df-concat 14498 df-s1 14524 df-substr 14569 df-pfx 14599 df-struct 17078 df-sets 17095 df-slot 17113 df-ndx 17125 df-base 17141 df-ress 17162 df-plusg 17194 df-mulr 17195 df-sca 17197 df-vsca 17198 df-ip 17199 df-tset 17200 df-ple 17201 df-ocomp 17202 df-ds 17203 df-hom 17205 df-cco 17206 df-0g 17365 df-gsum 17366 df-prds 17371 df-pws 17373 df-mre 17509 df-mrc 17510 df-mri 17511 df-acs 17512 df-proset 18221 df-drs 18222 df-poset 18240 df-ipo 18455 df-chn 18533 df-mgm 18569 df-sgrp 18648 df-mnd 18664 df-mhm 18712 df-submnd 18713 df-grp 18870 df-minusg 18871 df-sbg 18872 df-mulg 19002 df-subg 19057 df-ghm 19146 df-cntz 19250 df-cmn 19715 df-abl 19716 df-mgp 20080 df-rng 20092 df-ur 20121 df-ring 20174 df-cring 20175 df-oppr 20277 df-dvdsr 20297 df-unit 20298 df-invr 20328 df-nzr 20450 df-subrng 20483 df-subrg 20507 df-drng 20668 df-field 20669 df-sdrg 20724 df-lmod 20817 df-lss 20887 df-lsp 20927 df-lmhm 20978 df-lbs 21031 df-lvec 21059 df-sra 21129 df-rgmod 21130 df-lidl 21167 df-rsp 21168 df-dsmm 21691 df-frlm 21706 df-uvc 21742 df-lindf 21765 df-linds 21766 df-dim 33737 df-fldext 33779 df-extdg 33780

This theorem is referenced by: constrext2chnlem 33888

W3C validator