Metamath Proof Explorer

Theorem submatminr1

Description: If we take a submatrix by removing the row I and column J , then the result is the same on the matrix with row I and column J modified by the minMatR1 operator. (Contributed by Thierry Arnoux, 25-Aug-2020)

Ref Expression
Hypotheses submateq.a 
|- A = ( ( 1 ... N ) Mat R )
submateq.b 
|- B = ( Base ` A )
submateq.n 
|- ( ph -> N e. NN )
submateq.i 
|- ( ph -> I e. ( 1 ... N ) )
submateq.j 
|- ( ph -> J e. ( 1 ... N ) )
submatminr1.r 
|- ( ph -> R e. Ring )
submatminr1.m 
|- ( ph -> M e. B )
submatminr1.e 
|- E = ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J )
Assertion submatminr1 
|- ( ph -> ( I ( subMat1 ` M ) J ) = ( I ( subMat1 ` E ) J ) )

Proof

Step Hyp Ref Expression
1 submateq.a 
 |-  A = ( ( 1 ... N ) Mat R )
2 submateq.b 
 |-  B = ( Base ` A )
3 submateq.n 
 |-  ( ph -> N e. NN )
4 submateq.i 
 |-  ( ph -> I e. ( 1 ... N ) )
5 submateq.j 
 |-  ( ph -> J e. ( 1 ... N ) )
6 submatminr1.r 
 |-  ( ph -> R e. Ring )
7 submatminr1.m 
 |-  ( ph -> M e. B )
8 submatminr1.e 
 |-  E = ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J )
9 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
10 1 2 9 minmar1marrep 
 |-  ( ( R e. Ring /\ M e. B ) -> ( ( ( 1 ... N ) minMatR1 R ) ` M ) = ( M ( ( 1 ... N ) matRRep R ) ( 1r ` R ) ) )
11 6 7 10 syl2anc 
 |-  ( ph -> ( ( ( 1 ... N ) minMatR1 R ) ` M ) = ( M ( ( 1 ... N ) matRRep R ) ( 1r ` R ) ) )
12 11 oveqd 
 |-  ( ph -> ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J ) = ( I ( M ( ( 1 ... N ) matRRep R ) ( 1r ` R ) ) J ) )
13 8 12 syl5eq 
 |-  ( ph -> E = ( I ( M ( ( 1 ... N ) matRRep R ) ( 1r ` R ) ) J ) )
14 eqid 
 |-  ( Base ` R ) = ( Base ` R )
15 14 9 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
16 6 15 syl 
 |-  ( ph -> ( 1r ` R ) e. ( Base ` R ) )
17 1 2 marrepcl 
 |-  ( ( ( R e. Ring /\ M e. B /\ ( 1r ` R ) e. ( Base ` R ) ) /\ ( I e. ( 1 ... N ) /\ J e. ( 1 ... N ) ) ) -> ( I ( M ( ( 1 ... N ) matRRep R ) ( 1r ` R ) ) J ) e. B )
18 6 7 16 4 5 17 syl32anc 
 |-  ( ph -> ( I ( M ( ( 1 ... N ) matRRep R ) ( 1r ` R ) ) J ) e. B )
19 13 18 eqeltrd 
 |-  ( ph -> E e. B )
20 13 3ad2ant1 
 |-  ( ( ph /\ i e. ( ( 1 ... N ) \ { I } ) /\ j e. ( ( 1 ... N ) \ { J } ) ) -> E = ( I ( M ( ( 1 ... N ) matRRep R ) ( 1r ` R ) ) J ) )
21 20 oveqd 
 |-  ( ( ph /\ i e. ( ( 1 ... N ) \ { I } ) /\ j e. ( ( 1 ... N ) \ { J } ) ) -> ( i E j ) = ( i ( I ( M ( ( 1 ... N ) matRRep R ) ( 1r ` R ) ) J ) j ) )
22 7 3ad2ant1 
 |-  ( ( ph /\ i e. ( ( 1 ... N ) \ { I } ) /\ j e. ( ( 1 ... N ) \ { J } ) ) -> M e. B )
23 16 3ad2ant1 
 |-  ( ( ph /\ i e. ( ( 1 ... N ) \ { I } ) /\ j e. ( ( 1 ... N ) \ { J } ) ) -> ( 1r ` R ) e. ( Base ` R ) )
24 4 3ad2ant1 
 |-  ( ( ph /\ i e. ( ( 1 ... N ) \ { I } ) /\ j e. ( ( 1 ... N ) \ { J } ) ) -> I e. ( 1 ... N ) )
25 5 3ad2ant1 
 |-  ( ( ph /\ i e. ( ( 1 ... N ) \ { I } ) /\ j e. ( ( 1 ... N ) \ { J } ) ) -> J e. ( 1 ... N ) )
26 simp2 
 |-  ( ( ph /\ i e. ( ( 1 ... N ) \ { I } ) /\ j e. ( ( 1 ... N ) \ { J } ) ) -> i e. ( ( 1 ... N ) \ { I } ) )
27 26 eldifad 
 |-  ( ( ph /\ i e. ( ( 1 ... N ) \ { I } ) /\ j e. ( ( 1 ... N ) \ { J } ) ) -> i e. ( 1 ... N ) )
28 simp3 
 |-  ( ( ph /\ i e. ( ( 1 ... N ) \ { I } ) /\ j e. ( ( 1 ... N ) \ { J } ) ) -> j e. ( ( 1 ... N ) \ { J } ) )
29 28 eldifad 
 |-  ( ( ph /\ i e. ( ( 1 ... N ) \ { I } ) /\ j e. ( ( 1 ... N ) \ { J } ) ) -> j e. ( 1 ... N ) )
30 eqid 
 |-  ( ( 1 ... N ) matRRep R ) = ( ( 1 ... N ) matRRep R )
31 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
32 1 2 30 31 marrepeval 
 |-  ( ( ( M e. B /\ ( 1r ` R ) e. ( Base ` R ) ) /\ ( I e. ( 1 ... N ) /\ J e. ( 1 ... N ) ) /\ ( i e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) ) -> ( i ( I ( M ( ( 1 ... N ) matRRep R ) ( 1r ` R ) ) J ) j ) = if ( i = I , if ( j = J , ( 1r ` R ) , ( 0g ` R ) ) , ( i M j ) ) )
33 22 23 24 25 27 29 32 syl222anc 
 |-  ( ( ph /\ i e. ( ( 1 ... N ) \ { I } ) /\ j e. ( ( 1 ... N ) \ { J } ) ) -> ( i ( I ( M ( ( 1 ... N ) matRRep R ) ( 1r ` R ) ) J ) j ) = if ( i = I , if ( j = J , ( 1r ` R ) , ( 0g ` R ) ) , ( i M j ) ) )
34 eldifsn 
 |-  ( i e. ( ( 1 ... N ) \ { I } ) <-> ( i e. ( 1 ... N ) /\ i =/= I ) )
35 26 34 sylib 
 |-  ( ( ph /\ i e. ( ( 1 ... N ) \ { I } ) /\ j e. ( ( 1 ... N ) \ { J } ) ) -> ( i e. ( 1 ... N ) /\ i =/= I ) )
36 35 simprd 
 |-  ( ( ph /\ i e. ( ( 1 ... N ) \ { I } ) /\ j e. ( ( 1 ... N ) \ { J } ) ) -> i =/= I )
37 36 neneqd 
 |-  ( ( ph /\ i e. ( ( 1 ... N ) \ { I } ) /\ j e. ( ( 1 ... N ) \ { J } ) ) -> -. i = I )
38 37 iffalsed 
 |-  ( ( ph /\ i e. ( ( 1 ... N ) \ { I } ) /\ j e. ( ( 1 ... N ) \ { J } ) ) -> if ( i = I , if ( j = J , ( 1r ` R ) , ( 0g ` R ) ) , ( i M j ) ) = ( i M j ) )
39 21 33 38 3eqtrrd 
 |-  ( ( ph /\ i e. ( ( 1 ... N ) \ { I } ) /\ j e. ( ( 1 ... N ) \ { J } ) ) -> ( i M j ) = ( i E j ) )
40 1 2 3 4 5 7 19 39 submateq 
 |-  ( ph -> ( I ( subMat1 ` M ) J ) = ( I ( subMat1 ` E ) J ) )