Metamath Proof Explorer


Theorem drgextvsca

Description: The scalar multiplication operation of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023)

Ref Expression
Hypotheses drgext.b 𝐵 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 )
drgext.1 ( 𝜑𝐸 ∈ DivRing )
drgext.2 ( 𝜑𝑈 ∈ ( SubRing ‘ 𝐸 ) )
Assertion drgextvsca ( 𝜑 → ( .r𝐸 ) = ( ·𝑠𝐵 ) )

Proof

Step Hyp Ref Expression
1 drgext.b 𝐵 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 )
2 drgext.1 ( 𝜑𝐸 ∈ DivRing )
3 drgext.2 ( 𝜑𝑈 ∈ ( SubRing ‘ 𝐸 ) )
4 1 a1i ( 𝜑𝐵 = ( ( subringAlg ‘ 𝐸 ) ‘ 𝑈 ) )
5 eqid ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
6 5 subrgss ( 𝑈 ∈ ( SubRing ‘ 𝐸 ) → 𝑈 ⊆ ( Base ‘ 𝐸 ) )
7 3 6 syl ( 𝜑𝑈 ⊆ ( Base ‘ 𝐸 ) )
8 4 7 sravsca ( 𝜑 → ( .r𝐸 ) = ( ·𝑠𝐵 ) )