Metamath Proof Explorer

Theorem submaval

Description: Third 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 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 ) ) )

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 submaval0 
 |-  ( M e. B -> ( Q ` M ) = ( k e. N , l e. N |-> ( i e. ( N \ { k } ) , j e. ( N \ { l } ) |-> ( i M j ) ) ) )
5 4 3ad2ant1 
 |-  ( ( M e. B /\ K e. N /\ L e. N ) -> ( Q ` M ) = ( k e. N , l e. N |-> ( i e. ( N \ { k } ) , j e. ( N \ { l } ) |-> ( i M j ) ) ) )
6 simp2 
 |-  ( ( M e. B /\ K e. N /\ L e. N ) -> K e. N )
7 simpl3 
 |-  ( ( ( M e. B /\ K e. N /\ L e. N ) /\ k = K ) -> L e. N )
8 1 3 matrcl 
 |-  ( M e. B -> ( N e. Fin /\ R e. _V ) )
9 8 simpld 
 |-  ( M e. B -> N e. Fin )
10 diffi 
 |-  ( N e. Fin -> ( N \ { k } ) e. Fin )
11 9 10 syl 
 |-  ( M e. B -> ( N \ { k } ) e. Fin )
12 diffi 
 |-  ( N e. Fin -> ( N \ { l } ) e. Fin )
13 9 12 syl 
 |-  ( M e. B -> ( N \ { l } ) e. Fin )
14 11 13 jca 
 |-  ( M e. B -> ( ( N \ { k } ) e. Fin /\ ( N \ { l } ) e. Fin ) )
15 14 3ad2ant1 
 |-  ( ( M e. B /\ K e. N /\ L e. N ) -> ( ( N \ { k } ) e. Fin /\ ( N \ { l } ) e. Fin ) )
16 15 adantr 
 |-  ( ( ( M e. B /\ K e. N /\ L e. N ) /\ ( k = K /\ l = L ) ) -> ( ( N \ { k } ) e. Fin /\ ( N \ { l } ) e. Fin ) )
17 mpoexga 
 |-  ( ( ( N \ { k } ) e. Fin /\ ( N \ { l } ) e. Fin ) -> ( i e. ( N \ { k } ) , j e. ( N \ { l } ) |-> ( i M j ) ) e. _V )
18 16 17 syl 
 |-  ( ( ( M e. B /\ K e. N /\ L e. N ) /\ ( k = K /\ l = L ) ) -> ( i e. ( N \ { k } ) , j e. ( N \ { l } ) |-> ( i M j ) ) e. _V )
19 sneq 
 |-  ( k = K -> { k } = { K } )
20 19 difeq2d 
 |-  ( k = K -> ( N \ { k } ) = ( N \ { K } ) )
21 20 adantr 
 |-  ( ( k = K /\ l = L ) -> ( N \ { k } ) = ( N \ { K } ) )
22 sneq 
 |-  ( l = L -> { l } = { L } )
23 22 difeq2d 
 |-  ( l = L -> ( N \ { l } ) = ( N \ { L } ) )
24 23 adantl 
 |-  ( ( k = K /\ l = L ) -> ( N \ { l } ) = ( N \ { L } ) )
25 eqidd 
 |-  ( ( k = K /\ l = L ) -> ( i M j ) = ( i M j ) )
26 21 24 25 mpoeq123dv 
 |-  ( ( k = K /\ l = L ) -> ( i e. ( N \ { k } ) , j e. ( N \ { l } ) |-> ( i M j ) ) = ( i e. ( N \ { K } ) , j e. ( N \ { L } ) |-> ( i M j ) ) )
27 26 adantl 
 |-  ( ( ( M e. B /\ K e. N /\ L e. N ) /\ ( k = K /\ l = L ) ) -> ( i e. ( N \ { k } ) , j e. ( N \ { l } ) |-> ( i M j ) ) = ( i e. ( N \ { K } ) , j e. ( N \ { L } ) |-> ( i M j ) ) )
28 6 7 18 27 ovmpodv2 
 |-  ( ( M e. B /\ K e. N /\ L e. N ) -> ( ( Q ` M ) = ( k e. N , l e. N |-> ( i e. ( N \ { k } ) , j e. ( N \ { l } ) |-> ( i M j ) ) ) -> ( K ( Q ` M ) L ) = ( i e. ( N \ { K } ) , j e. ( N \ { L } ) |-> ( i M j ) ) ) )
29 5 28 mpd 
 |-  ( ( M e. B /\ K e. N /\ L e. N ) -> ( K ( Q ` M ) L ) = ( i e. ( N \ { K } ) , j e. ( N \ { L } ) |-> ( i M j ) ) )