Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  extdg1id Structured version   Visualization version   GIF version

Theorem extdg1id 31738
Description: If the degree of the extension 𝐸/FldExt𝐹 is 1, then 𝐸 and 𝐹 are identical. (Contributed by Thierry Arnoux, 6-Aug-2023.)
Assertion
Ref Expression
extdg1id ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → 𝐸 = 𝐹)

Proof of Theorem extdg1id
Dummy variables 𝑎 𝑥 𝑏 𝑖 𝑣 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fldextress 31727 . . 3 (𝐸/FldExt𝐹𝐹 = (𝐸s (Base‘𝐹)))
21adantr 481 . 2 ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → 𝐹 = (𝐸s (Base‘𝐹)))
3 fldextsralvec 31730 . . . . . . 7 (𝐸/FldExt𝐹 → ((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LVec)
43adantr 481 . . . . . 6 ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → ((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LVec)
5 eqid 2738 . . . . . . 7 (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))
65lbsex 20427 . . . . . 6 (((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LVec → (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))) ≠ ∅)
74, 6syl 17 . . . . 5 ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))) ≠ ∅)
8 n0 4280 . . . . 5 ((LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))) ≠ ∅ ↔ ∃𝑏 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
97, 8sylib 217 . . . 4 ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → ∃𝑏 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
10 simpr 485 . . . . . 6 (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) → 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
115dimval 31686 . . . . . . . 8 ((((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LVec ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) → (dim‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = (♯‘𝑏))
124, 11sylan 580 . . . . . . 7 (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) → (dim‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = (♯‘𝑏))
13 extdgval 31729 . . . . . . . . . 10 (𝐸/FldExt𝐹 → (𝐸[:]𝐹) = (dim‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
1413adantr 481 . . . . . . . . 9 ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → (𝐸[:]𝐹) = (dim‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
15 simpr 485 . . . . . . . . 9 ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → (𝐸[:]𝐹) = 1)
1614, 15eqtr3d 2780 . . . . . . . 8 ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → (dim‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = 1)
1716adantr 481 . . . . . . 7 (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) → (dim‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = 1)
1812, 17eqtr3d 2780 . . . . . 6 (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) → (♯‘𝑏) = 1)
19 hash1snb 14134 . . . . . . 7 (𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))) → ((♯‘𝑏) = 1 ↔ ∃𝑥 𝑏 = {𝑥}))
2019biimpa 477 . . . . . 6 ((𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))) ∧ (♯‘𝑏) = 1) → ∃𝑥 𝑏 = {𝑥})
2110, 18, 20syl2anc 584 . . . . 5 (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) → ∃𝑥 𝑏 = {𝑥})
22 simpr 485 . . . . . . . . . 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 766 . . . . . . . . . . . . . . . 16 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝑏 = {𝑥})
24 eqidd 2739 . . . . . . . . . . . . . . . . . . . 20 (𝐸/FldExt𝐹 → ((subringAlg ‘𝐸)‘(Base‘𝐹)) = ((subringAlg ‘𝐸)‘(Base‘𝐹)))
25 eqid 2738 . . . . . . . . . . . . . . . . . . . . . 22 (Base‘𝐹) = (Base‘𝐹)
2625fldextsubrg 31726 . . . . . . . . . . . . . . . . . . . . 21 (𝐸/FldExt𝐹 → (Base‘𝐹) ∈ (SubRing‘𝐸))
27 eqid 2738 . . . . . . . . . . . . . . . . . . . . . 22 (Base‘𝐸) = (Base‘𝐸)
2827subrgss 20025 . . . . . . . . . . . . . . . . . . . . 21 ((Base‘𝐹) ∈ (SubRing‘𝐸) → (Base‘𝐹) ⊆ (Base‘𝐸))
2926, 28syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝐸/FldExt𝐹 → (Base‘𝐹) ⊆ (Base‘𝐸))
3024, 29sravsca 20449 . . . . . . . . . . . . . . . . . . 19 (𝐸/FldExt𝐹 → (.r𝐸) = ( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
3130eqcomd 2744 . . . . . . . . . . . . . . . . . 18 (𝐸/FldExt𝐹 → ( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = (.r𝐸))
3231ad5antr 731 . . . . . . . . . . . . . . . . 17 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ 𝑖𝑏) → ( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = (.r𝐸))
3332oveqd 7292 . . . . . . . . . . . . . . . 16 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ 𝑖𝑏) → ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖) = ((𝑣𝑖)(.r𝐸)𝑖))
3423, 33mpteq12dva 5163 . . . . . . . . . . . . . . 15 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)) = (𝑖 ∈ {𝑥} ↦ ((𝑣𝑖)(.r𝐸)𝑖)))
3534oveq2d 7291 . . . . . . . . . . . . . 14 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝐸 Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) = (𝐸 Σg (𝑖 ∈ {𝑥} ↦ ((𝑣𝑖)(.r𝐸)𝑖))))
36 eqid 2738 . . . . . . . . . . . . . . . . 17 ((subringAlg ‘𝐸)‘(Base‘𝐹)) = ((subringAlg ‘𝐸)‘(Base‘𝐹))
37 fldextfld1 31724 . . . . . . . . . . . . . . . . . . 19 (𝐸/FldExt𝐹𝐸 ∈ Field)
38 isfld 20000 . . . . . . . . . . . . . . . . . . . 20 (𝐸 ∈ Field ↔ (𝐸 ∈ DivRing ∧ 𝐸 ∈ CRing))
3938simplbi 498 . . . . . . . . . . . . . . . . . . 19 (𝐸 ∈ Field → 𝐸 ∈ DivRing)
4037, 39syl 17 . . . . . . . . . . . . . . . . . 18 (𝐸/FldExt𝐹𝐸 ∈ DivRing)
4140adantr 481 . . . . . . . . . . . . . . . . 17 ((𝐸/FldExt𝐹𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) → 𝐸 ∈ DivRing)
4226adantr 481 . . . . . . . . . . . . . . . . 17 ((𝐸/FldExt𝐹𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) → (Base‘𝐹) ∈ (SubRing‘𝐸))
43 eqid 2738 . . . . . . . . . . . . . . . . 17 (𝐸s (Base‘𝐹)) = (𝐸s (Base‘𝐹))
44 fldextfld2 31725 . . . . . . . . . . . . . . . . . . . 20 (𝐸/FldExt𝐹𝐹 ∈ Field)
45 isfld 20000 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 ∈ Field ↔ (𝐹 ∈ DivRing ∧ 𝐹 ∈ CRing))
4645simplbi 498 . . . . . . . . . . . . . . . . . . . 20 (𝐹 ∈ Field → 𝐹 ∈ DivRing)
4744, 46syl 17 . . . . . . . . . . . . . . . . . . 19 (𝐸/FldExt𝐹𝐹 ∈ DivRing)
481, 47eqeltrrd 2840 . . . . . . . . . . . . . . . . . 18 (𝐸/FldExt𝐹 → (𝐸s (Base‘𝐹)) ∈ DivRing)
4948adantr 481 . . . . . . . . . . . . . . . . 17 ((𝐸/FldExt𝐹𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) → (𝐸s (Base‘𝐹)) ∈ DivRing)
50 simpr 485 . . . . . . . . . . . . . . . . 17 ((𝐸/FldExt𝐹𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) → 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
5136, 41, 42, 43, 49, 50drgextgsum 31682 . . . . . . . . . . . . . . . 16 ((𝐸/FldExt𝐹𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) → (𝐸 Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))))
5251adantlr 712 . . . . . . . . . . . . . . 15 (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) → (𝐸 Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))))
5352ad2antrr 723 . . . . . . . . . . . . . 14 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝐸 Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))))
54 drngring 19998 . . . . . . . . . . . . . . . . . . 19 (𝐸 ∈ DivRing → 𝐸 ∈ Ring)
5537, 39, 543syl 18 . . . . . . . . . . . . . . . . . 18 (𝐸/FldExt𝐹𝐸 ∈ Ring)
56 ringmnd 19793 . . . . . . . . . . . . . . . . . 18 (𝐸 ∈ Ring → 𝐸 ∈ Mnd)
5755, 56syl 17 . . . . . . . . . . . . . . . . 17 (𝐸/FldExt𝐹𝐸 ∈ Mnd)
5857ad4antr 729 . . . . . . . . . . . . . . . 16 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝐸 ∈ Mnd)
59 vex 3436 . . . . . . . . . . . . . . . . 17 𝑥 ∈ V
6059a1i 11 . . . . . . . . . . . . . . . 16 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝑥 ∈ V)
6155ad3antrrr 727 . . . . . . . . . . . . . . . . . 18 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → 𝐸 ∈ Ring)
6261adantr 481 . . . . . . . . . . . . . . . . 17 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝐸 ∈ Ring)
6329ad3antrrr 727 . . . . . . . . . . . . . . . . . . 19 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (Base‘𝐹) ⊆ (Base‘𝐸))
6463adantr 481 . . . . . . . . . . . . . . . . . 18 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (Base‘𝐹) ⊆ (Base‘𝐸))
65 elmapi 8637 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏) → 𝑣:𝑏⟶(Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))))
6665adantl 482 . . . . . . . . . . . . . . . . . . . 20 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝑣:𝑏⟶(Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))))
67 vsnid 4598 . . . . . . . . . . . . . . . . . . . . 21 𝑥 ∈ {𝑥}
6867, 23eleqtrrid 2846 . . . . . . . . . . . . . . . . . . . 20 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝑥𝑏)
6966, 68ffvelrnd 6962 . . . . . . . . . . . . . . . . . . 19 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝑣𝑥) ∈ (Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))))
7024, 29srasca 20447 . . . . . . . . . . . . . . . . . . . . . 22 (𝐸/FldExt𝐹 → (𝐸s (Base‘𝐹)) = (Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
711, 70eqtrd 2778 . . . . . . . . . . . . . . . . . . . . 21 (𝐸/FldExt𝐹𝐹 = (Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
7271fveq2d 6778 . . . . . . . . . . . . . . . . . . . 20 (𝐸/FldExt𝐹 → (Base‘𝐹) = (Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))))
7372ad4antr 729 . . . . . . . . . . . . . . . . . . 19 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (Base‘𝐹) = (Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))))
7469, 73eleqtrrd 2842 . . . . . . . . . . . . . . . . . 18 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝑣𝑥) ∈ (Base‘𝐹))
7564, 74sseldd 3922 . . . . . . . . . . . . . . . . 17 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝑣𝑥) ∈ (Base‘𝐸))
76 simpr 485 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → 𝑏 = {𝑥})
77 simplr 766 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
78 eqid 2738 . . . . . . . . . . . . . . . . . . . . . . 23 (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹)))
7978, 5lbsss 20339 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))) → 𝑏 ⊆ (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
8077, 79syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → 𝑏 ⊆ (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
8176, 80eqsstrrd 3960 . . . . . . . . . . . . . . . . . . . 20 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → {𝑥} ⊆ (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
8259snss 4719 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹))) ↔ {𝑥} ⊆ (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
8381, 82sylibr 233 . . . . . . . . . . . . . . . . . . 19 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → 𝑥 ∈ (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
84 eqidd 2739 . . . . . . . . . . . . . . . . . . . 20 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → ((subringAlg ‘𝐸)‘(Base‘𝐹)) = ((subringAlg ‘𝐸)‘(Base‘𝐹)))
8584, 63srabase 20441 . . . . . . . . . . . . . . . . . . 19 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (Base‘𝐸) = (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
8683, 85eleqtrrd 2842 . . . . . . . . . . . . . . . . . 18 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → 𝑥 ∈ (Base‘𝐸))
8786adantr 481 . . . . . . . . . . . . . . . . 17 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝑥 ∈ (Base‘𝐸))
88 eqid 2738 . . . . . . . . . . . . . . . . . 18 (.r𝐸) = (.r𝐸)
8927, 88ringcl 19800 . . . . . . . . . . . . . . . . 17 ((𝐸 ∈ Ring ∧ (𝑣𝑥) ∈ (Base‘𝐸) ∧ 𝑥 ∈ (Base‘𝐸)) → ((𝑣𝑥)(.r𝐸)𝑥) ∈ (Base‘𝐸))
9062, 75, 87, 89syl3anc 1370 . . . . . . . . . . . . . . . 16 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → ((𝑣𝑥)(.r𝐸)𝑥) ∈ (Base‘𝐸))
91 simpr 485 . . . . . . . . . . . . . . . . . 18 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ 𝑖 = 𝑥) → 𝑖 = 𝑥)
9291fveq2d 6778 . . . . . . . . . . . . . . . . 17 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ 𝑖 = 𝑥) → (𝑣𝑖) = (𝑣𝑥))
9392, 91oveq12d 7293 . . . . . . . . . . . . . . . 16 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ 𝑖 = 𝑥) → ((𝑣𝑖)(.r𝐸)𝑖) = ((𝑣𝑥)(.r𝐸)𝑥))
9427, 58, 60, 90, 93gsumsnd 19553 . . . . . . . . . . . . . . 15 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝐸 Σg (𝑖 ∈ {𝑥} ↦ ((𝑣𝑖)(.r𝐸)𝑖))) = ((𝑣𝑥)(.r𝐸)𝑥))
951fveq2d 6778 . . . . . . . . . . . . . . . . . 18 (𝐸/FldExt𝐹 → (.r𝐹) = (.r‘(𝐸s (Base‘𝐹))))
9643, 88ressmulr 17017 . . . . . . . . . . . . . . . . . . 19 ((Base‘𝐹) ∈ (SubRing‘𝐸) → (.r𝐸) = (.r‘(𝐸s (Base‘𝐹))))
9726, 96syl 17 . . . . . . . . . . . . . . . . . 18 (𝐸/FldExt𝐹 → (.r𝐸) = (.r‘(𝐸s (Base‘𝐹))))
9895, 97eqtr4d 2781 . . . . . . . . . . . . . . . . 17 (𝐸/FldExt𝐹 → (.r𝐹) = (.r𝐸))
9998ad4antr 729 . . . . . . . . . . . . . . . 16 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (.r𝐹) = (.r𝐸))
10099oveqd 7292 . . . . . . . . . . . . . . 15 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → ((𝑣𝑥)(.r𝐹)𝑥) = ((𝑣𝑥)(.r𝐸)𝑥))
10194, 100eqtr4d 2781 . . . . . . . . . . . . . 14 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝐸 Σg (𝑖 ∈ {𝑥} ↦ ((𝑣𝑖)(.r𝐸)𝑖))) = ((𝑣𝑥)(.r𝐹)𝑥))
10235, 53, 1013eqtr3d 2786 . . . . . . . . . . . . 13 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) = ((𝑣𝑥)(.r𝐹)𝑥))
103102adantlr 712 . . . . . . . . . . . 12 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) = ((𝑣𝑥)(.r𝐹)𝑥))
104 drngring 19998 . . . . . . . . . . . . . . 15 (𝐹 ∈ DivRing → 𝐹 ∈ Ring)
10544, 46, 1043syl 18 . . . . . . . . . . . . . 14 (𝐸/FldExt𝐹𝐹 ∈ Ring)
106105ad5antr 731 . . . . . . . . . . . . 13 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝐹 ∈ Ring)
10774adantlr 712 . . . . . . . . . . . . 13 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝑣𝑥) ∈ (Base‘𝐹))
108 eqid 2738 . . . . . . . . . . . . . . . . . . . 20 (1r𝐸) = (1r𝐸)
109 eqid 2738 . . . . . . . . . . . . . . . . . . . 20 (Unit‘𝐸) = (Unit‘𝐸)
110 eqid 2738 . . . . . . . . . . . . . . . . . . . 20 (invr𝐸) = (invr𝐸)
111 simp-5l 782 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝐸/FldExt𝐹)
112111, 55syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝐸 ∈ Ring)
11387adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝑥 ∈ (Base‘𝐸))
11475adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (𝑣𝑥) ∈ (Base‘𝐸))
11538simprbi 497 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐸 ∈ Field → 𝐸 ∈ CRing)
116111, 37, 1153syl 18 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝐸 ∈ CRing)
11727, 88crngcom 19801 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐸 ∈ CRing ∧ 𝑥 ∈ (Base‘𝐸) ∧ (𝑣𝑥) ∈ (Base‘𝐸)) → (𝑥(.r𝐸)(𝑣𝑥)) = ((𝑣𝑥)(.r𝐸)𝑥))
118116, 113, 114, 117syl3anc 1370 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (𝑥(.r𝐸)(𝑣𝑥)) = ((𝑣𝑥)(.r𝐸)𝑥))
119 simpr 485 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))))
12052ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . . 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‘𝐹)))𝑖))))
12134adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)) = (𝑖 ∈ {𝑥} ↦ ((𝑣𝑖)(.r𝐸)𝑖)))
122121oveq2d 7291 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (𝐸 Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) = (𝐸 Σg (𝑖 ∈ {𝑥} ↦ ((𝑣𝑖)(.r𝐸)𝑖))))
123119, 120, 1223eqtr2d 2784 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (1r𝐸) = (𝐸 Σg (𝑖 ∈ {𝑥} ↦ ((𝑣𝑖)(.r𝐸)𝑖))))
12494adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (𝐸 Σg (𝑖 ∈ {𝑥} ↦ ((𝑣𝑖)(.r𝐸)𝑖))) = ((𝑣𝑥)(.r𝐸)𝑥))
125123, 124eqtrd 2778 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (1r𝐸) = ((𝑣𝑥)(.r𝐸)𝑥))
126118, 125eqtr4d 2781 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (𝑥(.r𝐸)(𝑣𝑥)) = (1r𝐸))
127125eqcomd 2744 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → ((𝑣𝑥)(.r𝐸)𝑥) = (1r𝐸))
12827, 88, 108, 109, 110, 112, 113, 114, 126, 127invrvald 21825 . . . . . . . . . . . . . . . . . . 19 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (𝑥 ∈ (Unit‘𝐸) ∧ ((invr𝐸)‘𝑥) = (𝑣𝑥)))
129128simpld 495 . . . . . . . . . . . . . . . . . 18 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝑥 ∈ (Unit‘𝐸))
130109, 110unitinvinv 19917 . . . . . . . . . . . . . . . . . 18 ((𝐸 ∈ Ring ∧ 𝑥 ∈ (Unit‘𝐸)) → ((invr𝐸)‘((invr𝐸)‘𝑥)) = 𝑥)
13162, 129, 130syl2an2r 682 . . . . . . . . . . . . . . . . 17 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → ((invr𝐸)‘((invr𝐸)‘𝑥)) = 𝑥)
132111, 37, 393syl 18 . . . . . . . . . . . . . . . . . 18 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝐸 ∈ DivRing)
133111, 26syl 17 . . . . . . . . . . . . . . . . . 18 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (Base‘𝐹) ∈ (SubRing‘𝐸))
134111, 1syl 17 . . . . . . . . . . . . . . . . . . 19 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝐹 = (𝐸s (Base‘𝐹)))
135111, 44, 463syl 18 . . . . . . . . . . . . . . . . . . 19 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝐹 ∈ DivRing)
136134, 135eqeltrrd 2840 . . . . . . . . . . . . . . . . . 18 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (𝐸s (Base‘𝐹)) ∈ DivRing)
137128simprd 496 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → ((invr𝐸)‘𝑥) = (𝑣𝑥))
13874adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (𝑣𝑥) ∈ (Base‘𝐹))
139137, 138eqeltrd 2839 . . . . . . . . . . . . . . . . . . 19 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → ((invr𝐸)‘𝑥) ∈ (Base‘𝐹))
140 eqidd 2739 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐸/FldExt𝐹 → (0g𝐸) = (0g𝐸))
14124, 140, 29sralmod0 20458 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐸/FldExt𝐹 → (0g𝐸) = (0g‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
142141ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) → (0g𝐸) = (0g‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
1435lbslinds 21040 . . . . . . . . . . . . . . . . . . . . . . . . 25 (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))) ⊆ (LIndS‘((subringAlg ‘𝐸)‘(Base‘𝐹)))
144143, 10sselid 3919 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) → 𝑏 ∈ (LIndS‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
145 eqid 2738 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0g‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = (0g‘((subringAlg ‘𝐸)‘(Base‘𝐹)))
1461450nellinds 31566 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LVec ∧ 𝑏 ∈ (LIndS‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) → ¬ (0g‘((subringAlg ‘𝐸)‘(Base‘𝐹))) ∈ 𝑏)
1474, 144, 146syl2an2r 682 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) → ¬ (0g‘((subringAlg ‘𝐸)‘(Base‘𝐹))) ∈ 𝑏)
148142, 147eqneltrd 2858 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) → ¬ (0g𝐸) ∈ 𝑏)
149148ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → ¬ (0g𝐸) ∈ 𝑏)
150 nelne2 3042 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝑏 ∧ ¬ (0g𝐸) ∈ 𝑏) → 𝑥 ≠ (0g𝐸))
15168, 149, 150syl2an2r 682 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝑥 ≠ (0g𝐸))
152 eqid 2738 . . . . . . . . . . . . . . . . . . . . 21 (0g𝐸) = (0g𝐸)
15327, 152, 110drnginvrn0 20009 . . . . . . . . . . . . . . . . . . . 20 ((𝐸 ∈ DivRing ∧ 𝑥 ∈ (Base‘𝐸) ∧ 𝑥 ≠ (0g𝐸)) → ((invr𝐸)‘𝑥) ≠ (0g𝐸))
154132, 113, 151, 153syl3anc 1370 . . . . . . . . . . . . . . . . . . 19 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → ((invr𝐸)‘𝑥) ≠ (0g𝐸))
155 eldifsn 4720 . . . . . . . . . . . . . . . . . . 19 (((invr𝐸)‘𝑥) ∈ ((Base‘𝐹) ∖ {(0g𝐸)}) ↔ (((invr𝐸)‘𝑥) ∈ (Base‘𝐹) ∧ ((invr𝐸)‘𝑥) ≠ (0g𝐸)))
156139, 154, 155sylanbrc 583 . . . . . . . . . . . . . . . . . 18 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → ((invr𝐸)‘𝑥) ∈ ((Base‘𝐹) ∖ {(0g𝐸)}))
157 fveq2 6774 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = ((invr𝐸)‘𝑥) → ((invr𝐸)‘𝑎) = ((invr𝐸)‘((invr𝐸)‘𝑥)))
158157eleq1d 2823 . . . . . . . . . . . . . . . . . . 19 (𝑎 = ((invr𝐸)‘𝑥) → (((invr𝐸)‘𝑎) ∈ (Base‘𝐹) ↔ ((invr𝐸)‘((invr𝐸)‘𝑥)) ∈ (Base‘𝐹)))
15943, 152, 110issubdrg 20049 . . . . . . . . . . . . . . . . . . . . 21 ((𝐸 ∈ DivRing ∧ (Base‘𝐹) ∈ (SubRing‘𝐸)) → ((𝐸s (Base‘𝐹)) ∈ DivRing ↔ ∀𝑎 ∈ ((Base‘𝐹) ∖ {(0g𝐸)})((invr𝐸)‘𝑎) ∈ (Base‘𝐹)))
160159biimpa 477 . . . . . . . . . . . . . . . . . . . 20 (((𝐸 ∈ DivRing ∧ (Base‘𝐹) ∈ (SubRing‘𝐸)) ∧ (𝐸s (Base‘𝐹)) ∈ DivRing) → ∀𝑎 ∈ ((Base‘𝐹) ∖ {(0g𝐸)})((invr𝐸)‘𝑎) ∈ (Base‘𝐹))
161160adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝐸 ∈ DivRing ∧ (Base‘𝐹) ∈ (SubRing‘𝐸)) ∧ (𝐸s (Base‘𝐹)) ∈ DivRing) ∧ ((invr𝐸)‘𝑥) ∈ ((Base‘𝐹) ∖ {(0g𝐸)})) → ∀𝑎 ∈ ((Base‘𝐹) ∖ {(0g𝐸)})((invr𝐸)‘𝑎) ∈ (Base‘𝐹))
162 simpr 485 . . . . . . . . . . . . . . . . . . 19 ((((𝐸 ∈ DivRing ∧ (Base‘𝐹) ∈ (SubRing‘𝐸)) ∧ (𝐸s (Base‘𝐹)) ∈ DivRing) ∧ ((invr𝐸)‘𝑥) ∈ ((Base‘𝐹) ∖ {(0g𝐸)})) → ((invr𝐸)‘𝑥) ∈ ((Base‘𝐹) ∖ {(0g𝐸)}))
163158, 161, 162rspcdva 3562 . . . . . . . . . . . . . . . . . 18 ((((𝐸 ∈ DivRing ∧ (Base‘𝐹) ∈ (SubRing‘𝐸)) ∧ (𝐸s (Base‘𝐹)) ∈ DivRing) ∧ ((invr𝐸)‘𝑥) ∈ ((Base‘𝐹) ∖ {(0g𝐸)})) → ((invr𝐸)‘((invr𝐸)‘𝑥)) ∈ (Base‘𝐹))
164132, 133, 136, 156, 163syl1111anc 837 . . . . . . . . . . . . . . . . 17 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → ((invr𝐸)‘((invr𝐸)‘𝑥)) ∈ (Base‘𝐹))
165131, 164eqeltrrd 2840 . . . . . . . . . . . . . . . 16 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝑥 ∈ (Base‘𝐹))
166165adantrl 713 . . . . . . . . . . . . . . 15 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (𝑣 finSupp (0g‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))))) → 𝑥 ∈ (Base‘𝐹))
16727, 108ringidcl 19807 . . . . . . . . . . . . . . . . . 18 (𝐸 ∈ Ring → (1r𝐸) ∈ (Base‘𝐸))
16861, 167syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (1r𝐸) ∈ (Base‘𝐸))
169168, 85eleqtrd 2841 . . . . . . . . . . . . . . . 16 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (1r𝐸) ∈ (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
170 eqid 2738 . . . . . . . . . . . . . . . . 17 (Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) = (Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
171 eqid 2738 . . . . . . . . . . . . . . . . 17 (Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = (Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))
172 eqid 2738 . . . . . . . . . . . . . . . . 17 (0g‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) = (0g‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
173 eqid 2738 . . . . . . . . . . . . . . . . 17 ( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = ( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))
1744ad2antrr 723 . . . . . . . . . . . . . . . . . 18 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → ((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LVec)
175 lveclmod 20368 . . . . . . . . . . . . . . . . . 18 (((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LVec → ((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LMod)
176174, 175syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → ((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LMod)
17778, 170, 171, 172, 173, 176, 77lbslsp 31572 . . . . . . . . . . . . . . . 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‘𝐹)))𝑖))))))
178169, 177mpbid 231 . . . . . . . . . . . . . . 15 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → ∃𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)(𝑣 finSupp (0g‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))))
179166, 178r19.29a 3218 . . . . . . . . . . . . . 14 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → 𝑥 ∈ (Base‘𝐹))
180179ad2antrr 723 . . . . . . . . . . . . 13 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝑥 ∈ (Base‘𝐹))
181 eqid 2738 . . . . . . . . . . . . . 14 (.r𝐹) = (.r𝐹)
18225, 181ringcl 19800 . . . . . . . . . . . . 13 ((𝐹 ∈ Ring ∧ (𝑣𝑥) ∈ (Base‘𝐹) ∧ 𝑥 ∈ (Base‘𝐹)) → ((𝑣𝑥)(.r𝐹)𝑥) ∈ (Base‘𝐹))
183106, 107, 180, 182syl3anc 1370 . . . . . . . . . . . 12 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → ((𝑣𝑥)(.r𝐹)𝑥) ∈ (Base‘𝐹))
184103, 183eqeltrd 2839 . . . . . . . . . . 11 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) ∈ (Base‘𝐹))
185184ad2antrr 723 . . . . . . . . . 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‘𝐹))
18622, 185eqeltrd 2839 . . . . . . . . 9 ((((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ 𝑣 finSupp (0g‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹))))) ∧ 𝑢 = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝑢 ∈ (Base‘𝐹))
187186anasss 467 . . . . . . . 8 (((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (𝑣 finSupp (0g‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑢 = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))))) → 𝑢 ∈ (Base‘𝐹))
18885eleq2d 2824 . . . . . . . . . 10 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (𝑢 ∈ (Base‘𝐸) ↔ 𝑢 ∈ (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹)))))
18978, 170, 171, 172, 173, 176, 77lbslsp 31572 . . . . . . . . . 10 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (𝑢 ∈ (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹))) ↔ ∃𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)(𝑣 finSupp (0g‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑢 = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))))))
190188, 189bitrd 278 . . . . . . . . 9 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (𝑢 ∈ (Base‘𝐸) ↔ ∃𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)(𝑣 finSupp (0g‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑢 = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))))))
191190biimpa 477 . . . . . . . 8 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) → ∃𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)(𝑣 finSupp (0g‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑢 = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))))
192187, 191r19.29a 3218 . . . . . . 7 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) → 𝑢 ∈ (Base‘𝐹))
193192ex 413 . . . . . 6 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (𝑢 ∈ (Base‘𝐸) → 𝑢 ∈ (Base‘𝐹)))
194193ssrdv 3927 . . . . 5 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (Base‘𝐸) ⊆ (Base‘𝐹))
19521, 194exlimddv 1938 . . . 4 (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) → (Base‘𝐸) ⊆ (Base‘𝐹))
1969, 195exlimddv 1938 . . 3 ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → (Base‘𝐸) ⊆ (Base‘𝐹))
197 simpr 485 . . . 4 (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ (Base‘𝐸) ⊆ (Base‘𝐹)) → (Base‘𝐸) ⊆ (Base‘𝐹))
19837ad2antrr 723 . . . 4 (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ (Base‘𝐸) ⊆ (Base‘𝐹)) → 𝐸 ∈ Field)
199 fvexd 6789 . . . 4 (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ (Base‘𝐸) ⊆ (Base‘𝐹)) → (Base‘𝐹) ∈ V)
20043, 27ressid2 16945 . . . 4 (((Base‘𝐸) ⊆ (Base‘𝐹) ∧ 𝐸 ∈ Field ∧ (Base‘𝐹) ∈ V) → (𝐸s (Base‘𝐹)) = 𝐸)
201197, 198, 199, 200syl3anc 1370 . . 3 (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ (Base‘𝐸) ⊆ (Base‘𝐹)) → (𝐸s (Base‘𝐹)) = 𝐸)
202196, 201mpdan 684 . 2 ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → (𝐸s (Base‘𝐹)) = 𝐸)
2032, 202eqtr2d 2779 1 ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → 𝐸 = 𝐹)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396   = wceq 1539  wex 1782  wcel 2106  wne 2943  wral 3064  wrex 3065  Vcvv 3432  cdif 3884  wss 3887  c0 4256  {csn 4561   class class class wbr 5074  cmpt 5157  wf 6429  cfv 6433  (class class class)co 7275  m cmap 8615   finSupp cfsupp 9128  1c1 10872  chash 14044  Basecbs 16912  s cress 16941  .rcmulr 16963  Scalarcsca 16965   ·𝑠 cvsca 16966  0gc0g 17150   Σg cgsu 17151  Mndcmnd 18385  1rcur 19737  Ringcrg 19783  CRingccrg 19784  Unitcui 19881  invrcinvr 19913  DivRingcdr 19991  Fieldcfield 19992  SubRingcsubrg 20020  LModclmod 20123  LBasisclbs 20336  LVecclvec 20364  subringAlg csra 20430  LIndSclinds 21012  dimcldim 31684  /FldExtcfldext 31713  [:]cextdg 31716
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-reg 9351  ax-inf2 9399  ax-ac2 10219  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-iin 4927  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-se 5545  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-isom 6442  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-of 7533  df-rpss 7576  df-om 7713  df-1st 7831  df-2nd 7832  df-supp 7978  df-tpos 8042  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-oadd 8301  df-er 8498  df-map 8617  df-ixp 8686  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-fsupp 9129  df-sup 9201  df-oi 9269  df-r1 9522  df-rank 9523  df-dju 9659  df-card 9697  df-acn 9700  df-ac 9872  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-nn 11974  df-2 12036  df-3 12037  df-4 12038  df-5 12039  df-6 12040  df-7 12041  df-8 12042  df-9 12043  df-n0 12234  df-xnn0 12306  df-z 12320  df-dec 12438  df-uz 12583  df-fz 13240  df-fzo 13383  df-seq 13722  df-hash 14045  df-struct 16848  df-sets 16865  df-slot 16883  df-ndx 16895  df-base 16913  df-ress 16942  df-plusg 16975  df-mulr 16976  df-sca 16978  df-vsca 16979  df-ip 16980  df-tset 16981  df-ple 16982  df-ocomp 16983  df-ds 16984  df-hom 16986  df-cco 16987  df-0g 17152  df-gsum 17153  df-prds 17158  df-pws 17160  df-mre 17295  df-mrc 17296  df-mri 17297  df-acs 17298  df-proset 18013  df-drs 18014  df-poset 18031  df-ipo 18246  df-mgm 18326  df-sgrp 18375  df-mnd 18386  df-mhm 18430  df-submnd 18431  df-grp 18580  df-minusg 18581  df-sbg 18582  df-mulg 18701  df-subg 18752  df-ghm 18832  df-cntz 18923  df-cmn 19388  df-abl 19389  df-mgp 19721  df-ur 19738  df-ring 19785  df-cring 19786  df-oppr 19862  df-dvdsr 19883  df-unit 19884  df-invr 19914  df-drng 19993  df-field 19994  df-subrg 20022  df-lmod 20125  df-lss 20194  df-lsp 20234  df-lmhm 20284  df-lbs 20337  df-lvec 20365  df-sra 20434  df-rgmod 20435  df-nzr 20529  df-dsmm 20939  df-frlm 20954  df-uvc 20990  df-lindf 21013  df-linds 21014  df-dim 31685  df-fldext 31717  df-extdg 31718
This theorem is referenced by:  extdg1b  31739
  Copyright terms: Public domain W3C validator