Theorem submaval0

Description: Second substitution for a submatrix. (Contributed by AV, 28-Dec-2018)

	Ref	Expression
Hypotheses	submafval.a	|- A = ( N Mat R )
	submafval.q	|- Q = ( N subMat R )
	submafval.b	|- B = ( Base ` A )
Assertion	submaval0	|- ( M e. B -> ( Q ` M ) = ( k e. N , l e. N |-> ( i e. ( N \ { k } ) , j e. ( N \ { l } ) |-> ( i M j ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		submafval.a	|- A = ( N Mat R )
2		submafval.q	|- Q = ( N subMat R )
3		submafval.b	|- B = ( Base ` A )
4	1 3	matrcl	|- ( M e. B -> ( N e. Fin /\ R e. _V ) )
5	4	simpld	|- ( M e. B -> N e. Fin )
6		mpoexga	|- ( ( N e. Fin /\ N e. Fin ) -> ( k e. N , l e. N |-> ( i e. ( N \ { k } ) , j e. ( N \ { l } ) |-> ( i M j ) ) ) e. _V )
7	5 5 6	syl2anc	|- ( M e. B -> ( k e. N , l e. N |-> ( i e. ( N \ { k } ) , j e. ( N \ { l } ) |-> ( i M j ) ) ) e. _V )
8		oveq	|- ( m = M -> ( i m j ) = ( i M j ) )
9	8	mpoeq3dv	|- ( m = M -> ( i e. ( N \ { k } ) , j e. ( N \ { l } ) |-> ( i m j ) ) = ( i e. ( N \ { k } ) , j e. ( N \ { l } ) |-> ( i M j ) ) )
10	9	mpoeq3dv	|- ( m = M -> ( k e. N , l e. N |-> ( i e. ( N \ { k } ) , j e. ( N \ { l } ) |-> ( i m j ) ) ) = ( k e. N , l e. N |-> ( i e. ( N \ { k } ) , j e. ( N \ { l } ) |-> ( i M j ) ) ) )
11	1 2 3	submafval	|- Q = ( m e. B |-> ( k e. N , l e. N |-> ( i e. ( N \ { k } ) , j e. ( N \ { l } ) |-> ( i m j ) ) ) )
12	10 11	fvmptg	|- ( ( M e. B /\ ( k e. N , l e. N |-> ( i e. ( N \ { k } ) , j e. ( N \ { l } ) |-> ( i M j ) ) ) e. _V ) -> ( Q ` M ) = ( k e. N , l e. N |-> ( i e. ( N \ { k } ) , j e. ( N \ { l } ) |-> ( i M j ) ) ) )
13	7 12	mpdan	|- ( M e. B -> ( Q ` M ) = ( k e. N , l e. N |-> ( i e. ( N \ { k } ) , j e. ( N \ { l } ) |-> ( i M j ) ) ) )