Metamath Proof Explorer


Theorem scmatel

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

Ref Expression
Hypotheses scmatval.k 𝐾 = ( Base ‘ 𝑅 )
scmatval.a 𝐴 = ( 𝑁 Mat 𝑅 )
scmatval.b 𝐵 = ( Base ‘ 𝐴 )
scmatval.1 1 = ( 1r𝐴 )
scmatval.t · = ( ·𝑠𝐴 )
scmatval.s 𝑆 = ( 𝑁 ScMat 𝑅 )
Assertion scmatel ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → ( 𝑀𝑆 ↔ ( 𝑀𝐵 ∧ ∃ 𝑐𝐾 𝑀 = ( 𝑐 · 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 scmatval.k 𝐾 = ( Base ‘ 𝑅 )
2 scmatval.a 𝐴 = ( 𝑁 Mat 𝑅 )
3 scmatval.b 𝐵 = ( Base ‘ 𝐴 )
4 scmatval.1 1 = ( 1r𝐴 )
5 scmatval.t · = ( ·𝑠𝐴 )
6 scmatval.s 𝑆 = ( 𝑁 ScMat 𝑅 )
7 1 2 3 4 5 6 scmatval ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → 𝑆 = { 𝑚𝐵 ∣ ∃ 𝑐𝐾 𝑚 = ( 𝑐 · 1 ) } )
8 7 eleq2d ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → ( 𝑀𝑆𝑀 ∈ { 𝑚𝐵 ∣ ∃ 𝑐𝐾 𝑚 = ( 𝑐 · 1 ) } ) )
9 eqeq1 ( 𝑚 = 𝑀 → ( 𝑚 = ( 𝑐 · 1 ) ↔ 𝑀 = ( 𝑐 · 1 ) ) )
10 9 rexbidv ( 𝑚 = 𝑀 → ( ∃ 𝑐𝐾 𝑚 = ( 𝑐 · 1 ) ↔ ∃ 𝑐𝐾 𝑀 = ( 𝑐 · 1 ) ) )
11 10 elrab ( 𝑀 ∈ { 𝑚𝐵 ∣ ∃ 𝑐𝐾 𝑚 = ( 𝑐 · 1 ) } ↔ ( 𝑀𝐵 ∧ ∃ 𝑐𝐾 𝑀 = ( 𝑐 · 1 ) ) )
12 8 11 bitrdi ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → ( 𝑀𝑆 ↔ ( 𝑀𝐵 ∧ ∃ 𝑐𝐾 𝑀 = ( 𝑐 · 1 ) ) ) )