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 34403

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 6885	. . . . . 6 ⊢ (𝑑 = ∅ → (♯‘𝑑) = (♯‘∅))
3	2	breq2d 5114	. . . . 5 ⊢ (𝑑 = ∅ → (0 < (♯‘𝑑) ↔ 0 < (♯‘∅)))
4		fveq2 6885	. . . . . . . 8 ⊢ (𝑑 = ∅ → (lastS‘𝑑) = (lastS‘∅))
5	4	oveq2d 7436	. . . . . . 7 ⊢ (𝑑 = ∅ → (𝑊 ↾_s (lastS‘𝑑)) = (𝑊 ↾_s (lastS‘∅)))
6		fveq1 6884	. . . . . . . 8 ⊢ (𝑑 = ∅ → (𝑑‘0) = (∅‘0))
7	6	oveq2d 7436	. . . . . . 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 7438	. . . . . . . 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 6885	. . . . . 6 ⊢ (𝑑 = 𝑐 → (♯‘𝑑) = (♯‘𝑐))
15	14	breq2d 5114	. . . . 5 ⊢ (𝑑 = 𝑐 → (0 < (♯‘𝑑) ↔ 0 < (♯‘𝑐)))
16		fveq2 6885	. . . . . . . 8 ⊢ (𝑑 = 𝑐 → (lastS‘𝑑) = (lastS‘𝑐))
17	16	oveq2d 7436	. . . . . . 7 ⊢ (𝑑 = 𝑐 → (𝑊 ↾_s (lastS‘𝑑)) = (𝑊 ↾_s (lastS‘𝑐)))
18		fveq1 6884	. . . . . . . 8 ⊢ (𝑑 = 𝑐 → (𝑑‘0) = (𝑐‘0))
19	18	oveq2d 7436	. . . . . . 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 7438	. . . . . . . 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 6885	. . . . . 6 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (♯‘𝑑) = (♯‘(𝑐 ++ ⟨“𝑔”⟩)))
27	26	breq2d 5114	. . . . 5 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (0 < (♯‘𝑑) ↔ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))))
28		fveq2 6885	. . . . . . . 8 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (lastS‘𝑑) = (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))
29	28	oveq2d 7436	. . . . . . 7 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (𝑊 ↾_s (lastS‘𝑑)) = (𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩))))
30		fveq1 6884	. . . . . . . 8 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (𝑑‘0) = ((𝑐 ++ ⟨“𝑔”⟩)‘0))
31	30	oveq2d 7436	. . . . . . 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 7438	. . . . . . . . 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 7428	. . . . . . . . 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 6885	. . . . . 6 ⊢ (𝑑 = 𝑇 → (♯‘𝑑) = (♯‘𝑇))
43	42	breq2d 5114	. . . . 5 ⊢ (𝑑 = 𝑇 → (0 < (♯‘𝑑) ↔ 0 < (♯‘𝑇)))
44		fveq2 6885	. . . . . . . 8 ⊢ (𝑑 = 𝑇 → (lastS‘𝑑) = (lastS‘𝑇))
45	44	oveq2d 7436	. . . . . . 7 ⊢ (𝑑 = 𝑇 → (𝑊 ↾_s (lastS‘𝑑)) = (𝑊 ↾_s (lastS‘𝑇)))
46		fveq1 6884	. . . . . . . 8 ⊢ (𝑑 = 𝑇 → (𝑑‘0) = (𝑇‘0))
47	46	oveq2d 7436	. . . . . . 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 7438	. . . . . . . 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 11311	. . . . . . . 8 ⊢ 0 ∈ ℝ
56	55	ltnri 11420	. . . . . . 7 ⊢ ¬ 0 < 0
57	56	a1i 11	. . . . . 6 ⊢ (𝜑 → ¬ 0 < 0)
58		hash0 14512	. . . . . . 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 21056	. . . . . . . . . 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 34334	. . . . . . . . 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 18783	. . . . . . . . . . 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 14783	. . . . . . . . . 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 7436	. . . . . . . 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 7435	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (𝑐 ++ ⟨“𝑔”⟩) = (∅ ++ ⟨“𝑔”⟩))
77		s0s1 15074	. . . . . . . . . . . 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 6887	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain (SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → ((𝑐 ++ ⟨“𝑔”⟩)‘0) = (⟨“𝑔”⟩‘0))
80		s1fv 14759	. . . . . . . . . . 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 7436	. . . . . . . 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 7428	. . . . . . . . . 10 ⊢ (𝑚 = 0 → (2↑𝑚) = (2↑0))
86		2cn 12419	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
87		exp0 14209	. . . . . . . . . . 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 12622	. . . . . . . . 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 7438	. . . . . . . . 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 34335	. . . . . . . . . 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 14714	. . . . . . . . . . . . . 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 7432	. . . . . . . . . . . . . . . . . 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 7428	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑔 → (𝑊 ↾_s 𝑒) = (𝑊 ↾_s 𝑔))
114	113	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → (𝑊 ↾_s 𝑒) = (𝑊 ↾_s 𝑔))
115		oveq2 7428	. . . . . . . . . . . . . . . . . . 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 7438	. . . . . . . . . . . . . . . . . 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 5507	. . . . . . . . . . . . 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 14533	. . . . . . . . . . . . . 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 7428	. . . . . . . . . . . . 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 34333	. . . . . . . . 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 7436	. . . . . . . . 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 14751	. . . . . . . . . . 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 14730	. . . . . . . . . . 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 7436	. . . . . . . . 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 7428	. . . . . . . . . 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 12623	. . . . . . . . . . 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 12672	. . . . . . . . 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 7438	. . . . . . . . . 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 34338	. . . . . . . . . . 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 14290	. . . . . . . . . . . 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 11331	. . . . . . . . . . 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 7438	. . . . . . . . . . . 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 12418	. . . . . . . . . . . . . 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 14307	. . . . . . . . . . . . 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 13402	. . . . . . . . . . . . 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 14291	. . . . . . . . . . 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 18796	. . 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 7438	. . . . 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 1569 ∈ wcel 2144 ≠ wne 2955 ∃wrex 3086 ∅c0 4278 class class class wbr 5102 {copab 5166 ‘cfv 6538 (class class class)co 7420 ℂcc 11199 ℝcr 11200 0cc0 11201 1c1 11202 + caddc 11204 · cmul 11206 < clt 11344 2c2 12398 ℕ₀cn0 12607 ·_e cxmu 13241 ↑cexp 14205 ♯chash 14475 Word cword 14659 lastSclsw 14708 ++ cconcat 14716 ⟨“cs1 14743 ↾_s cress 17409 Chain cchn 18780 Fieldcfield 20982 SubDRingcsdrg 21044 /_FldExtcfldext 34313 [:]cextdg 34315

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-reg 9587 ax-inf2 9643 ax-ac2 10542 ax-cnex 11257 ax-resscn 11258 ax-1cn 11259 ax-icn 11260 ax-addcl 11261 ax-addrcl 11262 ax-mulcl 11263 ax-mulrcl 11264 ax-mulcom 11265 ax-addass 11266 ax-mulass 11267 ax-distr 11268 ax-i2m1 11269 ax-1ne0 11270 ax-1rid 11271 ax-rnegex 11272 ax-rrecex 11273 ax-cnre 11274 ax-pre-lttri 11275 ax-pre-lttrn 11276 ax-pre-ltadd 11277 ax-pre-mulgt0 11278

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 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-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 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 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-of 7693 df-rpss 7739 df-om 7878 df-1st 8001 df-2nd 8002 df-supp 8178 df-tpos 8244 df-frecs 8300 df-wrecs 8331 df-recs 8380 df-rdg 8419 df-1o 8477 df-2o 8478 df-oadd 8481 df-er 8718 df-map 8850 df-ixp 8927 df-en 8975 df-dom 8976 df-sdom 8977 df-fin 8978 df-fsupp 9355 df-sup 9435 df-oi 9505 df-r1 9769 df-rank 9770 df-scott 9930 df-dju 9983 df-card 10021 df-acn 10024 df-ac 10196 df-pnf 11346 df-mnf 11347 df-xr 11348 df-ltxr 11349 df-le 11350 df-sub 11544 df-neg 11545 df-nn 12337 df-2 12406 df-3 12407 df-4 12408 df-5 12409 df-6 12410 df-7 12411 df-8 12412 df-9 12413 df-n0 12608 df-xnn0 12681 df-z 12695 df-dec 12816 df-uz 12967 df-rp 13122 df-xmul 13244 df-fz 13641 df-fzo 13790 df-seq 14146 df-exp 14206 df-hash 14476 df-word 14660 df-lsw 14709 df-concat 14717 df-s1 14744 df-substr 14790 df-pfx 14822 df-struct 17326 df-sets 17343 df-slot 17361 df-ndx 17373 df-base 17389 df-ress 17410 df-plusg 17442 df-mulr 17443 df-sca 17445 df-vsca 17446 df-ip 17447 df-tset 17448 df-ple 17449 df-ocomp 17450 df-ds 17451 df-hom 17453 df-cco 17454 df-0g 17613 df-gsum 17614 df-prds 17619 df-pws 17621 df-mre 17757 df-mrc 17758 df-mri 17759 df-acs 17760 df-proset 18469 df-drs 18470 df-poset 18488 df-ipo 18703 df-chn 18781 df-mgm 18817 df-sgrp 18909 df-mnd 18925 df-mhm 18979 df-submnd 18980 df-grp 19148 df-minusg 19149 df-sbg 19150 df-mulg 19279 df-subg 19334 df-ghm 19429 df-cntz 19532 df-cmn 19997 df-abl 19998 df-mgp 20362 df-rng 20376 df-ur 20409 df-ring 20462 df-cring 20463 df-oppr 20568 df-dvdsr 20588 df-unit 20589 df-invr 20619 df-nzr 20764 df-subrng 20799 df-subrg 20823 df-drng 20983 df-field 20984 df-sdrg 21045 df-lmod 21138 df-lss 21208 df-lsp 21248 df-lmhm 21298 df-lbs 21351 df-lvec 21379 df-sra 21449 df-rgmod 21450 df-lidl 21487 df-rsp 21488 df-dsmm 22039 df-frlm 22054 df-uvc 22090 df-lindf 22113 df-linds 22114 df-dim 34275 df-fldext 34316 df-extdg 34317

This theorem is used by: constrext2chnlem 34425

W3C validator