fldext2chn

Description: In a non-empty chain T of quadratic field extensions, the degree of the final extension is always a power of two. (Contributed by Thierry Arnoux, 19-Oct-2025)

	Ref	Expression
Hypotheses	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	fldext2chn	⊢ ( 𝜑 → ( 𝐿 /_FldExt 𝑄 ∧ ∃ 𝑛 ∈ ℕ₀ ( 𝐿 [:] 𝑄 ) = ( 2 ↑ 𝑛 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fldext2chn.e	⊢ 𝐸 = ( 𝑊 ↾_s 𝑒 )
2		fldext2chn.f	⊢ 𝐹 = ( 𝑊 ↾_s 𝑓 )
3		fldext2chn.l	⊢ < = { ⟨ 𝑓 , 𝑒 ⟩ ∣ ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 2 ) }
4		fldext2chn.t	⊢ ( 𝜑 → 𝑇 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) )
5		fldext2chn.w	⊢ ( 𝜑 → 𝑊 ∈ Field )
6		fldext2chn.1	⊢ ( 𝜑 → ( 𝑊 ↾_s ( 𝑇 ‘ 0 ) ) = 𝑄 )
7		fldext2chn.2	⊢ ( 𝜑 → ( 𝑊 ↾_s ( lastS ‘ 𝑇 ) ) = 𝐿 )
8		fldext2chn.3	⊢ ( 𝜑 → 0 < ( ♯ ‘ 𝑇 ) )
9		fveq2	⊢ ( 𝑑 = ∅ → ( ♯ ‘ 𝑑 ) = ( ♯ ‘ ∅ ) )
10	9	breq2d	⊢ ( 𝑑 = ∅ → ( 0 < ( ♯ ‘ 𝑑 ) ↔ 0 < ( ♯ ‘ ∅ ) ) )
11		fveq2	⊢ ( 𝑑 = ∅ → ( lastS ‘ 𝑑 ) = ( lastS ‘ ∅ ) )
12	11	oveq2d	⊢ ( 𝑑 = ∅ → ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) = ( 𝑊 ↾_s ( lastS ‘ ∅ ) ) )
13		fveq1	⊢ ( 𝑑 = ∅ → ( 𝑑 ‘ 0 ) = ( ∅ ‘ 0 ) )
14	13	oveq2d	⊢ ( 𝑑 = ∅ → ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) = ( 𝑊 ↾_s ( ∅ ‘ 0 ) ) )
15	12 14	breq12d	⊢ ( 𝑑 = ∅ → ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ↔ ( 𝑊 ↾_s ( lastS ‘ ∅ ) ) /_FldExt ( 𝑊 ↾_s ( ∅ ‘ 0 ) ) ) )
16	12 14	oveq12d	⊢ ( 𝑑 = ∅ → ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) [:] ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ) = ( ( 𝑊 ↾_s ( lastS ‘ ∅ ) ) [:] ( 𝑊 ↾_s ( ∅ ‘ 0 ) ) ) )
17	16	eqeq1d	⊢ ( 𝑑 = ∅ → ( ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) [:] ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ↔ ( ( 𝑊 ↾_s ( lastS ‘ ∅ ) ) [:] ( 𝑊 ↾_s ( ∅ ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) )
18	17	rexbidv	⊢ ( 𝑑 = ∅ → ( ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) [:] ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ ∅ ) ) [:] ( 𝑊 ↾_s ( ∅ ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) )
19	15 18	anbi12d	⊢ ( 𝑑 = ∅ → ( ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) [:] ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ↔ ( ( 𝑊 ↾_s ( lastS ‘ ∅ ) ) /_FldExt ( 𝑊 ↾_s ( ∅ ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ ∅ ) ) [:] ( 𝑊 ↾_s ( ∅ ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) )
20	10 19	imbi12d	⊢ ( 𝑑 = ∅ → ( ( 0 < ( ♯ ‘ 𝑑 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) [:] ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ↔ ( 0 < ( ♯ ‘ ∅ ) → ( ( 𝑊 ↾_s ( lastS ‘ ∅ ) ) /_FldExt ( 𝑊 ↾_s ( ∅ ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ ∅ ) ) [:] ( 𝑊 ↾_s ( ∅ ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) )
21		fveq2	⊢ ( 𝑑 = 𝑐 → ( ♯ ‘ 𝑑 ) = ( ♯ ‘ 𝑐 ) )
22	21	breq2d	⊢ ( 𝑑 = 𝑐 → ( 0 < ( ♯ ‘ 𝑑 ) ↔ 0 < ( ♯ ‘ 𝑐 ) ) )
23		fveq2	⊢ ( 𝑑 = 𝑐 → ( lastS ‘ 𝑑 ) = ( lastS ‘ 𝑐 ) )
24	23	oveq2d	⊢ ( 𝑑 = 𝑐 → ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) = ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) )
25		fveq1	⊢ ( 𝑑 = 𝑐 → ( 𝑑 ‘ 0 ) = ( 𝑐 ‘ 0 ) )
26	25	oveq2d	⊢ ( 𝑑 = 𝑐 → ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) = ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) )
27	24 26	breq12d	⊢ ( 𝑑 = 𝑐 → ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ↔ ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) )
28	24 26	oveq12d	⊢ ( 𝑑 = 𝑐 → ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) [:] ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ) = ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) )
29	28	eqeq1d	⊢ ( 𝑑 = 𝑐 → ( ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) [:] ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ↔ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) )
30	29	rexbidv	⊢ ( 𝑑 = 𝑐 → ( ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) [:] ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) )
31	27 30	anbi12d	⊢ ( 𝑑 = 𝑐 → ( ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) [:] ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ↔ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) )
32	22 31	imbi12d	⊢ ( 𝑑 = 𝑐 → ( ( 0 < ( ♯ ‘ 𝑑 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) [:] ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ↔ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) )
33		fveq2	⊢ ( 𝑑 = ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) → ( ♯ ‘ 𝑑 ) = ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) )
34	33	breq2d	⊢ ( 𝑑 = ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) → ( 0 < ( ♯ ‘ 𝑑 ) ↔ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) )
35		fveq2	⊢ ( 𝑑 = ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) → ( lastS ‘ 𝑑 ) = ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) )
36	35	oveq2d	⊢ ( 𝑑 = ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) → ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) = ( 𝑊 ↾_s ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) )
37		fveq1	⊢ ( 𝑑 = ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) → ( 𝑑 ‘ 0 ) = ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) )
38	37	oveq2d	⊢ ( 𝑑 = ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) → ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) = ( 𝑊 ↾_s ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) ) )
39	36 38	breq12d	⊢ ( 𝑑 = ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ↔ ( 𝑊 ↾_s ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) /_FldExt ( 𝑊 ↾_s ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) ) ) )
40	36 38	oveq12d	⊢ ( 𝑑 = ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) [:] ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ) = ( ( 𝑊 ↾_s ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) [:] ( 𝑊 ↾_s ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) ) ) )
41	40	eqeq1d	⊢ ( 𝑑 = ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) → ( ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) [:] ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ↔ ( ( 𝑊 ↾_s ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) [:] ( 𝑊 ↾_s ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) )
42	41	rexbidv	⊢ ( 𝑑 = ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) → ( ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) [:] ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) [:] ( 𝑊 ↾_s ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) )
43		oveq2	⊢ ( 𝑛 = 𝑚 → ( 2 ↑ 𝑛 ) = ( 2 ↑ 𝑚 ) )
44	43	eqeq2d	⊢ ( 𝑛 = 𝑚 → ( ( ( 𝑊 ↾_s ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) [:] ( 𝑊 ↾_s ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ↔ ( ( 𝑊 ↾_s ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) [:] ( 𝑊 ↾_s ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) ) ) = ( 2 ↑ 𝑚 ) ) )
45	44	cbvrexvw	⊢ ( ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) [:] ( 𝑊 ↾_s ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ↔ ∃ 𝑚 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) [:] ( 𝑊 ↾_s ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) ) ) = ( 2 ↑ 𝑚 ) )
46	42 45	bitrdi	⊢ ( 𝑑 = ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) → ( ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) [:] ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ↔ ∃ 𝑚 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) [:] ( 𝑊 ↾_s ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) ) ) = ( 2 ↑ 𝑚 ) ) )
47	39 46	anbi12d	⊢ ( 𝑑 = ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) → ( ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) [:] ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ↔ ( ( 𝑊 ↾_s ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) /_FldExt ( 𝑊 ↾_s ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) ) ∧ ∃ 𝑚 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) [:] ( 𝑊 ↾_s ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) ) ) = ( 2 ↑ 𝑚 ) ) ) )
48	34 47	imbi12d	⊢ ( 𝑑 = ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) → ( ( 0 < ( ♯ ‘ 𝑑 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) [:] ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ↔ ( 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) → ( ( 𝑊 ↾_s ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) /_FldExt ( 𝑊 ↾_s ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) ) ∧ ∃ 𝑚 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) [:] ( 𝑊 ↾_s ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) ) ) = ( 2 ↑ 𝑚 ) ) ) ) )
49		fveq2	⊢ ( 𝑑 = 𝑇 → ( ♯ ‘ 𝑑 ) = ( ♯ ‘ 𝑇 ) )
50	49	breq2d	⊢ ( 𝑑 = 𝑇 → ( 0 < ( ♯ ‘ 𝑑 ) ↔ 0 < ( ♯ ‘ 𝑇 ) ) )
51		fveq2	⊢ ( 𝑑 = 𝑇 → ( lastS ‘ 𝑑 ) = ( lastS ‘ 𝑇 ) )
52	51	oveq2d	⊢ ( 𝑑 = 𝑇 → ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) = ( 𝑊 ↾_s ( lastS ‘ 𝑇 ) ) )
53		fveq1	⊢ ( 𝑑 = 𝑇 → ( 𝑑 ‘ 0 ) = ( 𝑇 ‘ 0 ) )
54	53	oveq2d	⊢ ( 𝑑 = 𝑇 → ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) = ( 𝑊 ↾_s ( 𝑇 ‘ 0 ) ) )
55	52 54	breq12d	⊢ ( 𝑑 = 𝑇 → ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ↔ ( 𝑊 ↾_s ( lastS ‘ 𝑇 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑇 ‘ 0 ) ) ) )
56	52 54	oveq12d	⊢ ( 𝑑 = 𝑇 → ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) [:] ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ) = ( ( 𝑊 ↾_s ( lastS ‘ 𝑇 ) ) [:] ( 𝑊 ↾_s ( 𝑇 ‘ 0 ) ) ) )
57	56	eqeq1d	⊢ ( 𝑑 = 𝑇 → ( ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) [:] ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ↔ ( ( 𝑊 ↾_s ( lastS ‘ 𝑇 ) ) [:] ( 𝑊 ↾_s ( 𝑇 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) )
58	57	rexbidv	⊢ ( 𝑑 = 𝑇 → ( ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) [:] ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑇 ) ) [:] ( 𝑊 ↾_s ( 𝑇 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) )
59	55 58	anbi12d	⊢ ( 𝑑 = 𝑇 → ( ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) [:] ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ↔ ( ( 𝑊 ↾_s ( lastS ‘ 𝑇 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑇 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑇 ) ) [:] ( 𝑊 ↾_s ( 𝑇 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) )
60	50 59	imbi12d	⊢ ( 𝑑 = 𝑇 → ( ( 0 < ( ♯ ‘ 𝑑 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑑 ) ) [:] ( 𝑊 ↾_s ( 𝑑 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ↔ ( 0 < ( ♯ ‘ 𝑇 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑇 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑇 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑇 ) ) [:] ( 𝑊 ↾_s ( 𝑇 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) )
61		0re	⊢ 0 ∈ ℝ
62	61	ltnri	⊢ ¬ 0 < 0
63	62	a1i	⊢ ( 𝜑 → ¬ 0 < 0 )
64		hash0	⊢ ( ♯ ‘ ∅ ) = 0
65	64	breq2i	⊢ ( 0 < ( ♯ ‘ ∅ ) ↔ 0 < 0 )
66	63 65	sylnibr	⊢ ( 𝜑 → ¬ 0 < ( ♯ ‘ ∅ ) )
67	66	pm2.21d	⊢ ( 𝜑 → ( 0 < ( ♯ ‘ ∅ ) → ( ( 𝑊 ↾_s ( lastS ‘ ∅ ) ) /_FldExt ( 𝑊 ↾_s ( ∅ ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ ∅ ) ) [:] ( 𝑊 ↾_s ( ∅ ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) )
68	5	ad6antr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 = ∅ ) → 𝑊 ∈ Field )
69		simp-5r	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 = ∅ ) → 𝑔 ∈ ( SubDRing ‘ 𝑊 ) )
70		fldsdrgfld	⊢ ( ( 𝑊 ∈ Field ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) → ( 𝑊 ↾_s 𝑔 ) ∈ Field )
71	68 69 70	syl2anc	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 = ∅ ) → ( 𝑊 ↾_s 𝑔 ) ∈ Field )
72		fldextid	⊢ ( ( 𝑊 ↾_s 𝑔 ) ∈ Field → ( 𝑊 ↾_s 𝑔 ) /_FldExt ( 𝑊 ↾_s 𝑔 ) )
73	71 72	syl	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 = ∅ ) → ( 𝑊 ↾_s 𝑔 ) /_FldExt ( 𝑊 ↾_s 𝑔 ) )
74		simp-5r	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) → 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) )
75	74	chnwrd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) → 𝑐 ∈ Word ( SubDRing ‘ 𝑊 ) )
76	75	adantr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 = ∅ ) → 𝑐 ∈ Word ( SubDRing ‘ 𝑊 ) )
77		lswccats1	⊢ ( ( 𝑐 ∈ Word ( SubDRing ‘ 𝑊 ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) → ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) = 𝑔 )
78	76 69 77	syl2anc	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 = ∅ ) → ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) = 𝑔 )
79	78	oveq2d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 = ∅ ) → ( 𝑊 ↾_s ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) = ( 𝑊 ↾_s 𝑔 ) )
80		simpr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 = ∅ ) → 𝑐 = ∅ )
81	80	oveq1d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 = ∅ ) → ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) = ( ∅ ++ ⟨“ 𝑔 ”⟩ ) )
82		s0s1	⊢ ⟨“ 𝑔 ”⟩ = ( ∅ ++ ⟨“ 𝑔 ”⟩ )
83	81 82	eqtr4di	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 = ∅ ) → ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) = ⟨“ 𝑔 ”⟩ )
84	83	fveq1d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 = ∅ ) → ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) = ( ⟨“ 𝑔 ”⟩ ‘ 0 ) )
85		s1fv	⊢ ( 𝑔 ∈ ( SubDRing ‘ 𝑊 ) → ( ⟨“ 𝑔 ”⟩ ‘ 0 ) = 𝑔 )
86	69 85	syl	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 = ∅ ) → ( ⟨“ 𝑔 ”⟩ ‘ 0 ) = 𝑔 )
87	84 86	eqtrd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 = ∅ ) → ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) = 𝑔 )
88	87	oveq2d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 = ∅ ) → ( 𝑊 ↾_s ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) ) = ( 𝑊 ↾_s 𝑔 ) )
89	73 79 88	3brtr4d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 = ∅ ) → ( 𝑊 ↾_s ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) /_FldExt ( 𝑊 ↾_s ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) ) )
90		oveq2	⊢ ( 𝑚 = 0 → ( 2 ↑ 𝑚 ) = ( 2 ↑ 0 ) )
91		2cn	⊢ 2 ∈ ℂ
92		exp0	⊢ ( 2 ∈ ℂ → ( 2 ↑ 0 ) = 1 )
93	91 92	ax-mp	⊢ ( 2 ↑ 0 ) = 1
94	90 93	eqtrdi	⊢ ( 𝑚 = 0 → ( 2 ↑ 𝑚 ) = 1 )
95	94	eqeq2d	⊢ ( 𝑚 = 0 → ( ( ( 𝑊 ↾_s ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) [:] ( 𝑊 ↾_s ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) ) ) = ( 2 ↑ 𝑚 ) ↔ ( ( 𝑊 ↾_s ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) [:] ( 𝑊 ↾_s ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) ) ) = 1 ) )
96		0nn0	⊢ 0 ∈ ℕ₀
97	96	a1i	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 = ∅ ) → 0 ∈ ℕ₀ )
98	79 88	oveq12d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 = ∅ ) → ( ( 𝑊 ↾_s ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) [:] ( 𝑊 ↾_s ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) ) ) = ( ( 𝑊 ↾_s 𝑔 ) [:] ( 𝑊 ↾_s 𝑔 ) ) )
99		extdgid	⊢ ( ( 𝑊 ↾_s 𝑔 ) ∈ Field → ( ( 𝑊 ↾_s 𝑔 ) [:] ( 𝑊 ↾_s 𝑔 ) ) = 1 )
100	71 99	syl	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 = ∅ ) → ( ( 𝑊 ↾_s 𝑔 ) [:] ( 𝑊 ↾_s 𝑔 ) ) = 1 )
101	98 100	eqtrd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 = ∅ ) → ( ( 𝑊 ↾_s ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) [:] ( 𝑊 ↾_s ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) ) ) = 1 )
102	95 97 101	rspcedvdw	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 = ∅ ) → ∃ 𝑚 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) [:] ( 𝑊 ↾_s ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) ) ) = ( 2 ↑ 𝑚 ) )
103	89 102	jca	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < 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 ↑ 𝑚 ) ) )
104		simp-6r	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 ≠ ∅ ) ∧ 𝑜 ∈ ℕ₀ ) ∧ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑜 ) ) → ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) )
105		simpllr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 ≠ ∅ ) ∧ 𝑜 ∈ ℕ₀ ) ∧ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑜 ) ) → 𝑐 ≠ ∅ )
106	105	neneqd	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 ≠ ∅ ) ∧ 𝑜 ∈ ℕ₀ ) ∧ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑜 ) ) → ¬ 𝑐 = ∅ )
107	104 106	orcnd	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 ≠ ∅ ) ∧ 𝑜 ∈ ℕ₀ ) ∧ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑜 ) ) → ( lastS ‘ 𝑐 ) < 𝑔 )
108	75	ad3antrrr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 ≠ ∅ ) ∧ 𝑜 ∈ ℕ₀ ) ∧ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑜 ) ) → 𝑐 ∈ Word ( SubDRing ‘ 𝑊 ) )
109		lswcl	⊢ ( ( 𝑐 ∈ Word ( SubDRing ‘ 𝑊 ) ∧ 𝑐 ≠ ∅ ) → ( lastS ‘ 𝑐 ) ∈ ( SubDRing ‘ 𝑊 ) )
110	108 105 109	syl2anc	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 ≠ ∅ ) ∧ 𝑜 ∈ ℕ₀ ) ∧ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑜 ) ) → ( lastS ‘ 𝑐 ) ∈ ( SubDRing ‘ 𝑊 ) )
111		simp-7r	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 ≠ ∅ ) ∧ 𝑜 ∈ ℕ₀ ) ∧ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑜 ) ) → 𝑔 ∈ ( SubDRing ‘ 𝑊 ) )
112	1 2	breq12i	⊢ ( 𝐸 /_FldExt 𝐹 ↔ ( 𝑊 ↾_s 𝑒 ) /_FldExt ( 𝑊 ↾_s 𝑓 ) )
113	1 2	oveq12i	⊢ ( 𝐸 [:] 𝐹 ) = ( ( 𝑊 ↾_s 𝑒 ) [:] ( 𝑊 ↾_s 𝑓 ) )
114	113	eqeq1i	⊢ ( ( 𝐸 [:] 𝐹 ) = 2 ↔ ( ( 𝑊 ↾_s 𝑒 ) [:] ( 𝑊 ↾_s 𝑓 ) ) = 2 )
115	112 114	anbi12i	⊢ ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 2 ) ↔ ( ( 𝑊 ↾_s 𝑒 ) /_FldExt ( 𝑊 ↾_s 𝑓 ) ∧ ( ( 𝑊 ↾_s 𝑒 ) [:] ( 𝑊 ↾_s 𝑓 ) ) = 2 ) )
116		oveq2	⊢ ( 𝑒 = 𝑔 → ( 𝑊 ↾_s 𝑒 ) = ( 𝑊 ↾_s 𝑔 ) )
117	116	adantr	⊢ ( ( 𝑒 = 𝑔 ∧ 𝑓 = ( lastS ‘ 𝑐 ) ) → ( 𝑊 ↾_s 𝑒 ) = ( 𝑊 ↾_s 𝑔 ) )
118		oveq2	⊢ ( 𝑓 = ( lastS ‘ 𝑐 ) → ( 𝑊 ↾_s 𝑓 ) = ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) )
119	118	adantl	⊢ ( ( 𝑒 = 𝑔 ∧ 𝑓 = ( lastS ‘ 𝑐 ) ) → ( 𝑊 ↾_s 𝑓 ) = ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) )
120	117 119	breq12d	⊢ ( ( 𝑒 = 𝑔 ∧ 𝑓 = ( lastS ‘ 𝑐 ) ) → ( ( 𝑊 ↾_s 𝑒 ) /_FldExt ( 𝑊 ↾_s 𝑓 ) ↔ ( 𝑊 ↾_s 𝑔 ) /_FldExt ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) ) )
121	117 119	oveq12d	⊢ ( ( 𝑒 = 𝑔 ∧ 𝑓 = ( lastS ‘ 𝑐 ) ) → ( ( 𝑊 ↾_s 𝑒 ) [:] ( 𝑊 ↾_s 𝑓 ) ) = ( ( 𝑊 ↾_s 𝑔 ) [:] ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) ) )
122	121	eqeq1d	⊢ ( ( 𝑒 = 𝑔 ∧ 𝑓 = ( lastS ‘ 𝑐 ) ) → ( ( ( 𝑊 ↾_s 𝑒 ) [:] ( 𝑊 ↾_s 𝑓 ) ) = 2 ↔ ( ( 𝑊 ↾_s 𝑔 ) [:] ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) ) = 2 ) )
123	120 122	anbi12d	⊢ ( ( 𝑒 = 𝑔 ∧ 𝑓 = ( lastS ‘ 𝑐 ) ) → ( ( ( 𝑊 ↾_s 𝑒 ) /_FldExt ( 𝑊 ↾_s 𝑓 ) ∧ ( ( 𝑊 ↾_s 𝑒 ) [:] ( 𝑊 ↾_s 𝑓 ) ) = 2 ) ↔ ( ( 𝑊 ↾_s 𝑔 ) /_FldExt ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) ∧ ( ( 𝑊 ↾_s 𝑔 ) [:] ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) ) = 2 ) ) )
124	115 123	bitrid	⊢ ( ( 𝑒 = 𝑔 ∧ 𝑓 = ( lastS ‘ 𝑐 ) ) → ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 2 ) ↔ ( ( 𝑊 ↾_s 𝑔 ) /_FldExt ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) ∧ ( ( 𝑊 ↾_s 𝑔 ) [:] ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) ) = 2 ) ) )
125	124	ancoms	⊢ ( ( 𝑓 = ( lastS ‘ 𝑐 ) ∧ 𝑒 = 𝑔 ) → ( ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 2 ) ↔ ( ( 𝑊 ↾_s 𝑔 ) /_FldExt ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) ∧ ( ( 𝑊 ↾_s 𝑔 ) [:] ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) ) = 2 ) ) )
126	125 3	brabga	⊢ ( ( ( lastS ‘ 𝑐 ) ∈ ( SubDRing ‘ 𝑊 ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) → ( ( lastS ‘ 𝑐 ) < 𝑔 ↔ ( ( 𝑊 ↾_s 𝑔 ) /_FldExt ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) ∧ ( ( 𝑊 ↾_s 𝑔 ) [:] ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) ) = 2 ) ) )
127	110 111 126	syl2anc	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < 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 ) ) )
128	107 127	mpbid	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < 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 ) )
129	128	simpld	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < 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 ‘ 𝑐 ) ) )
130		hashgt0	⊢ ( ( 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ∧ 𝑐 ≠ ∅ ) → 0 < ( ♯ ‘ 𝑐 ) )
131	74 130	sylan	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 ≠ ∅ ) → 0 < ( ♯ ‘ 𝑐 ) )
132		simpllr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < 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 ↑ 𝑛 ) ) ) )
133	131 132	mpd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < 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 ↑ 𝑛 ) ) )
134	133	simprd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 ≠ ∅ ) → ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) )
135		oveq2	⊢ ( 𝑛 = 𝑜 → ( 2 ↑ 𝑛 ) = ( 2 ↑ 𝑜 ) )
136	135	eqeq2d	⊢ ( 𝑛 = 𝑜 → ( ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ↔ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑜 ) ) )
137	136	cbvrexvw	⊢ ( ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ↔ ∃ 𝑜 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑜 ) )
138	134 137	sylib	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 ≠ ∅ ) → ∃ 𝑜 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑜 ) )
139	129 138	r19.29a	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 ≠ ∅ ) → ( 𝑊 ↾_s 𝑔 ) /_FldExt ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) )
140	133	simpld	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 ≠ ∅ ) → ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) )
141		fldexttr	⊢ ( ( ( 𝑊 ↾_s 𝑔 ) /_FldExt ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) ∧ ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) → ( 𝑊 ↾_s 𝑔 ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) )
142	139 140 141	syl2anc	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 ≠ ∅ ) → ( 𝑊 ↾_s 𝑔 ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) )
143	108 111 77	syl2anc	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 ≠ ∅ ) ∧ 𝑜 ∈ ℕ₀ ) ∧ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑜 ) ) → ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) = 𝑔 )
144	143	oveq2d	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 ≠ ∅ ) ∧ 𝑜 ∈ ℕ₀ ) ∧ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑜 ) ) → ( 𝑊 ↾_s ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) = ( 𝑊 ↾_s 𝑔 ) )
145	144 138	r19.29a	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 ≠ ∅ ) → ( 𝑊 ↾_s ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) = ( 𝑊 ↾_s 𝑔 ) )
146	111	s1cld	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 ≠ ∅ ) ∧ 𝑜 ∈ ℕ₀ ) ∧ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑜 ) ) → ⟨“ 𝑔 ”⟩ ∈ Word ( SubDRing ‘ 𝑊 ) )
147	131	ad2antrr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 ≠ ∅ ) ∧ 𝑜 ∈ ℕ₀ ) ∧ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑜 ) ) → 0 < ( ♯ ‘ 𝑐 ) )
148		ccatfv0	⊢ ( ( 𝑐 ∈ Word ( SubDRing ‘ 𝑊 ) ∧ ⟨“ 𝑔 ”⟩ ∈ Word ( SubDRing ‘ 𝑊 ) ∧ 0 < ( ♯ ‘ 𝑐 ) ) → ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) = ( 𝑐 ‘ 0 ) )
149	108 146 147 148	syl3anc	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 ≠ ∅ ) ∧ 𝑜 ∈ ℕ₀ ) ∧ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑜 ) ) → ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) = ( 𝑐 ‘ 0 ) )
150	149	oveq2d	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < 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 ) ) )
151	150 138	r19.29a	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 ≠ ∅ ) → ( 𝑊 ↾_s ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) ) = ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) )
152	142 145 151	3brtr4d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 ≠ ∅ ) → ( 𝑊 ↾_s ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) /_FldExt ( 𝑊 ↾_s ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) ) )
153		oveq2	⊢ ( 𝑚 = ( 𝑜 + 1 ) → ( 2 ↑ 𝑚 ) = ( 2 ↑ ( 𝑜 + 1 ) ) )
154	153	eqeq2d	⊢ ( 𝑚 = ( 𝑜 + 1 ) → ( ( ( 𝑊 ↾_s ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) [:] ( 𝑊 ↾_s ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) ) ) = ( 2 ↑ 𝑚 ) ↔ ( ( 𝑊 ↾_s ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) [:] ( 𝑊 ↾_s ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) ) ) = ( 2 ↑ ( 𝑜 + 1 ) ) ) )
155		simplr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 ≠ ∅ ) ∧ 𝑜 ∈ ℕ₀ ) ∧ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑜 ) ) → 𝑜 ∈ ℕ₀ )
156		1nn0	⊢ 1 ∈ ℕ₀
157	156	a1i	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 ≠ ∅ ) ∧ 𝑜 ∈ ℕ₀ ) ∧ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑜 ) ) → 1 ∈ ℕ₀ )
158	155 157	nn0addcld	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 ≠ ∅ ) ∧ 𝑜 ∈ ℕ₀ ) ∧ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑜 ) ) → ( 𝑜 + 1 ) ∈ ℕ₀ )
159	144 150	oveq12d	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < 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 ) ) ) )
160	140	ad2antrr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < 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 ) ) )
161		extdgmul	⊢ ( ( ( 𝑊 ↾_s 𝑔 ) /_FldExt ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) ∧ ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) → ( ( 𝑊 ↾_s 𝑔 ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( ( ( 𝑊 ↾_s 𝑔 ) [:] ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) ) ·_e ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) ) )
162	129 160 161	syl2anc	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < 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 ) ) ) ) )
163	91	a1i	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 ≠ ∅ ) ∧ 𝑜 ∈ ℕ₀ ) ∧ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑜 ) ) → 2 ∈ ℂ )
164	163 155	expcld	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 ≠ ∅ ) ∧ 𝑜 ∈ ℕ₀ ) ∧ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑜 ) ) → ( 2 ↑ 𝑜 ) ∈ ℂ )
165	163 164	mulcomd	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < 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 ) )
166	128	simprd	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < 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 )
167		simpr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < 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 ↑ 𝑜 ) )
168	166 167	oveq12d	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < 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 ↑ 𝑜 ) ) )
169		2re	⊢ 2 ∈ ℝ
170	169	a1i	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 ≠ ∅ ) ∧ 𝑜 ∈ ℕ₀ ) ∧ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑜 ) ) → 2 ∈ ℝ )
171	170 155	reexpcld	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 ≠ ∅ ) ∧ 𝑜 ∈ ℕ₀ ) ∧ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑜 ) ) → ( 2 ↑ 𝑜 ) ∈ ℝ )
172		rexmul	⊢ ( ( 2 ∈ ℝ ∧ ( 2 ↑ 𝑜 ) ∈ ℝ ) → ( 2 ·_e ( 2 ↑ 𝑜 ) ) = ( 2 · ( 2 ↑ 𝑜 ) ) )
173	170 171 172	syl2anc	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < 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 ↑ 𝑜 ) ) )
174	168 173	eqtrd	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < 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 ↑ 𝑜 ) ) )
175	163 155	expp1d	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < 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 ) )
176	165 174 175	3eqtr4d	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < 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 ) ) )
177	159 162 176	3eqtrd	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < 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 ) ) )
178	154 158 177	rspcedvdw	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < 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 ↑ 𝑚 ) )
179	178 138	r19.29a	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < Chain ( SubDRing ‘ 𝑊 ) ) ) ∧ 𝑔 ∈ ( SubDRing ‘ 𝑊 ) ) ∧ ( 𝑐 = ∅ ∨ ( lastS ‘ 𝑐 ) < 𝑔 ) ) ∧ ( 0 < ( ♯ ‘ 𝑐 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑐 ) ) [:] ( 𝑊 ↾_s ( 𝑐 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) ) ∧ 0 < ( ♯ ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) ∧ 𝑐 ≠ ∅ ) → ∃ 𝑚 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ) ) [:] ( 𝑊 ↾_s ( ( 𝑐 ++ ⟨“ 𝑔 ”⟩ ) ‘ 0 ) ) ) = ( 2 ↑ 𝑚 ) )
180	152 179	jca	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < 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	103 180	pm2.61dane	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < 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 ↑ 𝑚 ) ) )
182	181	ex	⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( < 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 ↑ 𝑚 ) ) ) )
183	20 32 48 60 4 67 182	chnind	⊢ ( 𝜑 → ( 0 < ( ♯ ‘ 𝑇 ) → ( ( 𝑊 ↾_s ( lastS ‘ 𝑇 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑇 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑇 ) ) [:] ( 𝑊 ↾_s ( 𝑇 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ) )
184	8 183	mpd	⊢ ( 𝜑 → ( ( 𝑊 ↾_s ( lastS ‘ 𝑇 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑇 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑇 ) ) [:] ( 𝑊 ↾_s ( 𝑇 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) )
185	7 6	breq12d	⊢ ( 𝜑 → ( ( 𝑊 ↾_s ( lastS ‘ 𝑇 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑇 ‘ 0 ) ) ↔ 𝐿 /_FldExt 𝑄 ) )
186	7 6	oveq12d	⊢ ( 𝜑 → ( ( 𝑊 ↾_s ( lastS ‘ 𝑇 ) ) [:] ( 𝑊 ↾_s ( 𝑇 ‘ 0 ) ) ) = ( 𝐿 [:] 𝑄 ) )
187	186	eqeq1d	⊢ ( 𝜑 → ( ( ( 𝑊 ↾_s ( lastS ‘ 𝑇 ) ) [:] ( 𝑊 ↾_s ( 𝑇 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ↔ ( 𝐿 [:] 𝑄 ) = ( 2 ↑ 𝑛 ) ) )
188	187	rexbidv	⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑇 ) ) [:] ( 𝑊 ↾_s ( 𝑇 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ₀ ( 𝐿 [:] 𝑄 ) = ( 2 ↑ 𝑛 ) ) )
189	185 188	anbi12d	⊢ ( 𝜑 → ( ( ( 𝑊 ↾_s ( lastS ‘ 𝑇 ) ) /_FldExt ( 𝑊 ↾_s ( 𝑇 ‘ 0 ) ) ∧ ∃ 𝑛 ∈ ℕ₀ ( ( 𝑊 ↾_s ( lastS ‘ 𝑇 ) ) [:] ( 𝑊 ↾_s ( 𝑇 ‘ 0 ) ) ) = ( 2 ↑ 𝑛 ) ) ↔ ( 𝐿 /_FldExt 𝑄 ∧ ∃ 𝑛 ∈ ℕ₀ ( 𝐿 [:] 𝑄 ) = ( 2 ↑ 𝑛 ) ) ) )
190	184 189	mpbid	⊢ ( 𝜑 → ( 𝐿 /_FldExt 𝑄 ∧ ∃ 𝑛 ∈ ℕ₀ ( 𝐿 [:] 𝑄 ) = ( 2 ↑ 𝑛 ) ) )

Metamath Proof Explorer

Theorem fldext2chn

Proof