Metamath Proof Explorer

Theorem 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/FldExtF∧E.:.F=1→E=F

Proof

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