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 )