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 34084

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 6881	. . . . . 6 ⊢ (𝑑 = ∅ → (♯‘𝑑) = (♯‘∅))
3	2	breq2d 5120	. . . . 5 ⊢ (𝑑 = ∅ → (0 < (♯‘𝑑) ↔ 0 < (♯‘∅)))
4		fveq2 6881	. . . . . . . 8 ⊢ (𝑑 = ∅ → (lastS‘𝑑) = (lastS‘∅))
5	4	oveq2d 7426	. . . . . . 7 ⊢ (𝑑 = ∅ → (𝑊 ↾_s (lastS‘𝑑)) = (𝑊 ↾_s (lastS‘∅)))
6		fveq1 6880	. . . . . . . 8 ⊢ (𝑑 = ∅ → (𝑑‘0) = (∅‘0))
7	6	oveq2d 7426	. . . . . . 7 ⊢ (𝑑 = ∅ → (𝑊 ↾_s (𝑑‘0)) = (𝑊 ↾_s (∅‘0)))
8	5, 7	breq12d 5121	. . . . . 6 ⊢ (𝑑 = ∅ → ((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ↔ (𝑊 ↾_s (lastS‘∅))/_FldExt(𝑊 ↾_s (∅‘0))))
9	5, 7	oveq12d 7428	. . . . . . . 8 ⊢ (𝑑 = ∅ → ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = ((𝑊 ↾_s (lastS‘∅))[:](𝑊 ↾_s (∅‘0))))
10	9	eqeq1d 2763	. . . . . . 7 ⊢ (𝑑 = ∅ → (((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ((𝑊 ↾_s (lastS‘∅))[:](𝑊 ↾_s (∅‘0))) = (2↑𝑛)))
11	10	rexbidv 3187	. . . . . 6 ⊢ (𝑑 = ∅ → (∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘∅))[:](𝑊 ↾_s (∅‘0))) = (2↑𝑛)))
12	8, 11	anbi12d 643	. . . . 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 347	. . . 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 6881	. . . . . 6 ⊢ (𝑑 = 𝑐 → (♯‘𝑑) = (♯‘𝑐))
15	14	breq2d 5120	. . . . 5 ⊢ (𝑑 = 𝑐 → (0 < (♯‘𝑑) ↔ 0 < (♯‘𝑐)))
16		fveq2 6881	. . . . . . . 8 ⊢ (𝑑 = 𝑐 → (lastS‘𝑑) = (lastS‘𝑐))
17	16	oveq2d 7426	. . . . . . 7 ⊢ (𝑑 = 𝑐 → (𝑊 ↾_s (lastS‘𝑑)) = (𝑊 ↾_s (lastS‘𝑐)))
18		fveq1 6880	. . . . . . . 8 ⊢ (𝑑 = 𝑐 → (𝑑‘0) = (𝑐‘0))
19	18	oveq2d 7426	. . . . . . 7 ⊢ (𝑑 = 𝑐 → (𝑊 ↾_s (𝑑‘0)) = (𝑊 ↾_s (𝑐‘0)))
20	17, 19	breq12d 5121	. . . . . 6 ⊢ (𝑑 = 𝑐 → ((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ↔ (𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0))))
21	17, 19	oveq12d 7428	. . . . . . . 8 ⊢ (𝑑 = 𝑐 → ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))))
22	21	eqeq1d 2763	. . . . . . 7 ⊢ (𝑑 = 𝑐 → (((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))
23	22	rexbidv 3187	. . . . . 6 ⊢ (𝑑 = 𝑐 → (∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))
24	20, 23	anbi12d 643	. . . . 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 347	. . . 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 6881	. . . . . 6 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (♯‘𝑑) = (♯‘(𝑐 ++ ⟨“𝑔”⟩)))
27	26	breq2d 5120	. . . . 5 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (0 < (♯‘𝑑) ↔ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))))
28		fveq2 6881	. . . . . . . 8 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (lastS‘𝑑) = (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))
29	28	oveq2d 7426	. . . . . . 7 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (𝑊 ↾_s (lastS‘𝑑)) = (𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩))))
30		fveq1 6880	. . . . . . . 8 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (𝑑‘0) = ((𝑐 ++ ⟨“𝑔”⟩)‘0))
31	30	oveq2d 7426	. . . . . . 7 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (𝑊 ↾_s (𝑑‘0)) = (𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0)))
32	29, 31	breq12d 5121	. . . . . 6 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → ((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ↔ (𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))/_FldExt(𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))))
33	29, 31	oveq12d 7428	. . . . . . . . 9 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))))
34	33	eqeq1d 2763	. . . . . . . 8 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑛)))
35	34	rexbidv 3187	. . . . . . 7 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑛)))
36		oveq2 7418	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → (2↑𝑛) = (2↑𝑚))
37	36	eqeq2d 2772	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → (((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑛) ↔ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚)))
38	37	cbvrexvw 3242	. . . . . . 7 ⊢ (∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑛) ↔ ∃𝑚 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚))
39	35, 38	bitrdi 290	. . . . . 6 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ∃𝑚 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚)))
40	32, 39	anbi12d 643	. . . . 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 347	. . . 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 6881	. . . . . 6 ⊢ (𝑑 = 𝑇 → (♯‘𝑑) = (♯‘𝑇))
43	42	breq2d 5120	. . . . 5 ⊢ (𝑑 = 𝑇 → (0 < (♯‘𝑑) ↔ 0 < (♯‘𝑇)))
44		fveq2 6881	. . . . . . . 8 ⊢ (𝑑 = 𝑇 → (lastS‘𝑑) = (lastS‘𝑇))
45	44	oveq2d 7426	. . . . . . 7 ⊢ (𝑑 = 𝑇 → (𝑊 ↾_s (lastS‘𝑑)) = (𝑊 ↾_s (lastS‘𝑇)))
46		fveq1 6880	. . . . . . . 8 ⊢ (𝑑 = 𝑇 → (𝑑‘0) = (𝑇‘0))
47	46	oveq2d 7426	. . . . . . 7 ⊢ (𝑑 = 𝑇 → (𝑊 ↾_s (𝑑‘0)) = (𝑊 ↾_s (𝑇‘0)))
48	45, 47	breq12d 5121	. . . . . 6 ⊢ (𝑑 = 𝑇 → ((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ↔ (𝑊 ↾_s (lastS‘𝑇))/_FldExt(𝑊 ↾_s (𝑇‘0))))
49	45, 47	oveq12d 7428	. . . . . . . 8 ⊢ (𝑑 = 𝑇 → ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = ((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))))
50	49	eqeq1d 2763	. . . . . . 7 ⊢ (𝑑 = 𝑇 → (((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (2↑𝑛)))
51	50	rexbidv 3187	. . . . . 6 ⊢ (𝑑 = 𝑇 → (∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (2↑𝑛)))
52	48, 51	anbi12d 643	. . . . 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 347	. . . 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 11209	. . . . . . . 8 ⊢ 0 ∈ ℝ
56	55	ltnri 11318	. . . . . . 7 ⊢ ¬ 0 < 0
57	56	a1i 11	. . . . . 6 ⊢ (𝜑 → ¬ 0 < 0)
58		hash0 14403	. . . . . . 7 ⊢ (♯‘∅) = 0
59	58	breq2i 5116	. . . . . 6 ⊢ (0 < (♯‘∅) ↔ 0 < 0)
60	57, 59	sylnibr 332	. . . . 5 ⊢ (𝜑 → ¬ 0 < (♯‘∅))
61	60	pm2.21d 122	. . . 4 ⊢ (𝜑 → (0 < (♯‘∅) → ((𝑊 ↾_s (lastS‘∅))/_FldExt(𝑊 ↾_s (∅‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘∅))[:](𝑊 ↾_s (∅‘0))) = (2↑𝑛))))
62		fldext2chn.w	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 ∈ Field)
63	62	ad6antr 748	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → 𝑊 ∈ Field)
64		simp-5r 797	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → 𝑔 ∈ (SubDRing‘𝑊))
65		fldsdrgfld 20880	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Field ∧ 𝑔 ∈ (SubDRing‘𝑊)) → (𝑊 ↾_s 𝑔) ∈ Field)
66	63, 64, 65	syl2anc 595	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (𝑊 ↾_s 𝑔) ∈ Field)
67		fldextid 34015	. . . . . . . . 9 ⊢ ((𝑊 ↾_s 𝑔) ∈ Field → (𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s 𝑔))
68	66, 67	syl 18	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s 𝑔))
69		simp-5r 797	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) → 𝑐 ∈ ( < Chain (SubDRing‘𝑊)))
70	69	chnwrd 18663	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) → 𝑐 ∈ Word (SubDRing‘𝑊))
71	70	adantr 485	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → 𝑐 ∈ Word (SubDRing‘𝑊))
72		lswccats1 14672	. . . . . . . . . 10 ⊢ ((𝑐 ∈ Word (SubDRing‘𝑊) ∧ 𝑔 ∈ (SubDRing‘𝑊)) → (lastS‘(𝑐 ++ ⟨“𝑔”⟩)) = 𝑔)
73	71, 64, 72	syl2anc 595	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (lastS‘(𝑐 ++ ⟨“𝑔”⟩)) = 𝑔)
74	73	oveq2d 7426	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩))) = (𝑊 ↾_s 𝑔))
75		simpr 489	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → 𝑐 = ∅)
76	75	oveq1d 7425	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (𝑐 ++ ⟨“𝑔”⟩) = (∅ ++ ⟨“𝑔”⟩))
77		s0s1 14959	. . . . . . . . . . . 12 ⊢ ⟨“𝑔”⟩ = (∅ ++ ⟨“𝑔”⟩)
78	76, 77	eqtr4di 2814	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (𝑐 ++ ⟨“𝑔”⟩) = ⟨“𝑔”⟩)
79	78	fveq1d 6883	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → ((𝑐 ++ ⟨“𝑔”⟩)‘0) = (⟨“𝑔”⟩‘0))
80		s1fv 14648	. . . . . . . . . . 11 ⊢ (𝑔 ∈ (SubDRing‘𝑊) → (⟨“𝑔”⟩‘0) = 𝑔)
81	64, 80	syl 18	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (⟨“𝑔”⟩‘0) = 𝑔)
82	79, 81	eqtrd 2796	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → ((𝑐 ++ ⟨“𝑔”⟩)‘0) = 𝑔)
83	82	oveq2d 7426	. . . . . . . 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 5142	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))/_FldExt(𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0)))
85		oveq2 7418	. . . . . . . . . 10 ⊢ (𝑚 = 0 → (2↑𝑚) = (2↑0))
86		2cn 12315	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
87		exp0 14101	. . . . . . . . . . 11 ⊢ (2 ∈ ℂ → (2↑0) = 1)
88	86, 87	ax-mp 5	. . . . . . . . . 10 ⊢ (2↑0) = 1
89	85, 88	eqtrdi 2812	. . . . . . . . 9 ⊢ (𝑚 = 0 → (2↑𝑚) = 1)
90	89	eqeq2d 2772	. . . . . . . 8 ⊢ (𝑚 = 0 → (((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚) ↔ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = 1))
91		0nn0 12518	. . . . . . . . 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 7428	. . . . . . . . 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 34016	. . . . . . . . . 10 ⊢ ((𝑊 ↾_s 𝑔) ∈ Field → ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s 𝑔)) = 1)
95	66, 94	syl 18	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s 𝑔)) = 1)
96	93, 95	eqtrd 2796	. . . . . . . 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 3583	. . . . . . 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 520	. . . . . 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 799	. . . . . . . . . . . . 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 787	. . . . . . . . . . . . . 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 2961	. . . . . . . . . . . . 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 891	. . . . . . . . . . . 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 742	. . . . . . . . . . . . . 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 14605	. . . . . . . . . . . . . 14 ⊢ ((𝑐 ∈ Word (SubDRing‘𝑊) ∧ 𝑐 ≠ ∅) → (lastS‘𝑐) ∈ (SubDRing‘𝑊))
105	103, 100, 104	syl2anc 595	. . . . . . . . . . . . 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 801	. . . . . . . . . . . . 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 5117	. . . . . . . . . . . . . . . . 17 ⊢ (𝐸/_FldExt𝐹 ↔ (𝑊 ↾_s 𝑒)/_FldExt(𝑊 ↾_s 𝑓))
110	107, 108	oveq12i 7422	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐸[:]𝐹) = ((𝑊 ↾_s 𝑒)[:](𝑊 ↾_s 𝑓))
111	110	eqeq1i 2766	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐸[:]𝐹) = 2 ↔ ((𝑊 ↾_s 𝑒)[:](𝑊 ↾_s 𝑓)) = 2)
112	109, 111	anbi12i 639	. . . . . . . . . . . . . . . 16 ⊢ ((𝐸/_FldExt𝐹 ∧ (𝐸[:]𝐹) = 2) ↔ ((𝑊 ↾_s 𝑒)/_FldExt(𝑊 ↾_s 𝑓) ∧ ((𝑊 ↾_s 𝑒)[:](𝑊 ↾_s 𝑓)) = 2))
113		oveq2 7418	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑔 → (𝑊 ↾_s 𝑒) = (𝑊 ↾_s 𝑔))
114	113	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → (𝑊 ↾_s 𝑒) = (𝑊 ↾_s 𝑔))
115		oveq2 7418	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (lastS‘𝑐) → (𝑊 ↾_s 𝑓) = (𝑊 ↾_s (lastS‘𝑐)))
116	115	adantl 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → (𝑊 ↾_s 𝑓) = (𝑊 ↾_s (lastS‘𝑐)))
117	114, 116	breq12d 5121	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → ((𝑊 ↾_s 𝑒)/_FldExt(𝑊 ↾_s 𝑓) ↔ (𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (lastS‘𝑐))))
118	114, 116	oveq12d 7428	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → ((𝑊 ↾_s 𝑒)[:](𝑊 ↾_s 𝑓)) = ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s (lastS‘𝑐))))
119	118	eqeq1d 2763	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → (((𝑊 ↾_s 𝑒)[:](𝑊 ↾_s 𝑓)) = 2 ↔ ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s (lastS‘𝑐))) = 2))
120	117, 119	anbi12d 643	. . . . . . . . . . . . . . . 16 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → (((𝑊 ↾_s 𝑒)/_FldExt(𝑊 ↾_s 𝑓) ∧ ((𝑊 ↾_s 𝑒)[:](𝑊 ↾_s 𝑓)) = 2) ↔ ((𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (lastS‘𝑐)) ∧ ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s (lastS‘𝑐))) = 2)))
121	112, 120	bitrid 286	. . . . . . . . . . . . . . 15 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → ((𝐸/_FldExt𝐹 ∧ (𝐸[:]𝐹) = 2) ↔ ((𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (lastS‘𝑐)) ∧ ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s (lastS‘𝑐))) = 2)))
122	121	ancoms 463	. . . . . . . . . . . . . 14 ⊢ ((𝑓 = (lastS‘𝑐) ∧ 𝑒 = 𝑔) → ((𝐸/_FldExt𝐹 ∧ (𝐸[:]𝐹) = 2) ↔ ((𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (lastS‘𝑐)) ∧ ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s (lastS‘𝑐))) = 2)))
123		fldext2chn.l	. . . . . . . . . . . . . 14 ⊢ < = {⟨𝑓, 𝑒⟩ ∣ (𝐸/_FldExt𝐹 ∧ (𝐸[:]𝐹) = 2)}
124	122, 123	brabga 5518	. . . . . . . . . . . . 13 ⊢ (((lastS‘𝑐) ∈ (SubDRing‘𝑊) ∧ 𝑔 ∈ (SubDRing‘𝑊)) → ((lastS‘𝑐) < 𝑔 ↔ ((𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (lastS‘𝑐)) ∧ ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s (lastS‘𝑐))) = 2)))
125	105, 106, 124	syl2anc 595	. . . . . . . . . . . 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 235	. . . . . . . . . . 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 499	. . . . . . . . . 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 14424	. . . . . . . . . . . . . 14 ⊢ ((𝑐 ∈ ( < Chain (SubDRing‘𝑊)) ∧ 𝑐 ≠ ∅) → 0 < (♯‘𝑐))
129	69, 128	sylan 591	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → 0 < (♯‘𝑐))
130		simpllr 787	. . . . . . . . . . . . 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 16	. . . . . . . . . . . 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 500	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛))
133		oveq2 7418	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑜 → (2↑𝑛) = (2↑𝑜))
134	133	eqeq2d 2772	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑜 → (((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛) ↔ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)))
135	134	cbvrexvw 3242	. . . . . . . . . . 11 ⊢ (∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛) ↔ ∃𝑜 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜))
136	132, 135	sylib 221	. . . . . . . . . 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 3171	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → (𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (lastS‘𝑐)))
138	131	simpld 499	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → (𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)))
139		fldexttr 34014	. . . . . . . . 9 ⊢ (((𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (lastS‘𝑐)) ∧ (𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0))) → (𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (𝑐‘0)))
140	137, 138, 139	syl2anc 595	. . . . . . . 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 595	. . . . . . . . . 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 7426	. . . . . . . . 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 3171	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘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)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → ⟨“𝑔”⟩ ∈ Word (SubDRing‘𝑊))
145	129	ad2antrr 738	. . . . . . . . . . 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 14621	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ Word (SubDRing‘𝑊) ∧ ⟨“𝑔”⟩ ∈ Word (SubDRing‘𝑊) ∧ 0 < (♯‘𝑐)) → ((𝑐 ++ ⟨“𝑔”⟩)‘0) = (𝑐‘0))
147	103, 144, 145, 146	syl3anc 1396	. . . . . . . . . 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 7426	. . . . . . . . 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 3171	. . . . . . . 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 5142	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → (𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))/_FldExt(𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0)))
151		oveq2 7418	. . . . . . . . . 10 ⊢ (𝑚 = (𝑜 + 1) → (2↑𝑚) = (2↑(𝑜 + 1)))
152	151	eqeq2d 2772	. . . . . . . . 9 ⊢ (𝑚 = (𝑜 + 1) → (((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚) ↔ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑(𝑜 + 1))))
153		simplr 780	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → 𝑜 ∈ ℕ₀)
154		1nn0 12519	. . . . . . . . . . 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 12568	. . . . . . . . 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 7428	. . . . . . . . . 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 738	. . . . . . . . . . 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 34019	. . . . . . . . . . 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 595	. . . . . . . . . 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 14182	. . . . . . . . . . . 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 11229	. . . . . . . . . . 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 500	. . . . . . . . . . . . 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 489	. . . . . . . . . . . . 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 7428	. . . . . . . . . . . 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 12314	. . . . . . . . . . . . . 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 14199	. . . . . . . . . . . . 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 13296	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ ∧ (2↑𝑜) ∈ ℝ) → (2 ·_e (2↑𝑜)) = (2 · (2↑𝑜)))
171	168, 169, 170	syl2anc 595	. . . . . . . . . . . 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 2796	. . . . . . . . . . 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 14183	. . . . . . . . . . 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 2806	. . . . . . . . . 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 2800	. . . . . . . . 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 3583	. . . . . . . 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 3171	. . . . . . 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 520	. . . . . 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 3043	. . . . 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 417	. . . 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 18676	. . 3 ⊢ (𝜑 → (0 < (♯‘𝑇) → ((𝑊 ↾_s (lastS‘𝑇))/_FldExt(𝑊 ↾_s (𝑇‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (2↑𝑛))))
182	1, 181	mpd 16	. 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 5121	. . 3 ⊢ (𝜑 → ((𝑊 ↾_s (lastS‘𝑇))/_FldExt(𝑊 ↾_s (𝑇‘0)) ↔ 𝐿/_FldExt𝑄))
186	183, 184	oveq12d 7428	. . . . 5 ⊢ (𝜑 → ((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (𝐿[:]𝑄))
187	186	eqeq1d 2763	. . . 4 ⊢ (𝜑 → (((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (2↑𝑛) ↔ (𝐿[:]𝑄) = (2↑𝑛)))
188	187	rexbidv 3187	. . 3 ⊢ (𝜑 → (∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (2↑𝑛) ↔ ∃𝑛 ∈ ℕ₀ (𝐿[:]𝑄) = (2↑𝑛)))
189	185, 188	anbi12d 643	. 2 ⊢ (𝜑 → (((𝑊 ↾_s (lastS‘𝑇))/_FldExt(𝑊 ↾_s (𝑇‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (2↑𝑛)) ↔ (𝐿/_FldExt𝑄 ∧ ∃𝑛 ∈ ℕ₀ (𝐿[:]𝑄) = (2↑𝑛))))
190	182, 189	mpbid 235	1 ⊢ (𝜑 → (𝐿/_FldExt𝑄 ∧ ∃𝑛 ∈ ℕ₀ (𝐿[:]𝑄) = (2↑𝑛)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 = wceq 1568 ∈ wcel 2141 ≠ wne 2956 ∃wrex 3087 ∅c0 4285 class class class wbr 5108 {copab 5172 ‘cfv 6536 (class class class)co 7410 ℂcc 11097 ℝcr 11098 0cc0 11099 1c1 11100 + caddc 11102 · cmul 11104 < clt 11242 2c2 12294 ℕ₀cn0 12503 ·_e cxmu 13135 ↑cexp 14097 ♯chash 14366 Word cword 14550 lastSclsw 14599 ++ cconcat 14607 ⟨“cs1 14633 ↾_s cress 17289 Chain cchn 18660 Fieldcfield 20813 SubDRingcsdrg 20868 /_FldExtcfldext 33994 [:]cextdg 33996

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1823 ax-4 1837 ax-5 1938 ax-6 1995 ax-7 2036 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-reg 9553 ax-inf2 9609 ax-ac2 10446 ax-cnex 11155 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 ax-pre-mulgt0 11176

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1571 df-fal 1581 df-ex 1808 df-nf 1812 df-sb 2095 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4595 df-uni 4872 df-int 4912 df-iun 4957 df-iin 4958 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-se 5615 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-of 7674 df-rpss 7720 df-om 7862 df-1st 7985 df-2nd 7986 df-supp 8156 df-tpos 8221 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8452 df-2o 8453 df-oadd 8456 df-er 8693 df-map 8825 df-ixp 8895 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-fsupp 9321 df-sup 9401 df-oi 9471 df-r1 9735 df-rank 9736 df-dju 9886 df-card 9924 df-acn 9927 df-ac 10099 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-sub 11442 df-neg 11443 df-nn 12233 df-2 12302 df-3 12303 df-4 12304 df-5 12305 df-6 12306 df-7 12307 df-8 12308 df-9 12309 df-n0 12504 df-xnn0 12577 df-z 12591 df-dec 12711 df-uz 12862 df-rp 13016 df-xmul 13138 df-fz 13535 df-fzo 13683 df-seq 14038 df-exp 14098 df-hash 14367 df-word 14551 df-lsw 14600 df-concat 14608 df-s1 14634 df-substr 14679 df-pfx 14709 df-struct 17206 df-sets 17223 df-slot 17241 df-ndx 17253 df-base 17269 df-ress 17290 df-plusg 17322 df-mulr 17323 df-sca 17325 df-vsca 17326 df-ip 17327 df-tset 17328 df-ple 17329 df-ocomp 17330 df-ds 17331 df-hom 17333 df-cco 17334 df-0g 17493 df-gsum 17494 df-prds 17499 df-pws 17501 df-mre 17637 df-mrc 17638 df-mri 17639 df-acs 17640 df-proset 18349 df-drs 18350 df-poset 18368 df-ipo 18583 df-chn 18661 df-mgm 18697 df-sgrp 18776 df-mnd 18792 df-mhm 18840 df-submnd 18841 df-grp 19002 df-minusg 19003 df-sbg 19004 df-mulg 19133 df-subg 19188 df-ghm 19283 df-cntz 19386 df-cmn 19851 df-abl 19852 df-mgp 20216 df-rng 20230 df-ur 20263 df-ring 20316 df-cring 20317 df-oppr 20418 df-dvdsr 20438 df-unit 20439 df-invr 20469 df-nzr 20595 df-subrng 20630 df-subrg 20654 df-drng 20814 df-field 20815 df-sdrg 20869 df-lmod 20962 df-lss 21032 df-lsp 21072 df-lmhm 21122 df-lbs 21175 df-lvec 21203 df-sra 21273 df-rgmod 21274 df-lidl 21311 df-rsp 21312 df-dsmm 21861 df-frlm 21876 df-uvc 21912 df-lindf 21935 df-linds 21936 df-dim 33956 df-fldext 33997 df-extdg 33998

This theorem is referenced by: constrext2chnlem 34106

W3C validator