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

Metamath Proof Explorer

Theorem matvscl

Description: Closure of the scalar multiplication in the matrix ring. ( lmodvscl analog.) (Contributed by AV, 27-Nov-2019)

Ref Expression
Hypotheses matvscl.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
matvscl.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
matvscl.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
matvscl.s ⊢ · = ( ·𝑠 ‘ 𝐴 )
Assertion matvscl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝐶 · 𝑋 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 matvscl.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
2 matvscl.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
3 matvscl.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
4 matvscl.s ⊢ · = ( ·𝑠 ‘ 𝐴 )
5 2 matlmod ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ LMod )
6 5 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) ) → 𝐴 ∈ LMod )
7 2 matsca2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 = ( Scalar ‘ 𝐴 ) )
8 7 fveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
9 1 8 eqtrid ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐾 = ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
10 9 eleq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐶 ∈ 𝐾 ↔ 𝐶 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) )
11 10 biimpd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐶 ∈ 𝐾 → 𝐶 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) )
12 11 adantrd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → 𝐶 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) )
13 12 imp ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) ) → 𝐶 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
14 simprr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
15 eqid ⊢ ( Scalar ‘ 𝐴 ) = ( Scalar ‘ 𝐴 )
16 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝐴 ) ) = ( Base ‘ ( Scalar ‘ 𝐴 ) )
17 3 15 4 16 lmodvscl ⊢ ( ( 𝐴 ∈ LMod ∧ 𝐶 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐶 · 𝑋 ) ∈ 𝐵 )
18 6 13 14 17 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝐶 · 𝑋 ) ∈ 𝐵 )