Theorem submaeval

Description: An entry of a submatrix of a square matrix. (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	submaeval	|- ( ( M e. B /\ ( K e. N /\ L e. N ) /\ ( I e. ( N \ { K } ) /\ J e. ( N \ { L } ) ) ) -> ( I ( K ( Q ` M ) L ) J ) = ( 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 2 3	submaval	|- ( ( M e. B /\ K e. N /\ L e. N ) -> ( K ( Q ` M ) L ) = ( i e. ( N \ { K } ) , j e. ( N \ { L } ) |-> ( i M j ) ) )
5	4	3expb	|- ( ( M e. B /\ ( K e. N /\ L e. N ) ) -> ( K ( Q ` M ) L ) = ( i e. ( N \ { K } ) , j e. ( N \ { L } ) |-> ( i M j ) ) )
6	5	3adant3	|- ( ( M e. B /\ ( K e. N /\ L e. N ) /\ ( I e. ( N \ { K } ) /\ J e. ( N \ { L } ) ) ) -> ( K ( Q ` M ) L ) = ( i e. ( N \ { K } ) , j e. ( N \ { L } ) |-> ( i M j ) ) )
7		simp3l	|- ( ( M e. B /\ ( K e. N /\ L e. N ) /\ ( I e. ( N \ { K } ) /\ J e. ( N \ { L } ) ) ) -> I e. ( N \ { K } ) )
8		simpl3r	|- ( ( ( M e. B /\ ( K e. N /\ L e. N ) /\ ( I e. ( N \ { K } ) /\ J e. ( N \ { L } ) ) ) /\ i = I ) -> J e. ( N \ { L } ) )
9		ovexd	|- ( ( ( M e. B /\ ( K e. N /\ L e. N ) /\ ( I e. ( N \ { K } ) /\ J e. ( N \ { L } ) ) ) /\ ( i = I /\ j = J ) ) -> ( i M j ) e. _V )
10		oveq12	|- ( ( i = I /\ j = J ) -> ( i M j ) = ( I M J ) )
11	10	adantl	|- ( ( ( M e. B /\ ( K e. N /\ L e. N ) /\ ( I e. ( N \ { K } ) /\ J e. ( N \ { L } ) ) ) /\ ( i = I /\ j = J ) ) -> ( i M j ) = ( I M J ) )
12	7 8 9 11	ovmpodv2	|- ( ( M e. B /\ ( K e. N /\ L e. N ) /\ ( I e. ( N \ { K } ) /\ J e. ( N \ { L } ) ) ) -> ( ( K ( Q ` M ) L ) = ( i e. ( N \ { K } ) , j e. ( N \ { L } ) |-> ( i M j ) ) -> ( I ( K ( Q ` M ) L ) J ) = ( I M J ) ) )
13	6 12	mpd	|- ( ( M e. B /\ ( K e. N /\ L e. N ) /\ ( I e. ( N \ { K } ) /\ J e. ( N \ { L } ) ) ) -> ( I ( K ( Q ` M ) L ) J ) = ( I M J ) )