Metamath Proof Explorer

Theorem smadiadetglem1

Description: Lemma 1 for smadiadetg . (Contributed by AV, 13-Feb-2019)

Ref Expression
Hypotheses smadiadet.a 
|- A = ( N Mat R )
smadiadet.b 
|- B = ( Base ` A )
smadiadet.r 
|- R e. CRing
smadiadet.d 
|- D = ( N maDet R )
smadiadet.h 
|- E = ( ( N \ { K } ) maDet R )
Assertion smadiadetglem1 
|- ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( ( K ( M ( N matRRep R ) S ) K ) |` ( ( N \ { K } ) X. N ) ) = ( ( K ( ( N minMatR1 R ) ` M ) K ) |` ( ( N \ { K } ) X. N ) ) )

Proof

Step Hyp Ref Expression
1 smadiadet.a 
 |-  A = ( N Mat R )
2 smadiadet.b 
 |-  B = ( Base ` A )
3 smadiadet.r 
 |-  R e. CRing
4 smadiadet.d 
 |-  D = ( N maDet R )
5 smadiadet.h 
 |-  E = ( ( N \ { K } ) maDet R )
6 mpodifsnif 
 |-  ( i e. ( N \ { K } ) , j e. N |-> if ( i = K , if ( j = K , S , ( 0g ` R ) ) , ( i M j ) ) ) = ( i e. ( N \ { K } ) , j e. N |-> ( i M j ) )
7 mpodifsnif 
 |-  ( i e. ( N \ { K } ) , j e. N |-> if ( i = K , if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) , ( i M j ) ) ) = ( i e. ( N \ { K } ) , j e. N |-> ( i M j ) )
8 6 7 eqtr4i 
 |-  ( i e. ( N \ { K } ) , j e. N |-> if ( i = K , if ( j = K , S , ( 0g ` R ) ) , ( i M j ) ) ) = ( i e. ( N \ { K } ) , j e. N |-> if ( i = K , if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) , ( i M j ) ) )
9 difss 
 |-  ( N \ { K } ) C_ N
10 ssid 
 |-  N C_ N
11 9 10 pm3.2i 
 |-  ( ( N \ { K } ) C_ N /\ N C_ N )
12 resmpo 
 |-  ( ( ( N \ { K } ) C_ N /\ N C_ N ) -> ( ( i e. N , j e. N |-> if ( i = K , if ( j = K , S , ( 0g ` R ) ) , ( i M j ) ) ) |` ( ( N \ { K } ) X. N ) ) = ( i e. ( N \ { K } ) , j e. N |-> if ( i = K , if ( j = K , S , ( 0g ` R ) ) , ( i M j ) ) ) )
13 11 12 mp1i 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( ( i e. N , j e. N |-> if ( i = K , if ( j = K , S , ( 0g ` R ) ) , ( i M j ) ) ) |` ( ( N \ { K } ) X. N ) ) = ( i e. ( N \ { K } ) , j e. N |-> if ( i = K , if ( j = K , S , ( 0g ` R ) ) , ( i M j ) ) ) )
14 resmpo 
 |-  ( ( ( N \ { K } ) C_ N /\ N C_ N ) -> ( ( i e. N , j e. N |-> if ( i = K , if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) , ( i M j ) ) ) |` ( ( N \ { K } ) X. N ) ) = ( i e. ( N \ { K } ) , j e. N |-> if ( i = K , if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) , ( i M j ) ) ) )
15 11 14 mp1i 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( ( i e. N , j e. N |-> if ( i = K , if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) , ( i M j ) ) ) |` ( ( N \ { K } ) X. N ) ) = ( i e. ( N \ { K } ) , j e. N |-> if ( i = K , if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) , ( i M j ) ) ) )
16 8 13 15 3eqtr4a 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( ( i e. N , j e. N |-> if ( i = K , if ( j = K , S , ( 0g ` R ) ) , ( i M j ) ) ) |` ( ( N \ { K } ) X. N ) ) = ( ( i e. N , j e. N |-> if ( i = K , if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) , ( i M j ) ) ) |` ( ( N \ { K } ) X. N ) ) )
17 simp1 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> M e. B )
18 simp3 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> S e. ( Base ` R ) )
19 simp2 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> K e. N )
20 eqid 
 |-  ( N matRRep R ) = ( N matRRep R )
21 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
22 1 2 20 21 marrepval 
 |-  ( ( ( M e. B /\ S e. ( Base ` R ) ) /\ ( K e. N /\ K e. N ) ) -> ( K ( M ( N matRRep R ) S ) K ) = ( i e. N , j e. N |-> if ( i = K , if ( j = K , S , ( 0g ` R ) ) , ( i M j ) ) ) )
23 17 18 19 19 22 syl22anc 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( K ( M ( N matRRep R ) S ) K ) = ( i e. N , j e. N |-> if ( i = K , if ( j = K , S , ( 0g ` R ) ) , ( i M j ) ) ) )
24 23 reseq1d 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( ( K ( M ( N matRRep R ) S ) K ) |` ( ( N \ { K } ) X. N ) ) = ( ( i e. N , j e. N |-> if ( i = K , if ( j = K , S , ( 0g ` R ) ) , ( i M j ) ) ) |` ( ( N \ { K } ) X. N ) ) )
25 crngring 
 |-  ( R e. CRing -> R e. Ring )
26 eqid 
 |-  ( Base ` R ) = ( Base ` R )
27 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
28 26 27 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
29 25 28 syl 
 |-  ( R e. CRing -> ( 1r ` R ) e. ( Base ` R ) )
30 3 29 mp1i 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( 1r ` R ) e. ( Base ` R ) )
31 1 2 20 21 marrepval 
 |-  ( ( ( M e. B /\ ( 1r ` R ) e. ( Base ` R ) ) /\ ( K e. N /\ K e. N ) ) -> ( K ( M ( N matRRep R ) ( 1r ` R ) ) K ) = ( i e. N , j e. N |-> if ( i = K , if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) , ( i M j ) ) ) )
32 17 30 19 19 31 syl22anc 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( K ( M ( N matRRep R ) ( 1r ` R ) ) K ) = ( i e. N , j e. N |-> if ( i = K , if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) , ( i M j ) ) ) )
33 32 reseq1d 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( ( K ( M ( N matRRep R ) ( 1r ` R ) ) K ) |` ( ( N \ { K } ) X. N ) ) = ( ( i e. N , j e. N |-> if ( i = K , if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) , ( i M j ) ) ) |` ( ( N \ { K } ) X. N ) ) )
34 16 24 33 3eqtr4d 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( ( K ( M ( N matRRep R ) S ) K ) |` ( ( N \ { K } ) X. N ) ) = ( ( K ( M ( N matRRep R ) ( 1r ` R ) ) K ) |` ( ( N \ { K } ) X. N ) ) )
35 3 25 ax-mp 
 |-  R e. Ring
36 1 2 27 minmar1marrep 
 |-  ( ( R e. Ring /\ M e. B ) -> ( ( N minMatR1 R ) ` M ) = ( M ( N matRRep R ) ( 1r ` R ) ) )
37 35 17 36 sylancr 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( ( N minMatR1 R ) ` M ) = ( M ( N matRRep R ) ( 1r ` R ) ) )
38 37 eqcomd 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( M ( N matRRep R ) ( 1r ` R ) ) = ( ( N minMatR1 R ) ` M ) )
39 38 oveqd 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( K ( M ( N matRRep R ) ( 1r ` R ) ) K ) = ( K ( ( N minMatR1 R ) ` M ) K ) )
40 39 reseq1d 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( ( K ( M ( N matRRep R ) ( 1r ` R ) ) K ) |` ( ( N \ { K } ) X. N ) ) = ( ( K ( ( N minMatR1 R ) ` M ) K ) |` ( ( N \ { K } ) X. N ) ) )
41 34 40 eqtrd 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( ( K ( M ( N matRRep R ) S ) K ) |` ( ( N \ { K } ) X. N ) ) = ( ( K ( ( N minMatR1 R ) ` M ) K ) |` ( ( N \ { K } ) X. N ) ) )