Metamath Proof Explorer

Theorem cpm2mfval

Description: Value of the inverse matrix transformation. (Contributed by AV, 14-Dec-2019)

		Ref	Expression
	Hypotheses	cpm2mfval.i	⊢ 𝐼 = ( 𝑁 cPolyMatToMat 𝑅 )
		cpm2mfval.s	⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
	Assertion	cpm2mfval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝐼 = ( 𝑚 ∈ 𝑆 ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe₁ ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cpm2mfval.i	⊢ 𝐼 = ( 𝑁 cPolyMatToMat 𝑅 )
2		cpm2mfval.s	⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
3		df-cpmat2mat	⊢ cPolyMatToMat = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( 𝑛 ConstPolyMat 𝑟 ) ↦ ( 𝑥 ∈ 𝑛 , 𝑦 ∈ 𝑛 ↦ ( ( coe₁ ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) )
4	3	a1i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → cPolyMatToMat = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( 𝑛 ConstPolyMat 𝑟 ) ↦ ( 𝑥 ∈ 𝑛 , 𝑦 ∈ 𝑛 ↦ ( ( coe₁ ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) ) )
5		oveq12	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑛 ConstPolyMat 𝑟 ) = ( 𝑁 ConstPolyMat 𝑅 ) )
6	5 2	eqtr4di	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑛 ConstPolyMat 𝑟 ) = 𝑆 )
7		simpl	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → 𝑛 = 𝑁 )
8		eqidd	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( ( coe₁ ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) = ( ( coe₁ ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) )
9	7 7 8	mpoeq123dv	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑥 ∈ 𝑛 , 𝑦 ∈ 𝑛 ↦ ( ( coe₁ ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe₁ ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) )
10	6 9	mpteq12dv	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑚 ∈ ( 𝑛 ConstPolyMat 𝑟 ) ↦ ( 𝑥 ∈ 𝑛 , 𝑦 ∈ 𝑛 ↦ ( ( coe₁ ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) = ( 𝑚 ∈ 𝑆 ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe₁ ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) )
11	10	adantl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) ∧ ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) ) → ( 𝑚 ∈ ( 𝑛 ConstPolyMat 𝑟 ) ↦ ( 𝑥 ∈ 𝑛 , 𝑦 ∈ 𝑛 ↦ ( ( coe₁ ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) = ( 𝑚 ∈ 𝑆 ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe₁ ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) )
12		simpl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝑁 ∈ Fin )
13		elex	⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V )
14	13	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝑅 ∈ V )
15	2	ovexi	⊢ 𝑆 ∈ V
16		mptexg	⊢ ( 𝑆 ∈ V → ( 𝑚 ∈ 𝑆 ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe₁ ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) ∈ V )
17	15 16	mp1i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( 𝑚 ∈ 𝑆 ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe₁ ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) ∈ V )
18	4 11 12 14 17	ovmpod	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 cPolyMatToMat 𝑅 ) = ( 𝑚 ∈ 𝑆 ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe₁ ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) )
19	1 18	syl5eq	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝐼 = ( 𝑚 ∈ 𝑆 ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe₁ ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) )