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 33762

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 6876	. . . . . 6 ⊢ (𝑑 = ∅ → (♯‘𝑑) = (♯‘∅))
3	2	breq2d 5131	. . . . 5 ⊢ (𝑑 = ∅ → (0 < (♯‘𝑑) ↔ 0 < (♯‘∅)))
4		fveq2 6876	. . . . . . . 8 ⊢ (𝑑 = ∅ → (lastS‘𝑑) = (lastS‘∅))
5	4	oveq2d 7421	. . . . . . 7 ⊢ (𝑑 = ∅ → (𝑊 ↾_s (lastS‘𝑑)) = (𝑊 ↾_s (lastS‘∅)))
6		fveq1 6875	. . . . . . . 8 ⊢ (𝑑 = ∅ → (𝑑‘0) = (∅‘0))
7	6	oveq2d 7421	. . . . . . 7 ⊢ (𝑑 = ∅ → (𝑊 ↾_s (𝑑‘0)) = (𝑊 ↾_s (∅‘0)))
8	5, 7	breq12d 5132	. . . . . 6 ⊢ (𝑑 = ∅ → ((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ↔ (𝑊 ↾_s (lastS‘∅))/_FldExt(𝑊 ↾_s (∅‘0))))
9	5, 7	oveq12d 7423	. . . . . . . 8 ⊢ (𝑑 = ∅ → ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = ((𝑊 ↾_s (lastS‘∅))[:](𝑊 ↾_s (∅‘0))))
10	9	eqeq1d 2737	. . . . . . 7 ⊢ (𝑑 = ∅ → (((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ((𝑊 ↾_s (lastS‘∅))[:](𝑊 ↾_s (∅‘0))) = (2↑𝑛)))
11	10	rexbidv 3164	. . . . . 6 ⊢ (𝑑 = ∅ → (∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘∅))[:](𝑊 ↾_s (∅‘0))) = (2↑𝑛)))
12	8, 11	anbi12d 632	. . . . 5 ⊢ (𝑑 = ∅ → (((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛)) ↔ ((𝑊 ↾_s (lastS‘∅))/_FldExt(𝑊 ↾_s (∅‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘∅))[:](𝑊 ↾_s (∅‘0))) = (2↑𝑛))))
13	3, 12	imbi12d 344	. . . 4 ⊢ (𝑑 = ∅ → ((0 < (♯‘𝑑) → ((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛))) ↔ (0 < (♯‘∅) → ((𝑊 ↾_s (lastS‘∅))/_FldExt(𝑊 ↾_s (∅‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘∅))[:](𝑊 ↾_s (∅‘0))) = (2↑𝑛)))))
14		fveq2 6876	. . . . . 6 ⊢ (𝑑 = 𝑐 → (♯‘𝑑) = (♯‘𝑐))
15	14	breq2d 5131	. . . . 5 ⊢ (𝑑 = 𝑐 → (0 < (♯‘𝑑) ↔ 0 < (♯‘𝑐)))
16		fveq2 6876	. . . . . . . 8 ⊢ (𝑑 = 𝑐 → (lastS‘𝑑) = (lastS‘𝑐))
17	16	oveq2d 7421	. . . . . . 7 ⊢ (𝑑 = 𝑐 → (𝑊 ↾_s (lastS‘𝑑)) = (𝑊 ↾_s (lastS‘𝑐)))
18		fveq1 6875	. . . . . . . 8 ⊢ (𝑑 = 𝑐 → (𝑑‘0) = (𝑐‘0))
19	18	oveq2d 7421	. . . . . . 7 ⊢ (𝑑 = 𝑐 → (𝑊 ↾_s (𝑑‘0)) = (𝑊 ↾_s (𝑐‘0)))
20	17, 19	breq12d 5132	. . . . . 6 ⊢ (𝑑 = 𝑐 → ((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ↔ (𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0))))
21	17, 19	oveq12d 7423	. . . . . . . 8 ⊢ (𝑑 = 𝑐 → ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))))
22	21	eqeq1d 2737	. . . . . . 7 ⊢ (𝑑 = 𝑐 → (((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))
23	22	rexbidv 3164	. . . . . 6 ⊢ (𝑑 = 𝑐 → (∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))
24	20, 23	anbi12d 632	. . . . 5 ⊢ (𝑑 = 𝑐 → (((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛)) ↔ ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛))))
25	15, 24	imbi12d 344	. . . 4 ⊢ (𝑑 = 𝑐 → ((0 < (♯‘𝑑) → ((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛))) ↔ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))))
26		fveq2 6876	. . . . . 6 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (♯‘𝑑) = (♯‘(𝑐 ++ ⟨“𝑔”⟩)))
27	26	breq2d 5131	. . . . 5 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (0 < (♯‘𝑑) ↔ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))))
28		fveq2 6876	. . . . . . . 8 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (lastS‘𝑑) = (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))
29	28	oveq2d 7421	. . . . . . 7 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (𝑊 ↾_s (lastS‘𝑑)) = (𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩))))
30		fveq1 6875	. . . . . . . 8 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (𝑑‘0) = ((𝑐 ++ ⟨“𝑔”⟩)‘0))
31	30	oveq2d 7421	. . . . . . 7 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (𝑊 ↾_s (𝑑‘0)) = (𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0)))
32	29, 31	breq12d 5132	. . . . . 6 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → ((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ↔ (𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))/_FldExt(𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))))
33	29, 31	oveq12d 7423	. . . . . . . . 9 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))))
34	33	eqeq1d 2737	. . . . . . . 8 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑛)))
35	34	rexbidv 3164	. . . . . . 7 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑛)))
36		oveq2 7413	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → (2↑𝑛) = (2↑𝑚))
37	36	eqeq2d 2746	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → (((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑛) ↔ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚)))
38	37	cbvrexvw 3221	. . . . . . 7 ⊢ (∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑛) ↔ ∃𝑚 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚))
39	35, 38	bitrdi 287	. . . . . 6 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ∃𝑚 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚)))
40	32, 39	anbi12d 632	. . . . 5 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → (((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛)) ↔ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))/_FldExt(𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0)) ∧ ∃𝑚 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚))))
41	27, 40	imbi12d 344	. . . 4 ⊢ (𝑑 = (𝑐 ++ ⟨“𝑔”⟩) → ((0 < (♯‘𝑑) → ((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛))) ↔ (0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩)) → ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))/_FldExt(𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0)) ∧ ∃𝑚 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚)))))
42		fveq2 6876	. . . . . 6 ⊢ (𝑑 = 𝑇 → (♯‘𝑑) = (♯‘𝑇))
43	42	breq2d 5131	. . . . 5 ⊢ (𝑑 = 𝑇 → (0 < (♯‘𝑑) ↔ 0 < (♯‘𝑇)))
44		fveq2 6876	. . . . . . . 8 ⊢ (𝑑 = 𝑇 → (lastS‘𝑑) = (lastS‘𝑇))
45	44	oveq2d 7421	. . . . . . 7 ⊢ (𝑑 = 𝑇 → (𝑊 ↾_s (lastS‘𝑑)) = (𝑊 ↾_s (lastS‘𝑇)))
46		fveq1 6875	. . . . . . . 8 ⊢ (𝑑 = 𝑇 → (𝑑‘0) = (𝑇‘0))
47	46	oveq2d 7421	. . . . . . 7 ⊢ (𝑑 = 𝑇 → (𝑊 ↾_s (𝑑‘0)) = (𝑊 ↾_s (𝑇‘0)))
48	45, 47	breq12d 5132	. . . . . 6 ⊢ (𝑑 = 𝑇 → ((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ↔ (𝑊 ↾_s (lastS‘𝑇))/_FldExt(𝑊 ↾_s (𝑇‘0))))
49	45, 47	oveq12d 7423	. . . . . . . 8 ⊢ (𝑑 = 𝑇 → ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = ((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))))
50	49	eqeq1d 2737	. . . . . . 7 ⊢ (𝑑 = 𝑇 → (((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (2↑𝑛)))
51	50	rexbidv 3164	. . . . . 6 ⊢ (𝑑 = 𝑇 → (∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛) ↔ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (2↑𝑛)))
52	48, 51	anbi12d 632	. . . . 5 ⊢ (𝑑 = 𝑇 → (((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛)) ↔ ((𝑊 ↾_s (lastS‘𝑇))/_FldExt(𝑊 ↾_s (𝑇‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (2↑𝑛))))
53	43, 52	imbi12d 344	. . . 4 ⊢ (𝑑 = 𝑇 → ((0 < (♯‘𝑑) → ((𝑊 ↾_s (lastS‘𝑑))/_FldExt(𝑊 ↾_s (𝑑‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑑))[:](𝑊 ↾_s (𝑑‘0))) = (2↑𝑛))) ↔ (0 < (♯‘𝑇) → ((𝑊 ↾_s (lastS‘𝑇))/_FldExt(𝑊 ↾_s (𝑇‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (2↑𝑛)))))
54		fldext2chn.t	. . . 4 ⊢ (𝜑 → 𝑇 ∈ ( < Chain(SubDRing‘𝑊)))
55		0re 11237	. . . . . . . 8 ⊢ 0 ∈ ℝ
56	55	ltnri 11344	. . . . . . 7 ⊢ ¬ 0 < 0
57	56	a1i 11	. . . . . 6 ⊢ (𝜑 → ¬ 0 < 0)
58		hash0 14385	. . . . . . 7 ⊢ (♯‘∅) = 0
59	58	breq2i 5127	. . . . . 6 ⊢ (0 < (♯‘∅) ↔ 0 < 0)
60	57, 59	sylnibr 329	. . . . 5 ⊢ (𝜑 → ¬ 0 < (♯‘∅))
61	60	pm2.21d 121	. . . 4 ⊢ (𝜑 → (0 < (♯‘∅) → ((𝑊 ↾_s (lastS‘∅))/_FldExt(𝑊 ↾_s (∅‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘∅))[:](𝑊 ↾_s (∅‘0))) = (2↑𝑛))))
62		fldext2chn.w	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 ∈ Field)
63	62	ad6antr 736	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → 𝑊 ∈ Field)
64		simp-5r 785	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → 𝑔 ∈ (SubDRing‘𝑊))
65		fldsdrgfld 20758	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Field ∧ 𝑔 ∈ (SubDRing‘𝑊)) → (𝑊 ↾_s 𝑔) ∈ Field)
66	63, 64, 65	syl2anc 584	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (𝑊 ↾_s 𝑔) ∈ Field)
67		fldextid 33701	. . . . . . . . 9 ⊢ ((𝑊 ↾_s 𝑔) ∈ Field → (𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s 𝑔))
68	66, 67	syl 17	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s 𝑔))
69		simp-5r 785	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) → 𝑐 ∈ ( < Chain(SubDRing‘𝑊)))
70	69	chnwrd 32987	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) → 𝑐 ∈ Word (SubDRing‘𝑊))
71	70	adantr 480	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → 𝑐 ∈ Word (SubDRing‘𝑊))
72		lswccats1 14652	. . . . . . . . . 10 ⊢ ((𝑐 ∈ Word (SubDRing‘𝑊) ∧ 𝑔 ∈ (SubDRing‘𝑊)) → (lastS‘(𝑐 ++ ⟨“𝑔”⟩)) = 𝑔)
73	71, 64, 72	syl2anc 584	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (lastS‘(𝑐 ++ ⟨“𝑔”⟩)) = 𝑔)
74	73	oveq2d 7421	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩))) = (𝑊 ↾_s 𝑔))
75		simpr 484	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → 𝑐 = ∅)
76	75	oveq1d 7420	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (𝑐 ++ ⟨“𝑔”⟩) = (∅ ++ ⟨“𝑔”⟩))
77		s0s1 14941	. . . . . . . . . . . 12 ⊢ ⟨“𝑔”⟩ = (∅ ++ ⟨“𝑔”⟩)
78	76, 77	eqtr4di 2788	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (𝑐 ++ ⟨“𝑔”⟩) = ⟨“𝑔”⟩)
79	78	fveq1d 6878	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → ((𝑐 ++ ⟨“𝑔”⟩)‘0) = (⟨“𝑔”⟩‘0))
80		s1fv 14628	. . . . . . . . . . 11 ⊢ (𝑔 ∈ (SubDRing‘𝑊) → (⟨“𝑔”⟩‘0) = 𝑔)
81	64, 80	syl 17	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (⟨“𝑔”⟩‘0) = 𝑔)
82	79, 81	eqtrd 2770	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → ((𝑐 ++ ⟨“𝑔”⟩)‘0) = 𝑔)
83	82	oveq2d 7421	. . . . . . . 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 5151	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → (𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))/_FldExt(𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0)))
85		oveq2 7413	. . . . . . . . . 10 ⊢ (𝑚 = 0 → (2↑𝑚) = (2↑0))
86		2cn 12315	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
87		exp0 14083	. . . . . . . . . . 11 ⊢ (2 ∈ ℂ → (2↑0) = 1)
88	86, 87	ax-mp 5	. . . . . . . . . 10 ⊢ (2↑0) = 1
89	85, 88	eqtrdi 2786	. . . . . . . . 9 ⊢ (𝑚 = 0 → (2↑𝑚) = 1)
90	89	eqeq2d 2746	. . . . . . . 8 ⊢ (𝑚 = 0 → (((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚) ↔ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = 1))
91		0nn0 12516	. . . . . . . . 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 7423	. . . . . . . . 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 33702	. . . . . . . . . 10 ⊢ ((𝑊 ↾_s 𝑔) ∈ Field → ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s 𝑔)) = 1)
95	66, 94	syl 17	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s 𝑔)) = 1)
96	93, 95	eqtrd 2770	. . . . . . . 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 3604	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → ∃𝑚 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚))
98	84, 97	jca 511	. . . . . 6 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 = ∅) → ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))/_FldExt(𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0)) ∧ ∃𝑚 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚)))
99		simp-6r 787	. . . . . . . . . . . . 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 775	. . . . . . . . . . . . . 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 2937	. . . . . . . . . . . . 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 878	. . . . . . . . . . . 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 730	. . . . . . . . . . . . . 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 14586	. . . . . . . . . . . . . 14 ⊢ ((𝑐 ∈ Word (SubDRing‘𝑊) ∧ 𝑐 ≠ ∅) → (lastS‘𝑐) ∈ (SubDRing‘𝑊))
105	103, 100, 104	syl2anc 584	. . . . . . . . . . . . 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 789	. . . . . . . . . . . . 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 5128	. . . . . . . . . . . . . . . . 17 ⊢ (𝐸/_FldExt𝐹 ↔ (𝑊 ↾_s 𝑒)/_FldExt(𝑊 ↾_s 𝑓))
110	107, 108	oveq12i 7417	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐸[:]𝐹) = ((𝑊 ↾_s 𝑒)[:](𝑊 ↾_s 𝑓))
111	110	eqeq1i 2740	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐸[:]𝐹) = 2 ↔ ((𝑊 ↾_s 𝑒)[:](𝑊 ↾_s 𝑓)) = 2)
112	109, 111	anbi12i 628	. . . . . . . . . . . . . . . 16 ⊢ ((𝐸/_FldExt𝐹 ∧ (𝐸[:]𝐹) = 2) ↔ ((𝑊 ↾_s 𝑒)/_FldExt(𝑊 ↾_s 𝑓) ∧ ((𝑊 ↾_s 𝑒)[:](𝑊 ↾_s 𝑓)) = 2))
113		oveq2 7413	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑔 → (𝑊 ↾_s 𝑒) = (𝑊 ↾_s 𝑔))
114	113	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → (𝑊 ↾_s 𝑒) = (𝑊 ↾_s 𝑔))
115		oveq2 7413	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (lastS‘𝑐) → (𝑊 ↾_s 𝑓) = (𝑊 ↾_s (lastS‘𝑐)))
116	115	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → (𝑊 ↾_s 𝑓) = (𝑊 ↾_s (lastS‘𝑐)))
117	114, 116	breq12d 5132	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → ((𝑊 ↾_s 𝑒)/_FldExt(𝑊 ↾_s 𝑓) ↔ (𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (lastS‘𝑐))))
118	114, 116	oveq12d 7423	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → ((𝑊 ↾_s 𝑒)[:](𝑊 ↾_s 𝑓)) = ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s (lastS‘𝑐))))
119	118	eqeq1d 2737	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → (((𝑊 ↾_s 𝑒)[:](𝑊 ↾_s 𝑓)) = 2 ↔ ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s (lastS‘𝑐))) = 2))
120	117, 119	anbi12d 632	. . . . . . . . . . . . . . . 16 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → (((𝑊 ↾_s 𝑒)/_FldExt(𝑊 ↾_s 𝑓) ∧ ((𝑊 ↾_s 𝑒)[:](𝑊 ↾_s 𝑓)) = 2) ↔ ((𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (lastS‘𝑐)) ∧ ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s (lastS‘𝑐))) = 2)))
121	112, 120	bitrid 283	. . . . . . . . . . . . . . 15 ⊢ ((𝑒 = 𝑔 ∧ 𝑓 = (lastS‘𝑐)) → ((𝐸/_FldExt𝐹 ∧ (𝐸[:]𝐹) = 2) ↔ ((𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (lastS‘𝑐)) ∧ ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s (lastS‘𝑐))) = 2)))
122	121	ancoms 458	. . . . . . . . . . . . . 14 ⊢ ((𝑓 = (lastS‘𝑐) ∧ 𝑒 = 𝑔) → ((𝐸/_FldExt𝐹 ∧ (𝐸[:]𝐹) = 2) ↔ ((𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (lastS‘𝑐)) ∧ ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s (lastS‘𝑐))) = 2)))
123		fldext2chn.l	. . . . . . . . . . . . . 14 ⊢ < = {⟨𝑓, 𝑒⟩ ∣ (𝐸/_FldExt𝐹 ∧ (𝐸[:]𝐹) = 2)}
124	122, 123	brabga 5509	. . . . . . . . . . . . 13 ⊢ (((lastS‘𝑐) ∈ (SubDRing‘𝑊) ∧ 𝑔 ∈ (SubDRing‘𝑊)) → ((lastS‘𝑐) < 𝑔 ↔ ((𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (lastS‘𝑐)) ∧ ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s (lastS‘𝑐))) = 2)))
125	105, 106, 124	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → ((lastS‘𝑐) < 𝑔 ↔ ((𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (lastS‘𝑐)) ∧ ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s (lastS‘𝑐))) = 2)))
126	102, 125	mpbid 232	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → ((𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (lastS‘𝑐)) ∧ ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s (lastS‘𝑐))) = 2))
127	126	simpld 494	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → (𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (lastS‘𝑐)))
128		hashgt0 14406	. . . . . . . . . . . . . 14 ⊢ ((𝑐 ∈ ( < Chain(SubDRing‘𝑊)) ∧ 𝑐 ≠ ∅) → 0 < (♯‘𝑐))
129	69, 128	sylan 580	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → 0 < (♯‘𝑐))
130		simpllr 775	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛))))
131	129, 130	mpd 15	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))
132	131	simprd 495	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛))
133		oveq2 7413	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑜 → (2↑𝑛) = (2↑𝑜))
134	133	eqeq2d 2746	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑜 → (((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛) ↔ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)))
135	134	cbvrexvw 3221	. . . . . . . . . . 11 ⊢ (∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛) ↔ ∃𝑜 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜))
136	132, 135	sylib 218	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → ∃𝑜 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜))
137	127, 136	r19.29a 3148	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → (𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (lastS‘𝑐)))
138	131	simpld 494	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → (𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)))
139		fldexttr 33700	. . . . . . . . 9 ⊢ (((𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (lastS‘𝑐)) ∧ (𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0))) → (𝑊 ↾_s 𝑔)/_FldExt(𝑊 ↾_s (𝑐‘0)))
140	137, 138, 139	syl2anc 584	. . . . . . . 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 584	. . . . . . . . . 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 7421	. . . . . . . . 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 3148	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → (𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩))) = (𝑊 ↾_s 𝑔))
144	106	s1cld 14621	. . . . . . . . . . 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 726	. . . . . . . . . . 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 14601	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ Word (SubDRing‘𝑊) ∧ ⟨“𝑔”⟩ ∈ Word (SubDRing‘𝑊) ∧ 0 < (♯‘𝑐)) → ((𝑐 ++ ⟨“𝑔”⟩)‘0) = (𝑐‘0))
147	103, 144, 145, 146	syl3anc 1373	. . . . . . . . . 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 7421	. . . . . . . . 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 3148	. . . . . . . 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 5151	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → (𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))/_FldExt(𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0)))
151		oveq2 7413	. . . . . . . . . 10 ⊢ (𝑚 = (𝑜 + 1) → (2↑𝑚) = (2↑(𝑜 + 1)))
152	151	eqeq2d 2746	. . . . . . . . 9 ⊢ (𝑚 = (𝑜 + 1) → (((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚) ↔ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑(𝑜 + 1))))
153		simplr 768	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → 𝑜 ∈ ℕ₀)
154		1nn0 12517	. . . . . . . . . . 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 12566	. . . . . . . . 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 7423	. . . . . . . . . 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 726	. . . . . . . . . . 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 33705	. . . . . . . . . . 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 584	. . . . . . . . . 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 14164	. . . . . . . . . . . 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 11256	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → (2 · (2↑𝑜)) = ((2↑𝑜) · 2))
164	126	simprd 495	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → ((𝑊 ↾_s 𝑔)[:](𝑊 ↾_s (lastS‘𝑐))) = 2)
165		simpr 484	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) ∧ 𝑜 ∈ ℕ₀) ∧ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜)) → ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑜))
166	164, 165	oveq12d 7423	. . . . . . . . . . . 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 14181	. . . . . . . . . . . . 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 13287	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ ∧ (2↑𝑜) ∈ ℝ) → (2 ·_e (2↑𝑜)) = (2 · (2↑𝑜)))
171	168, 169, 170	syl2anc 584	. . . . . . . . . . . 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 2770	. . . . . . . . . . 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 14165	. . . . . . . . . . 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 2780	. . . . . . . . . 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 2774	. . . . . . . . 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 3604	. . . . . . . 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 3148	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → ∃𝑚 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚))
178	150, 177	jca 511	. . . . . 6 ⊢ (((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) ∧ 𝑐 ≠ ∅) → ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))/_FldExt(𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0)) ∧ ∃𝑚 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚)))
179	98, 178	pm2.61dane 3019	. . . . 5 ⊢ ((((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) ∧ 0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩))) → ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))/_FldExt(𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0)) ∧ ∃𝑚 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚)))
180	179	ex 412	. . . 4 ⊢ (((((𝜑 ∧ 𝑐 ∈ ( < Chain(SubDRing‘𝑊))) ∧ 𝑔 ∈ (SubDRing‘𝑊)) ∧ (𝑐 = ∅ ∨ (lastS‘𝑐) < 𝑔)) ∧ (0 < (♯‘𝑐) → ((𝑊 ↾_s (lastS‘𝑐))/_FldExt(𝑊 ↾_s (𝑐‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑐))[:](𝑊 ↾_s (𝑐‘0))) = (2↑𝑛)))) → (0 < (♯‘(𝑐 ++ ⟨“𝑔”⟩)) → ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))/_FldExt(𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0)) ∧ ∃𝑚 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘(𝑐 ++ ⟨“𝑔”⟩)))[:](𝑊 ↾_s ((𝑐 ++ ⟨“𝑔”⟩)‘0))) = (2↑𝑚))))
181	13, 25, 41, 53, 54, 61, 180	chnind 32991	. . 3 ⊢ (𝜑 → (0 < (♯‘𝑇) → ((𝑊 ↾_s (lastS‘𝑇))/_FldExt(𝑊 ↾_s (𝑇‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (2↑𝑛))))
182	1, 181	mpd 15	. 2 ⊢ (𝜑 → ((𝑊 ↾_s (lastS‘𝑇))/_FldExt(𝑊 ↾_s (𝑇‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (2↑𝑛)))
183		fldext2chn.2	. . . 4 ⊢ (𝜑 → (𝑊 ↾_s (lastS‘𝑇)) = 𝐿)
184		fldext2chn.1	. . . 4 ⊢ (𝜑 → (𝑊 ↾_s (𝑇‘0)) = 𝑄)
185	183, 184	breq12d 5132	. . 3 ⊢ (𝜑 → ((𝑊 ↾_s (lastS‘𝑇))/_FldExt(𝑊 ↾_s (𝑇‘0)) ↔ 𝐿/_FldExt𝑄))
186	183, 184	oveq12d 7423	. . . . 5 ⊢ (𝜑 → ((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (𝐿[:]𝑄))
187	186	eqeq1d 2737	. . . 4 ⊢ (𝜑 → (((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (2↑𝑛) ↔ (𝐿[:]𝑄) = (2↑𝑛)))
188	187	rexbidv 3164	. . 3 ⊢ (𝜑 → (∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (2↑𝑛) ↔ ∃𝑛 ∈ ℕ₀ (𝐿[:]𝑄) = (2↑𝑛)))
189	185, 188	anbi12d 632	. 2 ⊢ (𝜑 → (((𝑊 ↾_s (lastS‘𝑇))/_FldExt(𝑊 ↾_s (𝑇‘0)) ∧ ∃𝑛 ∈ ℕ₀ ((𝑊 ↾_s (lastS‘𝑇))[:](𝑊 ↾_s (𝑇‘0))) = (2↑𝑛)) ↔ (𝐿/_FldExt𝑄 ∧ ∃𝑛 ∈ ℕ₀ (𝐿[:]𝑄) = (2↑𝑛))))
190	182, 189	mpbid 232	1 ⊢ (𝜑 → (𝐿/_FldExt𝑄 ∧ ∃𝑛 ∈ ℕ₀ (𝐿[:]𝑄) = (2↑𝑛)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 = wceq 1540 ∈ wcel 2108 ≠ wne 2932 ∃wrex 3060 ∅c0 4308 class class class wbr 5119 {copab 5181 ‘cfv 6531 (class class class)co 7405 ℂcc 11127 ℝcr 11128 0cc0 11129 1c1 11130 + caddc 11132 · cmul 11134 < clt 11269 2c2 12295 ℕ₀cn0 12501 ·_e cxmu 13127 ↑cexp 14079 ♯chash 14348 Word cword 14531 lastSclsw 14580 ++ cconcat 14588 ⟨“cs1 14613 ↾_s cress 17251 Fieldcfield 20690 SubDRingcsdrg 20746 Chaincchn 32984 /_FldExtcfldext 33678 [:]cextdg 33681

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-rep 5249 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7729 ax-reg 9606 ax-inf2 9655 ax-ac2 10477 ax-cnex 11185 ax-resscn 11186 ax-1cn 11187 ax-icn 11188 ax-addcl 11189 ax-addrcl 11190 ax-mulcl 11191 ax-mulrcl 11192 ax-mulcom 11193 ax-addass 11194 ax-mulass 11195 ax-distr 11196 ax-i2m1 11197 ax-1ne0 11198 ax-1rid 11199 ax-rnegex 11200 ax-rrecex 11201 ax-cnre 11202 ax-pre-lttri 11203 ax-pre-lttrn 11204 ax-pre-ltadd 11205 ax-pre-mulgt0 11206

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3359 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-tp 4606 df-op 4608 df-uni 4884 df-int 4923 df-iun 4969 df-iin 4970 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-se 5607 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6290 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6484 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-isom 6540 df-riota 7362 df-ov 7408 df-oprab 7409 df-mpo 7410 df-of 7671 df-rpss 7717 df-om 7862 df-1st 7988 df-2nd 7989 df-supp 8160 df-tpos 8225 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-1o 8480 df-2o 8481 df-oadd 8484 df-er 8719 df-map 8842 df-ixp 8912 df-en 8960 df-dom 8961 df-sdom 8962 df-fin 8963 df-fsupp 9374 df-sup 9454 df-oi 9524 df-r1 9778 df-rank 9779 df-dju 9915 df-card 9953 df-acn 9956 df-ac 10130 df-pnf 11271 df-mnf 11272 df-xr 11273 df-ltxr 11274 df-le 11275 df-sub 11468 df-neg 11469 df-nn 12241 df-2 12303 df-3 12304 df-4 12305 df-5 12306 df-6 12307 df-7 12308 df-8 12309 df-9 12310 df-n0 12502 df-xnn0 12575 df-z 12589 df-dec 12709 df-uz 12853 df-rp 13009 df-xmul 13130 df-fz 13525 df-fzo 13672 df-seq 14020 df-exp 14080 df-hash 14349 df-word 14532 df-lsw 14581 df-concat 14589 df-s1 14614 df-substr 14659 df-pfx 14689 df-struct 17166 df-sets 17183 df-slot 17201 df-ndx 17213 df-base 17229 df-ress 17252 df-plusg 17284 df-mulr 17285 df-sca 17287 df-vsca 17288 df-ip 17289 df-tset 17290 df-ple 17291 df-ocomp 17292 df-ds 17293 df-hom 17295 df-cco 17296 df-0g 17455 df-gsum 17456 df-prds 17461 df-pws 17463 df-mre 17598 df-mrc 17599 df-mri 17600 df-acs 17601 df-proset 18306 df-drs 18307 df-poset 18325 df-ipo 18538 df-mgm 18618 df-sgrp 18697 df-mnd 18713 df-mhm 18761 df-submnd 18762 df-grp 18919 df-minusg 18920 df-sbg 18921 df-mulg 19051 df-subg 19106 df-ghm 19196 df-cntz 19300 df-cmn 19763 df-abl 19764 df-mgp 20101 df-rng 20113 df-ur 20142 df-ring 20195 df-cring 20196 df-oppr 20297 df-dvdsr 20317 df-unit 20318 df-invr 20348 df-nzr 20473 df-subrng 20506 df-subrg 20530 df-drng 20691 df-field 20692 df-sdrg 20747 df-lmod 20819 df-lss 20889 df-lsp 20929 df-lmhm 20980 df-lbs 21033 df-lvec 21061 df-sra 21131 df-rgmod 21132 df-lidl 21169 df-rsp 21170 df-dsmm 21692 df-frlm 21707 df-uvc 21743 df-lindf 21766 df-linds 21767 df-chn 32985 df-dim 33639 df-fldext 33682 df-extdg 33683

This theorem is referenced by: constrext2chnlem 33784

W3C validator