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

Metamath Proof Explorer

Theorem srafldlvec

Description: Given a subfield F of a field 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 srafldlvec ( ( 𝐸 ∈ Field ∧ 𝐹 ∈ Field ∧ 𝑈 ∈ ( SubRing ‘ 𝐸 ) ) → 𝐴 ∈ LVec )

Proof

Step Hyp Ref Expression
1 sralvec.a ⊢ 𝐴 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 )
2 sralvec.f ⊢ 𝐹 = ( 𝐸 ↾s 𝑈 )
3 isfld ⊢ ( 𝐸 ∈ Field ↔ ( 𝐸 ∈ DivRing ∧ 𝐸 ∈ CRing ) )
4 3 simplbi ⊢ ( 𝐸 ∈ Field → 𝐸 ∈ DivRing )
5 isfld ⊢ ( 𝐹 ∈ Field ↔ ( 𝐹 ∈ DivRing ∧ 𝐹 ∈ CRing ) )
6 5 simplbi ⊢ ( 𝐹 ∈ Field → 𝐹 ∈ DivRing )
7 id ⊢ ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) → 𝑈 ∈ ( SubRing ‘ 𝐸 ) )
8 1 2 sralvec ⊢ ( ( 𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ ( SubRing ‘ 𝐸 ) ) → 𝐴 ∈ LVec )
9 4 6 7 8 syl3an ⊢ ( ( 𝐸 ∈ Field ∧ 𝐹 ∈ Field ∧ 𝑈 ∈ ( SubRing ‘ 𝐸 ) ) → 𝐴 ∈ LVec )