Metamath Proof Explorer

Theorem matassa

Description: Existence of the matrix algebra, see also the statement in Lang p. 505: "Then Mat_n(R) is an algebra over R" . (Contributed by Stefan O'Rear, 5-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 matassa.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
3 1 2 matbas2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
4 1 matsca2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 = ( Scalar ‘ 𝐴 ) )
5 eqidd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) )
6 eqidd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( ·𝑠 ‘ 𝐴 ) = ( ·𝑠 ‘ 𝐴 ) )
7 eqid ⊢ ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ )
8 1 7 matmulr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( .r ‘ 𝐴 ) )
9 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
10 1 matlmod ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ LMod )
11 9 10 sylan2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐴 ∈ LMod )
12 1 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
13 9 12 sylan2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐴 ∈ Ring )
14 9 ad2antlr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → 𝑅 ∈ Ring )
15 simpll ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → 𝑁 ∈ Fin )
16 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
17 simpr1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
18 simpr2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
19 simpr3 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
20 2 14 7 15 15 15 16 17 18 19 mamuvs1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → ( ( ( ( 𝑁 × 𝑁 ) × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑦 ) ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) = ( ( ( 𝑁 × 𝑁 ) × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) ( 𝑦 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ) )
21 3 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
22 18 21 eleqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → 𝑦 ∈ ( Base ‘ 𝐴 ) )
23 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
24 eqid ⊢ ( ·𝑠 ‘ 𝐴 ) = ( ·𝑠 ‘ 𝐴 )
25 eqid ⊢ ( 𝑁 × 𝑁 ) = ( 𝑁 × 𝑁 )
26 1 23 2 24 16 25 matvsca2 ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐴 ) 𝑦 ) = ( ( ( 𝑁 × 𝑁 ) × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑦 ) )
27 17 22 26 syl2anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐴 ) 𝑦 ) = ( ( ( 𝑁 × 𝑁 ) × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑦 ) )
28 27 oveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝐴 ) 𝑦 ) ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) = ( ( ( ( 𝑁 × 𝑁 ) × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑦 ) ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) )
29 2 14 7 15 15 15 18 19 mamucl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → ( 𝑦 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
30 29 21 eleqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → ( 𝑦 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ∈ ( Base ‘ 𝐴 ) )
31 1 23 2 24 16 25 matvsca2 ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑦 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ∈ ( Base ‘ 𝐴 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐴 ) ( 𝑦 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ) = ( ( ( 𝑁 × 𝑁 ) × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) ( 𝑦 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ) )
32 17 30 31 syl2anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐴 ) ( 𝑦 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ) = ( ( ( 𝑁 × 𝑁 ) × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) ( 𝑦 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ) )
33 20 28 32 3eqtr4d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝐴 ) 𝑦 ) ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) = ( 𝑥 ( ·𝑠 ‘ 𝐴 ) ( 𝑦 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ) )
34 simplr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → 𝑅 ∈ CRing )
35 34 2 16 7 15 15 15 18 17 19 mamuvs2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → ( 𝑦 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ( ( ( 𝑁 × 𝑁 ) × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) ) = ( ( ( 𝑁 × 𝑁 ) × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) ( 𝑦 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ) )
36 19 21 eleqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → 𝑧 ∈ ( Base ‘ 𝐴 ) )
37 1 23 2 24 16 25 matvsca2 ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐴 ) 𝑧 ) = ( ( ( 𝑁 × 𝑁 ) × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) )
38 17 36 37 syl2anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐴 ) 𝑧 ) = ( ( ( 𝑁 × 𝑁 ) × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) )
39 38 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → ( 𝑦 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ( 𝑥 ( ·𝑠 ‘ 𝐴 ) 𝑧 ) ) = ( 𝑦 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ( ( ( 𝑁 × 𝑁 ) × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) ) )
40 35 39 32 3eqtr4d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ) ) → ( 𝑦 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ( 𝑥 ( ·𝑠 ‘ 𝐴 ) 𝑧 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝐴 ) ( 𝑦 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑧 ) ) )
41 3 4 5 6 8 11 13 33 40 isassad ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐴 ∈ AssAlg )