cpmat

Description: Value of the constructor of the set of all constant polynomial matrices, i.e. the set of all N x N matrices of polynomials over a ring R . (Contributed by AV, 15-Nov-2019)

	Ref	Expression
Hypotheses	cpmat.s	$⊢ S = N ConstPolyMat R$
	cpmat.p	$⊢ P = {Poly}_{1} (R)$
	cpmat.c	$⊢ C = N Mat P$
	cpmat.b	$⊢ B = {Base}_{C}$
Assertion	cpmat	$⊢ (N \in Fin \land R \in V) \to S = \{m \in B \| \forall i \in N \forall j \in N \forall k \in ℕ {coe}_{1} (i m j) (k) = 0_{R}\}$

Proof

Step	Hyp	Ref	Expression
1		cpmat.s	$⊢ S = N ConstPolyMat R$
2		cpmat.p	$⊢ P = {Poly}_{1} (R)$
3		cpmat.c	$⊢ C = N Mat P$
4		cpmat.b	$⊢ B = {Base}_{C}$
5		df-cpmat	$⊢ ConstPolyMat = (n \in Fin, r \in V ⟼ \{m \in {Base}_{(n Mat {Poly}_{1} (r))} \| \forall i \in n \forall j \in n \forall k \in ℕ {coe}_{1} (i m j) (k) = 0_{r}\})$
6	5	a1i	$⊢ (N \in Fin \land R \in V) \to ConstPolyMat = (n \in Fin, r \in V ⟼ \{m \in {Base}_{(n Mat {Poly}_{1} (r))} \| \forall i \in n \forall j \in n \forall k \in ℕ {coe}_{1} (i m j) (k) = 0_{r}\})$
7		simpl	$⊢ (n = N \land r = R) \to n = N$
8		fveq2	$⊢ r = R \to {Poly}_{1} (r) = {Poly}_{1} (R)$
9	8	adantl	$⊢ (n = N \land r = R) \to {Poly}_{1} (r) = {Poly}_{1} (R)$
10	7 9	oveq12d	$⊢ (n = N \land r = R) \to n Mat {Poly}_{1} (r) = N Mat {Poly}_{1} (R)$
11	10	fveq2d	$⊢ (n = N \land r = R) \to {Base}_{(n Mat {Poly}_{1} (r))} = {Base}_{(N Mat {Poly}_{1} (R))}$
12	2	oveq2i	$⊢ N Mat P = N Mat {Poly}_{1} (R)$
13	3 12	eqtri	$⊢ C = N Mat {Poly}_{1} (R)$
14	13	fveq2i	$⊢ {Base}_{C} = {Base}_{(N Mat {Poly}_{1} (R))}$
15	4 14	eqtri	$⊢ B = {Base}_{(N Mat {Poly}_{1} (R))}$
16	11 15	eqtr4di	$⊢ (n = N \land r = R) \to {Base}_{(n Mat {Poly}_{1} (r))} = B$
17		fveq2	$⊢ r = R \to 0_{r} = 0_{R}$
18	17	adantl	$⊢ (n = N \land r = R) \to 0_{r} = 0_{R}$
19	18	eqeq2d	$⊢ (n = N \land r = R) \to ({coe}_{1} (i m j) (k) = 0_{r} \leftrightarrow {coe}_{1} (i m j) (k) = 0_{R})$
20	19	ralbidv	$⊢ (n = N \land r = R) \to (\forall k \in ℕ {coe}_{1} (i m j) (k) = 0_{r} \leftrightarrow \forall k \in ℕ {coe}_{1} (i m j) (k) = 0_{R})$
21	7 20	raleqbidv	$⊢ (n = N \land r = R) \to (\forall j \in n \forall k \in ℕ {coe}_{1} (i m j) (k) = 0_{r} \leftrightarrow \forall j \in N \forall k \in ℕ {coe}_{1} (i m j) (k) = 0_{R})$
22	7 21	raleqbidv	$⊢ (n = N \land r = R) \to (\forall i \in n \forall j \in n \forall k \in ℕ {coe}_{1} (i m j) (k) = 0_{r} \leftrightarrow \forall i \in N \forall j \in N \forall k \in ℕ {coe}_{1} (i m j) (k) = 0_{R})$
23	16 22	rabeqbidv	$⊢ (n = N \land r = R) \to \{m \in {Base}_{(n Mat {Poly}_{1} (r))} \| \forall i \in n \forall j \in n \forall k \in ℕ {coe}_{1} (i m j) (k) = 0_{r}\} = \{m \in B \| \forall i \in N \forall j \in N \forall k \in ℕ {coe}_{1} (i m j) (k) = 0_{R}\}$
24	23	adantl	$⊢ ((N \in Fin \land R \in V) \land (n = N \land r = R)) \to \{m \in {Base}_{(n Mat {Poly}_{1} (r))} \| \forall i \in n \forall j \in n \forall k \in ℕ {coe}_{1} (i m j) (k) = 0_{r}\} = \{m \in B \| \forall i \in N \forall j \in N \forall k \in ℕ {coe}_{1} (i m j) (k) = 0_{R}\}$
25		simpl	$⊢ (N \in Fin \land R \in V) \to N \in Fin$
26		elex	$⊢ R \in V \to R \in V$
27	26	adantl	$⊢ (N \in Fin \land R \in V) \to R \in V$
28	4	fvexi	$⊢ B \in V$
29		rabexg	$⊢ B \in V \to \{m \in B \| \forall i \in N \forall j \in N \forall k \in ℕ {coe}_{1} (i m j) (k) = 0_{R}\} \in V$
30	28 29	mp1i	$⊢ (N \in Fin \land R \in V) \to \{m \in B \| \forall i \in N \forall j \in N \forall k \in ℕ {coe}_{1} (i m j) (k) = 0_{R}\} \in V$
31	6 24 25 27 30	ovmpod	$⊢ (N \in Fin \land R \in V) \to N ConstPolyMat R = \{m \in B \| \forall i \in N \forall j \in N \forall k \in ℕ {coe}_{1} (i m j) (k) = 0_{R}\}$
32	1 31	eqtrid	$⊢ (N \in Fin \land R \in V) \to S = \{m \in B \| \forall i \in N \forall j \in N \forall k \in ℕ {coe}_{1} (i m j) (k) = 0_{R}\}$

Metamath Proof Explorer

Theorem cpmat

Proof