Theorem scmatmat

Description: An N x N scalar matrix over (the ring) R is an N x N matrix over (the ring) R . (Contributed by AV, 18-Dec-2019)

	Ref	Expression
Hypotheses	scmatmat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	scmatmat.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	scmatmat.s	⊢ 𝑆 = ( 𝑁 ScMat 𝑅 )
Assertion	scmatmat	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( 𝑀 ∈ 𝑆 → 𝑀 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		scmatmat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		scmatmat.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		scmatmat.s	⊢ 𝑆 = ( 𝑁 ScMat 𝑅 )
4		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5		eqid	⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
6		eqid	⊢ ( ·𝑠 ‘ 𝐴 ) = ( ·𝑠 ‘ 𝐴 )
7	4 1 2 5 6 3	scmatel	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( 𝑀 ∈ 𝑆 ↔ ( 𝑀 ∈ 𝐵 ∧ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) 𝑀 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) ) )
8		simpl	⊢ ( ( 𝑀 ∈ 𝐵 ∧ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) 𝑀 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) → 𝑀 ∈ 𝐵 )
9	7 8	biimtrdi	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( 𝑀 ∈ 𝑆 → 𝑀 ∈ 𝐵 ) )