Metamath Proof Explorer

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 𝑅 ) )