Metamath Proof Explorer

Theorem smadiadetglem2

Description: Lemma 2 for smadiadetg . (Contributed by AV, 14-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 )
smadiadetg.x 
|- .x. = ( .r ` R )
Assertion smadiadetglem2 
|- ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( ( K ( M ( N matRRep R ) S ) K ) |` ( { K } X. N ) ) = ( ( ( { K } X. N ) X. { S } ) oF .x. ( ( K ( ( N minMatR1 R ) ` M ) K ) |` ( { 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 smadiadetg.x 
 |-  .x. = ( .r ` R )
7 snex 
 |-  { K } e. _V
8 7 a1i 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> { K } e. _V )
9 1 2 matrcl 
 |-  ( M e. B -> ( N e. Fin /\ R e. _V ) )
10 elex 
 |-  ( N e. Fin -> N e. _V )
11 10 adantr 
 |-  ( ( N e. Fin /\ R e. _V ) -> N e. _V )
12 9 11 syl 
 |-  ( M e. B -> N e. _V )
13 12 3ad2ant1 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> N e. _V )
14 simp13 
 |-  ( ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) /\ i e. { K } /\ j e. N ) -> S e. ( Base ` R ) )
15 crngring 
 |-  ( R e. CRing -> R e. Ring )
16 3 15 mp1i 
 |-  ( ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) /\ i e. { K } /\ j e. N ) -> R e. Ring )
17 eqid 
 |-  ( Base ` R ) = ( Base ` R )
18 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
19 17 18 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
20 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
21 17 20 ring0cl 
 |-  ( R e. Ring -> ( 0g ` R ) e. ( Base ` R ) )
22 19 21 ifcld 
 |-  ( R e. Ring -> if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) e. ( Base ` R ) )
23 16 22 syl 
 |-  ( ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) /\ i e. { K } /\ j e. N ) -> if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) e. ( Base ` R ) )
24 fconstmpo 
 |-  ( ( { K } X. N ) X. { S } ) = ( i e. { K } , j e. N |-> S )
25 24 a1i 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( ( { K } X. N ) X. { S } ) = ( i e. { K } , j e. N |-> S ) )
26 eqidd 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( i e. { K } , j e. N |-> if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) ) = ( i e. { K } , j e. N |-> if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) ) )
27 8 13 14 23 25 26 offval22 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( ( ( { K } X. N ) X. { S } ) oF .x. ( i e. { K } , j e. N |-> if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) ) ) = ( i e. { K } , j e. N |-> ( S .x. if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) ) ) )
28 3 15 mp1i 
 |-  ( S e. ( Base ` R ) -> R e. Ring )
29 17 6 18 ringridm 
 |-  ( ( R e. Ring /\ S e. ( Base ` R ) ) -> ( S .x. ( 1r ` R ) ) = S )
30 28 29 mpancom 
 |-  ( S e. ( Base ` R ) -> ( S .x. ( 1r ` R ) ) = S )
31 30 3ad2ant3 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( S .x. ( 1r ` R ) ) = S )
32 31 ad2antrl 
 |-  ( ( j = K /\ ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) /\ j e. N ) ) -> ( S .x. ( 1r ` R ) ) = S )
33 iftrue 
 |-  ( j = K -> if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) = ( 1r ` R ) )
34 33 adantr 
 |-  ( ( j = K /\ ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) /\ j e. N ) ) -> if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) = ( 1r ` R ) )
35 34 oveq2d 
 |-  ( ( j = K /\ ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) /\ j e. N ) ) -> ( S .x. if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) ) = ( S .x. ( 1r ` R ) ) )
36 iftrue 
 |-  ( j = K -> if ( j = K , S , ( 0g ` R ) ) = S )
37 36 adantr 
 |-  ( ( j = K /\ ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) /\ j e. N ) ) -> if ( j = K , S , ( 0g ` R ) ) = S )
38 32 35 37 3eqtr4d 
 |-  ( ( j = K /\ ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) /\ j e. N ) ) -> ( S .x. if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) ) = if ( j = K , S , ( 0g ` R ) ) )
39 17 6 20 ringrz 
 |-  ( ( R e. Ring /\ S e. ( Base ` R ) ) -> ( S .x. ( 0g ` R ) ) = ( 0g ` R ) )
40 28 39 mpancom 
 |-  ( S e. ( Base ` R ) -> ( S .x. ( 0g ` R ) ) = ( 0g ` R ) )
41 40 3ad2ant3 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( S .x. ( 0g ` R ) ) = ( 0g ` R ) )
42 41 ad2antrl 
 |-  ( ( -. j = K /\ ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) /\ j e. N ) ) -> ( S .x. ( 0g ` R ) ) = ( 0g ` R ) )
43 iffalse 
 |-  ( -. j = K -> if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) = ( 0g ` R ) )
44 43 oveq2d 
 |-  ( -. j = K -> ( S .x. if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) ) = ( S .x. ( 0g ` R ) ) )
45 44 adantr 
 |-  ( ( -. j = K /\ ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) /\ j e. N ) ) -> ( S .x. if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) ) = ( S .x. ( 0g ` R ) ) )
46 iffalse 
 |-  ( -. j = K -> if ( j = K , S , ( 0g ` R ) ) = ( 0g ` R ) )
47 46 adantr 
 |-  ( ( -. j = K /\ ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) /\ j e. N ) ) -> if ( j = K , S , ( 0g ` R ) ) = ( 0g ` R ) )
48 42 45 47 3eqtr4d 
 |-  ( ( -. j = K /\ ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) /\ j e. N ) ) -> ( S .x. if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) ) = if ( j = K , S , ( 0g ` R ) ) )
49 38 48 pm2.61ian 
 |-  ( ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) /\ j e. N ) -> ( S .x. if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) ) = if ( j = K , S , ( 0g ` R ) ) )
50 49 3adant2 
 |-  ( ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) /\ i e. { K } /\ j e. N ) -> ( S .x. if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) ) = if ( j = K , S , ( 0g ` R ) ) )
51 50 mpoeq3dva 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( i e. { K } , j e. N |-> ( S .x. if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) ) ) = ( i e. { K } , j e. N |-> if ( j = K , S , ( 0g ` R ) ) ) )
52 27 51 eqtrd 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( ( ( { K } X. N ) X. { S } ) oF .x. ( i e. { K } , j e. N |-> if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) ) ) = ( i e. { K } , j e. N |-> if ( j = K , S , ( 0g ` R ) ) ) )
53 simp2 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> K e. N )
54 eqid 
 |-  ( N minMatR1 R ) = ( N minMatR1 R )
55 1 2 54 18 20 minmar1val 
 |-  ( ( M e. B /\ K e. N /\ K e. N ) -> ( K ( ( N minMatR1 R ) ` M ) K ) = ( i e. N , j e. N |-> if ( i = K , if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) , ( i M j ) ) ) )
56 53 55 syld3an3 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( K ( ( N minMatR1 R ) ` M ) K ) = ( i e. N , j e. N |-> if ( i = K , if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) , ( i M j ) ) ) )
57 56 reseq1d 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( ( K ( ( N minMatR1 R ) ` M ) K ) |` ( { K } X. N ) ) = ( ( i e. N , j e. N |-> if ( i = K , if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) , ( i M j ) ) ) |` ( { K } X. N ) ) )
58 snssi 
 |-  ( K e. N -> { K } C_ N )
59 58 3ad2ant2 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> { K } C_ N )
60 ssid 
 |-  N C_ N
61 resmpo 
 |-  ( ( { 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 ) ) ) |` ( { K } X. N ) ) = ( i e. { K } , j e. N |-> if ( i = K , if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) , ( i M j ) ) ) )
62 59 60 61 sylancl 
 |-  ( ( 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 ) ) ) |` ( { K } X. N ) ) = ( i e. { K } , j e. N |-> if ( i = K , if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) , ( i M j ) ) ) )
63 mposnif 
 |-  ( i e. { K } , j e. N |-> if ( i = K , if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) , ( i M j ) ) ) = ( i e. { K } , j e. N |-> if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) )
64 63 a1i 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( i e. { K } , j e. N |-> if ( i = K , if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) , ( i M j ) ) ) = ( i e. { K } , j e. N |-> if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) ) )
65 57 62 64 3eqtrd 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( ( K ( ( N minMatR1 R ) ` M ) K ) |` ( { K } X. N ) ) = ( i e. { K } , j e. N |-> if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) ) )
66 65 oveq2d 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( ( ( { K } X. N ) X. { S } ) oF .x. ( ( K ( ( N minMatR1 R ) ` M ) K ) |` ( { K } X. N ) ) ) = ( ( ( { K } X. N ) X. { S } ) oF .x. ( i e. { K } , j e. N |-> if ( j = K , ( 1r ` R ) , ( 0g ` R ) ) ) ) )
67 3simpb 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( M e. B /\ S e. ( Base ` R ) ) )
68 eqid 
 |-  ( N matRRep R ) = ( N matRRep R )
69 1 2 68 20 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 ) ) ) )
70 67 53 53 69 syl12anc 
 |-  ( ( 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 ) ) ) )
71 70 reseq1d 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( ( K ( M ( N matRRep R ) S ) K ) |` ( { K } X. N ) ) = ( ( i e. N , j e. N |-> if ( i = K , if ( j = K , S , ( 0g ` R ) ) , ( i M j ) ) ) |` ( { K } X. N ) ) )
72 resmpo 
 |-  ( ( { K } C_ N /\ N C_ N ) -> ( ( i e. N , j e. N |-> if ( i = K , if ( j = K , S , ( 0g ` R ) ) , ( i M j ) ) ) |` ( { K } X. N ) ) = ( i e. { K } , j e. N |-> if ( i = K , if ( j = K , S , ( 0g ` R ) ) , ( i M j ) ) ) )
73 59 60 72 sylancl 
 |-  ( ( 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 ) ) ) |` ( { K } X. N ) ) = ( i e. { K } , j e. N |-> if ( i = K , if ( j = K , S , ( 0g ` R ) ) , ( i M j ) ) ) )
74 mposnif 
 |-  ( i e. { K } , j e. N |-> if ( i = K , if ( j = K , S , ( 0g ` R ) ) , ( i M j ) ) ) = ( i e. { K } , j e. N |-> if ( j = K , S , ( 0g ` R ) ) )
75 74 a1i 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( i e. { K } , j e. N |-> if ( i = K , if ( j = K , S , ( 0g ` R ) ) , ( i M j ) ) ) = ( i e. { K } , j e. N |-> if ( j = K , S , ( 0g ` R ) ) ) )
76 71 73 75 3eqtrd 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( ( K ( M ( N matRRep R ) S ) K ) |` ( { K } X. N ) ) = ( i e. { K } , j e. N |-> if ( j = K , S , ( 0g ` R ) ) ) )
77 52 66 76 3eqtr4rd 
 |-  ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( ( K ( M ( N matRRep R ) S ) K ) |` ( { K } X. N ) ) = ( ( ( { K } X. N ) X. { S } ) oF .x. ( ( K ( ( N minMatR1 R ) ` M ) K ) |` ( { K } X. N ) ) ) )