Metamath Proof Explorer

Theorem fldext2chn

Description: In a non-empty tower T of quadratic field extensions, the degree of the extension of the first member by the last is a power of two. (Contributed by Thierry Arnoux, 19-Jun-2025)

Ref Expression
Hypotheses fldext2chn.l ⊢ < = { ⟨ 𝑓 , 𝑒 ⟩ ∣ ( 𝑒 /FldExt 𝑓 ∧ ( 𝑒 [:] 𝑓 ) = 2 ) }
fldext2chn.t ⊢ ( 𝜑 → 𝑇 ∈ ( < Chain Field ) )
fldext2chn.1 ⊢ ( 𝜑 → ( 𝑇 ‘ 0 ) = 𝑄 )
fldext2chn.2 ⊢ ( 𝜑 → ( lastS ‘ 𝑇 ) = 𝐹 )
fldext2chn.3 ⊢ ( 𝜑 → 0 < ( ♯ ‘ 𝑇 ) )
Assertion fldext2chn ( 𝜑 → ∃ 𝑛 ∈ ℕ0 ( 𝐹 [:] 𝑄 ) = ( 2 ↑ 𝑛 ) )

Proof

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