mat2pmatfval

Description: Value of the matrix transformation. (Contributed by AV, 31-Jul-2019)

	Ref	Expression
Hypotheses	mat2pmatfval.t	$⊢ T = N matToPolyMat R$
	mat2pmatfval.a	$⊢ A = N Mat R$
	mat2pmatfval.b	$⊢ B = {Base}_{A}$
	mat2pmatfval.p	$⊢ P = {Poly}_{1} (R)$
	mat2pmatfval.s	$⊢ S = algSc (P)$
Assertion	mat2pmatfval	$⊢ (N \in Fin \land R \in V) \to T = (m \in B ⟼ (x \in N, y \in N ⟼ S (x m y)))$

Proof

Step	Hyp	Ref	Expression
1		mat2pmatfval.t	$⊢ T = N matToPolyMat R$
2		mat2pmatfval.a	$⊢ A = N Mat R$
3		mat2pmatfval.b	$⊢ B = {Base}_{A}$
4		mat2pmatfval.p	$⊢ P = {Poly}_{1} (R)$
5		mat2pmatfval.s	$⊢ S = algSc (P)$
6		df-mat2pmat	$⊢ matToPolyMat = (n \in Fin, r \in V ⟼ (m \in {Base}_{(n Mat r)} ⟼ (x \in n, y \in n ⟼ algSc ({Poly}_{1} (r)) (x m y))))$
7	6	a1i	$⊢ (N \in Fin \land R \in V) \to matToPolyMat = (n \in Fin, r \in V ⟼ (m \in {Base}_{(n Mat r)} ⟼ (x \in n, y \in n ⟼ algSc ({Poly}_{1} (r)) (x m y))))$
8		oveq12	$⊢ (n = N \land r = R) \to n Mat r = N Mat R$
9	8	fveq2d	$⊢ (n = N \land r = R) \to {Base}_{(n Mat r)} = {Base}_{(N Mat R)}$
10	2	fveq2i	$⊢ {Base}_{A} = {Base}_{(N Mat R)}$
11	3 10	eqtr2i	$⊢ {Base}_{(N Mat R)} = B$
12	9 11	eqtrdi	$⊢ (n = N \land r = R) \to {Base}_{(n Mat r)} = B$
13		simpl	$⊢ (n = N \land r = R) \to n = N$
14		2fveq3	$⊢ r = R \to algSc ({Poly}_{1} (r)) = algSc ({Poly}_{1} (R))$
15	14	adantl	$⊢ (n = N \land r = R) \to algSc ({Poly}_{1} (r)) = algSc ({Poly}_{1} (R))$
16	4	fveq2i	$⊢ algSc (P) = algSc ({Poly}_{1} (R))$
17	5 16	eqtr2i	$⊢ algSc ({Poly}_{1} (R)) = S$
18	15 17	eqtrdi	$⊢ (n = N \land r = R) \to algSc ({Poly}_{1} (r)) = S$
19	18	fveq1d	$⊢ (n = N \land r = R) \to algSc ({Poly}_{1} (r)) (x m y) = S (x m y)$
20	13 13 19	mpoeq123dv	$⊢ (n = N \land r = R) \to (x \in n, y \in n ⟼ algSc ({Poly}_{1} (r)) (x m y)) = (x \in N, y \in N ⟼ S (x m y))$
21	12 20	mpteq12dv	$⊢ (n = N \land r = R) \to (m \in {Base}_{(n Mat r)} ⟼ (x \in n, y \in n ⟼ algSc ({Poly}_{1} (r)) (x m y))) = (m \in B ⟼ (x \in N, y \in N ⟼ S (x m y)))$
22	21	adantl	$⊢ ((N \in Fin \land R \in V) \land (n = N \land r = R)) \to (m \in {Base}_{(n Mat r)} ⟼ (x \in n, y \in n ⟼ algSc ({Poly}_{1} (r)) (x m y))) = (m \in B ⟼ (x \in N, y \in N ⟼ S (x m y)))$
23		simpl	$⊢ (N \in Fin \land R \in V) \to N \in Fin$
24		elex	$⊢ R \in V \to R \in V$
25	24	adantl	$⊢ (N \in Fin \land R \in V) \to R \in V$
26	3	fvexi	$⊢ B \in V$
27		mptexg	$⊢ B \in V \to (m \in B ⟼ (x \in N, y \in N ⟼ S (x m y))) \in V$
28	26 27	mp1i	$⊢ (N \in Fin \land R \in V) \to (m \in B ⟼ (x \in N, y \in N ⟼ S (x m y))) \in V$
29	7 22 23 25 28	ovmpod	$⊢ (N \in Fin \land R \in V) \to N matToPolyMat R = (m \in B ⟼ (x \in N, y \in N ⟼ S (x m y)))$
30	1 29	syl5eq	$⊢ (N \in Fin \land R \in V) \to T = (m \in B ⟼ (x \in N, y \in N ⟼ S (x m y)))$

Metamath Proof Explorer

Theorem mat2pmatfval

Proof