Theorem matecl

Description: Each entry (according to Wikipedia "Matrix (mathematics)", 30-Dec-2018, https://en.wikipedia.org/wiki/Matrix_(mathematics)#Definition (or element or component or coefficient or cell) of a matrix is an element of the underlying ring. (Contributed by AV, 16-Dec-2018)

	Ref	Expression
Hypotheses	matecl.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	matecl.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
Assertion	matecl	⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝑀 ∈ ( Base ‘ 𝐴 ) ) → ( 𝐼 𝑀 𝐽 ) ∈ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		matecl.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		matecl.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
3		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
4	1 3	matrcl	⊢ ( 𝑀 ∈ ( Base ‘ 𝐴 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
5	4	3ad2ant3	⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝑀 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
6	1 2	matbas2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( 𝐾 ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
7	6	eqcomd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( Base ‘ 𝐴 ) = ( 𝐾 ↑m ( 𝑁 × 𝑁 ) ) )
8	7	eleq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( 𝑀 ∈ ( Base ‘ 𝐴 ) ↔ 𝑀 ∈ ( 𝐾 ↑m ( 𝑁 × 𝑁 ) ) ) )
9	2	fvexi	⊢ 𝐾 ∈ V
10	9	a1i	⊢ ( 𝑅 ∈ V → 𝐾 ∈ V )
11		sqxpexg	⊢ ( 𝑁 ∈ Fin → ( 𝑁 × 𝑁 ) ∈ V )
12		elmapg	⊢ ( ( 𝐾 ∈ V ∧ ( 𝑁 × 𝑁 ) ∈ V ) → ( 𝑀 ∈ ( 𝐾 ↑m ( 𝑁 × 𝑁 ) ) ↔ 𝑀 : ( 𝑁 × 𝑁 ) ⟶ 𝐾 ) )
13	10 11 12	syl2anr	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( 𝑀 ∈ ( 𝐾 ↑m ( 𝑁 × 𝑁 ) ) ↔ 𝑀 : ( 𝑁 × 𝑁 ) ⟶ 𝐾 ) )
14		ffnov	⊢ ( 𝑀 : ( 𝑁 × 𝑁 ) ⟶ 𝐾 ↔ ( 𝑀 Fn ( 𝑁 × 𝑁 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) ∈ 𝐾 ) )
15		oveq1	⊢ ( 𝑖 = 𝐼 → ( 𝑖 𝑀 𝑗 ) = ( 𝐼 𝑀 𝑗 ) )
16	15	eleq1d	⊢ ( 𝑖 = 𝐼 → ( ( 𝑖 𝑀 𝑗 ) ∈ 𝐾 ↔ ( 𝐼 𝑀 𝑗 ) ∈ 𝐾 ) )
17		oveq2	⊢ ( 𝑗 = 𝐽 → ( 𝐼 𝑀 𝑗 ) = ( 𝐼 𝑀 𝐽 ) )
18	17	eleq1d	⊢ ( 𝑗 = 𝐽 → ( ( 𝐼 𝑀 𝑗 ) ∈ 𝐾 ↔ ( 𝐼 𝑀 𝐽 ) ∈ 𝐾 ) )
19	16 18	rspc2v	⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) ∈ 𝐾 → ( 𝐼 𝑀 𝐽 ) ∈ 𝐾 ) )
20	19	com12	⊢ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) ∈ 𝐾 → ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ( 𝐼 𝑀 𝐽 ) ∈ 𝐾 ) )
21	20	adantl	⊢ ( ( 𝑀 Fn ( 𝑁 × 𝑁 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) ∈ 𝐾 ) → ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ( 𝐼 𝑀 𝐽 ) ∈ 𝐾 ) )
22	21	a1i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( ( 𝑀 Fn ( 𝑁 × 𝑁 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) ∈ 𝐾 ) → ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ( 𝐼 𝑀 𝐽 ) ∈ 𝐾 ) ) )
23	14 22	biimtrid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( 𝑀 : ( 𝑁 × 𝑁 ) ⟶ 𝐾 → ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ( 𝐼 𝑀 𝐽 ) ∈ 𝐾 ) ) )
24	13 23	sylbid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( 𝑀 ∈ ( 𝐾 ↑m ( 𝑁 × 𝑁 ) ) → ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ( 𝐼 𝑀 𝐽 ) ∈ 𝐾 ) ) )
25	8 24	sylbid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( 𝑀 ∈ ( Base ‘ 𝐴 ) → ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ( 𝐼 𝑀 𝐽 ) ∈ 𝐾 ) ) )
26	25	com13	⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ( 𝑀 ∈ ( Base ‘ 𝐴 ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( 𝐼 𝑀 𝐽 ) ∈ 𝐾 ) ) )
27	26	ex	⊢ ( 𝐼 ∈ 𝑁 → ( 𝐽 ∈ 𝑁 → ( 𝑀 ∈ ( Base ‘ 𝐴 ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( 𝐼 𝑀 𝐽 ) ∈ 𝐾 ) ) ) )
28	27	3imp1	⊢ ( ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝑀 ∈ ( Base ‘ 𝐴 ) ) ∧ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) ) → ( 𝐼 𝑀 𝐽 ) ∈ 𝐾 )
29	5 28	mpdan	⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝑀 ∈ ( Base ‘ 𝐴 ) ) → ( 𝐼 𝑀 𝐽 ) ∈ 𝐾 )