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

Metamath Proof Explorer

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 ‘ 𝐴 ) ) → ( 𝐼 𝑀 𝐽 ) ∈ 𝐾 )