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

Metamath Proof Explorer

Theorem matring

Description: Existence of the matrix ring, see also the statement in Lang p. 504: "For a given integer n > 0 the set of square n x n matrices form a ring." (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypothesis matassa.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
Assertion matring ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )

Proof

Step Hyp Ref Expression
1 matassa.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
3 1 2 matbas2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
4 eqidd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( +g ‘ 𝐴 ) = ( +g ‘ 𝐴 ) )
5 eqid ⊢ ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ )
6 1 5 matmulr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( .r ‘ 𝐴 ) )
7 1 matgrp ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Grp )
8 simp1r ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) → 𝑅 ∈ Ring )
9 simp1l ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) → 𝑁 ∈ Fin )
10 simp2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) → 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
11 simp3 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) → 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
12 2 8 5 9 9 9 10 11 mamucl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) → ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑦 ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
13 simplr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → 𝑅 ∈ Ring )
14 simpll ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → 𝑁 ∈ Fin )
15 simpr1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
16 simpr2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
17 simpr3 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
18 2 13 14 14 14 14 15 16 17 5 5 5 5 mamuass ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → ( ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑦 ) ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) = ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ( 𝑦 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ) )
19 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
20 2 13 5 14 14 14 19 15 16 17 mamudir ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ( 𝑦 ∘f ( +g ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑦 ) ∘f ( +g ‘ 𝑅 ) ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ) )
21 3 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
22 16 21 eleqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → 𝑦 ∈ ( Base ‘ 𝐴 ) )
23 17 21 eleqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → 𝑧 ∈ ( Base ‘ 𝐴 ) )
24 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
25 eqid ⊢ ( +g ‘ 𝐴 ) = ( +g ‘ 𝐴 )
26 1 24 25 19 matplusg2 ⊢ ( ( 𝑦 ∈ ( Base ‘ 𝐴 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑦 ( +g ‘ 𝐴 ) 𝑧 ) = ( 𝑦 ∘f ( +g ‘ 𝑅 ) 𝑧 ) )
27 22 23 26 syl2anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → ( 𝑦 ( +g ‘ 𝐴 ) 𝑧 ) = ( 𝑦 ∘f ( +g ‘ 𝑅 ) 𝑧 ) )
28 27 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ( 𝑦 ( +g ‘ 𝐴 ) 𝑧 ) ) = ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ( 𝑦 ∘f ( +g ‘ 𝑅 ) 𝑧 ) ) )
29 2 13 5 14 14 14 15 16 mamucl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑦 ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
30 29 21 eleqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑦 ) ∈ ( Base ‘ 𝐴 ) )
31 2 13 5 14 14 14 15 17 mamucl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
32 31 21 eleqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ∈ ( Base ‘ 𝐴 ) )
33 1 24 25 19 matplusg2 ⊢ ( ( ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑦 ) ∈ ( Base ‘ 𝐴 ) ∧ ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ∈ ( Base ‘ 𝐴 ) ) → ( ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑦 ) ( +g ‘ 𝐴 ) ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ) = ( ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑦 ) ∘f ( +g ‘ 𝑅 ) ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ) )
34 30 32 33 syl2anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → ( ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑦 ) ( +g ‘ 𝐴 ) ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ) = ( ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑦 ) ∘f ( +g ‘ 𝑅 ) ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ) )
35 20 28 34 3eqtr4d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ( 𝑦 ( +g ‘ 𝐴 ) 𝑧 ) ) = ( ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑦 ) ( +g ‘ 𝐴 ) ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ) )
36 2 13 5 14 14 14 19 15 16 17 mamudi ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → ( ( 𝑥 ∘f ( +g ‘ 𝑅 ) 𝑦 ) ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) = ( ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ∘f ( +g ‘ 𝑅 ) ( 𝑦 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ) )
37 15 21 eleqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → 𝑥 ∈ ( Base ‘ 𝐴 ) )
38 1 24 25 19 matplusg2 ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) = ( 𝑥 ∘f ( +g ‘ 𝑅 ) 𝑦 ) )
39 37 22 38 syl2anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) = ( 𝑥 ∘f ( +g ‘ 𝑅 ) 𝑦 ) )
40 39 oveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → ( ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) = ( ( 𝑥 ∘f ( +g ‘ 𝑅 ) 𝑦 ) ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) )
41 2 13 5 14 14 14 16 17 mamucl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → ( 𝑦 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
42 41 21 eleqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → ( 𝑦 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ∈ ( Base ‘ 𝐴 ) )
43 1 24 25 19 matplusg2 ⊢ ( ( ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ∈ ( Base ‘ 𝐴 ) ∧ ( 𝑦 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ∈ ( Base ‘ 𝐴 ) ) → ( ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ( +g ‘ 𝐴 ) ( 𝑦 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ) = ( ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ∘f ( +g ‘ 𝑅 ) ( 𝑦 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ) )
44 32 42 43 syl2anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → ( ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ( +g ‘ 𝐴 ) ( 𝑦 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ) = ( ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ∘f ( +g ‘ 𝑅 ) ( 𝑦 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ) )
45 36 40 44 3eqtr4d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → ( ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) = ( ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ( +g ‘ 𝐴 ) ( 𝑦 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ) )
46 simpr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 ∈ Ring )
47 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
48 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
49 eqid ⊢ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑏 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑏 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
50 simpl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑁 ∈ Fin )
51 2 46 47 48 49 50 mamumat1cl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑏 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
52 simplr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) → 𝑅 ∈ Ring )
53 simpll ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) → 𝑁 ∈ Fin )
54 simpr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) → 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
55 2 52 47 48 49 53 53 5 54 mamulid ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) → ( ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑏 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑥 ) = 𝑥 )
56 2 52 47 48 49 53 53 5 54 mamurid ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) → ( 𝑥 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑏 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) = 𝑥 )
57 3 4 6 7 12 18 35 45 51 55 56 isringd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )