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 /FldExt F E .:. F = 1 E = F

Proof

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