extdg1id

Description: If the degree of the extension E /FldExt F is 1 , then E and F are identical. (Contributed by Thierry Arnoux, 6-Aug-2023)

		Ref	Expression
	Assertion	extdg1id	$⊢ (E /_{FldExt} F \land E [. : .] F = 1) \to E = F$

Proof

Step	Hyp	Ref	Expression
1		fldextress	$⊢ E /_{FldExt} F \to F = E ↾_{𝑠} {Base}_{F}$
2	1	adantr	$⊢ (E /_{FldExt} F \land E [. : .] F = 1) \to F = E ↾_{𝑠} {Base}_{F}$
3		fldextsralvec	$⊢ E /_{FldExt} F \to subringAlg (E) ({Base}_{F}) \in LVec$
4	3	adantr	$⊢ (E /_{FldExt} F \land E [. : .] F = 1) \to subringAlg (E) ({Base}_{F}) \in LVec$
5		eqid	$⊢ LBasis (subringAlg (E) ({Base}_{F})) = LBasis (subringAlg (E) ({Base}_{F}))$
6	5	lbsex	$⊢ subringAlg (E) ({Base}_{F}) \in LVec \to LBasis (subringAlg (E) ({Base}_{F})) \neq \emptyset$
7	4 6	syl	$⊢ (E /_{FldExt} F \land E [. : .] F = 1) \to LBasis (subringAlg (E) ({Base}_{F})) \neq \emptyset$
8		n0	$⊢ LBasis (subringAlg (E) ({Base}_{F})) \neq \emptyset \leftrightarrow \exists b b \in LBasis (subringAlg (E) ({Base}_{F}))$
9	7 8	sylib	$⊢ (E /_{FldExt} F \land E [. : .] F = 1) \to \exists b b \in LBasis (subringAlg (E) ({Base}_{F}))$
10		simpr	$⊢ ((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \to b \in LBasis (subringAlg (E) ({Base}_{F}))$
11	5	dimval	$⊢ (subringAlg (E) ({Base}_{F}) \in LVec \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \to \dim (subringAlg (E) ({Base}_{F})) = \|b\|$
12	4 11	sylan	$⊢ ((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \to \dim (subringAlg (E) ({Base}_{F})) = \|b\|$
13		extdgval	$⊢ E /_{FldExt} F \to E [. : .] F = \dim (subringAlg (E) ({Base}_{F}))$
14	13	adantr	$⊢ (E /_{FldExt} F \land E [. : .] F = 1) \to E [. : .] F = \dim (subringAlg (E) ({Base}_{F}))$
15		simpr	$⊢ (E /_{FldExt} F \land E [. : .] F = 1) \to E [. : .] F = 1$
16	14 15	eqtr3d	$⊢ (E /_{FldExt} F \land E [. : .] F = 1) \to \dim (subringAlg (E) ({Base}_{F})) = 1$
17	16	adantr	$⊢ ((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \to \dim (subringAlg (E) ({Base}_{F})) = 1$
18	12 17	eqtr3d	$⊢ ((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \to \|b\| = 1$
19		hash1snb	$⊢ b \in LBasis (subringAlg (E) ({Base}_{F})) \to (\|b\| = 1 \leftrightarrow \exists x b = \{x\})$
20	19	biimpa	$⊢ (b \in LBasis (subringAlg (E) ({Base}_{F})) \land \|b\| = 1) \to \exists x b = \{x\}$
21	10 18 20	syl2anc	$⊢ ((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \to \exists x b = \{x\}$
22		simpr	$⊢ (((((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land u \in {Base}_{E}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land {finSupp}_{0_{Scalar (subringAlg (E) ({Base}_{F}))}} (v)) \land u = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to u = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)$
23		simplr	$⊢ ((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \to b = \{x\}$
24		eqidd	$⊢ E /_{FldExt} F \to subringAlg (E) ({Base}_{F}) = subringAlg (E) ({Base}_{F})$
25		eqid	$⊢ {Base}_{F} = {Base}_{F}$
26	25	fldextsubrg	$⊢ E /_{FldExt} F \to {Base}_{F} \in SubRing (E)$
27		eqid	$⊢ {Base}_{E} = {Base}_{E}$
28	27	subrgss	$⊢ {Base}_{F} \in SubRing (E) \to {Base}_{F} \subseteq {Base}_{E}$
29	26 28	syl	$⊢ E /_{FldExt} F \to {Base}_{F} \subseteq {Base}_{E}$
30	24 29	sravsca	$⊢ E /_{FldExt} F \to \cdot_{E} = \cdot_{subringAlg (E) ({Base}_{F})}$
31	30	eqcomd	$⊢ E /_{FldExt} F \to \cdot_{subringAlg (E) ({Base}_{F})} = \cdot_{E}$
32	31	ad5antr	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land i \in b) \to \cdot_{subringAlg (E) ({Base}_{F})} = \cdot_{E}$
33	32	oveqd	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land i \in b) \to v (i) \cdot_{subringAlg (E) ({Base}_{F})} i = v (i) \cdot_{E} i$
34	23 33	mpteq12dva	$⊢ ((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \to (i \in b ⟼ v (i) \cdot_{subringAlg (E) ({Base}_{F})} i) = (i \in \{x\} ⟼ v (i) \cdot_{E} i)$
35	34	oveq2d	$⊢ ((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \to \underset{i \in b}{\sum_{E}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i) = \underset{i \in \{x\}}{\sum_{E}} (v (i) \cdot_{E} i)$
36		eqid	$⊢ subringAlg (E) ({Base}_{F}) = subringAlg (E) ({Base}_{F})$
37		fldextfld1	$⊢ E /_{FldExt} F \to E \in Field$
38		isfld	$⊢ E \in Field \leftrightarrow (E \in DivRing \land E \in CRing)$
39	38	simplbi	$⊢ E \in Field \to E \in DivRing$
40	37 39	syl	$⊢ E /_{FldExt} F \to E \in DivRing$
41	40	adantr	$⊢ (E /_{FldExt} F \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \to E \in DivRing$
42	26	adantr	$⊢ (E /_{FldExt} F \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \to {Base}_{F} \in SubRing (E)$
43		eqid	$⊢ E ↾_{𝑠} {Base}_{F} = E ↾_{𝑠} {Base}_{F}$
44		fldextfld2	$⊢ E /_{FldExt} F \to F \in Field$
45		isfld	$⊢ F \in Field \leftrightarrow (F \in DivRing \land F \in CRing)$
46	45	simplbi	$⊢ F \in Field \to F \in DivRing$
47	44 46	syl	$⊢ E /_{FldExt} F \to F \in DivRing$
48	1 47	eqeltrrd	$⊢ E /_{FldExt} F \to E ↾_{𝑠} {Base}_{F} \in DivRing$
49	48	adantr	$⊢ (E /_{FldExt} F \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \to E ↾_{𝑠} {Base}_{F} \in DivRing$
50		simpr	$⊢ (E /_{FldExt} F \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \to b \in LBasis (subringAlg (E) ({Base}_{F}))$
51	36 41 42 43 49 50	drgextgsum	$⊢ (E /_{FldExt} F \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \to \underset{i \in b}{\sum_{E}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i) = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)$
52	51	adantlr	$⊢ ((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \to \underset{i \in b}{\sum_{E}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i) = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)$
53	52	ad2antrr	$⊢ ((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \to \underset{i \in b}{\sum_{E}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i) = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)$
54		drngring	$⊢ E \in DivRing \to E \in Ring$
55	37 39 54	3syl	$⊢ E /_{FldExt} F \to E \in Ring$
56		ringmnd	$⊢ E \in Ring \to E \in Mnd$
57	55 56	syl	$⊢ E /_{FldExt} F \to E \in Mnd$
58	57	ad4antr	$⊢ ((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \to E \in Mnd$
59		vex	$⊢ x \in V$
60	59	a1i	$⊢ ((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \to x \in V$
61	55	ad3antrrr	$⊢ (((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \to E \in Ring$
62	61	adantr	$⊢ ((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \to E \in Ring$
63	29	ad3antrrr	$⊢ (((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \to {Base}_{F} \subseteq {Base}_{E}$
64	63	adantr	$⊢ ((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \to {Base}_{F} \subseteq {Base}_{E}$
65		elmapi	$⊢ v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b}) \to v : b ⟶ {Base}_{Scalar (subringAlg (E) ({Base}_{F}))}$
66	65	adantl	$⊢ ((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \to v : b ⟶ {Base}_{Scalar (subringAlg (E) ({Base}_{F}))}$
67		vsnid	$⊢ x \in \{x\}$
68	67 23	eleqtrrid	$⊢ ((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \to x \in b$
69	66 68	ffvelrnd	$⊢ ((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \to v (x) \in {Base}_{Scalar (subringAlg (E) ({Base}_{F}))}$
70	24 29	srasca	$⊢ E /_{FldExt} F \to E ↾_{𝑠} {Base}_{F} = Scalar (subringAlg (E) ({Base}_{F}))$
71	1 70	eqtrd	$⊢ E /_{FldExt} F \to F = Scalar (subringAlg (E) ({Base}_{F}))$
72	71	fveq2d	$⊢ E /_{FldExt} F \to {Base}_{F} = {Base}_{Scalar (subringAlg (E) ({Base}_{F}))}$
73	72	ad4antr	$⊢ ((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \to {Base}_{F} = {Base}_{Scalar (subringAlg (E) ({Base}_{F}))}$
74	69 73	eleqtrrd	$⊢ ((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \to v (x) \in {Base}_{F}$
75	64 74	sseldd	$⊢ ((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \to v (x) \in {Base}_{E}$
76		simpr	$⊢ (((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \to b = \{x\}$
77		simplr	$⊢ (((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \to b \in LBasis (subringAlg (E) ({Base}_{F}))$
78		eqid	$⊢ {Base}_{subringAlg (E) ({Base}_{F})} = {Base}_{subringAlg (E) ({Base}_{F})}$
79	78 5	lbsss	$⊢ b \in LBasis (subringAlg (E) ({Base}_{F})) \to b \subseteq {Base}_{subringAlg (E) ({Base}_{F})}$
80	77 79	syl	$⊢ (((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \to b \subseteq {Base}_{subringAlg (E) ({Base}_{F})}$
81	76 80	eqsstrrd	$⊢ (((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \to \{x\} \subseteq {Base}_{subringAlg (E) ({Base}_{F})}$
82	59	snss	$⊢ x \in {Base}_{subringAlg (E) ({Base}_{F})} \leftrightarrow \{x\} \subseteq {Base}_{subringAlg (E) ({Base}_{F})}$
83	81 82	sylibr	$⊢ (((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \to x \in {Base}_{subringAlg (E) ({Base}_{F})}$
84		eqidd	$⊢ (((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \to subringAlg (E) ({Base}_{F}) = subringAlg (E) ({Base}_{F})$
85	84 63	srabase	$⊢ (((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \to {Base}_{E} = {Base}_{subringAlg (E) ({Base}_{F})}$
86	83 85	eleqtrrd	$⊢ (((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \to x \in {Base}_{E}$
87	86	adantr	$⊢ ((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \to x \in {Base}_{E}$
88		eqid	$⊢ \cdot_{E} = \cdot_{E}$
89	27 88	ringcl	$⊢ (E \in Ring \land v (x) \in {Base}_{E} \land x \in {Base}_{E}) \to v (x) \cdot_{E} x \in {Base}_{E}$
90	62 75 87 89	syl3anc	$⊢ ((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \to v (x) \cdot_{E} x \in {Base}_{E}$
91		simpr	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land i = x) \to i = x$
92	91	fveq2d	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land i = x) \to v (i) = v (x)$
93	92 91	oveq12d	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land i = x) \to v (i) \cdot_{E} i = v (x) \cdot_{E} x$
94	27 58 60 90 93	gsumsnd	$⊢ ((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \to \underset{i \in \{x\}}{\sum_{E}} (v (i) \cdot_{E} i) = v (x) \cdot_{E} x$
95	1	fveq2d	$⊢ E /_{FldExt} F \to \cdot_{F} = \cdot_{(E ↾_{𝑠} {Base}_{F})}$
96	43 88	ressmulr	$⊢ {Base}_{F} \in SubRing (E) \to \cdot_{E} = \cdot_{(E ↾_{𝑠} {Base}_{F})}$
97	26 96	syl	$⊢ E /_{FldExt} F \to \cdot_{E} = \cdot_{(E ↾_{𝑠} {Base}_{F})}$
98	95 97	eqtr4d	$⊢ E /_{FldExt} F \to \cdot_{F} = \cdot_{E}$
99	98	ad4antr	$⊢ ((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \to \cdot_{F} = \cdot_{E}$
100	99	oveqd	$⊢ ((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \to v (x) \cdot_{F} x = v (x) \cdot_{E} x$
101	94 100	eqtr4d	$⊢ ((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \to \underset{i \in \{x\}}{\sum_{E}} (v (i) \cdot_{E} i) = v (x) \cdot_{F} x$
102	35 53 101	3eqtr3d	$⊢ ((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \to \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i) = v (x) \cdot_{F} x$
103	102	adantlr	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land u \in {Base}_{E}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \to \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i) = v (x) \cdot_{F} x$
104		drngring	$⊢ F \in DivRing \to F \in Ring$
105	44 46 104	3syl	$⊢ E /_{FldExt} F \to F \in Ring$
106	105	ad5antr	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land u \in {Base}_{E}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \to F \in Ring$
107	74	adantlr	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land u \in {Base}_{E}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \to v (x) \in {Base}_{F}$
108		eqid	$⊢ 1_{E} = 1_{E}$
109		eqid	$⊢ Unit (E) = Unit (E)$
110		eqid	$⊢ {inv}_{r} (E) = {inv}_{r} (E)$
111		simp-5l	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to E /_{FldExt} F$
112	111 55	syl	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to E \in Ring$
113	87	adantr	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to x \in {Base}_{E}$
114	75	adantr	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to v (x) \in {Base}_{E}$
115	38	simprbi	$⊢ E \in Field \to E \in CRing$
116	111 37 115	3syl	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to E \in CRing$
117	27 88	crngcom	$⊢ (E \in CRing \land x \in {Base}_{E} \land v (x) \in {Base}_{E}) \to x \cdot_{E} v (x) = v (x) \cdot_{E} x$
118	116 113 114 117	syl3anc	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to x \cdot_{E} v (x) = v (x) \cdot_{E} x$
119		simpr	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)$
120	52	ad3antrrr	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to \underset{i \in b}{\sum_{E}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i) = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)$
121	34	adantr	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to (i \in b ⟼ v (i) \cdot_{subringAlg (E) ({Base}_{F})} i) = (i \in \{x\} ⟼ v (i) \cdot_{E} i)$
122	121	oveq2d	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to \underset{i \in b}{\sum_{E}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i) = \underset{i \in \{x\}}{\sum_{E}} (v (i) \cdot_{E} i)$
123	119 120 122	3eqtr2d	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to 1_{E} = \underset{i \in \{x\}}{\sum_{E}} (v (i) \cdot_{E} i)$
124	94	adantr	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to \underset{i \in \{x\}}{\sum_{E}} (v (i) \cdot_{E} i) = v (x) \cdot_{E} x$
125	123 124	eqtrd	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to 1_{E} = v (x) \cdot_{E} x$
126	118 125	eqtr4d	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to x \cdot_{E} v (x) = 1_{E}$
127	125	eqcomd	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to v (x) \cdot_{E} x = 1_{E}$
128	27 88 108 109 110 112 113 114 126 127	invrvald	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to (x \in Unit (E) \land {inv}_{r} (E) (x) = v (x))$
129	128	simpld	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to x \in Unit (E)$
130	109 110	unitinvinv	$⊢ (E \in Ring \land x \in Unit (E)) \to {inv}_{r} (E) ({inv}_{r} (E) (x)) = x$
131	62 129 130	syl2an2r	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to {inv}_{r} (E) ({inv}_{r} (E) (x)) = x$
132	111 37 39	3syl	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to E \in DivRing$
133	111 26	syl	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to {Base}_{F} \in SubRing (E)$
134	111 1	syl	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to F = E ↾_{𝑠} {Base}_{F}$
135	111 44 46	3syl	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to F \in DivRing$
136	134 135	eqeltrrd	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to E ↾_{𝑠} {Base}_{F} \in DivRing$
137	128	simprd	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to {inv}_{r} (E) (x) = v (x)$
138	74	adantr	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to v (x) \in {Base}_{F}$
139	137 138	eqeltrd	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to {inv}_{r} (E) (x) \in {Base}_{F}$
140		eqidd	$⊢ E /_{FldExt} F \to 0_{E} = 0_{E}$
141	24 140 29	sralmod0	$⊢ E /_{FldExt} F \to 0_{E} = 0_{subringAlg (E) ({Base}_{F})}$
142	141	ad2antrr	$⊢ ((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \to 0_{E} = 0_{subringAlg (E) ({Base}_{F})}$
143	5	lbslinds	$⊢ LBasis (subringAlg (E) ({Base}_{F})) \subseteq LIndS (subringAlg (E) ({Base}_{F}))$
144	143 10	sseldi	$⊢ ((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \to b \in LIndS (subringAlg (E) ({Base}_{F}))$
145		eqid	$⊢ 0_{subringAlg (E) ({Base}_{F})} = 0_{subringAlg (E) ({Base}_{F})}$
146	145	0nellinds	$⊢ (subringAlg (E) ({Base}_{F}) \in LVec \land b \in LIndS (subringAlg (E) ({Base}_{F}))) \to \neg 0_{subringAlg (E) ({Base}_{F})} \in b$
147	4 144 146	syl2an2r	$⊢ ((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \to \neg 0_{subringAlg (E) ({Base}_{F})} \in b$
148	142 147	eqneltrd	$⊢ ((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \to \neg 0_{E} \in b$
149	148	ad3antrrr	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to \neg 0_{E} \in b$
150		nelne2	$⊢ (x \in b \land \neg 0_{E} \in b) \to x \neq 0_{E}$
151	68 149 150	syl2an2r	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to x \neq 0_{E}$
152		eqid	$⊢ 0_{E} = 0_{E}$
153	27 152 110	drnginvrn0	$⊢ (E \in DivRing \land x \in {Base}_{E} \land x \neq 0_{E}) \to {inv}_{r} (E) (x) \neq 0_{E}$
154	132 113 151 153	syl3anc	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to {inv}_{r} (E) (x) \neq 0_{E}$
155		eldifsn	$⊢ {inv}_{r} (E) (x) \in ({Base}_{F} ∖ \{0_{E}\}) \leftrightarrow ({inv}_{r} (E) (x) \in {Base}_{F} \land {inv}_{r} (E) (x) \neq 0_{E})$
156	139 154 155	sylanbrc	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to {inv}_{r} (E) (x) \in ({Base}_{F} ∖ \{0_{E}\})$
157		fveq2	$⊢ a = {inv}_{r} (E) (x) \to {inv}_{r} (E) (a) = {inv}_{r} (E) ({inv}_{r} (E) (x))$
158	157	eleq1d	$⊢ a = {inv}_{r} (E) (x) \to ({inv}_{r} (E) (a) \in {Base}_{F} \leftrightarrow {inv}_{r} (E) ({inv}_{r} (E) (x)) \in {Base}_{F})$
159	43 152 110	issubdrg	$⊢ (E \in DivRing \land {Base}_{F} \in SubRing (E)) \to (E ↾_{𝑠} {Base}_{F} \in DivRing \leftrightarrow \forall a \in ({Base}_{F} ∖ \{0_{E}\}) {inv}_{r} (E) (a) \in {Base}_{F})$
160	159	biimpa	$⊢ ((E \in DivRing \land {Base}_{F} \in SubRing (E)) \land E ↾_{𝑠} {Base}_{F} \in DivRing) \to \forall a \in ({Base}_{F} ∖ \{0_{E}\}) {inv}_{r} (E) (a) \in {Base}_{F}$
161	160	adantr	$⊢ (((E \in DivRing \land {Base}_{F} \in SubRing (E)) \land E ↾_{𝑠} {Base}_{F} \in DivRing) \land {inv}_{r} (E) (x) \in ({Base}_{F} ∖ \{0_{E}\})) \to \forall a \in ({Base}_{F} ∖ \{0_{E}\}) {inv}_{r} (E) (a) \in {Base}_{F}$
162		simpr	$⊢ (((E \in DivRing \land {Base}_{F} \in SubRing (E)) \land E ↾_{𝑠} {Base}_{F} \in DivRing) \land {inv}_{r} (E) (x) \in ({Base}_{F} ∖ \{0_{E}\})) \to {inv}_{r} (E) (x) \in ({Base}_{F} ∖ \{0_{E}\})$
163	158 161 162	rspcdva	$⊢ (((E \in DivRing \land {Base}_{F} \in SubRing (E)) \land E ↾_{𝑠} {Base}_{F} \in DivRing) \land {inv}_{r} (E) (x) \in ({Base}_{F} ∖ \{0_{E}\})) \to {inv}_{r} (E) ({inv}_{r} (E) (x)) \in {Base}_{F}$
164	132 133 136 156 163	syl1111anc	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to {inv}_{r} (E) ({inv}_{r} (E) (x)) \in {Base}_{F}$
165	131 164	eqeltrrd	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to x \in {Base}_{F}$
166	165	adantrl	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land ({finSupp}_{0_{Scalar (subringAlg (E) ({Base}_{F}))}} (v) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i))) \to x \in {Base}_{F}$
167	27 108	ringidcl	$⊢ E \in Ring \to 1_{E} \in {Base}_{E}$
168	61 167	syl	$⊢ (((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \to 1_{E} \in {Base}_{E}$
169	168 85	eleqtrd	$⊢ (((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \to 1_{E} \in {Base}_{subringAlg (E) ({Base}_{F})}$
170		eqid	$⊢ {Base}_{Scalar (subringAlg (E) ({Base}_{F}))} = {Base}_{Scalar (subringAlg (E) ({Base}_{F}))}$
171		eqid	$⊢ Scalar (subringAlg (E) ({Base}_{F})) = Scalar (subringAlg (E) ({Base}_{F}))$
172		eqid	$⊢ 0_{Scalar (subringAlg (E) ({Base}_{F}))} = 0_{Scalar (subringAlg (E) ({Base}_{F}))}$
173		eqid	$⊢ \cdot_{subringAlg (E) ({Base}_{F})} = \cdot_{subringAlg (E) ({Base}_{F})}$
174	4	ad2antrr	$⊢ (((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \to subringAlg (E) ({Base}_{F}) \in LVec$
175		lveclmod	$⊢ subringAlg (E) ({Base}_{F}) \in LVec \to subringAlg (E) ({Base}_{F}) \in LMod$
176	174 175	syl	$⊢ (((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \to subringAlg (E) ({Base}_{F}) \in LMod$
177	78 170 171 172 173 176 77	lbslsp	$⊢ (((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \to (1_{E} \in {Base}_{subringAlg (E) ({Base}_{F})} \leftrightarrow \exists v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b}) ({finSupp}_{0_{Scalar (subringAlg (E) ({Base}_{F}))}} (v) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)))$
178	169 177	mpbid	$⊢ (((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \to \exists v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b}) ({finSupp}_{0_{Scalar (subringAlg (E) ({Base}_{F}))}} (v) \land 1_{E} = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i))$
179	166 178	r19.29a	$⊢ (((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \to x \in {Base}_{F}$
180	179	ad2antrr	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land u \in {Base}_{E}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \to x \in {Base}_{F}$
181		eqid	$⊢ \cdot_{F} = \cdot_{F}$
182	25 181	ringcl	$⊢ (F \in Ring \land v (x) \in {Base}_{F} \land x \in {Base}_{F}) \to v (x) \cdot_{F} x \in {Base}_{F}$
183	106 107 180 182	syl3anc	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land u \in {Base}_{E}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \to v (x) \cdot_{F} x \in {Base}_{F}$
184	103 183	eqeltrd	$⊢ (((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land u \in {Base}_{E}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \to \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i) \in {Base}_{F}$
185	184	ad2antrr	$⊢ (((((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land u \in {Base}_{E}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land {finSupp}_{0_{Scalar (subringAlg (E) ({Base}_{F}))}} (v)) \land u = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i) \in {Base}_{F}$
186	22 185	eqeltrd	$⊢ (((((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land u \in {Base}_{E}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land {finSupp}_{0_{Scalar (subringAlg (E) ({Base}_{F}))}} (v)) \land u = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)) \to u \in {Base}_{F}$
187	186	anasss	$⊢ ((((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land u \in {Base}_{E}) \land v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b})) \land ({finSupp}_{0_{Scalar (subringAlg (E) ({Base}_{F}))}} (v) \land u = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i))) \to u \in {Base}_{F}$
188	85	eleq2d	$⊢ (((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \to (u \in {Base}_{E} \leftrightarrow u \in {Base}_{subringAlg (E) ({Base}_{F})})$
189	78 170 171 172 173 176 77	lbslsp	$⊢ (((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \to (u \in {Base}_{subringAlg (E) ({Base}_{F})} \leftrightarrow \exists v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b}) ({finSupp}_{0_{Scalar (subringAlg (E) ({Base}_{F}))}} (v) \land u = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)))$
190	188 189	bitrd	$⊢ (((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \to (u \in {Base}_{E} \leftrightarrow \exists v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b}) ({finSupp}_{0_{Scalar (subringAlg (E) ({Base}_{F}))}} (v) \land u = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i)))$
191	190	biimpa	$⊢ ((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land u \in {Base}_{E}) \to \exists v \in ({Base}_{Scalar (subringAlg (E) ({Base}_{F}))}^{b}) ({finSupp}_{0_{Scalar (subringAlg (E) ({Base}_{F}))}} (v) \land u = \underset{i \in b}{\sum_{subringAlg (E) ({Base}_{F})}} (v (i) \cdot_{subringAlg (E) ({Base}_{F})} i))$
192	187 191	r19.29a	$⊢ ((((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \land u \in {Base}_{E}) \to u \in {Base}_{F}$
193	192	ex	$⊢ (((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \to (u \in {Base}_{E} \to u \in {Base}_{F})$
194	193	ssrdv	$⊢ (((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \land b = \{x\}) \to {Base}_{E} \subseteq {Base}_{F}$
195	21 194	exlimddv	$⊢ ((E /_{FldExt} F \land E [. : .] F = 1) \land b \in LBasis (subringAlg (E) ({Base}_{F}))) \to {Base}_{E} \subseteq {Base}_{F}$
196	9 195	exlimddv	$⊢ (E /_{FldExt} F \land E [. : .] F = 1) \to {Base}_{E} \subseteq {Base}_{F}$
197		simpr	$⊢ ((E /_{FldExt} F \land E [. : .] F = 1) \land {Base}_{E} \subseteq {Base}_{F}) \to {Base}_{E} \subseteq {Base}_{F}$
198	37	ad2antrr	$⊢ ((E /_{FldExt} F \land E [. : .] F = 1) \land {Base}_{E} \subseteq {Base}_{F}) \to E \in Field$
199		fvexd	$⊢ ((E /_{FldExt} F \land E [. : .] F = 1) \land {Base}_{E} \subseteq {Base}_{F}) \to {Base}_{F} \in V$
200	43 27	ressid2	$⊢ ({Base}_{E} \subseteq {Base}_{F} \land E \in Field \land {Base}_{F} \in V) \to E ↾_{𝑠} {Base}_{F} = E$
201	197 198 199 200	syl3anc	$⊢ ((E /_{FldExt} F \land E [. : .] F = 1) \land {Base}_{E} \subseteq {Base}_{F}) \to E ↾_{𝑠} {Base}_{F} = E$
202	196 201	mpdan	$⊢ (E /_{FldExt} F \land E [. : .] F = 1) \to E ↾_{𝑠} {Base}_{F} = E$
203	2 202	eqtr2d	$⊢ (E /_{FldExt} F \land E [. : .] F = 1) \to E = F$

Metamath Proof Explorer

Theorem extdg1id

Proof