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