decpmatval0

Description: The matrix consisting of the coefficients in the polynomial entries of a polynomial matrix for the same power, most general version. (Contributed by AV, 2-Dec-2019)

		Ref	Expression
	Assertion	decpmatval0	$⊢ (M \in V \land K \in ℕ_{0}) \to M decompPMat K = (i \in dom dom M, j \in dom dom M ⟼ {coe}_{1} (i M j) (K))$

Proof

Step	Hyp	Ref	Expression
1		df-decpmat	$⊢ decompPMat = (m \in V, k \in ℕ_{0} ⟼ (i \in dom dom m, j \in dom dom m ⟼ {coe}_{1} (i m j) (k)))$
2	1	a1i	$⊢ (M \in V \land K \in ℕ_{0}) \to decompPMat = (m \in V, k \in ℕ_{0} ⟼ (i \in dom dom m, j \in dom dom m ⟼ {coe}_{1} (i m j) (k)))$
3		dmeq	$⊢ m = M \to dom m = dom M$
4	3	adantr	$⊢ (m = M \land k = K) \to dom m = dom M$
5	4	dmeqd	$⊢ (m = M \land k = K) \to dom dom m = dom dom M$
6		oveq	$⊢ m = M \to i m j = i M j$
7	6	fveq2d	$⊢ m = M \to {coe}_{1} (i m j) = {coe}_{1} (i M j)$
8	7	adantr	$⊢ (m = M \land k = K) \to {coe}_{1} (i m j) = {coe}_{1} (i M j)$
9		simpr	$⊢ (m = M \land k = K) \to k = K$
10	8 9	fveq12d	$⊢ (m = M \land k = K) \to {coe}_{1} (i m j) (k) = {coe}_{1} (i M j) (K)$
11	5 5 10	mpoeq123dv	$⊢ (m = M \land k = K) \to (i \in dom dom m, j \in dom dom m ⟼ {coe}_{1} (i m j) (k)) = (i \in dom dom M, j \in dom dom M ⟼ {coe}_{1} (i M j) (K))$
12	11	adantl	$⊢ ((M \in V \land K \in ℕ_{0}) \land (m = M \land k = K)) \to (i \in dom dom m, j \in dom dom m ⟼ {coe}_{1} (i m j) (k)) = (i \in dom dom M, j \in dom dom M ⟼ {coe}_{1} (i M j) (K))$
13		elex	$⊢ M \in V \to M \in V$
14	13	adantr	$⊢ (M \in V \land K \in ℕ_{0}) \to M \in V$
15		simpr	$⊢ (M \in V \land K \in ℕ_{0}) \to K \in ℕ_{0}$
16		dmexg	$⊢ M \in V \to dom M \in V$
17	16	dmexd	$⊢ M \in V \to dom dom M \in V$
18	17 17	jca	$⊢ M \in V \to (dom dom M \in V \land dom dom M \in V)$
19	18	adantr	$⊢ (M \in V \land K \in ℕ_{0}) \to (dom dom M \in V \land dom dom M \in V)$
20		mpoexga	$⊢ (dom dom M \in V \land dom dom M \in V) \to (i \in dom dom M, j \in dom dom M ⟼ {coe}_{1} (i M j) (K)) \in V$
21	19 20	syl	$⊢ (M \in V \land K \in ℕ_{0}) \to (i \in dom dom M, j \in dom dom M ⟼ {coe}_{1} (i M j) (K)) \in V$
22	2 12 14 15 21	ovmpod	$⊢ (M \in V \land K \in ℕ_{0}) \to M decompPMat K = (i \in dom dom M, j \in dom dom M ⟼ {coe}_{1} (i M j) (K))$

Metamath Proof Explorer

Theorem decpmatval0

Proof