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	$⊢ E = W ↾_{𝑠} e$
	fldext2chn.f	$⊢ F = W ↾_{𝑠} f$
	fldext2chn.l	$⊢ \underset{˙}{<} = \{⟨f, e⟩ \| (E /_{FldExt} F \land E [. : .] F = 2)\}$
	fldext2chn.t	$⊢ φ \to T \in {Chain}_{SubDRing (W)} \underset{˙}{<}$
	fldext2chn.w	$⊢ φ \to W \in Field$
	fldext2chn.1	$⊢ φ \to W ↾_{𝑠} T (0) = Q$
	fldext2chn.2	$⊢ φ \to W ↾_{𝑠} lastS (T) = L$
	fldext2chn.3	$⊢ φ \to 0 < \|T\|$
Assertion	fldext2chn	$⊢ φ \to (L /_{FldExt} Q \land \exists n \in ℕ_{0} L [. : .] Q = 2^{n})$

Proof

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

Metamath Proof Explorer

Theorem fldext2chn

Proof