Metamath Proof Explorer

Theorem maducoeval2

Description: An entry of the adjunct (cofactor) matrix. (Contributed by SO, 17-Jul-2018)

Ref Expression
Hypotheses madufval.a 
|- A = ( N Mat R )
madufval.d 
|- D = ( N maDet R )
madufval.j 
|- J = ( N maAdju R )
madufval.b 
|- B = ( Base ` A )
madufval.o 
|- .1. = ( 1r ` R )
madufval.z 
|- .0. = ( 0g ` R )
Assertion maducoeval2 
|- ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) -> ( I ( J ` M ) H ) = ( D ` ( k e. N , l e. N |-> if ( ( k = H \/ l = I ) , if ( ( l = I /\ k = H ) , .1. , .0. ) , ( k M l ) ) ) ) )

Proof

Step Hyp Ref Expression
1 madufval.a 
 |-  A = ( N Mat R )
2 madufval.d 
 |-  D = ( N maDet R )
3 madufval.j 
 |-  J = ( N maAdju R )
4 madufval.b 
 |-  B = ( Base ` A )
5 madufval.o 
 |-  .1. = ( 1r ` R )
6 madufval.z 
 |-  .0. = ( 0g ` R )
7 eleq2 
 |-  ( m = (/) -> ( k e. m <-> k e. (/) ) )
8 7 ifbid 
 |-  ( m = (/) -> if ( k e. m , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) = if ( k e. (/) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) )
9 8 ifeq2d 
 |-  ( m = (/) -> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. m , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) = if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. (/) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) )
10 9 mpoeq3dv 
 |-  ( m = (/) -> ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. m , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) = ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. (/) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) )
11 10 fveq2d 
 |-  ( m = (/) -> ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. m , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. (/) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) )
12 11 eqeq2d 
 |-  ( m = (/) -> ( ( I ( J ` M ) H ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. m , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) <-> ( I ( J ` M ) H ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. (/) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) ) )
13 eleq2 
 |-  ( m = n -> ( k e. m <-> k e. n ) )
14 13 ifbid 
 |-  ( m = n -> if ( k e. m , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) = if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) )
15 14 ifeq2d 
 |-  ( m = n -> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. m , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) = if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) )
16 15 mpoeq3dv 
 |-  ( m = n -> ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. m , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) = ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) )
17 16 fveq2d 
 |-  ( m = n -> ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. m , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) )
18 17 eqeq2d 
 |-  ( m = n -> ( ( I ( J ` M ) H ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. m , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) <-> ( I ( J ` M ) H ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) ) )
19 eleq2 
 |-  ( m = ( n u. { r } ) -> ( k e. m <-> k e. ( n u. { r } ) ) )
20 19 ifbid 
 |-  ( m = ( n u. { r } ) -> if ( k e. m , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) = if ( k e. ( n u. { r } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) )
21 20 ifeq2d 
 |-  ( m = ( n u. { r } ) -> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. m , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) = if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( n u. { r } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) )
22 21 mpoeq3dv 
 |-  ( m = ( n u. { r } ) -> ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. m , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) = ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( n u. { r } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) )
23 22 fveq2d 
 |-  ( m = ( n u. { r } ) -> ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. m , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( n u. { r } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) )
24 23 eqeq2d 
 |-  ( m = ( n u. { r } ) -> ( ( I ( J ` M ) H ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. m , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) <-> ( I ( J ` M ) H ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( n u. { r } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) ) )
25 eleq2 
 |-  ( m = ( N \ { H } ) -> ( k e. m <-> k e. ( N \ { H } ) ) )
26 25 ifbid 
 |-  ( m = ( N \ { H } ) -> if ( k e. m , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) = if ( k e. ( N \ { H } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) )
27 26 ifeq2d 
 |-  ( m = ( N \ { H } ) -> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. m , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) = if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( N \ { H } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) )
28 27 mpoeq3dv 
 |-  ( m = ( N \ { H } ) -> ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. m , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) = ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( N \ { H } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) )
29 28 fveq2d 
 |-  ( m = ( N \ { H } ) -> ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. m , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( N \ { H } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) )
30 29 eqeq2d 
 |-  ( m = ( N \ { H } ) -> ( ( I ( J ` M ) H ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. m , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) <-> ( I ( J ` M ) H ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( N \ { H } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) ) )
31 1 2 3 4 5 6 maducoeval 
 |-  ( ( M e. B /\ I e. N /\ H e. N ) -> ( I ( J ` M ) H ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , ( k M l ) ) ) ) )
32 31 3adant1l 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) -> ( I ( J ` M ) H ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , ( k M l ) ) ) ) )
33 noel 
 |-  -. k e. (/)
34 iffalse 
 |-  ( -. k e. (/) -> if ( k e. (/) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) = ( k M l ) )
35 33 34 mp1i 
 |-  ( ( k e. N /\ l e. N ) -> if ( k e. (/) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) = ( k M l ) )
36 35 ifeq2d 
 |-  ( ( k e. N /\ l e. N ) -> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. (/) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) = if ( k = H , if ( l = I , .1. , .0. ) , ( k M l ) ) )
37 36 mpoeq3ia 
 |-  ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. (/) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) = ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , ( k M l ) ) )
38 37 fveq2i 
 |-  ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. (/) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , ( k M l ) ) ) )
39 32 38 eqtr4di 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) -> ( I ( J ` M ) H ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. (/) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) )
40 eqid 
 |-  ( Base ` R ) = ( Base ` R )
41 eqid 
 |-  ( +g ` R ) = ( +g ` R )
42 eqid 
 |-  ( .r ` R ) = ( .r ` R )
43 simpl1l 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) -> R e. CRing )
44 simp1r 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) -> M e. B )
45 1 4 matrcl 
 |-  ( M e. B -> ( N e. Fin /\ R e. _V ) )
46 45 simpld 
 |-  ( M e. B -> N e. Fin )
47 44 46 syl 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) -> N e. Fin )
48 47 adantr 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) -> N e. Fin )
49 simp1l 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) -> R e. CRing )
50 49 ad2antrr 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ l e. N ) -> R e. CRing )
51 crngring 
 |-  ( R e. CRing -> R e. Ring )
52 50 51 syl 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ l e. N ) -> R e. Ring )
53 40 6 ring0cl 
 |-  ( R e. Ring -> .0. e. ( Base ` R ) )
54 52 53 syl 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ l e. N ) -> .0. e. ( Base ` R ) )
55 simpl1r 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) -> M e. B )
56 1 40 4 matbas2i 
 |-  ( M e. B -> M e. ( ( Base ` R ) ^m ( N X. N ) ) )
57 elmapi 
 |-  ( M e. ( ( Base ` R ) ^m ( N X. N ) ) -> M : ( N X. N ) --> ( Base ` R ) )
58 55 56 57 3syl 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) -> M : ( N X. N ) --> ( Base ` R ) )
59 58 adantr 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ l e. N ) -> M : ( N X. N ) --> ( Base ` R ) )
60 eldifi 
 |-  ( r e. ( ( N \ { H } ) \ n ) -> r e. ( N \ { H } ) )
61 60 ad2antll 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) -> r e. ( N \ { H } ) )
62 61 eldifad 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) -> r e. N )
63 62 adantr 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ l e. N ) -> r e. N )
64 simpr 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ l e. N ) -> l e. N )
65 59 63 64 fovrnd 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ l e. N ) -> ( r M l ) e. ( Base ` R ) )
66 54 65 ifcld 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ l e. N ) -> if ( l = I , .0. , ( r M l ) ) e. ( Base ` R ) )
67 40 5 ringidcl 
 |-  ( R e. Ring -> .1. e. ( Base ` R ) )
68 52 67 syl 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ l e. N ) -> .1. e. ( Base ` R ) )
69 68 54 ifcld 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ l e. N ) -> if ( l = I , .1. , .0. ) e. ( Base ` R ) )
70 54 3adant2 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ k e. N /\ l e. N ) -> .0. e. ( Base ` R ) )
71 58 fovrnda 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ ( k e. N /\ l e. N ) ) -> ( k M l ) e. ( Base ` R ) )
72 71 3impb 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ k e. N /\ l e. N ) -> ( k M l ) e. ( Base ` R ) )
73 70 72 ifcld 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ k e. N /\ l e. N ) -> if ( l = I , .0. , ( k M l ) ) e. ( Base ` R ) )
74 73 72 ifcld 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ k e. N /\ l e. N ) -> if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) e. ( Base ` R ) )
75 simpl2 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) -> I e. N )
76 58 62 75 fovrnd 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) -> ( r M I ) e. ( Base ` R ) )
77 simpl3 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) -> H e. N )
78 eldifsni 
 |-  ( r e. ( N \ { H } ) -> r =/= H )
79 61 78 syl 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) -> r =/= H )
80 2 40 41 42 43 48 66 69 74 76 62 77 79 mdetero 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) -> ( D ` ( k e. N , l e. N |-> if ( k = r , ( if ( l = I , .0. , ( r M l ) ) ( +g ` R ) ( ( r M I ) ( .r ` R ) if ( l = I , .1. , .0. ) ) ) , if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) ) = ( D ` ( k e. N , l e. N |-> if ( k = r , if ( l = I , .0. , ( r M l ) ) , if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) ) )
81 ifnot 
 |-  if ( -. l = I , ( r M l ) , .0. ) = if ( l = I , .0. , ( r M l ) )
82 81 eqcomi 
 |-  if ( l = I , .0. , ( r M l ) ) = if ( -. l = I , ( r M l ) , .0. )
83 82 a1i 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ l e. N ) -> if ( l = I , .0. , ( r M l ) ) = if ( -. l = I , ( r M l ) , .0. ) )
84 ovif2 
 |-  ( ( r M I ) ( .r ` R ) if ( l = I , .1. , .0. ) ) = if ( l = I , ( ( r M I ) ( .r ` R ) .1. ) , ( ( r M I ) ( .r ` R ) .0. ) )
85 76 adantr 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ l e. N ) -> ( r M I ) e. ( Base ` R ) )
86 40 42 5 ringridm 
 |-  ( ( R e. Ring /\ ( r M I ) e. ( Base ` R ) ) -> ( ( r M I ) ( .r ` R ) .1. ) = ( r M I ) )
87 52 85 86 syl2anc 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ l e. N ) -> ( ( r M I ) ( .r ` R ) .1. ) = ( r M I ) )
88 87 adantr 
 |-  ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ l e. N ) /\ l = I ) -> ( ( r M I ) ( .r ` R ) .1. ) = ( r M I ) )
89 oveq2 
 |-  ( l = I -> ( r M l ) = ( r M I ) )
90 89 adantl 
 |-  ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ l e. N ) /\ l = I ) -> ( r M l ) = ( r M I ) )
91 88 90 eqtr4d 
 |-  ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ l e. N ) /\ l = I ) -> ( ( r M I ) ( .r ` R ) .1. ) = ( r M l ) )
92 91 ifeq1da 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ l e. N ) -> if ( l = I , ( ( r M I ) ( .r ` R ) .1. ) , ( ( r M I ) ( .r ` R ) .0. ) ) = if ( l = I , ( r M l ) , ( ( r M I ) ( .r ` R ) .0. ) ) )
93 40 42 6 ringrz 
 |-  ( ( R e. Ring /\ ( r M I ) e. ( Base ` R ) ) -> ( ( r M I ) ( .r ` R ) .0. ) = .0. )
94 52 85 93 syl2anc 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ l e. N ) -> ( ( r M I ) ( .r ` R ) .0. ) = .0. )
95 94 ifeq2d 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ l e. N ) -> if ( l = I , ( r M l ) , ( ( r M I ) ( .r ` R ) .0. ) ) = if ( l = I , ( r M l ) , .0. ) )
96 92 95 eqtrd 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ l e. N ) -> if ( l = I , ( ( r M I ) ( .r ` R ) .1. ) , ( ( r M I ) ( .r ` R ) .0. ) ) = if ( l = I , ( r M l ) , .0. ) )
97 84 96 eqtrid 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ l e. N ) -> ( ( r M I ) ( .r ` R ) if ( l = I , .1. , .0. ) ) = if ( l = I , ( r M l ) , .0. ) )
98 83 97 oveq12d 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ l e. N ) -> ( if ( l = I , .0. , ( r M l ) ) ( +g ` R ) ( ( r M I ) ( .r ` R ) if ( l = I , .1. , .0. ) ) ) = ( if ( -. l = I , ( r M l ) , .0. ) ( +g ` R ) if ( l = I , ( r M l ) , .0. ) ) )
99 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
100 52 99 syl 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ l e. N ) -> R e. Mnd )
101 id 
 |-  ( -. l = I -> -. l = I )
102 imnan 
 |-  ( ( -. l = I -> -. l = I ) <-> -. ( -. l = I /\ l = I ) )
103 101 102 mpbi 
 |-  -. ( -. l = I /\ l = I )
104 103 a1i 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ l e. N ) -> -. ( -. l = I /\ l = I ) )
105 40 6 41 mndifsplit 
 |-  ( ( R e. Mnd /\ ( r M l ) e. ( Base ` R ) /\ -. ( -. l = I /\ l = I ) ) -> if ( ( -. l = I \/ l = I ) , ( r M l ) , .0. ) = ( if ( -. l = I , ( r M l ) , .0. ) ( +g ` R ) if ( l = I , ( r M l ) , .0. ) ) )
106 100 65 104 105 syl3anc 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ l e. N ) -> if ( ( -. l = I \/ l = I ) , ( r M l ) , .0. ) = ( if ( -. l = I , ( r M l ) , .0. ) ( +g ` R ) if ( l = I , ( r M l ) , .0. ) ) )
107 pm2.1 
 |-  ( -. l = I \/ l = I )
108 iftrue 
 |-  ( ( -. l = I \/ l = I ) -> if ( ( -. l = I \/ l = I ) , ( r M l ) , .0. ) = ( r M l ) )
109 107 108 mp1i 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ l e. N ) -> if ( ( -. l = I \/ l = I ) , ( r M l ) , .0. ) = ( r M l ) )
110 98 106 109 3eqtr2d 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ l e. N ) -> ( if ( l = I , .0. , ( r M l ) ) ( +g ` R ) ( ( r M I ) ( .r ` R ) if ( l = I , .1. , .0. ) ) ) = ( r M l ) )
111 110 3adant2 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ k e. N /\ l e. N ) -> ( if ( l = I , .0. , ( r M l ) ) ( +g ` R ) ( ( r M I ) ( .r ` R ) if ( l = I , .1. , .0. ) ) ) = ( r M l ) )
112 oveq1 
 |-  ( k = r -> ( k M l ) = ( r M l ) )
113 112 eqeq2d 
 |-  ( k = r -> ( ( if ( l = I , .0. , ( r M l ) ) ( +g ` R ) ( ( r M I ) ( .r ` R ) if ( l = I , .1. , .0. ) ) ) = ( k M l ) <-> ( if ( l = I , .0. , ( r M l ) ) ( +g ` R ) ( ( r M I ) ( .r ` R ) if ( l = I , .1. , .0. ) ) ) = ( r M l ) ) )
114 111 113 syl5ibrcom 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ k e. N /\ l e. N ) -> ( k = r -> ( if ( l = I , .0. , ( r M l ) ) ( +g ` R ) ( ( r M I ) ( .r ` R ) if ( l = I , .1. , .0. ) ) ) = ( k M l ) ) )
115 114 imp 
 |-  ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ k e. N /\ l e. N ) /\ k = r ) -> ( if ( l = I , .0. , ( r M l ) ) ( +g ` R ) ( ( r M I ) ( .r ` R ) if ( l = I , .1. , .0. ) ) ) = ( k M l ) )
116 iftrue 
 |-  ( k = r -> if ( k = r , ( if ( l = I , .0. , ( r M l ) ) ( +g ` R ) ( ( r M I ) ( .r ` R ) if ( l = I , .1. , .0. ) ) ) , if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) = ( if ( l = I , .0. , ( r M l ) ) ( +g ` R ) ( ( r M I ) ( .r ` R ) if ( l = I , .1. , .0. ) ) ) )
117 116 adantl 
 |-  ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ k e. N /\ l e. N ) /\ k = r ) -> if ( k = r , ( if ( l = I , .0. , ( r M l ) ) ( +g ` R ) ( ( r M I ) ( .r ` R ) if ( l = I , .1. , .0. ) ) ) , if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) = ( if ( l = I , .0. , ( r M l ) ) ( +g ` R ) ( ( r M I ) ( .r ` R ) if ( l = I , .1. , .0. ) ) ) )
118 79 neneqd 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) -> -. r = H )
119 118 3ad2ant1 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ k e. N /\ l e. N ) -> -. r = H )
120 eqeq1 
 |-  ( k = r -> ( k = H <-> r = H ) )
121 120 notbid 
 |-  ( k = r -> ( -. k = H <-> -. r = H ) )
122 119 121 syl5ibrcom 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ k e. N /\ l e. N ) -> ( k = r -> -. k = H ) )
123 122 imp 
 |-  ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ k e. N /\ l e. N ) /\ k = r ) -> -. k = H )
124 123 iffalsed 
 |-  ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ k e. N /\ l e. N ) /\ k = r ) -> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) = if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) )
125 eldifn 
 |-  ( r e. ( ( N \ { H } ) \ n ) -> -. r e. n )
126 125 ad2antll 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) -> -. r e. n )
127 126 3ad2ant1 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ k e. N /\ l e. N ) -> -. r e. n )
128 eleq1w 
 |-  ( k = r -> ( k e. n <-> r e. n ) )
129 128 notbid 
 |-  ( k = r -> ( -. k e. n <-> -. r e. n ) )
130 127 129 syl5ibrcom 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ k e. N /\ l e. N ) -> ( k = r -> -. k e. n ) )
131 130 imp 
 |-  ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ k e. N /\ l e. N ) /\ k = r ) -> -. k e. n )
132 131 iffalsed 
 |-  ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ k e. N /\ l e. N ) /\ k = r ) -> if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) = ( k M l ) )
133 124 132 eqtrd 
 |-  ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ k e. N /\ l e. N ) /\ k = r ) -> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) = ( k M l ) )
134 115 117 133 3eqtr4d 
 |-  ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ k e. N /\ l e. N ) /\ k = r ) -> if ( k = r , ( if ( l = I , .0. , ( r M l ) ) ( +g ` R ) ( ( r M I ) ( .r ` R ) if ( l = I , .1. , .0. ) ) ) , if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) = if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) )
135 iffalse 
 |-  ( -. k = r -> if ( k = r , ( if ( l = I , .0. , ( r M l ) ) ( +g ` R ) ( ( r M I ) ( .r ` R ) if ( l = I , .1. , .0. ) ) ) , if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) = if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) )
136 135 adantl 
 |-  ( ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ k e. N /\ l e. N ) /\ -. k = r ) -> if ( k = r , ( if ( l = I , .0. , ( r M l ) ) ( +g ` R ) ( ( r M I ) ( .r ` R ) if ( l = I , .1. , .0. ) ) ) , if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) = if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) )
137 134 136 pm2.61dan 
 |-  ( ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) /\ k e. N /\ l e. N ) -> if ( k = r , ( if ( l = I , .0. , ( r M l ) ) ( +g ` R ) ( ( r M I ) ( .r ` R ) if ( l = I , .1. , .0. ) ) ) , if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) = if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) )
138 137 mpoeq3dva 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) -> ( k e. N , l e. N |-> if ( k = r , ( if ( l = I , .0. , ( r M l ) ) ( +g ` R ) ( ( r M I ) ( .r ` R ) if ( l = I , .1. , .0. ) ) ) , if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) = ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) )
139 138 fveq2d 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) -> ( D ` ( k e. N , l e. N |-> if ( k = r , ( if ( l = I , .0. , ( r M l ) ) ( +g ` R ) ( ( r M I ) ( .r ` R ) if ( l = I , .1. , .0. ) ) ) , if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) )
140 neeq2 
 |-  ( k = H -> ( r =/= k <-> r =/= H ) )
141 140 biimparc 
 |-  ( ( r =/= H /\ k = H ) -> r =/= k )
142 141 necomd 
 |-  ( ( r =/= H /\ k = H ) -> k =/= r )
143 142 neneqd 
 |-  ( ( r =/= H /\ k = H ) -> -. k = r )
144 143 iffalsed 
 |-  ( ( r =/= H /\ k = H ) -> if ( k = r , if ( l = I , .0. , ( r M l ) ) , if ( l = I , .1. , .0. ) ) = if ( l = I , .1. , .0. ) )
145 iftrue 
 |-  ( k = H -> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) = if ( l = I , .1. , .0. ) )
146 145 adantl 
 |-  ( ( r =/= H /\ k = H ) -> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) = if ( l = I , .1. , .0. ) )
147 146 ifeq2d 
 |-  ( ( r =/= H /\ k = H ) -> if ( k = r , if ( l = I , .0. , ( r M l ) ) , if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) = if ( k = r , if ( l = I , .0. , ( r M l ) ) , if ( l = I , .1. , .0. ) ) )
148 iftrue 
 |-  ( k = H -> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( n u. { r } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) = if ( l = I , .1. , .0. ) )
149 148 adantl 
 |-  ( ( r =/= H /\ k = H ) -> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( n u. { r } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) = if ( l = I , .1. , .0. ) )
150 144 147 149 3eqtr4d 
 |-  ( ( r =/= H /\ k = H ) -> if ( k = r , if ( l = I , .0. , ( r M l ) ) , if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) = if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( n u. { r } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) )
151 112 ifeq2d 
 |-  ( k = r -> if ( l = I , .0. , ( k M l ) ) = if ( l = I , .0. , ( r M l ) ) )
152 vsnid 
 |-  r e. { r }
153 elun2 
 |-  ( r e. { r } -> r e. ( n u. { r } ) )
154 152 153 ax-mp 
 |-  r e. ( n u. { r } )
155 eleq1w 
 |-  ( k = r -> ( k e. ( n u. { r } ) <-> r e. ( n u. { r } ) ) )
156 154 155 mpbiri 
 |-  ( k = r -> k e. ( n u. { r } ) )
157 156 iftrued 
 |-  ( k = r -> if ( k e. ( n u. { r } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) = if ( l = I , .0. , ( k M l ) ) )
158 iftrue 
 |-  ( k = r -> if ( k = r , if ( l = I , .0. , ( r M l ) ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) = if ( l = I , .0. , ( r M l ) ) )
159 151 157 158 3eqtr4rd 
 |-  ( k = r -> if ( k = r , if ( l = I , .0. , ( r M l ) ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) = if ( k e. ( n u. { r } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) )
160 159 adantl 
 |-  ( ( ( r =/= H /\ -. k = H ) /\ k = r ) -> if ( k = r , if ( l = I , .0. , ( r M l ) ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) = if ( k e. ( n u. { r } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) )
161 iffalse 
 |-  ( -. k = r -> if ( k = r , if ( l = I , .0. , ( r M l ) ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) = if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) )
162 orc 
 |-  ( k e. n -> ( k e. n \/ k = r ) )
163 orel2 
 |-  ( -. k = r -> ( ( k e. n \/ k = r ) -> k e. n ) )
164 162 163 impbid2 
 |-  ( -. k = r -> ( k e. n <-> ( k e. n \/ k = r ) ) )
165 elun 
 |-  ( k e. ( n u. { r } ) <-> ( k e. n \/ k e. { r } ) )
166 velsn 
 |-  ( k e. { r } <-> k = r )
167 166 orbi2i 
 |-  ( ( k e. n \/ k e. { r } ) <-> ( k e. n \/ k = r ) )
168 165 167 bitr2i 
 |-  ( ( k e. n \/ k = r ) <-> k e. ( n u. { r } ) )
169 164 168 bitrdi 
 |-  ( -. k = r -> ( k e. n <-> k e. ( n u. { r } ) ) )
170 169 ifbid 
 |-  ( -. k = r -> if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) = if ( k e. ( n u. { r } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) )
171 161 170 eqtrd 
 |-  ( -. k = r -> if ( k = r , if ( l = I , .0. , ( r M l ) ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) = if ( k e. ( n u. { r } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) )
172 171 adantl 
 |-  ( ( ( r =/= H /\ -. k = H ) /\ -. k = r ) -> if ( k = r , if ( l = I , .0. , ( r M l ) ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) = if ( k e. ( n u. { r } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) )
173 160 172 pm2.61dan 
 |-  ( ( r =/= H /\ -. k = H ) -> if ( k = r , if ( l = I , .0. , ( r M l ) ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) = if ( k e. ( n u. { r } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) )
174 iffalse 
 |-  ( -. k = H -> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) = if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) )
175 174 ifeq2d 
 |-  ( -. k = H -> if ( k = r , if ( l = I , .0. , ( r M l ) ) , if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) = if ( k = r , if ( l = I , .0. , ( r M l ) ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) )
176 175 adantl 
 |-  ( ( r =/= H /\ -. k = H ) -> if ( k = r , if ( l = I , .0. , ( r M l ) ) , if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) = if ( k = r , if ( l = I , .0. , ( r M l ) ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) )
177 iffalse 
 |-  ( -. k = H -> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( n u. { r } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) = if ( k e. ( n u. { r } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) )
178 177 adantl 
 |-  ( ( r =/= H /\ -. k = H ) -> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( n u. { r } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) = if ( k e. ( n u. { r } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) )
179 173 176 178 3eqtr4d 
 |-  ( ( r =/= H /\ -. k = H ) -> if ( k = r , if ( l = I , .0. , ( r M l ) ) , if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) = if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( n u. { r } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) )
180 150 179 pm2.61dan 
 |-  ( r =/= H -> if ( k = r , if ( l = I , .0. , ( r M l ) ) , if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) = if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( n u. { r } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) )
181 180 mpoeq3dv 
 |-  ( r =/= H -> ( k e. N , l e. N |-> if ( k = r , if ( l = I , .0. , ( r M l ) ) , if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) = ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( n u. { r } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) )
182 181 fveq2d 
 |-  ( r =/= H -> ( D ` ( k e. N , l e. N |-> if ( k = r , if ( l = I , .0. , ( r M l ) ) , if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( n u. { r } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) )
183 79 182 syl 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) -> ( D ` ( k e. N , l e. N |-> if ( k = r , if ( l = I , .0. , ( r M l ) ) , if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( n u. { r } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) )
184 80 139 183 3eqtr3d 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) -> ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( n u. { r } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) )
185 184 eqeq2d 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) -> ( ( I ( J ` M ) H ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) <-> ( I ( J ` M ) H ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( n u. { r } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) ) )
186 185 biimpd 
 |-  ( ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) /\ ( n C_ ( N \ { H } ) /\ r e. ( ( N \ { H } ) \ n ) ) ) -> ( ( I ( J ` M ) H ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. n , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) -> ( I ( J ` M ) H ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( n u. { r } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) ) )
187 difss 
 |-  ( N \ { H } ) C_ N
188 ssfi 
 |-  ( ( N e. Fin /\ ( N \ { H } ) C_ N ) -> ( N \ { H } ) e. Fin )
189 47 187 188 sylancl 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) -> ( N \ { H } ) e. Fin )
190 12 18 24 30 39 186 189 findcard2d 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) -> ( I ( J ` M ) H ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( N \ { H } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) )
191 iba 
 |-  ( k = H -> ( l = I <-> ( l = I /\ k = H ) ) )
192 191 ifbid 
 |-  ( k = H -> if ( l = I , .1. , .0. ) = if ( ( l = I /\ k = H ) , .1. , .0. ) )
193 iftrue 
 |-  ( k = H -> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( N \ { H } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) = if ( l = I , .1. , .0. ) )
194 iftrue 
 |-  ( ( k = H \/ l = I ) -> if ( ( k = H \/ l = I ) , if ( ( l = I /\ k = H ) , .1. , .0. ) , ( k M l ) ) = if ( ( l = I /\ k = H ) , .1. , .0. ) )
195 194 orcs 
 |-  ( k = H -> if ( ( k = H \/ l = I ) , if ( ( l = I /\ k = H ) , .1. , .0. ) , ( k M l ) ) = if ( ( l = I /\ k = H ) , .1. , .0. ) )
196 192 193 195 3eqtr4d 
 |-  ( k = H -> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( N \ { H } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) = if ( ( k = H \/ l = I ) , if ( ( l = I /\ k = H ) , .1. , .0. ) , ( k M l ) ) )
197 196 adantl 
 |-  ( ( ( k e. N /\ l e. N ) /\ k = H ) -> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( N \ { H } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) = if ( ( k = H \/ l = I ) , if ( ( l = I /\ k = H ) , .1. , .0. ) , ( k M l ) ) )
198 iffalse 
 |-  ( -. k = H -> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( N \ { H } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) = if ( k e. ( N \ { H } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) )
199 198 adantl 
 |-  ( ( ( k e. N /\ l e. N ) /\ -. k = H ) -> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( N \ { H } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) = if ( k e. ( N \ { H } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) )
200 neqne 
 |-  ( -. k = H -> k =/= H )
201 200 anim2i 
 |-  ( ( k e. N /\ -. k = H ) -> ( k e. N /\ k =/= H ) )
202 201 adantlr 
 |-  ( ( ( k e. N /\ l e. N ) /\ -. k = H ) -> ( k e. N /\ k =/= H ) )
203 eldifsn 
 |-  ( k e. ( N \ { H } ) <-> ( k e. N /\ k =/= H ) )
204 202 203 sylibr 
 |-  ( ( ( k e. N /\ l e. N ) /\ -. k = H ) -> k e. ( N \ { H } ) )
205 204 iftrued 
 |-  ( ( ( k e. N /\ l e. N ) /\ -. k = H ) -> if ( k e. ( N \ { H } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) = if ( l = I , .0. , ( k M l ) ) )
206 biorf 
 |-  ( -. k = H -> ( l = I <-> ( k = H \/ l = I ) ) )
207 id 
 |-  ( -. k = H -> -. k = H )
208 207 intnand 
 |-  ( -. k = H -> -. ( l = I /\ k = H ) )
209 208 iffalsed 
 |-  ( -. k = H -> if ( ( l = I /\ k = H ) , .1. , .0. ) = .0. )
210 209 eqcomd 
 |-  ( -. k = H -> .0. = if ( ( l = I /\ k = H ) , .1. , .0. ) )
211 206 210 ifbieq1d 
 |-  ( -. k = H -> if ( l = I , .0. , ( k M l ) ) = if ( ( k = H \/ l = I ) , if ( ( l = I /\ k = H ) , .1. , .0. ) , ( k M l ) ) )
212 211 adantl 
 |-  ( ( ( k e. N /\ l e. N ) /\ -. k = H ) -> if ( l = I , .0. , ( k M l ) ) = if ( ( k = H \/ l = I ) , if ( ( l = I /\ k = H ) , .1. , .0. ) , ( k M l ) ) )
213 199 205 212 3eqtrd 
 |-  ( ( ( k e. N /\ l e. N ) /\ -. k = H ) -> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( N \ { H } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) = if ( ( k = H \/ l = I ) , if ( ( l = I /\ k = H ) , .1. , .0. ) , ( k M l ) ) )
214 197 213 pm2.61dan 
 |-  ( ( k e. N /\ l e. N ) -> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( N \ { H } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) = if ( ( k = H \/ l = I ) , if ( ( l = I /\ k = H ) , .1. , .0. ) , ( k M l ) ) )
215 214 mpoeq3ia 
 |-  ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( N \ { H } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) = ( k e. N , l e. N |-> if ( ( k = H \/ l = I ) , if ( ( l = I /\ k = H ) , .1. , .0. ) , ( k M l ) ) )
216 215 fveq2i 
 |-  ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , if ( k e. ( N \ { H } ) , if ( l = I , .0. , ( k M l ) ) , ( k M l ) ) ) ) ) = ( D ` ( k e. N , l e. N |-> if ( ( k = H \/ l = I ) , if ( ( l = I /\ k = H ) , .1. , .0. ) , ( k M l ) ) ) )
217 190 216 eqtrdi 
 |-  ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) -> ( I ( J ` M ) H ) = ( D ` ( k e. N , l e. N |-> if ( ( k = H \/ l = I ) , if ( ( l = I /\ k = H ) , .1. , .0. ) , ( k M l ) ) ) ) )