# Metamath Proof Explorer

## Theorem ressascl

Description: The injection of scalars is invariant between subalgebras and superalgebras. (Contributed by Mario Carneiro, 9-Mar-2015)

Ref Expression
Hypotheses ressascl.a ${⊢}{A}=\mathrm{algSc}\left({W}\right)$
ressascl.x ${⊢}{X}={W}{↾}_{𝑠}{S}$
Assertion ressascl ${⊢}{S}\in \mathrm{SubRing}\left({W}\right)\to {A}=\mathrm{algSc}\left({X}\right)$

### Proof

Step Hyp Ref Expression
1 ressascl.a ${⊢}{A}=\mathrm{algSc}\left({W}\right)$
2 ressascl.x ${⊢}{X}={W}{↾}_{𝑠}{S}$
3 eqid ${⊢}\mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({W}\right)$
4 2 3 resssca ${⊢}{S}\in \mathrm{SubRing}\left({W}\right)\to \mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({X}\right)$
5 4 fveq2d ${⊢}{S}\in \mathrm{SubRing}\left({W}\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}$
6 eqid ${⊢}{\cdot }_{{W}}={\cdot }_{{W}}$
7 2 6 ressvsca ${⊢}{S}\in \mathrm{SubRing}\left({W}\right)\to {\cdot }_{{W}}={\cdot }_{{X}}$
8 eqidd ${⊢}{S}\in \mathrm{SubRing}\left({W}\right)\to {x}={x}$
9 eqid ${⊢}{1}_{{W}}={1}_{{W}}$
10 2 9 subrg1 ${⊢}{S}\in \mathrm{SubRing}\left({W}\right)\to {1}_{{W}}={1}_{{X}}$
11 7 8 10 oveq123d ${⊢}{S}\in \mathrm{SubRing}\left({W}\right)\to {x}{\cdot }_{{W}}{1}_{{W}}={x}{\cdot }_{{X}}{1}_{{X}}$
12 5 11 mpteq12dv ${⊢}{S}\in \mathrm{SubRing}\left({W}\right)\to \left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}⟼{x}{\cdot }_{{W}}{1}_{{W}}\right)=\left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}⟼{x}{\cdot }_{{X}}{1}_{{X}}\right)$
13 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
14 1 3 13 6 9 asclfval ${⊢}{A}=\left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}⟼{x}{\cdot }_{{W}}{1}_{{W}}\right)$
15 eqid ${⊢}\mathrm{algSc}\left({X}\right)=\mathrm{algSc}\left({X}\right)$
16 eqid ${⊢}\mathrm{Scalar}\left({X}\right)=\mathrm{Scalar}\left({X}\right)$
17 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}$
18 eqid ${⊢}{\cdot }_{{X}}={\cdot }_{{X}}$
19 eqid ${⊢}{1}_{{X}}={1}_{{X}}$
20 15 16 17 18 19 asclfval ${⊢}\mathrm{algSc}\left({X}\right)=\left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({X}\right)}⟼{x}{\cdot }_{{X}}{1}_{{X}}\right)$
21 12 14 20 3eqtr4g ${⊢}{S}\in \mathrm{SubRing}\left({W}\right)\to {A}=\mathrm{algSc}\left({X}\right)$