pm2mpval - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > pm2mpval		Structured version Visualization version GIF version

Theorem pm2mpval 20419

Description: Value of the transformation of a polynomial matrix into a polynomial over matrices. (Contributed by AV, 5-Dec-2019.)

**Hypotheses**
Ref	Expression
pm2mpval.p	⊢ 𝑃 = (Poly₁‘𝑅)
pm2mpval.c	⊢ 𝐶 = (𝑁 Mat 𝑃)
pm2mpval.b	⊢ 𝐵 = (Base‘𝐶)
pm2mpval.m	⊢ ∗ = ( ·_𝑠 ‘𝑄)
pm2mpval.e	⊢ ↑ = (._g‘(mulGrp‘𝑄))
pm2mpval.x	⊢ 𝑋 = (var₁‘𝐴)
pm2mpval.a	⊢ 𝐴 = (𝑁 Mat 𝑅)
pm2mpval.q	⊢ 𝑄 = (Poly₁‘𝐴)
pm2mpval.t	⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅)

**Assertion**
Ref	Expression
pm2mpval	⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑇 = (𝑚 ∈ 𝐵 ↦ (𝑄 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑚 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))))))

Distinct variable groups: 𝐵,𝑚 𝑘,𝑁,𝑚 𝑅,𝑘,𝑚 𝑚,𝑉 Allowed substitution hints: 𝐴(𝑘,𝑚) 𝐵(𝑘) 𝐶(𝑘,𝑚) 𝑃(𝑘,𝑚) 𝑄(𝑘,𝑚) 𝑇(𝑘,𝑚) ↑ (𝑘,𝑚) ∗ (𝑘,𝑚) 𝑉(𝑘) 𝑋(𝑘,𝑚)

Proof of Theorem pm2mpval Dummy variables 𝑛 𝑟 𝑎 𝑞 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		pm2mpval.t	. 2 ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅)
2		df-pm2mp 20417	. . . 4 ⊢ pMatToMatPoly = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat (Poly₁‘𝑟))) ↦ ⦋(𝑛 Mat 𝑟) / 𝑎⦌⦋(Poly₁‘𝑎) / 𝑞⦌(𝑞 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑚 decompPMat 𝑘)( ·_𝑠 ‘𝑞)(𝑘(._g‘(mulGrp‘𝑞))(var₁‘𝑎)))))))
3	2	a1i 11	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → pMatToMatPoly = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat (Poly₁‘𝑟))) ↦ ⦋(𝑛 Mat 𝑟) / 𝑎⦌⦋(Poly₁‘𝑎) / 𝑞⦌(𝑞 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑚 decompPMat 𝑘)( ·_𝑠 ‘𝑞)(𝑘(._g‘(mulGrp‘𝑞))(var₁‘𝑎))))))))
4		simpl 472	. . . . . . . 8 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → 𝑛 = 𝑁)
5		fveq2 6103	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (Poly₁‘𝑟) = (Poly₁‘𝑅))
6	5	adantl 481	. . . . . . . 8 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Poly₁‘𝑟) = (Poly₁‘𝑅))
7	4, 6	oveq12d 6567	. . . . . . 7 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑛 Mat (Poly₁‘𝑟)) = (𝑁 Mat (Poly₁‘𝑅)))
8	7	fveq2d 6107	. . . . . 6 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Base‘(𝑛 Mat (Poly₁‘𝑟))) = (Base‘(𝑁 Mat (Poly₁‘𝑅))))
9		pm2mpval.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐶)
10		pm2mpval.c	. . . . . . . . 9 ⊢ 𝐶 = (𝑁 Mat 𝑃)
11		pm2mpval.p	. . . . . . . . . 10 ⊢ 𝑃 = (Poly₁‘𝑅)
12	11	oveq2i 6560	. . . . . . . . 9 ⊢ (𝑁 Mat 𝑃) = (𝑁 Mat (Poly₁‘𝑅))
13	10, 12	eqtri 2632	. . . . . . . 8 ⊢ 𝐶 = (𝑁 Mat (Poly₁‘𝑅))
14	13	fveq2i 6106	. . . . . . 7 ⊢ (Base‘𝐶) = (Base‘(𝑁 Mat (Poly₁‘𝑅)))
15	9, 14	eqtri 2632	. . . . . 6 ⊢ 𝐵 = (Base‘(𝑁 Mat (Poly₁‘𝑅)))
16	8, 15	syl6eqr 2662	. . . . 5 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Base‘(𝑛 Mat (Poly₁‘𝑟))) = 𝐵)
17	16	adantl 481	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) ∧ (𝑛 = 𝑁 ∧ 𝑟 = 𝑅)) → (Base‘(𝑛 Mat (Poly₁‘𝑟))) = 𝐵)
18		ovex 6577	. . . . . 6 ⊢ (𝑛 Mat 𝑟) ∈ V
19		fvex 6113	. . . . . . . 8 ⊢ (Poly₁‘𝑎) ∈ V
20	19	a1i 11	. . . . . . 7 ⊢ (𝑎 = (𝑛 Mat 𝑟) → (Poly₁‘𝑎) ∈ V)
21		simpr 476	. . . . . . . . 9 ⊢ ((𝑎 = (𝑛 Mat 𝑟) ∧ 𝑞 = (Poly₁‘𝑎)) → 𝑞 = (Poly₁‘𝑎))
22		fveq2 6103	. . . . . . . . . 10 ⊢ (𝑎 = (𝑛 Mat 𝑟) → (Poly₁‘𝑎) = (Poly₁‘(𝑛 Mat 𝑟)))
23	22	adantr 480	. . . . . . . . 9 ⊢ ((𝑎 = (𝑛 Mat 𝑟) ∧ 𝑞 = (Poly₁‘𝑎)) → (Poly₁‘𝑎) = (Poly₁‘(𝑛 Mat 𝑟)))
24	21, 23	eqtrd 2644	. . . . . . . 8 ⊢ ((𝑎 = (𝑛 Mat 𝑟) ∧ 𝑞 = (Poly₁‘𝑎)) → 𝑞 = (Poly₁‘(𝑛 Mat 𝑟)))
25	24	fveq2d 6107	. . . . . . . . . 10 ⊢ ((𝑎 = (𝑛 Mat 𝑟) ∧ 𝑞 = (Poly₁‘𝑎)) → ( ·_𝑠 ‘𝑞) = ( ·_𝑠 ‘(Poly₁‘(𝑛 Mat 𝑟))))
26		eqidd 2611	. . . . . . . . . 10 ⊢ ((𝑎 = (𝑛 Mat 𝑟) ∧ 𝑞 = (Poly₁‘𝑎)) → (𝑚 decompPMat 𝑘) = (𝑚 decompPMat 𝑘))
27	24	fveq2d 6107	. . . . . . . . . . . 12 ⊢ ((𝑎 = (𝑛 Mat 𝑟) ∧ 𝑞 = (Poly₁‘𝑎)) → (mulGrp‘𝑞) = (mulGrp‘(Poly₁‘(𝑛 Mat 𝑟))))
28	27	fveq2d 6107	. . . . . . . . . . 11 ⊢ ((𝑎 = (𝑛 Mat 𝑟) ∧ 𝑞 = (Poly₁‘𝑎)) → (._g‘(mulGrp‘𝑞)) = (._g‘(mulGrp‘(Poly₁‘(𝑛 Mat 𝑟)))))
29		eqidd 2611	. . . . . . . . . . 11 ⊢ ((𝑎 = (𝑛 Mat 𝑟) ∧ 𝑞 = (Poly₁‘𝑎)) → 𝑘 = 𝑘)
30		fveq2 6103	. . . . . . . . . . . 12 ⊢ (𝑎 = (𝑛 Mat 𝑟) → (var₁‘𝑎) = (var₁‘(𝑛 Mat 𝑟)))
31	30	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑎 = (𝑛 Mat 𝑟) ∧ 𝑞 = (Poly₁‘𝑎)) → (var₁‘𝑎) = (var₁‘(𝑛 Mat 𝑟)))
32	28, 29, 31	oveq123d 6570	. . . . . . . . . 10 ⊢ ((𝑎 = (𝑛 Mat 𝑟) ∧ 𝑞 = (Poly₁‘𝑎)) → (𝑘(._g‘(mulGrp‘𝑞))(var₁‘𝑎)) = (𝑘(._g‘(mulGrp‘(Poly₁‘(𝑛 Mat 𝑟))))(var₁‘(𝑛 Mat 𝑟))))
33	25, 26, 32	oveq123d 6570	. . . . . . . . 9 ⊢ ((𝑎 = (𝑛 Mat 𝑟) ∧ 𝑞 = (Poly₁‘𝑎)) → ((𝑚 decompPMat 𝑘)( ·_𝑠 ‘𝑞)(𝑘(._g‘(mulGrp‘𝑞))(var₁‘𝑎))) = ((𝑚 decompPMat 𝑘)( ·_𝑠 ‘(Poly₁‘(𝑛 Mat 𝑟)))(𝑘(._g‘(mulGrp‘(Poly₁‘(𝑛 Mat 𝑟))))(var₁‘(𝑛 Mat 𝑟)))))
34	33	mpteq2dv 4673	. . . . . . . 8 ⊢ ((𝑎 = (𝑛 Mat 𝑟) ∧ 𝑞 = (Poly₁‘𝑎)) → (𝑘 ∈ ℕ₀ ↦ ((𝑚 decompPMat 𝑘)( ·_𝑠 ‘𝑞)(𝑘(._g‘(mulGrp‘𝑞))(var₁‘𝑎)))) = (𝑘 ∈ ℕ₀ ↦ ((𝑚 decompPMat 𝑘)( ·_𝑠 ‘(Poly₁‘(𝑛 Mat 𝑟)))(𝑘(._g‘(mulGrp‘(Poly₁‘(𝑛 Mat 𝑟))))(var₁‘(𝑛 Mat 𝑟))))))
35	24, 34	oveq12d 6567	. . . . . . 7 ⊢ ((𝑎 = (𝑛 Mat 𝑟) ∧ 𝑞 = (Poly₁‘𝑎)) → (𝑞 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑚 decompPMat 𝑘)( ·_𝑠 ‘𝑞)(𝑘(._g‘(mulGrp‘𝑞))(var₁‘𝑎))))) = ((Poly₁‘(𝑛 Mat 𝑟)) Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑚 decompPMat 𝑘)( ·_𝑠 ‘(Poly₁‘(𝑛 Mat 𝑟)))(𝑘(._g‘(mulGrp‘(Poly₁‘(𝑛 Mat 𝑟))))(var₁‘(𝑛 Mat 𝑟)))))))
36	20, 35	csbied 3526	. . . . . 6 ⊢ (𝑎 = (𝑛 Mat 𝑟) → ⦋(Poly₁‘𝑎) / 𝑞⦌(𝑞 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑚 decompPMat 𝑘)( ·_𝑠 ‘𝑞)(𝑘(._g‘(mulGrp‘𝑞))(var₁‘𝑎))))) = ((Poly₁‘(𝑛 Mat 𝑟)) Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑚 decompPMat 𝑘)( ·_𝑠 ‘(Poly₁‘(𝑛 Mat 𝑟)))(𝑘(._g‘(mulGrp‘(Poly₁‘(𝑛 Mat 𝑟))))(var₁‘(𝑛 Mat 𝑟)))))))
37	18, 36	csbie 3525	. . . . 5 ⊢ ⦋(𝑛 Mat 𝑟) / 𝑎⦌⦋(Poly₁‘𝑎) / 𝑞⦌(𝑞 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑚 decompPMat 𝑘)( ·_𝑠 ‘𝑞)(𝑘(._g‘(mulGrp‘𝑞))(var₁‘𝑎))))) = ((Poly₁‘(𝑛 Mat 𝑟)) Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑚 decompPMat 𝑘)( ·_𝑠 ‘(Poly₁‘(𝑛 Mat 𝑟)))(𝑘(._g‘(mulGrp‘(Poly₁‘(𝑛 Mat 𝑟))))(var₁‘(𝑛 Mat 𝑟))))))
38		oveq12 6558	. . . . . . . . 9 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑛 Mat 𝑟) = (𝑁 Mat 𝑅))
39	38	fveq2d 6107	. . . . . . . 8 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Poly₁‘(𝑛 Mat 𝑟)) = (Poly₁‘(𝑁 Mat 𝑅)))
40		pm2mpval.q	. . . . . . . . 9 ⊢ 𝑄 = (Poly₁‘𝐴)
41		pm2mpval.a	. . . . . . . . . 10 ⊢ 𝐴 = (𝑁 Mat 𝑅)
42	41	fveq2i 6106	. . . . . . . . 9 ⊢ (Poly₁‘𝐴) = (Poly₁‘(𝑁 Mat 𝑅))
43	40, 42	eqtri 2632	. . . . . . . 8 ⊢ 𝑄 = (Poly₁‘(𝑁 Mat 𝑅))
44	39, 43	syl6eqr 2662	. . . . . . 7 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Poly₁‘(𝑛 Mat 𝑟)) = 𝑄)
45	39	fveq2d 6107	. . . . . . . . . 10 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → ( ·_𝑠 ‘(Poly₁‘(𝑛 Mat 𝑟))) = ( ·_𝑠 ‘(Poly₁‘(𝑁 Mat 𝑅))))
46		pm2mpval.m	. . . . . . . . . . 11 ⊢ ∗ = ( ·_𝑠 ‘𝑄)
47	43	fveq2i 6106	. . . . . . . . . . 11 ⊢ ( ·_𝑠 ‘𝑄) = ( ·_𝑠 ‘(Poly₁‘(𝑁 Mat 𝑅)))
48	46, 47	eqtri 2632	. . . . . . . . . 10 ⊢ ∗ = ( ·_𝑠 ‘(Poly₁‘(𝑁 Mat 𝑅)))
49	45, 48	syl6eqr 2662	. . . . . . . . 9 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → ( ·_𝑠 ‘(Poly₁‘(𝑛 Mat 𝑟))) = ∗ )
50		eqidd 2611	. . . . . . . . 9 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑚 decompPMat 𝑘) = (𝑚 decompPMat 𝑘))
51	39	fveq2d 6107	. . . . . . . . . . . 12 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (mulGrp‘(Poly₁‘(𝑛 Mat 𝑟))) = (mulGrp‘(Poly₁‘(𝑁 Mat 𝑅))))
52	51	fveq2d 6107	. . . . . . . . . . 11 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (._g‘(mulGrp‘(Poly₁‘(𝑛 Mat 𝑟)))) = (._g‘(mulGrp‘(Poly₁‘(𝑁 Mat 𝑅)))))
53		pm2mpval.e	. . . . . . . . . . . 12 ⊢ ↑ = (._g‘(mulGrp‘𝑄))
54	43	fveq2i 6106	. . . . . . . . . . . . 13 ⊢ (mulGrp‘𝑄) = (mulGrp‘(Poly₁‘(𝑁 Mat 𝑅)))
55	54	fveq2i 6106	. . . . . . . . . . . 12 ⊢ (._g‘(mulGrp‘𝑄)) = (._g‘(mulGrp‘(Poly₁‘(𝑁 Mat 𝑅))))
56	53, 55	eqtri 2632	. . . . . . . . . . 11 ⊢ ↑ = (._g‘(mulGrp‘(Poly₁‘(𝑁 Mat 𝑅))))
57	52, 56	syl6eqr 2662	. . . . . . . . . 10 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (._g‘(mulGrp‘(Poly₁‘(𝑛 Mat 𝑟)))) = ↑ )
58		eqidd 2611	. . . . . . . . . 10 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → 𝑘 = 𝑘)
59	38	fveq2d 6107	. . . . . . . . . . 11 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (var₁‘(𝑛 Mat 𝑟)) = (var₁‘(𝑁 Mat 𝑅)))
60		pm2mpval.x	. . . . . . . . . . . 12 ⊢ 𝑋 = (var₁‘𝐴)
61	41	fveq2i 6106	. . . . . . . . . . . 12 ⊢ (var₁‘𝐴) = (var₁‘(𝑁 Mat 𝑅))
62	60, 61	eqtri 2632	. . . . . . . . . . 11 ⊢ 𝑋 = (var₁‘(𝑁 Mat 𝑅))
63	59, 62	syl6eqr 2662	. . . . . . . . . 10 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (var₁‘(𝑛 Mat 𝑟)) = 𝑋)
64	57, 58, 63	oveq123d 6570	. . . . . . . . 9 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑘(._g‘(mulGrp‘(Poly₁‘(𝑛 Mat 𝑟))))(var₁‘(𝑛 Mat 𝑟))) = (𝑘 ↑ 𝑋))
65	49, 50, 64	oveq123d 6570	. . . . . . . 8 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → ((𝑚 decompPMat 𝑘)( ·_𝑠 ‘(Poly₁‘(𝑛 Mat 𝑟)))(𝑘(._g‘(mulGrp‘(Poly₁‘(𝑛 Mat 𝑟))))(var₁‘(𝑛 Mat 𝑟)))) = ((𝑚 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋)))
66	65	mpteq2dv 4673	. . . . . . 7 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑘 ∈ ℕ₀ ↦ ((𝑚 decompPMat 𝑘)( ·_𝑠 ‘(Poly₁‘(𝑛 Mat 𝑟)))(𝑘(._g‘(mulGrp‘(Poly₁‘(𝑛 Mat 𝑟))))(var₁‘(𝑛 Mat 𝑟))))) = (𝑘 ∈ ℕ₀ ↦ ((𝑚 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))))
67	44, 66	oveq12d 6567	. . . . . 6 ⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → ((Poly₁‘(𝑛 Mat 𝑟)) Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑚 decompPMat 𝑘)( ·_𝑠 ‘(Poly₁‘(𝑛 Mat 𝑟)))(𝑘(._g‘(mulGrp‘(Poly₁‘(𝑛 Mat 𝑟))))(var₁‘(𝑛 Mat 𝑟)))))) = (𝑄 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑚 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋)))))
68	67	adantl 481	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) ∧ (𝑛 = 𝑁 ∧ 𝑟 = 𝑅)) → ((Poly₁‘(𝑛 Mat 𝑟)) Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑚 decompPMat 𝑘)( ·_𝑠 ‘(Poly₁‘(𝑛 Mat 𝑟)))(𝑘(._g‘(mulGrp‘(Poly₁‘(𝑛 Mat 𝑟))))(var₁‘(𝑛 Mat 𝑟)))))) = (𝑄 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑚 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋)))))
69	37, 68	syl5eq 2656	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) ∧ (𝑛 = 𝑁 ∧ 𝑟 = 𝑅)) → ⦋(𝑛 Mat 𝑟) / 𝑎⦌⦋(Poly₁‘𝑎) / 𝑞⦌(𝑞 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑚 decompPMat 𝑘)( ·_𝑠 ‘𝑞)(𝑘(._g‘(mulGrp‘𝑞))(var₁‘𝑎))))) = (𝑄 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑚 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋)))))
70	17, 69	mpteq12dv 4663	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) ∧ (𝑛 = 𝑁 ∧ 𝑟 = 𝑅)) → (𝑚 ∈ (Base‘(𝑛 Mat (Poly₁‘𝑟))) ↦ ⦋(𝑛 Mat 𝑟) / 𝑎⦌⦋(Poly₁‘𝑎) / 𝑞⦌(𝑞 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑚 decompPMat 𝑘)( ·_𝑠 ‘𝑞)(𝑘(._g‘(mulGrp‘𝑞))(var₁‘𝑎)))))) = (𝑚 ∈ 𝐵 ↦ (𝑄 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑚 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))))))
71		simpl 472	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑁 ∈ Fin)
72		elex 3185	. . . 4 ⊢ (𝑅 ∈ 𝑉 → 𝑅 ∈ V)
73	72	adantl 481	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑅 ∈ V)
74		fvex 6113	. . . . . 6 ⊢ (Base‘𝐶) ∈ V
75	9, 74	eqeltri 2684	. . . . 5 ⊢ 𝐵 ∈ V
76	75	mptex 6390	. . . 4 ⊢ (𝑚 ∈ 𝐵 ↦ (𝑄 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑚 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))))) ∈ V
77	76	a1i 11	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝑚 ∈ 𝐵 ↦ (𝑄 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑚 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))))) ∈ V)
78	3, 70, 71, 73, 77	ovmpt2d 6686	. 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝑁 pMatToMatPoly 𝑅) = (𝑚 ∈ 𝐵 ↦ (𝑄 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑚 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))))))
79	1, 78	syl5eq 2656	1 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑇 = (𝑚 ∈ 𝐵 ↦ (𝑄 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑚 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 383 = wceq 1475 ∈ wcel 1977 Vcvv 3173 ⦋csb 3499 ↦ cmpt 4643 ‘cfv 5804 (class class class)co 6549 ↦ cmpt2 6551 Fincfn 7841 ℕ₀cn0 11169 Basecbs 15695 ·_𝑠 cvsca 15772 Σ_g cgsu 15924 ._gcmg 17363 mulGrpcmgp 18312 var₁cv1 19367 Poly₁cpl1 19368 Mat cmat 20032 decompPMat cdecpmat 20386 pMatToMatPoly cpm2mp 20416

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pr 4833

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-ral 2901 df-rex 2902 df-reu 2903 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-id 4953 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-pm2mp 20417

This theorem is referenced by: pm2mpfval 20420 pm2mpf 20422

W3C validator