Theorem minmar1val0

Description: Second substitution for the definition of a matrix for a minor. (Contributed by AV, 31-Dec-2018)

	Ref	Expression
Hypotheses	minmar1fval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	minmar1fval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	minmar1fval.q	⊢ 𝑄 = ( 𝑁 minMatR1 𝑅 )
	minmar1fval.o	⊢ 1 = ( 1r ‘ 𝑅 )
	minmar1fval.z	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	minmar1val0	⊢ ( 𝑀 ∈ 𝐵 → ( 𝑄 ‘ 𝑀 ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		minmar1fval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		minmar1fval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		minmar1fval.q	⊢ 𝑄 = ( 𝑁 minMatR1 𝑅 )
4		minmar1fval.o	⊢ 1 = ( 1r ‘ 𝑅 )
5		minmar1fval.z	⊢ 0 = ( 0g ‘ 𝑅 )
6	1 2	matrcl	⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
7	6	simpld	⊢ ( 𝑀 ∈ 𝐵 → 𝑁 ∈ Fin )
8		mpoexga	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ) ∈ V )
9	7 7 8	syl2anc	⊢ ( 𝑀 ∈ 𝐵 → ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ) ∈ V )
10		oveq	⊢ ( 𝑚 = 𝑀 → ( 𝑖 𝑚 𝑗 ) = ( 𝑖 𝑀 𝑗 ) )
11	10	ifeq2d	⊢ ( 𝑚 = 𝑀 → if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , 0 ) , ( 𝑖 𝑚 𝑗 ) ) = if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) )
12	11	mpoeq3dv	⊢ ( 𝑚 = 𝑀 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , 0 ) , ( 𝑖 𝑚 𝑗 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) )
13	12	mpoeq3dv	⊢ ( 𝑚 = 𝑀 → ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , 0 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ) )
14	1 2 3 4 5	minmar1fval	⊢ 𝑄 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , 0 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) )
15	13 14	fvmptg	⊢ ( ( 𝑀 ∈ 𝐵 ∧ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ) ∈ V ) → ( 𝑄 ‘ 𝑀 ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ) )
16	9 15	mpdan	⊢ ( 𝑀 ∈ 𝐵 → ( 𝑄 ‘ 𝑀 ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ) )