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 32580
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 32569 . . 3 (𝐸/FldExt𝐹𝐹 = (𝐸s (Base‘𝐹)))
21adantr 481 . 2 ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → 𝐹 = (𝐸s (Base‘𝐹)))
3 fldextsralvec 32572 . . . . . . 7 (𝐸/FldExt𝐹 → ((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LVec)
43adantr 481 . . . . . 6 ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → ((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LVec)
5 eqid 2731 . . . . . . 7 (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))
65lbsex 20727 . . . . . 6 (((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LVec → (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))) ≠ ∅)
74, 6syl 17 . . . . 5 ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))) ≠ ∅)
8 n0 4342 . . . . 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 32525 . . . . . . . 8 ((((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LVec ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) → (dim‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = (♯‘𝑏))
124, 11sylan 580 . . . . . . 7 (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) → (dim‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = (♯‘𝑏))
13 extdgval 32571 . . . . . . . . . 10 (𝐸/FldExt𝐹 → (𝐸[:]𝐹) = (dim‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
1413adantr 481 . . . . . . . . 9 ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → (𝐸[:]𝐹) = (dim‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
15 simpr 485 . . . . . . . . 9 ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → (𝐸[:]𝐹) = 1)
1614, 15eqtr3d 2773 . . . . . . . 8 ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → (dim‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = 1)
1716adantr 481 . . . . . . 7 (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) → (dim‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = 1)
1812, 17eqtr3d 2773 . . . . . 6 (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) → (♯‘𝑏) = 1)
19 hash1snb 14361 . . . . . . 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 767 . . . . . . . . . . . . . . . 16 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝑏 = {𝑥})
24 eqidd 2732 . . . . . . . . . . . . . . . . . . . 20 (𝐸/FldExt𝐹 → ((subringAlg ‘𝐸)‘(Base‘𝐹)) = ((subringAlg ‘𝐸)‘(Base‘𝐹)))
25 eqid 2731 . . . . . . . . . . . . . . . . . . . . . 22 (Base‘𝐹) = (Base‘𝐹)
2625fldextsubrg 32568 . . . . . . . . . . . . . . . . . . . . 21 (𝐸/FldExt𝐹 → (Base‘𝐹) ∈ (SubRing‘𝐸))
27 eqid 2731 . . . . . . . . . . . . . . . . . . . . . 22 (Base‘𝐸) = (Base‘𝐸)
2827subrgss 20313 . . . . . . . . . . . . . . . . . . . . 21 ((Base‘𝐹) ∈ (SubRing‘𝐸) → (Base‘𝐹) ⊆ (Base‘𝐸))
2926, 28syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝐸/FldExt𝐹 → (Base‘𝐹) ⊆ (Base‘𝐸))
3024, 29sravsca 20749 . . . . . . . . . . . . . . . . . . 19 (𝐸/FldExt𝐹 → (.r𝐸) = ( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
3130eqcomd 2737 . . . . . . . . . . . . . . . . . 18 (𝐸/FldExt𝐹 → ( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = (.r𝐸))
3231ad5antr 732 . . . . . . . . . . . . . . . . 17 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ 𝑖𝑏) → ( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = (.r𝐸))
3332oveqd 7410 . . . . . . . . . . . . . . . 16 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ 𝑖𝑏) → ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖) = ((𝑣𝑖)(.r𝐸)𝑖))
3423, 33mpteq12dva 5230 . . . . . . . . . . . . . . 15 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)) = (𝑖 ∈ {𝑥} ↦ ((𝑣𝑖)(.r𝐸)𝑖)))
3534oveq2d 7409 . . . . . . . . . . . . . 14 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝐸 Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) = (𝐸 Σg (𝑖 ∈ {𝑥} ↦ ((𝑣𝑖)(.r𝐸)𝑖))))
36 eqid 2731 . . . . . . . . . . . . . . . . 17 ((subringAlg ‘𝐸)‘(Base‘𝐹)) = ((subringAlg ‘𝐸)‘(Base‘𝐹))
37 fldextfld1 32566 . . . . . . . . . . . . . . . . . . 19 (𝐸/FldExt𝐹𝐸 ∈ Field)
38 isfld 20276 . . . . . . . . . . . . . . . . . . . 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 2731 . . . . . . . . . . . . . . . . 17 (𝐸s (Base‘𝐹)) = (𝐸s (Base‘𝐹))
44 fldextfld2 32567 . . . . . . . . . . . . . . . . . . . 20 (𝐸/FldExt𝐹𝐹 ∈ Field)
45 isfld 20276 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 ∈ Field ↔ (𝐹 ∈ DivRing ∧ 𝐹 ∈ CRing))
4645simplbi 498 . . . . . . . . . . . . . . . . . . . 20 (𝐹 ∈ Field → 𝐹 ∈ DivRing)
4744, 46syl 17 . . . . . . . . . . . . . . . . . . 19 (𝐸/FldExt𝐹𝐹 ∈ DivRing)
481, 47eqeltrrd 2833 . . . . . . . . . . . . . . . . . 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 32521 . . . . . . . . . . . . . . . 16 ((𝐸/FldExt𝐹𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) → (𝐸 Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))))
5251adantlr 713 . . . . . . . . . . . . . . 15 (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) → (𝐸 Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))))
5352ad2antrr 724 . . . . . . . . . . . . . 14 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝐸 Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))))
54 drngring 20272 . . . . . . . . . . . . . . . . . . 19 (𝐸 ∈ DivRing → 𝐸 ∈ Ring)
5537, 39, 543syl 18 . . . . . . . . . . . . . . . . . 18 (𝐸/FldExt𝐹𝐸 ∈ Ring)
56 ringmnd 20024 . . . . . . . . . . . . . . . . . 18 (𝐸 ∈ Ring → 𝐸 ∈ Mnd)
5755, 56syl 17 . . . . . . . . . . . . . . . . 17 (𝐸/FldExt𝐹𝐸 ∈ Mnd)
5857ad4antr 730 . . . . . . . . . . . . . . . 16 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝐸 ∈ Mnd)
59 vex 3477 . . . . . . . . . . . . . . . . 17 𝑥 ∈ V
6059a1i 11 . . . . . . . . . . . . . . . 16 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝑥 ∈ V)
6155ad3antrrr 728 . . . . . . . . . . . . . . . . . 18 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → 𝐸 ∈ Ring)
6261adantr 481 . . . . . . . . . . . . . . . . 17 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝐸 ∈ Ring)
6329ad3antrrr 728 . . . . . . . . . . . . . . . . . . 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 8826 . . . . . . . . . . . . . . . . . . . . 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 4659 . . . . . . . . . . . . . . . . . . . . 21 𝑥 ∈ {𝑥}
6867, 23eleqtrrid 2839 . . . . . . . . . . . . . . . . . . . 20 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝑥𝑏)
6966, 68ffvelcdmd 7072 . . . . . . . . . . . . . . . . . . 19 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝑣𝑥) ∈ (Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))))
7024, 29srasca 20747 . . . . . . . . . . . . . . . . . . . . . 22 (𝐸/FldExt𝐹 → (𝐸s (Base‘𝐹)) = (Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
711, 70eqtrd 2771 . . . . . . . . . . . . . . . . . . . . 21 (𝐸/FldExt𝐹𝐹 = (Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
7271fveq2d 6882 . . . . . . . . . . . . . . . . . . . 20 (𝐸/FldExt𝐹 → (Base‘𝐹) = (Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))))
7372ad4antr 730 . . . . . . . . . . . . . . . . . . 19 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (Base‘𝐹) = (Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))))
7469, 73eleqtrrd 2835 . . . . . . . . . . . . . . . . . 18 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝑣𝑥) ∈ (Base‘𝐹))
7564, 74sseldd 3979 . . . . . . . . . . . . . . . . 17 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝑣𝑥) ∈ (Base‘𝐸))
76 simpr 485 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → 𝑏 = {𝑥})
77 simplr 767 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
78 eqid 2731 . . . . . . . . . . . . . . . . . . . . . . 23 (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹)))
7978, 5lbsss 20637 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))) → 𝑏 ⊆ (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
8077, 79syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → 𝑏 ⊆ (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
8176, 80eqsstrrd 4017 . . . . . . . . . . . . . . . . . . . 20 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → {𝑥} ⊆ (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
8259snss 4782 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹))) ↔ {𝑥} ⊆ (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
8381, 82sylibr 233 . . . . . . . . . . . . . . . . . . 19 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → 𝑥 ∈ (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
84 eqidd 2732 . . . . . . . . . . . . . . . . . . . 20 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → ((subringAlg ‘𝐸)‘(Base‘𝐹)) = ((subringAlg ‘𝐸)‘(Base‘𝐹)))
8584, 63srabase 20741 . . . . . . . . . . . . . . . . . . 19 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (Base‘𝐸) = (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
8683, 85eleqtrrd 2835 . . . . . . . . . . . . . . . . . 18 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → 𝑥 ∈ (Base‘𝐸))
8786adantr 481 . . . . . . . . . . . . . . . . 17 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝑥 ∈ (Base‘𝐸))
88 eqid 2731 . . . . . . . . . . . . . . . . . 18 (.r𝐸) = (.r𝐸)
8927, 88ringcl 20031 . . . . . . . . . . . . . . . . 17 ((𝐸 ∈ Ring ∧ (𝑣𝑥) ∈ (Base‘𝐸) ∧ 𝑥 ∈ (Base‘𝐸)) → ((𝑣𝑥)(.r𝐸)𝑥) ∈ (Base‘𝐸))
9062, 75, 87, 89syl3anc 1371 . . . . . . . . . . . . . . . 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 6882 . . . . . . . . . . . . . . . . 17 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ 𝑖 = 𝑥) → (𝑣𝑖) = (𝑣𝑥))
9392, 91oveq12d 7411 . . . . . . . . . . . . . . . 16 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ 𝑖 = 𝑥) → ((𝑣𝑖)(.r𝐸)𝑖) = ((𝑣𝑥)(.r𝐸)𝑥))
9427, 58, 60, 90, 93gsumsnd 19779 . . . . . . . . . . . . . . 15 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝐸 Σg (𝑖 ∈ {𝑥} ↦ ((𝑣𝑖)(.r𝐸)𝑖))) = ((𝑣𝑥)(.r𝐸)𝑥))
951fveq2d 6882 . . . . . . . . . . . . . . . . . 18 (𝐸/FldExt𝐹 → (.r𝐹) = (.r‘(𝐸s (Base‘𝐹))))
9643, 88ressmulr 17234 . . . . . . . . . . . . . . . . . . 19 ((Base‘𝐹) ∈ (SubRing‘𝐸) → (.r𝐸) = (.r‘(𝐸s (Base‘𝐹))))
9726, 96syl 17 . . . . . . . . . . . . . . . . . 18 (𝐸/FldExt𝐹 → (.r𝐸) = (.r‘(𝐸s (Base‘𝐹))))
9895, 97eqtr4d 2774 . . . . . . . . . . . . . . . . 17 (𝐸/FldExt𝐹 → (.r𝐹) = (.r𝐸))
9998ad4antr 730 . . . . . . . . . . . . . . . 16 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (.r𝐹) = (.r𝐸))
10099oveqd 7410 . . . . . . . . . . . . . . 15 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → ((𝑣𝑥)(.r𝐹)𝑥) = ((𝑣𝑥)(.r𝐸)𝑥))
10194, 100eqtr4d 2774 . . . . . . . . . . . . . 14 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝐸 Σg (𝑖 ∈ {𝑥} ↦ ((𝑣𝑖)(.r𝐸)𝑖))) = ((𝑣𝑥)(.r𝐹)𝑥))
10235, 53, 1013eqtr3d 2779 . . . . . . . . . . . . 13 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) = ((𝑣𝑥)(.r𝐹)𝑥))
103102adantlr 713 . . . . . . . . . . . 12 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) = ((𝑣𝑥)(.r𝐹)𝑥))
104 drngring 20272 . . . . . . . . . . . . . . 15 (𝐹 ∈ DivRing → 𝐹 ∈ Ring)
10544, 46, 1043syl 18 . . . . . . . . . . . . . 14 (𝐸/FldExt𝐹𝐹 ∈ Ring)
106105ad5antr 732 . . . . . . . . . . . . 13 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝐹 ∈ Ring)
10774adantlr 713 . . . . . . . . . . . . 13 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (𝑣𝑥) ∈ (Base‘𝐹))
108 eqid 2731 . . . . . . . . . . . . . . . . . . . 20 (1r𝐸) = (1r𝐸)
109 eqid 2731 . . . . . . . . . . . . . . . . . . . 20 (Unit‘𝐸) = (Unit‘𝐸)
110 eqid 2731 . . . . . . . . . . . . . . . . . . . 20 (invr𝐸) = (invr𝐸)
111 simp-5l 783 . . . . . . . . . . . . . . . . . . . . 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 20032 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐸 ∈ CRing ∧ 𝑥 ∈ (Base‘𝐸) ∧ (𝑣𝑥) ∈ (Base‘𝐸)) → (𝑥(.r𝐸)(𝑣𝑥)) = ((𝑣𝑥)(.r𝐸)𝑥))
118116, 113, 114, 117syl3anc 1371 . . . . . . . . . . . . . . . . . . . . 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 728 . . . . . . . . . . . . . . . . . . . . . . 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 7409 . . . . . . . . . . . . . . . . . . . . . . 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 2777 . . . . . . . . . . . . . . . . . . . . . 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 2771 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (1r𝐸) = ((𝑣𝑥)(.r𝐸)𝑥))
126118, 125eqtr4d 2774 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → (𝑥(.r𝐸)(𝑣𝑥)) = (1r𝐸))
127125eqcomd 2737 . . . . . . . . . . . . . . . . . . . 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 22107 . . . . . . . . . . . . . . . . . . 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 20157 . . . . . . . . . . . . . . . . . 18 ((𝐸 ∈ Ring ∧ 𝑥 ∈ (Unit‘𝐸)) → ((invr𝐸)‘((invr𝐸)‘𝑥)) = 𝑥)
13162, 129, 130syl2an2r 683 . . . . . . . . . . . . . . . . 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 2833 . . . . . . . . . . . . . . . . . 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 2832 . . . . . . . . . . . . . . . . . . 19 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → ((invr𝐸)‘𝑥) ∈ (Base‘𝐹))
140 eqidd 2732 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐸/FldExt𝐹 → (0g𝐸) = (0g𝐸))
14124, 140, 29sralmod0 20758 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐸/FldExt𝐹 → (0g𝐸) = (0g‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
142141ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) → (0g𝐸) = (0g‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
1435lbslinds 21321 . . . . . . . . . . . . . . . . . . . . . . . . 25 (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹))) ⊆ (LIndS‘((subringAlg ‘𝐸)‘(Base‘𝐹)))
144143, 10sselid 3976 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) → 𝑏 ∈ (LIndS‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
145 eqid 2731 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0g‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = (0g‘((subringAlg ‘𝐸)‘(Base‘𝐹)))
1461450nellinds 32345 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LVec ∧ 𝑏 ∈ (LIndS‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) → ¬ (0g‘((subringAlg ‘𝐸)‘(Base‘𝐹))) ∈ 𝑏)
1474, 144, 146syl2an2r 683 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) → ¬ (0g‘((subringAlg ‘𝐸)‘(Base‘𝐹))) ∈ 𝑏)
148142, 147eqneltrd 2852 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) → ¬ (0g𝐸) ∈ 𝑏)
149148ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → ¬ (0g𝐸) ∈ 𝑏)
150 nelne2 3039 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝑏 ∧ ¬ (0g𝐸) ∈ 𝑏) → 𝑥 ≠ (0g𝐸))
15168, 149, 150syl2an2r 683 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝑥 ≠ (0g𝐸))
152 eqid 2731 . . . . . . . . . . . . . . . . . . . . 21 (0g𝐸) = (0g𝐸)
15327, 152, 110drnginvrn0 20287 . . . . . . . . . . . . . . . . . . . 20 ((𝐸 ∈ DivRing ∧ 𝑥 ∈ (Base‘𝐸) ∧ 𝑥 ≠ (0g𝐸)) → ((invr𝐸)‘𝑥) ≠ (0g𝐸))
154132, 113, 151, 153syl3anc 1371 . . . . . . . . . . . . . . . . . . 19 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → ((invr𝐸)‘𝑥) ≠ (0g𝐸))
155 eldifsn 4783 . . . . . . . . . . . . . . . . . . 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 6878 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = ((invr𝐸)‘𝑥) → ((invr𝐸)‘𝑎) = ((invr𝐸)‘((invr𝐸)‘𝑥)))
158157eleq1d 2817 . . . . . . . . . . . . . . . . . . 19 (𝑎 = ((invr𝐸)‘𝑥) → (((invr𝐸)‘𝑎) ∈ (Base‘𝐹) ↔ ((invr𝐸)‘((invr𝐸)‘𝑥)) ∈ (Base‘𝐹)))
15943, 152, 110issubdrg 20338 . . . . . . . . . . . . . . . . . . . . 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 3610 . . . . . . . . . . . . . . . . . 18 ((((𝐸 ∈ DivRing ∧ (Base‘𝐹) ∈ (SubRing‘𝐸)) ∧ (𝐸s (Base‘𝐹)) ∈ DivRing) ∧ ((invr𝐸)‘𝑥) ∈ ((Base‘𝐹) ∖ {(0g𝐸)})) → ((invr𝐸)‘((invr𝐸)‘𝑥)) ∈ (Base‘𝐹))
164132, 133, 136, 156, 163syl1111anc 838 . . . . . . . . . . . . . . . . 17 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → ((invr𝐸)‘((invr𝐸)‘𝑥)) ∈ (Base‘𝐹))
165131, 164eqeltrrd 2833 . . . . . . . . . . . . . . . 16 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) ∧ (1r𝐸) = (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖)))) → 𝑥 ∈ (Base‘𝐹))
166165adantrl 714 . . . . . . . . . . . . . . 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 20040 . . . . . . . . . . . . . . . . . 18 (𝐸 ∈ Ring → (1r𝐸) ∈ (Base‘𝐸))
16861, 167syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (1r𝐸) ∈ (Base‘𝐸))
169168, 85eleqtrd 2834 . . . . . . . . . . . . . . . 16 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (1r𝐸) ∈ (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
170 eqid 2731 . . . . . . . . . . . . . . . . 17 (Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) = (Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
171 eqid 2731 . . . . . . . . . . . . . . . . 17 (Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = (Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))
172 eqid 2731 . . . . . . . . . . . . . . . . 17 (0g‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) = (0g‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹))))
173 eqid 2731 . . . . . . . . . . . . . . . . 17 ( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹))) = ( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))
1744ad2antrr 724 . . . . . . . . . . . . . . . . . 18 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → ((subringAlg ‘𝐸)‘(Base‘𝐹)) ∈ LVec)
175 lveclmod 20666 . . . . . . . . . . . . . . . . . 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 32351 . . . . . . . . . . . . . . . 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 3161 . . . . . . . . . . . . . 14 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → 𝑥 ∈ (Base‘𝐹))
180179ad2antrr 724 . . . . . . . . . . . . 13 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → 𝑥 ∈ (Base‘𝐹))
181 eqid 2731 . . . . . . . . . . . . . 14 (.r𝐹) = (.r𝐹)
18225, 181ringcl 20031 . . . . . . . . . . . . 13 ((𝐹 ∈ Ring ∧ (𝑣𝑥) ∈ (Base‘𝐹) ∧ 𝑥 ∈ (Base‘𝐹)) → ((𝑣𝑥)(.r𝐹)𝑥) ∈ (Base‘𝐹))
183106, 107, 180, 182syl3anc 1371 . . . . . . . . . . . 12 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → ((𝑣𝑥)(.r𝐹)𝑥) ∈ (Base‘𝐹))
184103, 183eqeltrd 2832 . . . . . . . . . . 11 ((((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) ∧ 𝑣 ∈ ((Base‘(Scalar‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ↑m 𝑏)) → (((subringAlg ‘𝐸)‘(Base‘𝐹)) Σg (𝑖𝑏 ↦ ((𝑣𝑖)( ·𝑠 ‘((subringAlg ‘𝐸)‘(Base‘𝐹)))𝑖))) ∈ (Base‘𝐹))
185184ad2antrr 724 . . . . . . . . . 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 2832 . . . . . . . . 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 2818 . . . . . . . . . 10 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (𝑢 ∈ (Base‘𝐸) ↔ 𝑢 ∈ (Base‘((subringAlg ‘𝐸)‘(Base‘𝐹)))))
18978, 170, 171, 172, 173, 176, 77lbslsp 32351 . . . . . . . . . 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 3161 . . . . . . 7 (((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) ∧ 𝑢 ∈ (Base‘𝐸)) → 𝑢 ∈ (Base‘𝐹))
193192ex 413 . . . . . 6 ((((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ 𝑏 ∈ (LBasis‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) ∧ 𝑏 = {𝑥}) → (𝑢 ∈ (Base‘𝐸) → 𝑢 ∈ (Base‘𝐹)))
194193ssrdv 3984 . . . . 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 724 . . . 4 (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ (Base‘𝐸) ⊆ (Base‘𝐹)) → 𝐸 ∈ Field)
199 fvexd 6893 . . . 4 (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ (Base‘𝐸) ⊆ (Base‘𝐹)) → (Base‘𝐹) ∈ V)
20043, 27ressid2 17159 . . . 4 (((Base‘𝐸) ⊆ (Base‘𝐹) ∧ 𝐸 ∈ Field ∧ (Base‘𝐹) ∈ V) → (𝐸s (Base‘𝐹)) = 𝐸)
201197, 198, 199, 200syl3anc 1371 . . 3 (((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) ∧ (Base‘𝐸) ⊆ (Base‘𝐹)) → (𝐸s (Base‘𝐹)) = 𝐸)
202196, 201mpdan 685 . 2 ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → (𝐸s (Base‘𝐹)) = 𝐸)
2032, 202eqtr2d 2772 1 ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → 𝐸 = 𝐹)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396   = wceq 1541  wex 1781  wcel 2106  wne 2939  wral 3060  wrex 3069  Vcvv 3473  cdif 3941  wss 3944  c0 4318  {csn 4622   class class class wbr 5141  cmpt 5224  wf 6528  cfv 6532  (class class class)co 7393  m cmap 8803   finSupp cfsupp 9344  1c1 11093  chash 14272  Basecbs 17126  s cress 17155  .rcmulr 17180  Scalarcsca 17182   ·𝑠 cvsca 17183  0gc0g 17367   Σg cgsu 17368  Mndcmnd 18602  1rcur 19963  Ringcrg 20014  CRingccrg 20015  Unitcui 20121  invrcinvr 20153  DivRingcdr 20265  Fieldcfield 20266  SubRingcsubrg 20308  LModclmod 20420  LBasisclbs 20634  LVecclvec 20662  subringAlg csra 20730  LIndSclinds 21293  dimcldim 32523  /FldExtcfldext 32555  [:]cextdg 32558
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  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 2702  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7708  ax-reg 9569  ax-inf2 9618  ax-ac2 10440  ax-cnex 11148  ax-resscn 11149  ax-1cn 11150  ax-icn 11151  ax-addcl 11152  ax-addrcl 11153  ax-mulcl 11154  ax-mulrcl 11155  ax-mulcom 11156  ax-addass 11157  ax-mulass 11158  ax-distr 11159  ax-i2m1 11160  ax-1ne0 11161  ax-1rid 11162  ax-rnegex 11163  ax-rrecex 11164  ax-cnre 11165  ax-pre-lttri 11166  ax-pre-lttrn 11167  ax-pre-ltadd 11168  ax-pre-mulgt0 11169
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-tp 4627  df-op 4629  df-uni 4902  df-int 4944  df-iun 4992  df-iin 4993  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6289  df-ord 6356  df-on 6357  df-lim 6358  df-suc 6359  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539  df-fv 6540  df-isom 6541  df-riota 7349  df-ov 7396  df-oprab 7397  df-mpo 7398  df-of 7653  df-rpss 7696  df-om 7839  df-1st 7957  df-2nd 7958  df-supp 8129  df-tpos 8193  df-frecs 8248  df-wrecs 8279  df-recs 8353  df-rdg 8392  df-1o 8448  df-oadd 8452  df-er 8686  df-map 8805  df-ixp 8875  df-en 8923  df-dom 8924  df-sdom 8925  df-fin 8926  df-fsupp 9345  df-sup 9419  df-oi 9487  df-r1 9741  df-rank 9742  df-dju 9878  df-card 9916  df-acn 9919  df-ac 10093  df-pnf 11232  df-mnf 11233  df-xr 11234  df-ltxr 11235  df-le 11236  df-sub 11428  df-neg 11429  df-nn 12195  df-2 12257  df-3 12258  df-4 12259  df-5 12260  df-6 12261  df-7 12262  df-8 12263  df-9 12264  df-n0 12455  df-xnn0 12527  df-z 12541  df-dec 12660  df-uz 12805  df-fz 13467  df-fzo 13610  df-seq 13949  df-hash 14273  df-struct 17062  df-sets 17079  df-slot 17097  df-ndx 17109  df-base 17127  df-ress 17156  df-plusg 17192  df-mulr 17193  df-sca 17195  df-vsca 17196  df-ip 17197  df-tset 17198  df-ple 17199  df-ocomp 17200  df-ds 17201  df-hom 17203  df-cco 17204  df-0g 17369  df-gsum 17370  df-prds 17375  df-pws 17377  df-mre 17512  df-mrc 17513  df-mri 17514  df-acs 17515  df-proset 18230  df-drs 18231  df-poset 18248  df-ipo 18463  df-mgm 18543  df-sgrp 18592  df-mnd 18603  df-mhm 18647  df-submnd 18648  df-grp 18797  df-minusg 18798  df-sbg 18799  df-mulg 18923  df-subg 18975  df-ghm 19056  df-cntz 19147  df-cmn 19614  df-abl 19615  df-mgp 19947  df-ur 19964  df-ring 20016  df-cring 20017  df-oppr 20102  df-dvdsr 20123  df-unit 20124  df-invr 20154  df-nzr 20242  df-drng 20267  df-field 20268  df-subrg 20310  df-lmod 20422  df-lss 20492  df-lsp 20532  df-lmhm 20582  df-lbs 20635  df-lvec 20663  df-sra 20734  df-rgmod 20735  df-dsmm 21220  df-frlm 21235  df-uvc 21271  df-lindf 21294  df-linds 21295  df-dim 32524  df-fldext 32559  df-extdg 32560
This theorem is referenced by:  extdg1b  32581
  Copyright terms: Public domain W3C validator