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 ˙ = 1 R
madufval.z 0 ˙ = 0 R
Assertion maducoeval2 R CRing M B I N H N I J M H = D k N , l 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 ˙ = 1 R
6 madufval.z 0 ˙ = 0 R
7 eleq2 m = k m k
8 7 ifbid m = if k m if l = I 0 ˙ k M l k M l = if k if l = I 0 ˙ k M l k M l
9 8 ifeq2d m = if k = H if l = I 1 ˙ 0 ˙ if k m if l = I 0 ˙ k M l k M l = if k = H if l = I 1 ˙ 0 ˙ if k if l = I 0 ˙ k M l k M l
10 9 mpoeq3dv m = k N , l N if k = H if l = I 1 ˙ 0 ˙ if k m if l = I 0 ˙ k M l k M l = k N , l N if k = H if l = I 1 ˙ 0 ˙ if k if l = I 0 ˙ k M l k M l
11 10 fveq2d m = D k N , l N if k = H if l = I 1 ˙ 0 ˙ if k m if l = I 0 ˙ k M l k M l = D k N , l N if k = H if l = I 1 ˙ 0 ˙ if k if l = I 0 ˙ k M l k M l
12 11 eqeq2d m = I J M H = D k N , l N if k = H if l = I 1 ˙ 0 ˙ if k m if l = I 0 ˙ k M l k M l I J M H = D k N , l N if k = H if l = I 1 ˙ 0 ˙ if k if l = I 0 ˙ k M l k M l
13 eleq2 m = n k m k n
14 13 ifbid m = n if k m if l = I 0 ˙ k M l k M l = if k 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 m if l = I 0 ˙ k M l k M l = if k = H if l = I 1 ˙ 0 ˙ if k n if l = I 0 ˙ k M l k M l
16 15 mpoeq3dv m = n k N , l N if k = H if l = I 1 ˙ 0 ˙ if k m if l = I 0 ˙ k M l k M l = k N , l N if k = H if l = I 1 ˙ 0 ˙ if k n if l = I 0 ˙ k M l k M l
17 16 fveq2d m = n D k N , l N if k = H if l = I 1 ˙ 0 ˙ if k m if l = I 0 ˙ k M l k M l = D k N , l N if k = H if l = I 1 ˙ 0 ˙ if k n if l = I 0 ˙ k M l k M l
18 17 eqeq2d m = n I J M H = D k N , l N if k = H if l = I 1 ˙ 0 ˙ if k m if l = I 0 ˙ k M l k M l I J M H = D k N , l N if k = H if l = I 1 ˙ 0 ˙ if k n if l = I 0 ˙ k M l k M l
19 eleq2 m = n r k m k n r
20 19 ifbid m = n r if k m if l = I 0 ˙ k M l k M l = if k n r if l = I 0 ˙ k M l k M l
21 20 ifeq2d m = n r if k = H if l = I 1 ˙ 0 ˙ if k m if l = I 0 ˙ k M l k M l = if k = H if l = I 1 ˙ 0 ˙ if k n r if l = I 0 ˙ k M l k M l
22 21 mpoeq3dv m = n r k N , l N if k = H if l = I 1 ˙ 0 ˙ if k m if l = I 0 ˙ k M l k M l = k N , l N if k = H if l = I 1 ˙ 0 ˙ if k n r if l = I 0 ˙ k M l k M l
23 22 fveq2d m = n r D k N , l N if k = H if l = I 1 ˙ 0 ˙ if k m if l = I 0 ˙ k M l k M l = D k N , l N if k = H if l = I 1 ˙ 0 ˙ if k n r if l = I 0 ˙ k M l k M l
24 23 eqeq2d m = n r I J M H = D k N , l N if k = H if l = I 1 ˙ 0 ˙ if k m if l = I 0 ˙ k M l k M l I J M H = D k N , l N if k = H if l = I 1 ˙ 0 ˙ if k n r if l = I 0 ˙ k M l k M l
25 eleq2 m = N H k m k N H
26 25 ifbid m = N H if k m if l = I 0 ˙ k M l k M l = if k 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 m if l = I 0 ˙ k M l k M l = if k = H if l = I 1 ˙ 0 ˙ if k N H if l = I 0 ˙ k M l k M l
28 27 mpoeq3dv m = N H k N , l N if k = H if l = I 1 ˙ 0 ˙ if k m if l = I 0 ˙ k M l k M l = k N , l N if k = H if l = I 1 ˙ 0 ˙ if k N H if l = I 0 ˙ k M l k M l
29 28 fveq2d m = N H D k N , l N if k = H if l = I 1 ˙ 0 ˙ if k m if l = I 0 ˙ k M l k M l = D k N , l N if k = H if l = I 1 ˙ 0 ˙ if k N H if l = I 0 ˙ k M l k M l
30 29 eqeq2d m = N H I J M H = D k N , l N if k = H if l = I 1 ˙ 0 ˙ if k m if l = I 0 ˙ k M l k M l I J M H = D k N , l N if k = H if l = I 1 ˙ 0 ˙ if k N H if l = I 0 ˙ k M l k M l
31 1 2 3 4 5 6 maducoeval M B I N H N I J M H = D k N , l N if k = H if l = I 1 ˙ 0 ˙ k M l
32 31 3adant1l R CRing M B I N H N I J M H = D k N , l N if k = H if l = I 1 ˙ 0 ˙ k M l
33 noel ¬ k
34 iffalse ¬ k if k if l = I 0 ˙ k M l k M l = k M l
35 33 34 mp1i k N l N if k if l = I 0 ˙ k M l k M l = k M l
36 35 ifeq2d k N l N if k = H if l = I 1 ˙ 0 ˙ if k 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 N , l N if k = H if l = I 1 ˙ 0 ˙ if k if l = I 0 ˙ k M l k M l = k N , l N if k = H if l = I 1 ˙ 0 ˙ k M l
38 37 fveq2i D k N , l N if k = H if l = I 1 ˙ 0 ˙ if k if l = I 0 ˙ k M l k M l = D k N , l N if k = H if l = I 1 ˙ 0 ˙ k M l
39 32 38 eqtr4di R CRing M B I N H N I J M H = D k N , l N if k = H if l = I 1 ˙ 0 ˙ if k if l = I 0 ˙ k M l k M l
40 eqid Base R = Base R
41 eqid + R = + R
42 eqid R = R
43 simpl1l R CRing M B I N H N n N H r N H n R CRing
44 simp1r R CRing M B I N H N M B
45 1 4 matrcl M B N Fin R V
46 45 simpld M B N Fin
47 44 46 syl R CRing M B I N H N N Fin
48 47 adantr R CRing M B I N H N n N H r N H n N Fin
49 simp1l R CRing M B I N H N R CRing
50 49 ad2antrr R CRing M B I N H N n N H r N H n l N R CRing
51 crngring R CRing R Ring
52 50 51 syl R CRing M B I N H N n N H r N H n l N R Ring
53 40 6 ring0cl R Ring 0 ˙ Base R
54 52 53 syl R CRing M B I N H N n N H r N H n l N 0 ˙ Base R
55 simpl1r R CRing M B I N H N n N H r N H n M B
56 1 40 4 matbas2i M B M Base R N × N
57 elmapi M Base R N × N M : N × N Base R
58 55 56 57 3syl R CRing M B I N H N n N H r N H n M : N × N Base R
59 58 adantr R CRing M B I N H N n N H r N H n l N M : N × N Base R
60 eldifi r N H n r N H
61 60 ad2antll R CRing M B I N H N n N H r N H n r N H
62 61 eldifad R CRing M B I N H N n N H r N H n r N
63 62 adantr R CRing M B I N H N n N H r N H n l N r N
64 simpr R CRing M B I N H N n N H r N H n l N l N
65 59 63 64 fovrnd R CRing M B I N H N n N H r N H n l N r M l Base R
66 54 65 ifcld R CRing M B I N H N n N H r N H n l N if l = I 0 ˙ r M l Base R
67 40 5 ringidcl R Ring 1 ˙ Base R
68 52 67 syl R CRing M B I N H N n N H r N H n l N 1 ˙ Base R
69 68 54 ifcld R CRing M B I N H N n N H r N H n l N if l = I 1 ˙ 0 ˙ Base R
70 54 3adant2 R CRing M B I N H N n N H r N H n k N l N 0 ˙ Base R
71 58 fovrnda R CRing M B I N H N n N H r N H n k N l N k M l Base R
72 71 3impb R CRing M B I N H N n N H r N H n k N l N k M l Base R
73 70 72 ifcld R CRing M B I N H N n N H r N H n k N l N if l = I 0 ˙ k M l Base R
74 73 72 ifcld R CRing M B I N H N n N H r N H n k N l N if k n if l = I 0 ˙ k M l k M l Base R
75 simpl2 R CRing M B I N H N n N H r N H n I N
76 58 62 75 fovrnd R CRing M B I N H N n N H r N H n r M I Base R
77 simpl3 R CRing M B I N H N n N H r N H n H N
78 eldifsni r N H r H
79 61 78 syl R CRing M B I N H N n N H r N H n r H
80 2 40 41 42 43 48 66 69 74 76 62 77 79 mdetero R CRing M B I N H N n N H r N H n D k N , l N if k = r if l = I 0 ˙ r M l + R r M I R if l = I 1 ˙ 0 ˙ if k = H if l = I 1 ˙ 0 ˙ if k n if l = I 0 ˙ k M l k M l = D k N , l N if k = r if l = I 0 ˙ r M l if k = H if l = I 1 ˙ 0 ˙ if k 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 CRing M B I N H N n N H r N H n l N if l = I 0 ˙ r M l = if ¬ l = I r M l 0 ˙
84 ovif2 r M I R if l = I 1 ˙ 0 ˙ = if l = I r M I R 1 ˙ r M I R 0 ˙
85 76 adantr R CRing M B I N H N n N H r N H n l N r M I Base R
86 40 42 5 ringridm R Ring r M I Base R r M I R 1 ˙ = r M I
87 52 85 86 syl2anc R CRing M B I N H N n N H r N H n l N r M I R 1 ˙ = r M I
88 87 adantr R CRing M B I N H N n N H r N H n l N l = I r M I R 1 ˙ = r M I
89 oveq2 l = I r M l = r M I
90 89 adantl R CRing M B I N H N n N H r N H n l N l = I r M l = r M I
91 88 90 eqtr4d R CRing M B I N H N n N H r N H n l N l = I r M I R 1 ˙ = r M l
92 91 ifeq1da R CRing M B I N H N n N H r N H n l N if l = I r M I R 1 ˙ r M I R 0 ˙ = if l = I r M l r M I R 0 ˙
93 40 42 6 ringrz R Ring r M I Base R r M I R 0 ˙ = 0 ˙
94 52 85 93 syl2anc R CRing M B I N H N n N H r N H n l N r M I R 0 ˙ = 0 ˙
95 94 ifeq2d R CRing M B I N H N n N H r N H n l N if l = I r M l r M I R 0 ˙ = if l = I r M l 0 ˙
96 92 95 eqtrd R CRing M B I N H N n N H r N H n l N if l = I r M I R 1 ˙ r M I R 0 ˙ = if l = I r M l 0 ˙
97 84 96 syl5eq R CRing M B I N H N n N H r N H n l N r M I R if l = I 1 ˙ 0 ˙ = if l = I r M l 0 ˙
98 83 97 oveq12d R CRing M B I N H N n N H r N H n l N if l = I 0 ˙ r M l + R r M I R if l = I 1 ˙ 0 ˙ = if ¬ l = I r M l 0 ˙ + R if l = I r M l 0 ˙
99 ringmnd R Ring R Mnd
100 52 99 syl R CRing M B I N H N n N H r N H n l N R 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 CRing M B I N H N n N H r N H n l N ¬ ¬ l = I l = I
105 40 6 41 mndifsplit R Mnd r M l Base R ¬ ¬ l = I l = I if ¬ l = I l = I r M l 0 ˙ = if ¬ l = I r M l 0 ˙ + R if l = I r M l 0 ˙
106 100 65 104 105 syl3anc R CRing M B I N H N n N H r N H n l N if ¬ l = I l = I r M l 0 ˙ = if ¬ l = I r M l 0 ˙ + 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 CRing M B I N H N n N H r N H n l N if ¬ l = I l = I r M l 0 ˙ = r M l
110 98 106 109 3eqtr2d R CRing M B I N H N n N H r N H n l N if l = I 0 ˙ r M l + R r M I R if l = I 1 ˙ 0 ˙ = r M l
111 110 3adant2 R CRing M B I N H N n N H r N H n k N l N if l = I 0 ˙ r M l + R r M I 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 + R r M I R if l = I 1 ˙ 0 ˙ = k M l if l = I 0 ˙ r M l + R r M I R if l = I 1 ˙ 0 ˙ = r M l
114 111 113 syl5ibrcom R CRing M B I N H N n N H r N H n k N l N k = r if l = I 0 ˙ r M l + R r M I R if l = I 1 ˙ 0 ˙ = k M l
115 114 imp R CRing M B I N H N n N H r N H n k N l N k = r if l = I 0 ˙ r M l + R r M I R if l = I 1 ˙ 0 ˙ = k M l
116 iftrue k = r if k = r if l = I 0 ˙ r M l + R r M I R if l = I 1 ˙ 0 ˙ if k = H if l = I 1 ˙ 0 ˙ if k n if l = I 0 ˙ k M l k M l = if l = I 0 ˙ r M l + R r M I R if l = I 1 ˙ 0 ˙
117 116 adantl R CRing M B I N H N n N H r N H n k N l N k = r if k = r if l = I 0 ˙ r M l + R r M I R if l = I 1 ˙ 0 ˙ if k = H if l = I 1 ˙ 0 ˙ if k n if l = I 0 ˙ k M l k M l = if l = I 0 ˙ r M l + R r M I R if l = I 1 ˙ 0 ˙
118 79 neneqd R CRing M B I N H N n N H r N H n ¬ r = H
119 118 3ad2ant1 R CRing M B I N H N n N H r N H n k N l 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 CRing M B I N H N n N H r N H n k N l N k = r ¬ k = H
123 122 imp R CRing M B I N H N n N H r N H n k N l N k = r ¬ k = H
124 123 iffalsed R CRing M B I N H N n N H r N H n k N l N k = r if k = H if l = I 1 ˙ 0 ˙ if k n if l = I 0 ˙ k M l k M l = if k n if l = I 0 ˙ k M l k M l
125 eldifn r N H n ¬ r n
126 125 ad2antll R CRing M B I N H N n N H r N H n ¬ r n
127 126 3ad2ant1 R CRing M B I N H N n N H r N H n k N l N ¬ r n
128 eleq1w k = r k n r n
129 128 notbid k = r ¬ k n ¬ r n
130 127 129 syl5ibrcom R CRing M B I N H N n N H r N H n k N l N k = r ¬ k n
131 130 imp R CRing M B I N H N n N H r N H n k N l N k = r ¬ k n
132 131 iffalsed R CRing M B I N H N n N H r N H n k N l N k = r if k n if l = I 0 ˙ k M l k M l = k M l
133 124 132 eqtrd R CRing M B I N H N n N H r N H n k N l N k = r if k = H if l = I 1 ˙ 0 ˙ if k n if l = I 0 ˙ k M l k M l = k M l
134 115 117 133 3eqtr4d R CRing M B I N H N n N H r N H n k N l N k = r if k = r if l = I 0 ˙ r M l + R r M I R if l = I 1 ˙ 0 ˙ if k = H if l = I 1 ˙ 0 ˙ if k n if l = I 0 ˙ k M l k M l = if k = H if l = I 1 ˙ 0 ˙ if k 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 + R r M I R if l = I 1 ˙ 0 ˙ if k = H if l = I 1 ˙ 0 ˙ if k n if l = I 0 ˙ k M l k M l = if k = H if l = I 1 ˙ 0 ˙ if k n if l = I 0 ˙ k M l k M l
136 135 adantl R CRing M B I N H N n N H r N H n k N l N ¬ k = r if k = r if l = I 0 ˙ r M l + R r M I R if l = I 1 ˙ 0 ˙ if k = H if l = I 1 ˙ 0 ˙ if k n if l = I 0 ˙ k M l k M l = if k = H if l = I 1 ˙ 0 ˙ if k n if l = I 0 ˙ k M l k M l
137 134 136 pm2.61dan R CRing M B I N H N n N H r N H n k N l N if k = r if l = I 0 ˙ r M l + R r M I R if l = I 1 ˙ 0 ˙ if k = H if l = I 1 ˙ 0 ˙ if k n if l = I 0 ˙ k M l k M l = if k = H if l = I 1 ˙ 0 ˙ if k n if l = I 0 ˙ k M l k M l
138 137 mpoeq3dva R CRing M B I N H N n N H r N H n k N , l N if k = r if l = I 0 ˙ r M l + R r M I R if l = I 1 ˙ 0 ˙ if k = H if l = I 1 ˙ 0 ˙ if k n if l = I 0 ˙ k M l k M l = k N , l N if k = H if l = I 1 ˙ 0 ˙ if k n if l = I 0 ˙ k M l k M l
139 138 fveq2d R CRing M B I N H N n N H r N H n D k N , l N if k = r if l = I 0 ˙ r M l + R r M I R if l = I 1 ˙ 0 ˙ if k = H if l = I 1 ˙ 0 ˙ if k n if l = I 0 ˙ k M l k M l = D k N , l N if k = H if l = I 1 ˙ 0 ˙ if k 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 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 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 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 n 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 n 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 n if l = I 0 ˙ k M l k M l = if k = H if l = I 1 ˙ 0 ˙ if k n 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 r
153 elun2 r r r n r
154 152 153 ax-mp r n r
155 eleq1w k = r k n r r n r
156 154 155 mpbiri k = r k n r
157 156 iftrued k = r if k n 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 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 n if l = I 0 ˙ k M l k M l = if k n 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 n if l = I 0 ˙ k M l k M l = if k n 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 n if l = I 0 ˙ k M l k M l = if k n if l = I 0 ˙ k M l k M l
162 orc k n k n k = r
163 orel2 ¬ k = r k n k = r k n
164 162 163 impbid2 ¬ k = r k n k n k = r
165 elun k n r k n k r
166 velsn k r k = r
167 166 orbi2i k n k r k n k = r
168 165 167 bitr2i k n k = r k n r
169 164 168 bitrdi ¬ k = r k n k n r
170 169 ifbid ¬ k = r if k n if l = I 0 ˙ k M l k M l = if k n 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 n if l = I 0 ˙ k M l k M l = if k n 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 n if l = I 0 ˙ k M l k M l = if k n 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 n if l = I 0 ˙ k M l k M l = if k n 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 n if l = I 0 ˙ k M l k M l = if k 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 n if l = I 0 ˙ k M l k M l = if k = r if l = I 0 ˙ r M l if k 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 n if l = I 0 ˙ k M l k M l = if k = r if l = I 0 ˙ r M l if k 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 n r if l = I 0 ˙ k M l k M l = if k n 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 n r if l = I 0 ˙ k M l k M l = if k n 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 n if l = I 0 ˙ k M l k M l = if k = H if l = I 1 ˙ 0 ˙ if k n 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 n if l = I 0 ˙ k M l k M l = if k = H if l = I 1 ˙ 0 ˙ if k n r if l = I 0 ˙ k M l k M l
181 180 mpoeq3dv r H k N , l N if k = r if l = I 0 ˙ r M l if k = H if l = I 1 ˙ 0 ˙ if k n if l = I 0 ˙ k M l k M l = k N , l N if k = H if l = I 1 ˙ 0 ˙ if k n r if l = I 0 ˙ k M l k M l
182 181 fveq2d r H D k N , l N if k = r if l = I 0 ˙ r M l if k = H if l = I 1 ˙ 0 ˙ if k n if l = I 0 ˙ k M l k M l = D k N , l N if k = H if l = I 1 ˙ 0 ˙ if k n r if l = I 0 ˙ k M l k M l
183 79 182 syl R CRing M B I N H N n N H r N H n D k N , l N if k = r if l = I 0 ˙ r M l if k = H if l = I 1 ˙ 0 ˙ if k n if l = I 0 ˙ k M l k M l = D k N , l N if k = H if l = I 1 ˙ 0 ˙ if k n r if l = I 0 ˙ k M l k M l
184 80 139 183 3eqtr3d R CRing M B I N H N n N H r N H n D k N , l N if k = H if l = I 1 ˙ 0 ˙ if k n if l = I 0 ˙ k M l k M l = D k N , l N if k = H if l = I 1 ˙ 0 ˙ if k n r if l = I 0 ˙ k M l k M l
185 184 eqeq2d R CRing M B I N H N n N H r N H n I J M H = D k N , l N if k = H if l = I 1 ˙ 0 ˙ if k n if l = I 0 ˙ k M l k M l I J M H = D k N , l N if k = H if l = I 1 ˙ 0 ˙ if k n r if l = I 0 ˙ k M l k M l
186 185 biimpd R CRing M B I N H N n N H r N H n I J M H = D k N , l N if k = H if l = I 1 ˙ 0 ˙ if k n if l = I 0 ˙ k M l k M l I J M H = D k N , l N if k = H if l = I 1 ˙ 0 ˙ if k n r if l = I 0 ˙ k M l k M l
187 difss N H N
188 ssfi N Fin N H N N H Fin
189 47 187 188 sylancl R CRing M B I N H N N H Fin
190 12 18 24 30 39 186 189 findcard2d R CRing M B I N H N I J M H = D k N , l N if k = H if l = I 1 ˙ 0 ˙ if k 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 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 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 N l N k = H if k = H if l = I 1 ˙ 0 ˙ if k 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 N H if l = I 0 ˙ k M l k M l = if k N H if l = I 0 ˙ k M l k M l
199 198 adantl k N l N ¬ k = H if k = H if l = I 1 ˙ 0 ˙ if k N H if l = I 0 ˙ k M l k M l = if k N H if l = I 0 ˙ k M l k M l
200 neqne ¬ k = H k H
201 200 anim2i k N ¬ k = H k N k H
202 201 adantlr k N l N ¬ k = H k N k H
203 eldifsn k N H k N k H
204 202 203 sylibr k N l N ¬ k = H k N H
205 204 iftrued k N l N ¬ k = H if k 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 N l 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 N l N ¬ k = H if k = H if l = I 1 ˙ 0 ˙ if k 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 N l N if k = H if l = I 1 ˙ 0 ˙ if k 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 N , l N if k = H if l = I 1 ˙ 0 ˙ if k N H if l = I 0 ˙ k M l k M l = k N , l N if k = H l = I if l = I k = H 1 ˙ 0 ˙ k M l
216 215 fveq2i D k N , l N if k = H if l = I 1 ˙ 0 ˙ if k N H if l = I 0 ˙ k M l k M l = D k N , l N if k = H l = I if l = I k = H 1 ˙ 0 ˙ k M l
217 190 216 eqtrdi R CRing M B I N H N I J M H = D k N , l N if k = H l = I if l = I k = H 1 ˙ 0 ˙ k M l