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