Metamath Proof Explorer


Theorem dmatel

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

Ref Expression
Hypotheses dmatval.a 𝐴 = ( 𝑁 Mat 𝑅 )
dmatval.b 𝐵 = ( Base ‘ 𝐴 )
dmatval.0 0 = ( 0g𝑅 )
dmatval.d 𝐷 = ( 𝑁 DMat 𝑅 )
Assertion dmatel ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → ( 𝑀𝐷 ↔ ( 𝑀𝐵 ∧ ∀ 𝑖𝑁𝑗𝑁 ( 𝑖𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ) )

Proof

Step Hyp Ref Expression
1 dmatval.a 𝐴 = ( 𝑁 Mat 𝑅 )
2 dmatval.b 𝐵 = ( Base ‘ 𝐴 )
3 dmatval.0 0 = ( 0g𝑅 )
4 dmatval.d 𝐷 = ( 𝑁 DMat 𝑅 )
5 1 2 3 4 dmatval ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → 𝐷 = { 𝑚𝐵 ∣ ∀ 𝑖𝑁𝑗𝑁 ( 𝑖𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) } )
6 5 eleq2d ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → ( 𝑀𝐷𝑀 ∈ { 𝑚𝐵 ∣ ∀ 𝑖𝑁𝑗𝑁 ( 𝑖𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) } ) )
7 oveq ( 𝑚 = 𝑀 → ( 𝑖 𝑚 𝑗 ) = ( 𝑖 𝑀 𝑗 ) )
8 7 eqeq1d ( 𝑚 = 𝑀 → ( ( 𝑖 𝑚 𝑗 ) = 0 ↔ ( 𝑖 𝑀 𝑗 ) = 0 ) )
9 8 imbi2d ( 𝑚 = 𝑀 → ( ( 𝑖𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) ↔ ( 𝑖𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) )
10 9 2ralbidv ( 𝑚 = 𝑀 → ( ∀ 𝑖𝑁𝑗𝑁 ( 𝑖𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) ↔ ∀ 𝑖𝑁𝑗𝑁 ( 𝑖𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) )
11 10 elrab ( 𝑀 ∈ { 𝑚𝐵 ∣ ∀ 𝑖𝑁𝑗𝑁 ( 𝑖𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) } ↔ ( 𝑀𝐵 ∧ ∀ 𝑖𝑁𝑗𝑁 ( 𝑖𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) )
12 6 11 bitrdi ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → ( 𝑀𝐷 ↔ ( 𝑀𝐵 ∧ ∀ 𝑖𝑁𝑗𝑁 ( 𝑖𝑗 → ( 𝑖 𝑀 𝑗 ) = 0 ) ) ) )