matval

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

	Ref	Expression
Hypotheses	matval.a	$⊢ A = N Mat R$
	matval.g	$⊢ G = R freeLMod (N \times N)$
	matval.t	$⊢ \underset{˙}{\cdot} = R maMul ⟨N, N, N⟩$
Assertion	matval	$⊢ (N \in Fin \land R \in V) \to A = G sSet ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩$

Step	Hyp	Ref	Expression
1		matval.a	$⊢ A = N Mat R$
2		matval.g	$⊢ G = R freeLMod (N \times N)$
3		matval.t	$⊢ \underset{˙}{\cdot} = R maMul ⟨N, N, N⟩$
4		elex	$⊢ R \in V \to R \in V$
5		id	$⊢ r = R \to r = R$
6		id	$⊢ n = N \to n = N$
7	6	sqxpeqd	$⊢ n = N \to n \times n = N \times N$
8	5 7	oveqan12rd	$⊢ (n = N \land r = R) \to r freeLMod (n \times n) = R freeLMod (N \times N)$
9	8 2	eqtr4di	$⊢ (n = N \land r = R) \to r freeLMod (n \times n) = G$
10	6 6 6	oteq123d	$⊢ n = N \to ⟨n, n, n⟩ = ⟨N, N, N⟩$
11	5 10	oveqan12rd	$⊢ (n = N \land r = R) \to r maMul ⟨n, n, n⟩ = R maMul ⟨N, N, N⟩$
12	11 3	eqtr4di	$⊢ (n = N \land r = R) \to r maMul ⟨n, n, n⟩ = \underset{˙}{\cdot}$
13	12	opeq2d	$⊢ (n = N \land r = R) \to ⟨\cdot_{ndx}, r maMul ⟨n, n, n⟩⟩ = ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩$
14	9 13	oveq12d	$⊢ (n = N \land r = R) \to (r freeLMod (n \times n)) sSet ⟨\cdot_{ndx}, r maMul ⟨n, n, n⟩⟩ = G sSet ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩$
15		df-mat	$⊢ Mat = (n \in Fin, r \in V ⟼ (r freeLMod (n \times n)) sSet ⟨\cdot_{ndx}, r maMul ⟨n, n, n⟩⟩)$
16		ovex	$⊢ G sSet ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩ \in V$
17	14 15 16	ovmpoa	$⊢ (N \in Fin \land R \in V) \to N Mat R = G sSet ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩$
18	4 17	sylan2	$⊢ (N \in Fin \land R \in V) \to N Mat R = G sSet ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩$
19	1 18	syl5eq	$⊢ (N \in Fin \land R \in V) \to A = G sSet ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩$

Metamath Proof Explorer