This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sralvec

Description: Given a sub division ring F of a division ring E , E may be considered as a vector space over F , which becomes the field of scalars. (Contributed by Thierry Arnoux, 24-May-2023)

Ref Expression
Hypotheses sralvec.a ⊢ 𝐴 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 )
sralvec.f ⊢ 𝐹 = ( 𝐸 ↾s 𝑈 )
Assertion sralvec ( ( 𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ ( SubRing ‘ 𝐸 ) ) → 𝐴 ∈ LVec )

Proof

Step Hyp Ref Expression
1 sralvec.a ⊢ 𝐴 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 )
2 sralvec.f ⊢ 𝐹 = ( 𝐸 ↾s 𝑈 )
3 eqid ⊢ ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 ) = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 )
4 3 sralmod ⊢ ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) → ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 ) ∈ LMod )
5 4 3ad2ant3 ⊢ ( ( 𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ ( SubRing ‘ 𝐸 ) ) → ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 ) ∈ LMod )
6 1 5 eqeltrid ⊢ ( ( 𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ ( SubRing ‘ 𝐸 ) ) → 𝐴 ∈ LMod )
7 1 a1i ⊢ ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) → 𝐴 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 ) )
8 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
9 8 subrgss ⊢ ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) → 𝑈 ⊆ ( Base ‘ 𝐸 ) )
10 7 9 srasca ⊢ ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) → ( 𝐸 ↾s 𝑈 ) = ( Scalar ‘ 𝐴 ) )
11 2 10 eqtrid ⊢ ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) → 𝐹 = ( Scalar ‘ 𝐴 ) )
12 11 3ad2ant3 ⊢ ( ( 𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ ( SubRing ‘ 𝐸 ) ) → 𝐹 = ( Scalar ‘ 𝐴 ) )
13 simp2 ⊢ ( ( 𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ ( SubRing ‘ 𝐸 ) ) → 𝐹 ∈ DivRing )
14 12 13 eqeltrrd ⊢ ( ( 𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ ( SubRing ‘ 𝐸 ) ) → ( Scalar ‘ 𝐴 ) ∈ DivRing )
15 eqid ⊢ ( Scalar ‘ 𝐴 ) = ( Scalar ‘ 𝐴 )
16 15 islvec ⊢ ( 𝐴 ∈ LVec ↔ ( 𝐴 ∈ LMod ∧ ( Scalar ‘ 𝐴 ) ∈ DivRing ) )
17 6 14 16 sylanbrc ⊢ ( ( 𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ ( SubRing ‘ 𝐸 ) ) → 𝐴 ∈ LVec )