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	⊢ 𝐴 = ( algSc ‘ 𝑊 )
	rnasclassa.u	⊢ 𝑈 = ( 𝑊 ↾s ran 𝐴 )
	rnasclassa.w	⊢ ( 𝜑 → 𝑊 ∈ AssAlg )
Assertion	rnasclassa	⊢ ( 𝜑 → 𝑈 ∈ AssAlg )

Proof

Step	Hyp	Ref	Expression
1		rnasclassa.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
2		rnasclassa.u	⊢ 𝑈 = ( 𝑊 ↾s ran 𝐴 )
3		rnasclassa.w	⊢ ( 𝜑 → 𝑊 ∈ AssAlg )
4		ssidd	⊢ ( 𝜑 → ran 𝐴 ⊆ ran 𝐴 )
5	1 3	rnasclsubrg	⊢ ( 𝜑 → ran 𝐴 ∈ ( SubRing ‘ 𝑊 ) )
6		eqid	⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
7	1 6	issubassa2	⊢ ( ( 𝑊 ∈ AssAlg ∧ ran 𝐴 ∈ ( SubRing ‘ 𝑊 ) ) → ( ran 𝐴 ∈ ( LSubSp ‘ 𝑊 ) ↔ ran 𝐴 ⊆ ran 𝐴 ) )
8	2 6	issubassa3	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( ran 𝐴 ∈ ( SubRing ‘ 𝑊 ) ∧ ran 𝐴 ∈ ( LSubSp ‘ 𝑊 ) ) ) → 𝑈 ∈ AssAlg )
9	8	expr	⊢ ( ( 𝑊 ∈ AssAlg ∧ ran 𝐴 ∈ ( SubRing ‘ 𝑊 ) ) → ( ran 𝐴 ∈ ( LSubSp ‘ 𝑊 ) → 𝑈 ∈ AssAlg ) )
10	7 9	sylbird	⊢ ( ( 𝑊 ∈ AssAlg ∧ ran 𝐴 ∈ ( SubRing ‘ 𝑊 ) ) → ( ran 𝐴 ⊆ ran 𝐴 → 𝑈 ∈ AssAlg ) )
11	3 5 10	syl2anc	⊢ ( 𝜑 → ( ran 𝐴 ⊆ ran 𝐴 → 𝑈 ∈ AssAlg ) )
12	4 11	mpd	⊢ ( 𝜑 → 𝑈 ∈ AssAlg )