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

Metamath Proof Explorer

Theorem matval

Description: Value of the matrix algebra. (Contributed by Stefan O'Rear, 4-Sep-2015)

Ref Expression
Hypotheses matval.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
matval.g ⊢ 𝐺 = ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) )
matval.t ⊢ · = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ )
Assertion matval ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝐴 = ( 𝐺 sSet ⟨ ( .r ‘ ndx ) , · ⟩ ) )

Proof

Step Hyp Ref Expression
1 matval.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 matval.g ⊢ 𝐺 = ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) )
3 matval.t ⊢ · = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ )
4 elex ⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V )
5 id ⊢ ( 𝑟 = 𝑅 → 𝑟 = 𝑅 )
6 id ⊢ ( 𝑛 = 𝑁 → 𝑛 = 𝑁 )
7 6 sqxpeqd ⊢ ( 𝑛 = 𝑁 → ( 𝑛 × 𝑛 ) = ( 𝑁 × 𝑁 ) )
8 5 7 oveqan12rd ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑟 freeLMod ( 𝑛 × 𝑛 ) ) = ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) )
9 8 2 eqtr4di ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑟 freeLMod ( 𝑛 × 𝑛 ) ) = 𝐺 )
10 6 6 6 oteq123d ⊢ ( 𝑛 = 𝑁 → ⟨ 𝑛 , 𝑛 , 𝑛 ⟩ = ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ )
11 5 10 oveqan12rd ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑟 maMul ⟨ 𝑛 , 𝑛 , 𝑛 ⟩ ) = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) )
12 11 3 eqtr4di ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑟 maMul ⟨ 𝑛 , 𝑛 , 𝑛 ⟩ ) = · )
13 12 opeq2d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ⟨ ( .r ‘ ndx ) , ( 𝑟 maMul ⟨ 𝑛 , 𝑛 , 𝑛 ⟩ ) ⟩ = ⟨ ( .r ‘ ndx ) , · ⟩ )
14 9 13 oveq12d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( ( 𝑟 freeLMod ( 𝑛 × 𝑛 ) ) sSet ⟨ ( .r ‘ ndx ) , ( 𝑟 maMul ⟨ 𝑛 , 𝑛 , 𝑛 ⟩ ) ⟩ ) = ( 𝐺 sSet ⟨ ( .r ‘ ndx ) , · ⟩ ) )
15 df-mat ⊢ Mat = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ( ( 𝑟 freeLMod ( 𝑛 × 𝑛 ) ) sSet ⟨ ( .r ‘ ndx ) , ( 𝑟 maMul ⟨ 𝑛 , 𝑛 , 𝑛 ⟩ ) ⟩ ) )
16 ovex ⊢ ( 𝐺 sSet ⟨ ( .r ‘ ndx ) , · ⟩ ) ∈ V
17 14 15 16 ovmpoa ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( 𝑁 Mat 𝑅 ) = ( 𝐺 sSet ⟨ ( .r ‘ ndx ) , · ⟩ ) )
18 4 17 sylan2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 Mat 𝑅 ) = ( 𝐺 sSet ⟨ ( .r ‘ ndx ) , · ⟩ ) )
19 1 18 eqtrid ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝐴 = ( 𝐺 sSet ⟨ ( .r ‘ ndx ) , · ⟩ ) )