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 ‘ 𝐸 ) = ( ·𝑠 ‘ 𝐵 ) ) |
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 ‘ 𝐸 ) = ( ·𝑠 ‘ 𝐵 ) ) |