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=algSc⁡W
rnasclassa.u ⊢U=W↾𝑠ran⁡A
rnasclassa.w ⊢φ→W∈AssAlg
Assertion rnasclassa ⊢φ→U∈AssAlg

Proof

Step Hyp Ref Expression
1 rnasclassa.a ⊢A=algSc⁡W
2 rnasclassa.u ⊢U=W↾𝑠ran⁡A
3 rnasclassa.w ⊢φ→W∈AssAlg
4 ssidd ⊢φ→ran⁡A⊆ran⁡A
5 1 3 rnasclsubrg ⊢φ→ran⁡A∈SubRing⁡W
6 eqid ⊢LSubSp⁡W=LSubSp⁡W
7 1 6 issubassa2 ⊢W∈AssAlg∧ran⁡A∈SubRing⁡W→ran⁡A∈LSubSp⁡W↔ran⁡A⊆ran⁡A
8 2 6 issubassa3 ⊢W∈AssAlg∧ran⁡A∈SubRing⁡W∧ran⁡A∈LSubSp⁡W→U∈AssAlg
9 8 expr ⊢W∈AssAlg∧ran⁡A∈SubRing⁡W→ran⁡A∈LSubSp⁡W→U∈AssAlg
10 7 9 sylbird ⊢W∈AssAlg∧ran⁡A∈SubRing⁡W→ran⁡A⊆ran⁡A→U∈AssAlg
11 3 5 10 syl2anc ⊢φ→ran⁡A⊆ran⁡A→U∈AssAlg
12 4 11 mpd ⊢φ→U∈AssAlg