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 34294

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 6873	. . . . . 6 ⊢ (𝑑 = ∅ → (♯‘𝑑) = (♯‘∅))
3	2	breq2d 5114	. . . . 5 ⊢ (𝑑 = ∅ → (0 < (♯‘𝑑) ↔ 0 < (♯‘∅)))
4		fveq2 6873	. . . . . . . 8 ⊢ (𝑑 = ∅ → (lastS‘𝑑) = (lastS‘∅))
5	4	oveq2d 7424	. . . . . . 7 ⊢ (𝑑 = ∅ → (𝑊 ↾_s (lastS‘𝑑)) = (𝑊 ↾_s (lastS‘∅)))
6		fveq1 6872	. . . . . . . 8 ⊢ (𝑑 = ∅ → (𝑑‘0) = (∅‘0))
7	6	oveq2d 7424	. . . . . . 7 ⊢ (𝑑 = ∅ → (𝑊 ↾_s (𝑑‘0)) = (𝑊 ↾_s (∅‘0)))
8	5, 7	breq12d 5115	. . . . . 6 ⊢ (𝑑 = ∅ → ((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ↔ (𝑊 ↾_s (lastS‘∅))/_FldExt(𝑊 ↾_s (∅‘0))))
9	5, 7	oveq12d 7426	. . . . . . . 8 ⊢ (𝑑 = ∅ → ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = ((𝑊 ↾_s (lastS‘∅))[:](𝑊 ↾_s (∅‘0))))
10	9	eqeq1d 2762	. . . . . . 7 ⊢ (𝑑 = ∅ → (((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ((𝑊 ↾_s (lastS‘∅))[:](𝑊 ↾_s (∅‘0))) = (2↑𝑛)))
11	10	rexbidv 3186	. . . . . 6 ⊢ (𝑑 = ∅ → (∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘∅))[:](𝑊 ↾_s (∅‘0))) = (2↑𝑛)))
12	8, 11	anbi12d 644	. . . . 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 6873	. . . . . 6 ⊢ (𝑑 = 𝑐 → (♯‘𝑑) = (♯‘𝑐))
15	14	breq2d 5114	. . . . 5 ⊢ (𝑑 = 𝑐 → (0 < (♯‘𝑑) ↔ 0 < (♯‘𝑐)))
16		fveq2 6873	. . . . . . . 8 ⊢ (𝑑 = 𝑐 → (lastS‘𝑑) = (lastS‘𝑐))
17	16	oveq2d 7424	. . . . . . 7 ⊢ (𝑑 = 𝑐 → (𝑊 ↾_s (lastS‘𝑑)) = (𝑊 ↾_s (lastS‘𝑐)))
18		fveq1 6872	. . . . . . . 8 ⊢ (𝑑 = 𝑐 → (𝑑‘0) = (𝑐‘0))
19	18	oveq2d 7424	. . . . . . 7 ⊢ (𝑑 = 𝑐 → (𝑊 ↾_s (𝑑‘0)) = (𝑊 ↾_s (𝑐‘0)))
20	17, 19	breq12d 5115	. . . . . 6 ⊢ (𝑑 = 𝑐 → ((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ↔ (𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0))))
21	17, 19	oveq12d 7426	. . . . . . . 8 ⊢ (𝑑 = 𝑐 → ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))))
22	21	eqeq1d 2762	. . . . . . 7 ⊢ (𝑑 = 𝑐 → (((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))
23	22	rexbidv 3186	. . . . . 6 ⊢ (𝑑 = 𝑐 → (∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))
24	20, 23	anbi12d 644	. . . . 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 6873	. . . . . 6 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (♯‘𝑑) = (♯‘(𝑐 ++ ⟨“𝑔”⟩)))
27	26	breq2d 5114	. . . . 5 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (0 < (♯‘𝑑) ↔ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))))
28		fveq2 6873	. . . . . . . 8 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (lastS‘𝑑) = (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))
29	28	oveq2d 7424	. . . . . . 7 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (𝑊 ↾_s (lastS‘𝑑)) = (𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩))))
30		fveq1 6872	. . . . . . . 8 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (𝑑‘0) = ((𝑐 ++ ⟨“𝑔”⟩)‘0))
31	30	oveq2d 7424	. . . . . . 7 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (𝑊 ↾_s (𝑑‘0)) = (𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0)))
32	29, 31	breq12d 5115	. . . . . 6 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → ((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ↔ (𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))/_FldExt(𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))))
33	29, 31	oveq12d 7426	. . . . . . . . 9 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))))
34	33	eqeq1d 2762	. . . . . . . 8 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑛)))
35	34	rexbidv 3186	. . . . . . 7 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑛)))
36		oveq2 7416	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → (2↑𝑛) = (2↑𝑚))
37	36	eqeq2d 2771	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → (((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑛) ↔ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚)))
38	37	cbvrexvw 3241	. . . . . . 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 644	. . . . 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 6873	. . . . . 6 ⊢ (𝑑 = 𝑇 → (♯‘𝑑) = (♯‘𝑇))
43	42	breq2d 5114	. . . . 5 ⊢ (𝑑 = 𝑇 → (0 < (♯‘𝑑) ↔ 0 < (♯‘𝑇)))
44		fveq2 6873	. . . . . . . 8 ⊢ (𝑑 = 𝑇 → (lastS‘𝑑) = (lastS‘𝑇))
45	44	oveq2d 7424	. . . . . . 7 ⊢ (𝑑 = 𝑇 → (𝑊 ↾_s (lastS‘𝑑)) = (𝑊 ↾_s (lastS‘𝑇)))
46		fveq1 6872	. . . . . . . 8 ⊢ (𝑑 = 𝑇 → (𝑑‘0) = (𝑇‘0))
47	46	oveq2d 7424	. . . . . . 7 ⊢ (𝑑 = 𝑇 → (𝑊 ↾_s (𝑑‘0)) = (𝑊 ↾_s (𝑇‘0)))
48	45, 47	breq12d 5115	. . . . . 6 ⊢ (𝑑 = 𝑇 → ((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ↔ (𝑊 ↾_s (lastS‘𝑇))/_FldExt(𝑊 ↾_s (𝑇‘0))))
49	45, 47	oveq12d 7426	. . . . . . . 8 ⊢ (𝑑 = 𝑇 → ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = ((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))))
50	49	eqeq1d 2762	. . . . . . 7 ⊢ (𝑑 = 𝑇 → (((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (2↑𝑛)))
51	50	rexbidv 3186	. . . . . 6 ⊢ (𝑑 = 𝑇 → (∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (2↑𝑛)))
52	48, 51	anbi12d 644	. . . . 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 11282	. . . . . . . 8 ⊢ 0 ∈ ℝ
56	55	ltnri 11391	. . . . . . 7 ⊢ ¬ 0 < 0
57	56	a1i 11	. . . . . 6 ⊢ (𝜑 → ¬ 0 < 0)
58		hash0 14479	. . . . . . 7 ⊢ (♯‘∅) = 0
59	58	breq2i 5110	. . . . . 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 749	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → 𝑊 ∈ Field)
64		simp-5r 798	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → 𝑔 ∈ (SubDRing‘𝑊))
65		fldsdrgfld 21017	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Field ∧ 𝑔 ∈ (SubDRing‘𝑊)) → (𝑊 ↾_s 𝑔) ∈ Field)
66	63, 64, 65	syl2anc 596	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (𝑊 ↾_s 𝑔) ∈ Field)
67		fldextid 34225	. . . . . . . . 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 798	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) → 𝑐 ∈ ( < Chain (SubDRing‘𝑊)))
70	69	chnwrd 18744	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) → 𝑐 ∈ Word (SubDRing‘𝑊))
71	70	adantr 486	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → 𝑐 ∈ Word (SubDRing‘𝑊))
72		lswccats1 14750	. . . . . . . . . 10 ⊢ ((𝑐 ∈ Word (SubDRing‘𝑊) ∧ 𝑔 ∈ (SubDRing‘𝑊)) → (lastS‘(𝑐 ++ ⟨“𝑔”⟩)) = 𝑔)
73	71, 64, 72	syl2anc 596	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (lastS‘(𝑐 ++ ⟨“𝑔”⟩)) = 𝑔)
74	73	oveq2d 7424	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩))) = (𝑊 ↾_s 𝑔))
75		simpr 490	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → 𝑐 = ∅)
76	75	oveq1d 7423	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (𝑐 ++ ⟨“𝑔”⟩) = (∅ ++ ⟨“𝑔”⟩))
77		s0s1 15041	. . . . . . . . . . . 12 ⊢ ⟨“𝑔”⟩ = (∅ ++ ⟨“𝑔”⟩)
78	76, 77	eqtr4di 2813	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (𝑐 ++ ⟨“𝑔”⟩) = ⟨“𝑔”⟩)
79	78	fveq1d 6875	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → ((𝑐 ++ ⟨“𝑔”⟩)‘0) = (⟨“𝑔”⟩‘0))
80		s1fv 14726	. . . . . . . . . . 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 2795	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → ((𝑐 ++ ⟨“𝑔”⟩)‘0) = 𝑔)
83	82	oveq2d 7424	. . . . . . . 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 5136	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))/_FldExt(𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0)))
85		oveq2 7416	. . . . . . . . . 10 ⊢ (𝑚 = 0 → (2↑𝑚) = (2↑0))
86		2cn 12388	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
87		exp0 14177	. . . . . . . . . . 11 ⊢ (2 ∈ ℂ → (2↑0) = 1)
88	86, 87	ax-mp 5	. . . . . . . . . 10 ⊢ (2↑0) = 1
89	85, 88	eqtrdi 2811	. . . . . . . . 9 ⊢ (𝑚 = 0 → (2↑𝑚) = 1)
90	89	eqeq2d 2771	. . . . . . . 8 ⊢ (𝑚 = 0 → (((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚) ↔ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = 1))
91		0nn0 12591	. . . . . . . . 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 7426	. . . . . . . . 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 34226	. . . . . . . . . 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 2795	. . . . . . . 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 3579	. . . . . . 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 521	. . . . . 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 800	. . . . . . . . . . . . 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 788	. . . . . . . . . . . . . 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 2960	. . . . . . . . . . . . 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 892	. . . . . . . . . . . 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 743	. . . . . . . . . . . . . 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 14681	. . . . . . . . . . . . . 14 ⊢ ((𝑐 ∈ Word (SubDRing‘𝑊) ∧ 𝑐 ≠ ∅) → (lastS‘𝑐) ∈ (SubDRing‘𝑊))
105	103, 100, 104	syl2anc 596	. . . . . . . . . . . . 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 802	. . . . . . . . . . . . 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 5111	. . . . . . . . . . . . . . . . 17 ⊢ (𝐸/_FldExt𝐹 ↔ (𝑊 ↾_s 𝑒)/_FldExt(𝑊 ↾_s 𝑓))
110	107, 108	oveq12i 7420	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐸[:]𝐹) = ((𝑊 ↾_s 𝑒)[:](𝑊 ↾_s 𝑓))
111	110	eqeq1i 2765	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐸[:]𝐹) = 2 ↔ ((𝑊 ↾_s 𝑒)[:](𝑊 ↾_s 𝑓)) = 2)
112	109, 111	anbi12i 640	. . . . . . . . . . . . . . . 16 ⊢ ((𝐸/_FldExt𝐹 ∧ (𝐸[:]𝐹) = 2) ↔ ((𝑊 ↾_s 𝑒)/_FldExt(𝑊 ↾_s 𝑓) ∧ ((𝑊 ↾_s 𝑒)[:](𝑊 ↾_s 𝑓)) = 2))
113		oveq2 7416	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑔 → (𝑊 ↾_s 𝑒) = (𝑊 ↾_s 𝑔))
114	113	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → (𝑊 ↾_s 𝑒) = (𝑊 ↾_s 𝑔))
115		oveq2 7416	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (lastS‘𝑐) → (𝑊 ↾_s 𝑓) = (𝑊 ↾_s (lastS‘𝑐)))
116	115	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → (𝑊 ↾_s 𝑓) = (𝑊 ↾_s (lastS‘𝑐)))
117	114, 116	breq12d 5115	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → ((𝑊 ↾_s 𝑒)/_FldExt(𝑊 ↾_s 𝑓) ↔ (𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (lastS‘𝑐))))
118	114, 116	oveq12d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → ((𝑊 ↾_s 𝑒)[:](𝑊 ↾_s 𝑓)) = ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s (lastS‘𝑐))))
119	118	eqeq1d 2762	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → (((𝑊 ↾_s 𝑒)[:](𝑊 ↾_s 𝑓)) = 2 ↔ ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s (lastS‘𝑐))) = 2))
120	117, 119	anbi12d 644	. . . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . . 14 ⊢ ((𝑓 = (lastS‘𝑐) ∧ 𝑒 = 𝑔) → ((𝐸/_FldExt𝐹 ∧ (𝐸[:]𝐹) = 2) ↔ ((𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (lastS‘𝑐)) ∧ ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s (lastS‘𝑐))) = 2)))
123		fldext2chn.l	. . . . . . . . . . . . . 14 ⊢ < = {⟨𝑓, 𝑒⟩ ∣ (𝐸/_FldExt𝐹 ∧ (𝐸[:]𝐹) = 2)}
124	122, 123	brabga 5504	. . . . . . . . . . . . 13 ⊢ (((lastS‘𝑐) ∈ (SubDRing‘𝑊) ∧ 𝑔 ∈ (SubDRing‘𝑊)) → ((lastS‘𝑐) < 𝑔 ↔ ((𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (lastS‘𝑐)) ∧ ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s (lastS‘𝑐))) = 2)))
125	105, 106, 124	syl2anc 596	. . . . . . . . . . . 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 500	. . . . . . . . . 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 14500	. . . . . . . . . . . . . 14 ⊢ ((𝑐 ∈ ( < Chain (SubDRing‘𝑊)) ∧ 𝑐 ≠ ∅) → 0 < (♯‘𝑐))
129	69, 128	sylan 592	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → 0 < (♯‘𝑐))
130		simpllr 788	. . . . . . . . . . . . 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 501	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛))
133		oveq2 7416	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑜 → (2↑𝑛) = (2↑𝑜))
134	133	eqeq2d 2771	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑜 → (((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛) ↔ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)))
135	134	cbvrexvw 3241	. . . . . . . . . . 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 3170	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → (𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (lastS‘𝑐)))
138	131	simpld 500	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → (𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)))
139		fldexttr 34224	. . . . . . . . 9 ⊢ (((𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (lastS‘𝑐)) ∧ (𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0))) → (𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (𝑐‘0)))
140	137, 138, 139	syl2anc 596	. . . . . . . 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 596	. . . . . . . . . 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 7424	. . . . . . . . 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 3170	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → (𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩))) = (𝑊 ↾_s 𝑔))
144	106	s1cld 14718	. . . . . . . . . . 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 739	. . . . . . . . . . 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 14697	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ Word (SubDRing‘𝑊) ∧ ⟨“𝑔”⟩ ∈ Word (SubDRing‘𝑊) ∧ 0 < (♯‘𝑐)) → ((𝑐 ++ ⟨“𝑔”⟩)‘0) = (𝑐‘0))
147	103, 144, 145, 146	syl3anc 1398	. . . . . . . . . 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 7424	. . . . . . . . 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 3170	. . . . . . . 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 5136	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → (𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))/_FldExt(𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0)))
151		oveq2 7416	. . . . . . . . . 10 ⊢ (𝑚 = (𝑜 + 1) → (2↑𝑚) = (2↑(𝑜 + 1)))
152	151	eqeq2d 2771	. . . . . . . . 9 ⊢ (𝑚 = (𝑜 + 1) → (((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚) ↔ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑(𝑜 + 1))))
153		simplr 781	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → 𝑜 ∈ ℕ₀)
154		1nn0 12592	. . . . . . . . . . 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 12641	. . . . . . . . 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 7426	. . . . . . . . . 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 739	. . . . . . . . . . 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 34229	. . . . . . . . . . 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 596	. . . . . . . . . 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 14258	. . . . . . . . . . . 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 11302	. . . . . . . . . . 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 501	. . . . . . . . . . . . 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 490	. . . . . . . . . . . . 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 7426	. . . . . . . . . . . 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 12387	. . . . . . . . . . . . . 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 14275	. . . . . . . . . . . . 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 13371	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ ∧ (2↑𝑜) ∈ ℝ) → (2 ·_e (2↑𝑜)) = (2 · (2↑𝑜)))
171	168, 169, 170	syl2anc 596	. . . . . . . . . . . 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 2795	. . . . . . . . . . 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 14259	. . . . . . . . . . 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 2805	. . . . . . . . . 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 2799	. . . . . . . . 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 3579	. . . . . . . 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 3170	. . . . . . 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 521	. . . . . 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 3042	. . . . 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 418	. . . 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 18757	. . 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 5115	. . 3 ⊢ (𝜑 → ((𝑊 ↾_s (lastS‘𝑇))/_FldExt(𝑊 ↾_s (𝑇‘0)) ↔ 𝐿/_FldExt𝑄))
186	183, 184	oveq12d 7426	. . . . 5 ⊢ (𝜑 → ((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (𝐿[:]𝑄))
187	186	eqeq1d 2762	. . . 4 ⊢ (𝜑 → (((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (2↑𝑛) ↔ (𝐿[:]𝑄) = (2↑𝑛)))
188	187	rexbidv 3186	. . 3 ⊢ (𝜑 → (∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (2↑𝑛) ↔ ∃𝑛 ∈ ℕ₀ (𝐿[:]𝑄) = (2↑𝑛)))
189	185, 188	anbi12d 644	. 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

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 = wceq 1570 ∈ wcel 2145 ≠ wne 2955 ∃wrex 3086 ∅c0 4278 class class class wbr 5102 {copab 5166 ‘cfv 6527 (class class class)co 7408 ℂcc 11170 ℝcr 11171 0cc0 11172 1c1 11173 + caddc 11175 · cmul 11177 < clt 11315 2c2 12367 ℕ₀cn0 12576 ·_e cxmu 13210 ↑cexp 14173 ♯chash 14442 Word cword 14626 lastSclsw 14675 ++ cconcat 14683 ⟨“cs1 14710 ↾_s cress 17370 Chain cchn 18741 Fieldcfield 20943 SubDRingcsdrg 21005 /_FldExtcfldext 34204 [:]cextdg 34206

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7734 ax-reg 9564 ax-inf2 9620 ax-ac2 10513 ax-cnex 11228 ax-resscn 11229 ax-1cn 11230 ax-icn 11231 ax-addcl 11232 ax-addrcl 11233 ax-mulcl 11234 ax-mulrcl 11235 ax-mulcom 11236 ax-addass 11237 ax-mulass 11238 ax-distr 11239 ax-i2m1 11240 ax-1ne0 11241 ax-1rid 11242 ax-rnegex 11243 ax-rrecex 11244 ax-cnre 11245 ax-pre-lttri 11246 ax-pre-lttrn 11247 ax-pre-ltadd 11248 ax-pre-mulgt0 11249

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-tp 4588 df-op 4590 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-se 5601 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6293 df-ord 6354 df-on 6355 df-lim 6356 df-suc 6357 df-iota 6483 df-fun 6529 df-fn 6530 df-f 6531 df-f1 6532 df-fo 6533 df-f1o 6534 df-fv 6535 df-isom 6536 df-riota 7365 df-ov 7411 df-oprab 7412 df-mpo 7413 df-of 7676 df-rpss 7722 df-om 7861 df-1st 7984 df-2nd 7985 df-supp 8156 df-tpos 8221 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8454 df-2o 8455 df-oadd 8458 df-er 8695 df-map 8827 df-ixp 8904 df-en 8952 df-dom 8953 df-sdom 8954 df-fin 8955 df-fsupp 9332 df-sup 9412 df-oi 9482 df-r1 9746 df-rank 9747 df-scott 9901 df-dju 9954 df-card 9992 df-acn 9995 df-ac 10167 df-pnf 11317 df-mnf 11318 df-xr 11319 df-ltxr 11320 df-le 11321 df-sub 11515 df-neg 11516 df-nn 12306 df-2 12375 df-3 12376 df-4 12377 df-5 12378 df-6 12379 df-7 12380 df-8 12381 df-9 12382 df-n0 12577 df-xnn0 12650 df-z 12664 df-dec 12785 df-uz 12936 df-rp 13091 df-xmul 13213 df-fz 13610 df-fzo 13758 df-seq 14114 df-exp 14174 df-hash 14443 df-word 14627 df-lsw 14676 df-concat 14684 df-s1 14711 df-substr 14757 df-pfx 14789 df-struct 17287 df-sets 17304 df-slot 17322 df-ndx 17334 df-base 17350 df-ress 17371 df-plusg 17403 df-mulr 17404 df-sca 17406 df-vsca 17407 df-ip 17408 df-tset 17409 df-ple 17410 df-ocomp 17411 df-ds 17412 df-hom 17414 df-cco 17415 df-0g 17574 df-gsum 17575 df-prds 17580 df-pws 17582 df-mre 17718 df-mrc 17719 df-mri 17720 df-acs 17721 df-proset 18430 df-drs 18431 df-poset 18449 df-ipo 18664 df-chn 18742 df-mgm 18778 df-sgrp 18870 df-mnd 18886 df-mhm 18940 df-submnd 18941 df-grp 19109 df-minusg 19110 df-sbg 19111 df-mulg 19240 df-subg 19295 df-ghm 19390 df-cntz 19493 df-cmn 19958 df-abl 19959 df-mgp 20323 df-rng 20337 df-ur 20370 df-ring 20423 df-cring 20424 df-oppr 20529 df-dvdsr 20549 df-unit 20550 df-invr 20580 df-nzr 20725 df-subrng 20760 df-subrg 20784 df-drng 20944 df-field 20945 df-sdrg 21006 df-lmod 21099 df-lss 21169 df-lsp 21209 df-lmhm 21259 df-lbs 21312 df-lvec 21340 df-sra 21410 df-rgmod 21411 df-lidl 21448 df-rsp 21449 df-dsmm 22000 df-frlm 22015 df-uvc 22051 df-lindf 22074 df-linds 22075 df-dim 34166 df-fldext 34207 df-extdg 34208

This theorem is used by: constrext2chnlem 34316

W3C validator