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