This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 = ( 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 )