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	syl5eq	⊢ ( 𝑈 ∈ ( 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 )