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 ) , · ⟩ ) )