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