This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mat0op

Description: Value of a zero matrix as operation. (Contributed by AV, 2-Dec-2018)

Ref Expression
Hypotheses mat0op.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
mat0op.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion mat0op ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 0g ‘ 𝐴 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 0 ) )

Proof

Step Hyp Ref Expression
1 mat0op.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 mat0op.z ⊢ 0 = ( 0g ‘ 𝑅 )
3 eqid ⊢ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) = ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) )
4 1 3 mat0 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 0g ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( 0g ‘ 𝐴 ) )
5 fconstmpo ⊢ ( ( 𝑁 × 𝑁 ) × { ( 0g ‘ 𝑅 ) } ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) )
6 simpr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 ∈ Ring )
7 sqxpexg ⊢ ( 𝑁 ∈ Fin → ( 𝑁 × 𝑁 ) ∈ V )
8 7 adantr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑁 × 𝑁 ) ∈ V )
9 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
10 3 9 frlm0 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 × 𝑁 ) ∈ V ) → ( ( 𝑁 × 𝑁 ) × { ( 0g ‘ 𝑅 ) } ) = ( 0g ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) )
11 6 8 10 syl2anc ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑁 × 𝑁 ) × { ( 0g ‘ 𝑅 ) } ) = ( 0g ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) )
12 2 eqcomi ⊢ ( 0g ‘ 𝑅 ) = 0
13 12 a1i ⊢ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 0g ‘ 𝑅 ) = 0 )
14 13 mpoeq3ia ⊢ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 0 )
15 14 a1i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 0 ) )
16 5 11 15 3eqtr3a ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 0g ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 0 ) )
17 4 16 eqtr3d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 0g ‘ 𝐴 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 0 ) )