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 = ( algSc ` W )
	rnasclassa.u	|- U = ( W |`s ran A )
	rnasclassa.w	|- ( ph -> W e. AssAlg )
Assertion	rnasclassa	|- ( ph -> U e. AssAlg )

Proof

Step	Hyp	Ref	Expression
1		rnasclassa.a	|- A = ( algSc ` W )
2		rnasclassa.u	|- U = ( W |`s ran A )
3		rnasclassa.w	|- ( ph -> W e. AssAlg )
4		ssidd	|- ( ph -> ran A C_ ran A )
5	1 3	rnasclsubrg	|- ( ph -> ran A e. ( SubRing ` W ) )
6		eqid	|- ( LSubSp ` W ) = ( LSubSp ` W )
7	1 6	issubassa2	|- ( ( W e. AssAlg /\ ran A e. ( SubRing ` W ) ) -> ( ran A e. ( LSubSp ` W ) <-> ran A C_ ran A ) )
8	2 6	issubassa3	|- ( ( W e. AssAlg /\ ( ran A e. ( SubRing ` W ) /\ ran A e. ( LSubSp ` W ) ) ) -> U e. AssAlg )
9	8	expr	|- ( ( W e. AssAlg /\ ran A e. ( SubRing ` W ) ) -> ( ran A e. ( LSubSp ` W ) -> U e. AssAlg ) )
10	7 9	sylbird	|- ( ( W e. AssAlg /\ ran A e. ( SubRing ` W ) ) -> ( ran A C_ ran A -> U e. AssAlg ) )
11	3 5 10	syl2anc	|- ( ph -> ( ran A C_ ran A -> U e. AssAlg ) )
12	4 11	mpd	|- ( ph -> U e. AssAlg )