| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fldextress 33704 | . . 3
⊢ (𝐸/FldExt𝐹 → 𝐹 = (𝐸 ↾s (Base‘𝐹))) | 
| 2 | 1 | adantr 480 | . 2
⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → 𝐹 = (𝐸 ↾s (Base‘𝐹))) | 
| 3 |  | fldextsralvec 33707 | . . . . . . 7
⊢ (𝐸/FldExt𝐹 → ((subringAlg
‘𝐸)‘(Base‘𝐹)) ∈ LVec) | 
| 4 | 3 | adantr 480 | . . . . . 6
⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → ((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LVec) | 
| 5 |  | eqid 2736 | . . . . . . 7
⊢
(LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹))) | 
| 6 | 5 | lbsex 21168 | . . . . . 6
⊢
(((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LVec →
(LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))) ≠ ∅) | 
| 7 | 4, 6 | syl 17 | . . . . 5
⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹))) ≠ ∅) | 
| 8 |  | n0 4352 | . . . . 5
⊢
((LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))) ≠ ∅ ↔ ∃𝑏 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) | 
| 9 | 7, 8 | sylib 218 | . . . 4
⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → ∃𝑏 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) | 
| 10 |  | simpr 484 | . . . . . 6
⊢ (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) | 
| 11 | 5 | dimval 33652 | . . . . . . . 8
⊢
((((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LVec ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → (dim‘((subringAlg
‘𝐸)‘(Base‘𝐹))) = (♯‘𝑏)) | 
| 12 | 4, 11 | sylan 580 | . . . . . . 7
⊢ (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → (dim‘((subringAlg
‘𝐸)‘(Base‘𝐹))) = (♯‘𝑏)) | 
| 13 |  | extdgval 33706 | . . . . . . . . . 10
⊢ (𝐸/FldExt𝐹 → (𝐸[:]𝐹) = (dim‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) | 
| 14 | 13 | adantr 480 | . . . . . . . . 9
⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → (𝐸[:]𝐹) = (dim‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) | 
| 15 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → (𝐸[:]𝐹) = 1) | 
| 16 | 14, 15 | eqtr3d 2778 | . . . . . . . 8
⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → (dim‘((subringAlg
‘𝐸)‘(Base‘𝐹))) = 1) | 
| 17 | 16 | adantr 480 | . . . . . . 7
⊢ (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → (dim‘((subringAlg
‘𝐸)‘(Base‘𝐹))) = 1) | 
| 18 | 12, 17 | eqtr3d 2778 | . . . . . 6
⊢ (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → (♯‘𝑏) = 1) | 
| 19 |  | hash1snb 14459 | . . . . . . 7
⊢ (𝑏 ∈
(LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))) → ((♯‘𝑏) = 1 ↔ ∃𝑥 𝑏 = {𝑥})) | 
| 20 | 19 | biimpa 476 | . . . . . 6
⊢ ((𝑏 ∈
(LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))) ∧ (♯‘𝑏) = 1) → ∃𝑥 𝑏 = {𝑥}) | 
| 21 | 10, 18, 20 | syl2anc 584 | . . . . 5
⊢ (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → ∃𝑥 𝑏 = {𝑥}) | 
| 22 |  | simpr 484 | . . . . . . . . . 10
⊢
((((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ 𝑣 finSupp
(0g‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹))))) ∧ 𝑢 = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝑢 = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) | 
| 23 |  | simplr 768 | . . . . . . . . . . . . . . . 16
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝑏 = {𝑥}) | 
| 24 |  | eqidd 2737 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐸/FldExt𝐹 → ((subringAlg
‘𝐸)‘(Base‘𝐹)) = ((subringAlg ‘𝐸)‘(Base‘𝐹))) | 
| 25 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(Base‘𝐹) =
(Base‘𝐹) | 
| 26 | 25 | fldextsubrg 33703 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐸/FldExt𝐹 → (Base‘𝐹) ∈ (SubRing‘𝐸)) | 
| 27 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(Base‘𝐸) =
(Base‘𝐸) | 
| 28 | 27 | subrgss 20573 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((Base‘𝐹)
∈ (SubRing‘𝐸)
→ (Base‘𝐹)
⊆ (Base‘𝐸)) | 
| 29 | 26, 28 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐸/FldExt𝐹 → (Base‘𝐹) ⊆ (Base‘𝐸)) | 
| 30 | 24, 29 | sravsca 21186 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐸/FldExt𝐹 →
(.r‘𝐸) = (
·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) | 
| 31 | 30 | eqcomd 2742 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐸/FldExt𝐹 → (
·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = (.r‘𝐸)) | 
| 32 | 31 | ad5antr 734 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ 𝑖 ∈ 𝑏) → (
·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = (.r‘𝐸)) | 
| 33 | 32 | oveqd 7449 | . . . . . . . . . . . . . . . 16
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ 𝑖 ∈ 𝑏) → ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖) = ((𝑣‘𝑖)(.r‘𝐸)𝑖)) | 
| 34 | 23, 33 | mpteq12dva 5230 | . . . . . . . . . . . . . . 15
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)) = (𝑖 ∈ {𝑥} ↦ ((𝑣‘𝑖)(.r‘𝐸)𝑖))) | 
| 35 | 34 | oveq2d 7448 | . . . . . . . . . . . . . 14
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝐸 Σg (𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) = (𝐸 Σg (𝑖 ∈ {𝑥} ↦ ((𝑣‘𝑖)(.r‘𝐸)𝑖)))) | 
| 36 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢
((subringAlg ‘𝐸)‘(Base‘𝐹)) = ((subringAlg ‘𝐸)‘(Base‘𝐹)) | 
| 37 |  | fldextfld1 33701 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐸/FldExt𝐹 → 𝐸 ∈ Field) | 
| 38 |  | isfld 20741 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐸 ∈ Field ↔ (𝐸 ∈ DivRing ∧ 𝐸 ∈ CRing)) | 
| 39 | 38 | simplbi 497 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐸 ∈ Field → 𝐸 ∈
DivRing) | 
| 40 | 37, 39 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐸/FldExt𝐹 → 𝐸 ∈ DivRing) | 
| 41 | 40 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐸/FldExt𝐹 ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → 𝐸 ∈ DivRing) | 
| 42 | 26 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐸/FldExt𝐹 ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → (Base‘𝐹) ∈ (SubRing‘𝐸)) | 
| 43 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢ (𝐸 ↾s
(Base‘𝐹)) = (𝐸 ↾s
(Base‘𝐹)) | 
| 44 |  | fldextfld2 33702 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐸/FldExt𝐹 → 𝐹 ∈ Field) | 
| 45 |  | isfld 20741 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐹 ∈ Field ↔ (𝐹 ∈ DivRing ∧ 𝐹 ∈ CRing)) | 
| 46 | 45 | simplbi 497 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹 ∈ Field → 𝐹 ∈
DivRing) | 
| 47 | 44, 46 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐸/FldExt𝐹 → 𝐹 ∈ DivRing) | 
| 48 | 1, 47 | eqeltrrd 2841 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐸/FldExt𝐹 → (𝐸 ↾s (Base‘𝐹)) ∈
DivRing) | 
| 49 | 48 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐸/FldExt𝐹 ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → (𝐸 ↾s (Base‘𝐹)) ∈
DivRing) | 
| 50 |  | simpr 484 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐸/FldExt𝐹 ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) | 
| 51 | 36, 41, 42, 43, 49, 50 | drgextgsum 33646 | . . . . . . . . . . . . . . . 16
⊢ ((𝐸/FldExt𝐹 ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → (𝐸 Σg (𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) | 
| 52 | 51 | adantlr 715 | . . . . . . . . . . . . . . 15
⊢ (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → (𝐸 Σg (𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) | 
| 53 | 52 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝐸 Σg (𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) | 
| 54 |  | drngring 20737 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐸 ∈ DivRing → 𝐸 ∈ Ring) | 
| 55 | 37, 39, 54 | 3syl 18 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐸/FldExt𝐹 → 𝐸 ∈ Ring) | 
| 56 |  | ringmnd 20241 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐸 ∈ Ring → 𝐸 ∈ Mnd) | 
| 57 | 55, 56 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝐸/FldExt𝐹 → 𝐸 ∈ Mnd) | 
| 58 | 57 | ad4antr 732 | . . . . . . . . . . . . . . . 16
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝐸 ∈ Mnd) | 
| 59 |  | vex 3483 | . . . . . . . . . . . . . . . . 17
⊢ 𝑥 ∈ V | 
| 60 | 59 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝑥 ∈ V) | 
| 61 | 55 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → 𝐸 ∈ Ring) | 
| 62 | 61 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝐸 ∈ Ring) | 
| 63 | 29 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (Base‘𝐹) ⊆ (Base‘𝐸)) | 
| 64 | 63 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (Base‘𝐹) ⊆ (Base‘𝐸)) | 
| 65 |  | elmapi 8890 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏) → 𝑣:𝑏⟶(Base‘(Scalar‘((subringAlg
‘𝐸)‘(Base‘𝐹))))) | 
| 66 | 65 | adantl 481 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝑣:𝑏⟶(Base‘(Scalar‘((subringAlg
‘𝐸)‘(Base‘𝐹))))) | 
| 67 |  | vsnid 4662 | . . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑥 ∈ {𝑥} | 
| 68 | 67, 23 | eleqtrrid 2847 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝑥 ∈ 𝑏) | 
| 69 | 66, 68 | ffvelcdmd 7104 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝑣‘𝑥) ∈
(Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹))))) | 
| 70 | 24, 29 | srasca 21184 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐸/FldExt𝐹 → (𝐸 ↾s (Base‘𝐹)) = (Scalar‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) | 
| 71 | 1, 70 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐸/FldExt𝐹 → 𝐹 = (Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) | 
| 72 | 71 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐸/FldExt𝐹 → (Base‘𝐹) =
(Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹))))) | 
| 73 | 72 | ad4antr 732 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (Base‘𝐹) = (Base‘(Scalar‘((subringAlg
‘𝐸)‘(Base‘𝐹))))) | 
| 74 | 69, 73 | eleqtrrd 2843 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝑣‘𝑥) ∈ (Base‘𝐹)) | 
| 75 | 64, 74 | sseldd 3983 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝑣‘𝑥) ∈ (Base‘𝐸)) | 
| 76 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → 𝑏 = {𝑥}) | 
| 77 |  | simplr 768 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) | 
| 78 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(Base‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹))) | 
| 79 | 78, 5 | lbsss 21077 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 ∈
(LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))) → 𝑏 ⊆ (Base‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) | 
| 80 | 77, 79 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → 𝑏 ⊆ (Base‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) | 
| 81 | 76, 80 | eqsstrrd 4018 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → {𝑥} ⊆ (Base‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) | 
| 82 | 59 | snss 4784 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (Base‘((subringAlg
‘𝐸)‘(Base‘𝐹))) ↔ {𝑥} ⊆ (Base‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) | 
| 83 | 81, 82 | sylibr 234 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → 𝑥 ∈ (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) | 
| 84 |  | eqidd 2737 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → ((subringAlg ‘𝐸)‘(Base‘𝐹)) = ((subringAlg ‘𝐸)‘(Base‘𝐹))) | 
| 85 | 84, 63 | srabase 21178 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (Base‘𝐸) = (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) | 
| 86 | 83, 85 | eleqtrrd 2843 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → 𝑥 ∈ (Base‘𝐸)) | 
| 87 | 86 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝑥 ∈ (Base‘𝐸)) | 
| 88 |  | eqid 2736 | . . . . . . . . . . . . . . . . . 18
⊢
(.r‘𝐸) = (.r‘𝐸) | 
| 89 | 27, 88 | ringcl 20248 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐸 ∈ Ring ∧ (𝑣‘𝑥) ∈ (Base‘𝐸) ∧ 𝑥 ∈ (Base‘𝐸)) → ((𝑣‘𝑥)(.r‘𝐸)𝑥) ∈ (Base‘𝐸)) | 
| 90 | 62, 75, 87, 89 | syl3anc 1372 | . . . . . . . . . . . . . . . 16
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → ((𝑣‘𝑥)(.r‘𝐸)𝑥) ∈ (Base‘𝐸)) | 
| 91 |  | simpr 484 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ 𝑖 = 𝑥) → 𝑖 = 𝑥) | 
| 92 | 91 | fveq2d 6909 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ 𝑖 = 𝑥) → (𝑣‘𝑖) = (𝑣‘𝑥)) | 
| 93 | 92, 91 | oveq12d 7450 | . . . . . . . . . . . . . . . 16
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ 𝑖 = 𝑥) → ((𝑣‘𝑖)(.r‘𝐸)𝑖) = ((𝑣‘𝑥)(.r‘𝐸)𝑥)) | 
| 94 | 27, 58, 60, 90, 93 | gsumsnd 19971 | . . . . . . . . . . . . . . 15
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝐸 Σg (𝑖 ∈ {𝑥} ↦ ((𝑣‘𝑖)(.r‘𝐸)𝑖))) = ((𝑣‘𝑥)(.r‘𝐸)𝑥)) | 
| 95 | 1 | fveq2d 6909 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐸/FldExt𝐹 →
(.r‘𝐹) =
(.r‘(𝐸
↾s (Base‘𝐹)))) | 
| 96 | 43, 88 | ressmulr 17352 | . . . . . . . . . . . . . . . . . . 19
⊢
((Base‘𝐹)
∈ (SubRing‘𝐸)
→ (.r‘𝐸) = (.r‘(𝐸 ↾s (Base‘𝐹)))) | 
| 97 | 26, 96 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐸/FldExt𝐹 →
(.r‘𝐸) =
(.r‘(𝐸
↾s (Base‘𝐹)))) | 
| 98 | 95, 97 | eqtr4d 2779 | . . . . . . . . . . . . . . . . 17
⊢ (𝐸/FldExt𝐹 →
(.r‘𝐹) =
(.r‘𝐸)) | 
| 99 | 98 | ad4antr 732 | . . . . . . . . . . . . . . . 16
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (.r‘𝐹) = (.r‘𝐸)) | 
| 100 | 99 | oveqd 7449 | . . . . . . . . . . . . . . 15
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → ((𝑣‘𝑥)(.r‘𝐹)𝑥) = ((𝑣‘𝑥)(.r‘𝐸)𝑥)) | 
| 101 | 94, 100 | eqtr4d 2779 | . . . . . . . . . . . . . 14
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝐸 Σg (𝑖 ∈ {𝑥} ↦ ((𝑣‘𝑖)(.r‘𝐸)𝑖))) = ((𝑣‘𝑥)(.r‘𝐹)𝑥)) | 
| 102 | 35, 53, 101 | 3eqtr3d 2784 | . . . . . . . . . . . . 13
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) = ((𝑣‘𝑥)(.r‘𝐹)𝑥)) | 
| 103 | 102 | adantlr 715 | . . . . . . . . . . . 12
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) = ((𝑣‘𝑥)(.r‘𝐹)𝑥)) | 
| 104 |  | drngring 20737 | . . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ DivRing → 𝐹 ∈ Ring) | 
| 105 | 44, 46, 104 | 3syl 18 | . . . . . . . . . . . . . 14
⊢ (𝐸/FldExt𝐹 → 𝐹 ∈ Ring) | 
| 106 | 105 | ad5antr 734 | . . . . . . . . . . . . 13
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝐹 ∈ Ring) | 
| 107 | 74 | adantlr 715 | . . . . . . . . . . . . 13
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝑣‘𝑥) ∈ (Base‘𝐹)) | 
| 108 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . 20
⊢
(1r‘𝐸) = (1r‘𝐸) | 
| 109 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . 20
⊢
(Unit‘𝐸) =
(Unit‘𝐸) | 
| 110 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . 20
⊢
(invr‘𝐸) = (invr‘𝐸) | 
| 111 |  | simp-5l 784 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝐸/FldExt𝐹) | 
| 112 | 111, 55 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝐸 ∈ Ring) | 
| 113 | 87 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝑥 ∈ (Base‘𝐸)) | 
| 114 | 75 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (𝑣‘𝑥) ∈ (Base‘𝐸)) | 
| 115 | 38 | simprbi 496 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐸 ∈ Field → 𝐸 ∈ CRing) | 
| 116 | 111, 37, 115 | 3syl 18 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝐸 ∈ CRing) | 
| 117 | 27, 88 | crngcom 20249 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐸 ∈ CRing ∧ 𝑥 ∈ (Base‘𝐸) ∧ (𝑣‘𝑥) ∈ (Base‘𝐸)) → (𝑥(.r‘𝐸)(𝑣‘𝑥)) = ((𝑣‘𝑥)(.r‘𝐸)𝑥)) | 
| 118 | 116, 113,
114, 117 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (𝑥(.r‘𝐸)(𝑣‘𝑥)) = ((𝑣‘𝑥)(.r‘𝐸)𝑥)) | 
| 119 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) | 
| 120 | 52 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (𝐸 Σg (𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) | 
| 121 | 34 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)) = (𝑖 ∈ {𝑥} ↦ ((𝑣‘𝑖)(.r‘𝐸)𝑖))) | 
| 122 | 121 | oveq2d 7448 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (𝐸 Σg (𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) = (𝐸 Σg (𝑖 ∈ {𝑥} ↦ ((𝑣‘𝑖)(.r‘𝐸)𝑖)))) | 
| 123 | 119, 120,
122 | 3eqtr2d 2782 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (1r‘𝐸) = (𝐸 Σg (𝑖 ∈ {𝑥} ↦ ((𝑣‘𝑖)(.r‘𝐸)𝑖)))) | 
| 124 | 94 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (𝐸 Σg (𝑖 ∈ {𝑥} ↦ ((𝑣‘𝑖)(.r‘𝐸)𝑖))) = ((𝑣‘𝑥)(.r‘𝐸)𝑥)) | 
| 125 | 123, 124 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (1r‘𝐸) = ((𝑣‘𝑥)(.r‘𝐸)𝑥)) | 
| 126 | 118, 125 | eqtr4d 2779 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (𝑥(.r‘𝐸)(𝑣‘𝑥)) = (1r‘𝐸)) | 
| 127 | 125 | eqcomd 2742 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → ((𝑣‘𝑥)(.r‘𝐸)𝑥) = (1r‘𝐸)) | 
| 128 | 27, 88, 108, 109, 110, 112, 113, 114, 126, 127 | invrvald 22683 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (𝑥 ∈ (Unit‘𝐸) ∧ ((invr‘𝐸)‘𝑥) = (𝑣‘𝑥))) | 
| 129 | 128 | simpld 494 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝑥 ∈ (Unit‘𝐸)) | 
| 130 | 109, 110 | unitinvinv 20392 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐸 ∈ Ring ∧ 𝑥 ∈ (Unit‘𝐸)) →
((invr‘𝐸)‘((invr‘𝐸)‘𝑥)) = 𝑥) | 
| 131 | 62, 129, 130 | syl2an2r 685 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → ((invr‘𝐸)‘((invr‘𝐸)‘𝑥)) = 𝑥) | 
| 132 | 111, 37, 39 | 3syl 18 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝐸 ∈ DivRing) | 
| 133 | 111, 26 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (Base‘𝐹) ∈ (SubRing‘𝐸)) | 
| 134 | 111, 1 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝐹 = (𝐸 ↾s (Base‘𝐹))) | 
| 135 | 111, 44, 46 | 3syl 18 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝐹 ∈ DivRing) | 
| 136 | 134, 135 | eqeltrrd 2841 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (𝐸 ↾s (Base‘𝐹)) ∈
DivRing) | 
| 137 | 128 | simprd 495 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → ((invr‘𝐸)‘𝑥) = (𝑣‘𝑥)) | 
| 138 | 74 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (𝑣‘𝑥) ∈ (Base‘𝐹)) | 
| 139 | 137, 138 | eqeltrd 2840 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → ((invr‘𝐸)‘𝑥) ∈ (Base‘𝐹)) | 
| 140 |  | eqidd 2737 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐸/FldExt𝐹 →
(0g‘𝐸) =
(0g‘𝐸)) | 
| 141 | 24, 140, 29 | sralmod0 21196 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐸/FldExt𝐹 →
(0g‘𝐸) =
(0g‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) | 
| 142 | 141 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → (0g‘𝐸) =
(0g‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) | 
| 143 | 5 | lbslinds 21854 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))) ⊆ (LIndS‘((subringAlg
‘𝐸)‘(Base‘𝐹))) | 
| 144 | 143, 10 | sselid 3980 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → 𝑏 ∈ (LIndS‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) | 
| 145 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(0g‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = (0g‘((subringAlg
‘𝐸)‘(Base‘𝐹))) | 
| 146 | 145 | 0nellinds 33399 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LVec ∧ 𝑏 ∈ (LIndS‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → ¬
(0g‘((subringAlg ‘𝐸)‘(Base‘𝐹))) ∈ 𝑏) | 
| 147 | 4, 144, 146 | syl2an2r 685 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → ¬
(0g‘((subringAlg ‘𝐸)‘(Base‘𝐹))) ∈ 𝑏) | 
| 148 | 142, 147 | eqneltrd 2860 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → ¬ (0g‘𝐸) ∈ 𝑏) | 
| 149 | 148 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → ¬ (0g‘𝐸) ∈ 𝑏) | 
| 150 |  | nelne2 3039 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ 𝑏 ∧ ¬ (0g‘𝐸) ∈ 𝑏) → 𝑥 ≠ (0g‘𝐸)) | 
| 151 | 68, 149, 150 | syl2an2r 685 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝑥 ≠ (0g‘𝐸)) | 
| 152 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(0g‘𝐸) = (0g‘𝐸) | 
| 153 | 27, 152, 110 | drnginvrn0 20755 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐸 ∈ DivRing ∧ 𝑥 ∈ (Base‘𝐸) ∧ 𝑥 ≠ (0g‘𝐸)) → ((invr‘𝐸)‘𝑥) ≠ (0g‘𝐸)) | 
| 154 | 132, 113,
151, 153 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → ((invr‘𝐸)‘𝑥) ≠ (0g‘𝐸)) | 
| 155 |  | eldifsn 4785 | . . . . . . . . . . . . . . . . . . 19
⊢
(((invr‘𝐸)‘𝑥) ∈ ((Base‘𝐹) ∖ {(0g‘𝐸)}) ↔
(((invr‘𝐸)‘𝑥) ∈ (Base‘𝐹) ∧ ((invr‘𝐸)‘𝑥) ≠ (0g‘𝐸))) | 
| 156 | 139, 154,
155 | sylanbrc 583 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → ((invr‘𝐸)‘𝑥) ∈ ((Base‘𝐹) ∖ {(0g‘𝐸)})) | 
| 157 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = ((invr‘𝐸)‘𝑥) → ((invr‘𝐸)‘𝑎) = ((invr‘𝐸)‘((invr‘𝐸)‘𝑥))) | 
| 158 | 157 | eleq1d 2825 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = ((invr‘𝐸)‘𝑥) → (((invr‘𝐸)‘𝑎) ∈ (Base‘𝐹) ↔ ((invr‘𝐸)‘((invr‘𝐸)‘𝑥)) ∈ (Base‘𝐹))) | 
| 159 | 43, 152, 110 | issubdrg 20782 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐸 ∈ DivRing ∧
(Base‘𝐹) ∈
(SubRing‘𝐸)) →
((𝐸 ↾s
(Base‘𝐹)) ∈
DivRing ↔ ∀𝑎
∈ ((Base‘𝐹)
∖ {(0g‘𝐸)})((invr‘𝐸)‘𝑎) ∈ (Base‘𝐹))) | 
| 160 | 159 | biimpa 476 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐸 ∈ DivRing ∧
(Base‘𝐹) ∈
(SubRing‘𝐸)) ∧
(𝐸 ↾s
(Base‘𝐹)) ∈
DivRing) → ∀𝑎
∈ ((Base‘𝐹)
∖ {(0g‘𝐸)})((invr‘𝐸)‘𝑎) ∈ (Base‘𝐹)) | 
| 161 | 160 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐸 ∈ DivRing ∧
(Base‘𝐹) ∈
(SubRing‘𝐸)) ∧
(𝐸 ↾s
(Base‘𝐹)) ∈
DivRing) ∧ ((invr‘𝐸)‘𝑥) ∈ ((Base‘𝐹) ∖ {(0g‘𝐸)})) → ∀𝑎 ∈ ((Base‘𝐹) ∖
{(0g‘𝐸)})((invr‘𝐸)‘𝑎) ∈ (Base‘𝐹)) | 
| 162 |  | simpr 484 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐸 ∈ DivRing ∧
(Base‘𝐹) ∈
(SubRing‘𝐸)) ∧
(𝐸 ↾s
(Base‘𝐹)) ∈
DivRing) ∧ ((invr‘𝐸)‘𝑥) ∈ ((Base‘𝐹) ∖ {(0g‘𝐸)})) →
((invr‘𝐸)‘𝑥) ∈ ((Base‘𝐹) ∖ {(0g‘𝐸)})) | 
| 163 | 158, 161,
162 | rspcdva 3622 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝐸 ∈ DivRing ∧
(Base‘𝐹) ∈
(SubRing‘𝐸)) ∧
(𝐸 ↾s
(Base‘𝐹)) ∈
DivRing) ∧ ((invr‘𝐸)‘𝑥) ∈ ((Base‘𝐹) ∖ {(0g‘𝐸)})) →
((invr‘𝐸)‘((invr‘𝐸)‘𝑥)) ∈ (Base‘𝐹)) | 
| 164 | 132, 133,
136, 156, 163 | syl1111anc 840 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → ((invr‘𝐸)‘((invr‘𝐸)‘𝑥)) ∈ (Base‘𝐹)) | 
| 165 | 131, 164 | eqeltrrd 2841 | . . . . . . . . . . . . . . . 16
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝑥 ∈ (Base‘𝐹)) | 
| 166 | 165 | adantrl 716 | . . . . . . . . . . . . . . 15
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (𝑣 finSupp
(0g‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))))) → 𝑥 ∈ (Base‘𝐹)) | 
| 167 | 27, 108 | ringidcl 20263 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐸 ∈ Ring →
(1r‘𝐸)
∈ (Base‘𝐸)) | 
| 168 | 61, 167 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (1r‘𝐸) ∈ (Base‘𝐸)) | 
| 169 | 168, 85 | eleqtrd 2842 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (1r‘𝐸) ∈
(Base‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) | 
| 170 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢
(Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) =
(Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) | 
| 171 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢
(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = (Scalar‘((subringAlg
‘𝐸)‘(Base‘𝐹))) | 
| 172 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢
(0g‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) =
(0g‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) | 
| 173 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢ (
·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = (
·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹))) | 
| 174 | 4 | ad2antrr 726 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → ((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LVec) | 
| 175 |  | lveclmod 21106 | . . . . . . . . . . . . . . . . . 18
⊢
(((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LVec → ((subringAlg
‘𝐸)‘(Base‘𝐹)) ∈ LMod) | 
| 176 | 174, 175 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → ((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LMod) | 
| 177 | 78, 170, 171, 172, 173, 176, 77 | lbslsp 33406 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → ((1r‘𝐸) ∈
(Base‘((subringAlg ‘𝐸)‘(Base‘𝐹))) ↔ ∃𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)(𝑣 finSupp
(0g‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))))) | 
| 178 | 169, 177 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → ∃𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)(𝑣 finSupp
(0g‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ (1r‘𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))))) | 
| 179 | 166, 178 | r19.29a 3161 | . . . . . . . . . . . . . 14
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → 𝑥 ∈ (Base‘𝐹)) | 
| 180 | 179 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝑥 ∈ (Base‘𝐹)) | 
| 181 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢
(.r‘𝐹) = (.r‘𝐹) | 
| 182 | 25, 181 | ringcl 20248 | . . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Ring ∧ (𝑣‘𝑥) ∈ (Base‘𝐹) ∧ 𝑥 ∈ (Base‘𝐹)) → ((𝑣‘𝑥)(.r‘𝐹)𝑥) ∈ (Base‘𝐹)) | 
| 183 | 106, 107,
180, 182 | syl3anc 1372 | . . . . . . . . . . . 12
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → ((𝑣‘𝑥)(.r‘𝐹)𝑥) ∈ (Base‘𝐹)) | 
| 184 | 103, 183 | eqeltrd 2840 | . . . . . . . . . . 11
⊢
((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) ∈ (Base‘𝐹)) | 
| 185 | 184 | ad2antrr 726 | . . . . . . . . . 10
⊢
((((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ 𝑣 finSupp
(0g‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹))))) ∧ 𝑢 = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg
(𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) ∈ (Base‘𝐹)) | 
| 186 | 22, 185 | eqeltrd 2840 | . . . . . . . . 9
⊢
((((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ 𝑣 finSupp
(0g‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹))))) ∧ 𝑢 = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝑢 ∈ (Base‘𝐹)) | 
| 187 | 186 | anasss 466 | . . . . . . . 8
⊢
(((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) ∧ 𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (𝑣 finSupp
(0g‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑢 = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))))) → 𝑢 ∈ (Base‘𝐹)) | 
| 188 | 85 | eleq2d 2826 | . . . . . . . . . 10
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (𝑢 ∈ (Base‘𝐸) ↔ 𝑢 ∈ (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹))))) | 
| 189 | 78, 170, 171, 172, 173, 176, 77 | lbslsp 33406 | . . . . . . . . . 10
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (𝑢 ∈ (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹))) ↔ ∃𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)(𝑣 finSupp
(0g‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑢 = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))))) | 
| 190 | 188, 189 | bitrd 279 | . . . . . . . . 9
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (𝑢 ∈ (Base‘𝐸) ↔ ∃𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)(𝑣 finSupp
(0g‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑢 = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))))) | 
| 191 | 190 | biimpa 476 | . . . . . . . 8
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) → ∃𝑣 ∈
((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)(𝑣 finSupp
(0g‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑢 = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖 ∈ 𝑏 ↦ ((𝑣‘𝑖)( ·𝑠
‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))))) | 
| 192 | 187, 191 | r19.29a 3161 | . . . . . . 7
⊢
(((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) → 𝑢 ∈ (Base‘𝐹)) | 
| 193 | 192 | ex 412 | . . . . . 6
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (𝑢 ∈ (Base‘𝐸) → 𝑢 ∈ (Base‘𝐹))) | 
| 194 | 193 | ssrdv 3988 | . . . . 5
⊢ ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (Base‘𝐸) ⊆ (Base‘𝐹)) | 
| 195 | 21, 194 | exlimddv 1934 | . . . 4
⊢ (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg
‘𝐸)‘(Base‘𝐹)))) → (Base‘𝐸) ⊆ (Base‘𝐹)) | 
| 196 | 9, 195 | exlimddv 1934 | . . 3
⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → (Base‘𝐸) ⊆ (Base‘𝐹)) | 
| 197 |  | simpr 484 | . . . 4
⊢ (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ (Base‘𝐸) ⊆ (Base‘𝐹)) → (Base‘𝐸) ⊆ (Base‘𝐹)) | 
| 198 | 37 | ad2antrr 726 | . . . 4
⊢ (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ (Base‘𝐸) ⊆ (Base‘𝐹)) → 𝐸 ∈ Field) | 
| 199 |  | fvexd 6920 | . . . 4
⊢ (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ (Base‘𝐸) ⊆ (Base‘𝐹)) → (Base‘𝐹) ∈ V) | 
| 200 | 43, 27 | ressid2 17279 | . . . 4
⊢
(((Base‘𝐸)
⊆ (Base‘𝐹)
∧ 𝐸 ∈ Field ∧
(Base‘𝐹) ∈ V)
→ (𝐸
↾s (Base‘𝐹)) = 𝐸) | 
| 201 | 197, 198,
199, 200 | syl3anc 1372 | . . 3
⊢ (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ (Base‘𝐸) ⊆ (Base‘𝐹)) → (𝐸 ↾s (Base‘𝐹)) = 𝐸) | 
| 202 | 196, 201 | mpdan 687 | . 2
⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → (𝐸 ↾s (Base‘𝐹)) = 𝐸) | 
| 203 | 2, 202 | eqtr2d 2777 | 1
⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → 𝐸 = 𝐹) |