Metamath Proof Explorer

Theorem cpm2mval

Description: The result of an inverse matrix transformation. (Contributed by AV, 12-Nov-2019) (Revised by AV, 14-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		cpm2mfval.i	⊢ 𝐼 = ( 𝑁 cPolyMatToMat 𝑅 )
2		cpm2mfval.s	⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
3	1 2	cpm2mfval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝐼 = ( 𝑚 ∈ 𝑆 ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe₁ ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) )
4	3	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝑆 ) → 𝐼 = ( 𝑚 ∈ 𝑆 ↦ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe₁ ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) )
5		oveq	⊢ ( 𝑚 = 𝑀 → ( 𝑥 𝑚 𝑦 ) = ( 𝑥 𝑀 𝑦 ) )
6	5	fveq2d	⊢ ( 𝑚 = 𝑀 → ( coe₁ ‘ ( 𝑥 𝑚 𝑦 ) ) = ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) )
7	6	fveq1d	⊢ ( 𝑚 = 𝑀 → ( ( coe₁ ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) )
8	7	mpoeq3dv	⊢ ( 𝑚 = 𝑀 → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe₁ ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) )
9	8	adantl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝑆 ) ∧ 𝑚 = 𝑀 ) → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe₁ ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) )
10		simp3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝑆 ) → 𝑀 ∈ 𝑆 )
11		simp1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝑆 ) → 𝑁 ∈ Fin )
12		mpoexga	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ∈ V )
13	11 11 12	syl2anc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝑆 ) → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ∈ V )
14	4 9 10 13	fvmptd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝑆 ) → ( 𝐼 ‘ 𝑀 ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) )