This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )