# Metamath Proof Explorer

## Theorem rnasclassa

Description: The scalar multiples of the unit vector form a subalgebra of the vectors. (Contributed by SN, 16-Nov-2023)

Ref Expression
Hypotheses rnasclassa.a ${⊢}{A}=\mathrm{algSc}\left({W}\right)$
rnasclassa.u ${⊢}{U}={W}{↾}_{𝑠}\mathrm{ran}{A}$
rnasclassa.w ${⊢}{\phi }\to {W}\in \mathrm{AssAlg}$
Assertion rnasclassa ${⊢}{\phi }\to {U}\in \mathrm{AssAlg}$

### Proof

Step Hyp Ref Expression
1 rnasclassa.a ${⊢}{A}=\mathrm{algSc}\left({W}\right)$
2 rnasclassa.u ${⊢}{U}={W}{↾}_{𝑠}\mathrm{ran}{A}$
3 rnasclassa.w ${⊢}{\phi }\to {W}\in \mathrm{AssAlg}$
4 ssidd ${⊢}{\phi }\to \mathrm{ran}{A}\subseteq \mathrm{ran}{A}$
5 1 3 rnasclsubrg ${⊢}{\phi }\to \mathrm{ran}{A}\in \mathrm{SubRing}\left({W}\right)$
6 eqid ${⊢}\mathrm{LSubSp}\left({W}\right)=\mathrm{LSubSp}\left({W}\right)$
7 1 6 issubassa2 ${⊢}\left({W}\in \mathrm{AssAlg}\wedge \mathrm{ran}{A}\in \mathrm{SubRing}\left({W}\right)\right)\to \left(\mathrm{ran}{A}\in \mathrm{LSubSp}\left({W}\right)↔\mathrm{ran}{A}\subseteq \mathrm{ran}{A}\right)$
8 2 6 issubassa3 ${⊢}\left({W}\in \mathrm{AssAlg}\wedge \left(\mathrm{ran}{A}\in \mathrm{SubRing}\left({W}\right)\wedge \mathrm{ran}{A}\in \mathrm{LSubSp}\left({W}\right)\right)\right)\to {U}\in \mathrm{AssAlg}$
9 8 expr ${⊢}\left({W}\in \mathrm{AssAlg}\wedge \mathrm{ran}{A}\in \mathrm{SubRing}\left({W}\right)\right)\to \left(\mathrm{ran}{A}\in \mathrm{LSubSp}\left({W}\right)\to {U}\in \mathrm{AssAlg}\right)$
10 7 9 sylbird ${⊢}\left({W}\in \mathrm{AssAlg}\wedge \mathrm{ran}{A}\in \mathrm{SubRing}\left({W}\right)\right)\to \left(\mathrm{ran}{A}\subseteq \mathrm{ran}{A}\to {U}\in \mathrm{AssAlg}\right)$
11 3 5 10 syl2anc ${⊢}{\phi }\to \left(\mathrm{ran}{A}\subseteq \mathrm{ran}{A}\to {U}\in \mathrm{AssAlg}\right)$
12 4 11 mpd ${⊢}{\phi }\to {U}\in \mathrm{AssAlg}$