rnasclassa

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

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

Metamath Proof Explorer