Theorem mat0scmat

Description: The empty matrix over a ring is a scalar matrix (and therefore, by scmatdmat , also a diagonal matrix). (Contributed by AV, 21-Dec-2019)

	Ref	Expression
Assertion	mat0scmat	⊢ ( 𝑅 ∈ Ring → ∅ ∈ ( ∅ ScMat 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2	1	snid	⊢ ∅ ∈ { ∅ }
3		mat0dimbas0	⊢ ( 𝑅 ∈ Ring → ( Base ‘ ( ∅ Mat 𝑅 ) ) = { ∅ } )
4	2 3	eleqtrrid	⊢ ( 𝑅 ∈ Ring → ∅ ∈ ( Base ‘ ( ∅ Mat 𝑅 ) ) )
5		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
7	5 6	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
8		oveq1	⊢ ( 𝑐 = ( 1r ‘ 𝑅 ) → ( 𝑐 ( ·𝑠 ‘ ( ∅ Mat 𝑅 ) ) ∅ ) = ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ ( ∅ Mat 𝑅 ) ) ∅ ) )
9	8	eqeq2d	⊢ ( 𝑐 = ( 1r ‘ 𝑅 ) → ( ∅ = ( 𝑐 ( ·𝑠 ‘ ( ∅ Mat 𝑅 ) ) ∅ ) ↔ ∅ = ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ ( ∅ Mat 𝑅 ) ) ∅ ) ) )
10	9	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑐 = ( 1r ‘ 𝑅 ) ) → ( ∅ = ( 𝑐 ( ·𝑠 ‘ ( ∅ Mat 𝑅 ) ) ∅ ) ↔ ∅ = ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ ( ∅ Mat 𝑅 ) ) ∅ ) ) )
11		eqid	⊢ ( ∅ Mat 𝑅 ) = ( ∅ Mat 𝑅 )
12	11	mat0dimscm	⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ ( ∅ Mat 𝑅 ) ) ∅ ) = ∅ )
13	7 12	mpdan	⊢ ( 𝑅 ∈ Ring → ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ ( ∅ Mat 𝑅 ) ) ∅ ) = ∅ )
14	13	eqcomd	⊢ ( 𝑅 ∈ Ring → ∅ = ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ ( ∅ Mat 𝑅 ) ) ∅ ) )
15	7 10 14	rspcedvd	⊢ ( 𝑅 ∈ Ring → ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ∅ = ( 𝑐 ( ·𝑠 ‘ ( ∅ Mat 𝑅 ) ) ∅ ) )
16	11	mat0dimid	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ ( ∅ Mat 𝑅 ) ) = ∅ )
17	16	oveq2d	⊢ ( 𝑅 ∈ Ring → ( 𝑐 ( ·𝑠 ‘ ( ∅ Mat 𝑅 ) ) ( 1r ‘ ( ∅ Mat 𝑅 ) ) ) = ( 𝑐 ( ·𝑠 ‘ ( ∅ Mat 𝑅 ) ) ∅ ) )
18	17	eqeq2d	⊢ ( 𝑅 ∈ Ring → ( ∅ = ( 𝑐 ( ·𝑠 ‘ ( ∅ Mat 𝑅 ) ) ( 1r ‘ ( ∅ Mat 𝑅 ) ) ) ↔ ∅ = ( 𝑐 ( ·𝑠 ‘ ( ∅ Mat 𝑅 ) ) ∅ ) ) )
19	18	rexbidv	⊢ ( 𝑅 ∈ Ring → ( ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ∅ = ( 𝑐 ( ·𝑠 ‘ ( ∅ Mat 𝑅 ) ) ( 1r ‘ ( ∅ Mat 𝑅 ) ) ) ↔ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ∅ = ( 𝑐 ( ·𝑠 ‘ ( ∅ Mat 𝑅 ) ) ∅ ) ) )
20	15 19	mpbird	⊢ ( 𝑅 ∈ Ring → ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ∅ = ( 𝑐 ( ·𝑠 ‘ ( ∅ Mat 𝑅 ) ) ( 1r ‘ ( ∅ Mat 𝑅 ) ) ) )
21		0fin	⊢ ∅ ∈ Fin
22		eqid	⊢ ( Base ‘ ( ∅ Mat 𝑅 ) ) = ( Base ‘ ( ∅ Mat 𝑅 ) )
23		eqid	⊢ ( 1r ‘ ( ∅ Mat 𝑅 ) ) = ( 1r ‘ ( ∅ Mat 𝑅 ) )
24		eqid	⊢ ( ·𝑠 ‘ ( ∅ Mat 𝑅 ) ) = ( ·𝑠 ‘ ( ∅ Mat 𝑅 ) )
25		eqid	⊢ ( ∅ ScMat 𝑅 ) = ( ∅ ScMat 𝑅 )
26	5 11 22 23 24 25	scmatel	⊢ ( ( ∅ ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ∅ ∈ ( ∅ ScMat 𝑅 ) ↔ ( ∅ ∈ ( Base ‘ ( ∅ Mat 𝑅 ) ) ∧ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ∅ = ( 𝑐 ( ·𝑠 ‘ ( ∅ Mat 𝑅 ) ) ( 1r ‘ ( ∅ Mat 𝑅 ) ) ) ) ) )
27	21 26	mpan	⊢ ( 𝑅 ∈ Ring → ( ∅ ∈ ( ∅ ScMat 𝑅 ) ↔ ( ∅ ∈ ( Base ‘ ( ∅ Mat 𝑅 ) ) ∧ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ∅ = ( 𝑐 ( ·𝑠 ‘ ( ∅ Mat 𝑅 ) ) ( 1r ‘ ( ∅ Mat 𝑅 ) ) ) ) ) )
28	4 20 27	mpbir2and	⊢ ( 𝑅 ∈ Ring → ∅ ∈ ( ∅ ScMat 𝑅 ) )