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=NMatR
madufval.d ⊢D=NmaDetR
madufval.j ⊢J=NmaAdjuR
madufval.b ⊢B=BaseA
madufval.o ⊢1˙=1R
madufval.z ⊢0˙=0R
Assertion maducoeval2 ⊢R∈CRing∧M∈B∧I∈N∧H∈N→IJ⁡MH=D⁡k∈N,l∈N⟼ifk=H∨l=Iifl=I∧k=H1˙0˙kMl

Proof

Step Hyp Ref Expression
1 madufval.a ⊢A=NMatR
2 madufval.d ⊢D=NmaDetR
3 madufval.j ⊢J=NmaAdjuR
4 madufval.b ⊢B=BaseA
5 madufval.o ⊢1˙=1R
6 madufval.z ⊢0˙=0R
7 eleq2 ⊢m=∅→k∈m↔k∈∅
8 7 ifbid ⊢m=∅→ifk∈mifl=I0˙kMlkMl=ifk∈∅ifl=I0˙kMlkMl
9 8 ifeq2d ⊢m=∅→ifk=Hifl=I1˙0˙ifk∈mifl=I0˙kMlkMl=ifk=Hifl=I1˙0˙ifk∈∅ifl=I0˙kMlkMl
10 9 mpoeq3dv ⊢m=∅→k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈mifl=I0˙kMlkMl=k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈∅ifl=I0˙kMlkMl
11 10 fveq2d ⊢m=∅→D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈mifl=I0˙kMlkMl=D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈∅ifl=I0˙kMlkMl
12 11 eqeq2d ⊢m=∅→IJ⁡MH=D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈mifl=I0˙kMlkMl↔IJ⁡MH=D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈∅ifl=I0˙kMlkMl
13 eleq2 ⊢m=n→k∈m↔k∈n
14 13 ifbid ⊢m=n→ifk∈mifl=I0˙kMlkMl=ifk∈nifl=I0˙kMlkMl
15 14 ifeq2d ⊢m=n→ifk=Hifl=I1˙0˙ifk∈mifl=I0˙kMlkMl=ifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl
16 15 mpoeq3dv ⊢m=n→k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈mifl=I0˙kMlkMl=k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl
17 16 fveq2d ⊢m=n→D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈mifl=I0˙kMlkMl=D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl
18 17 eqeq2d ⊢m=n→IJ⁡MH=D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈mifl=I0˙kMlkMl↔IJ⁡MH=D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl
19 eleq2 ⊢m=n∪r→k∈m↔k∈n∪r
20 19 ifbid ⊢m=n∪r→ifk∈mifl=I0˙kMlkMl=ifk∈n∪rifl=I0˙kMlkMl
21 20 ifeq2d ⊢m=n∪r→ifk=Hifl=I1˙0˙ifk∈mifl=I0˙kMlkMl=ifk=Hifl=I1˙0˙ifk∈n∪rifl=I0˙kMlkMl
22 21 mpoeq3dv ⊢m=n∪r→k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈mifl=I0˙kMlkMl=k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈n∪rifl=I0˙kMlkMl
23 22 fveq2d ⊢m=n∪r→D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈mifl=I0˙kMlkMl=D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈n∪rifl=I0˙kMlkMl
24 23 eqeq2d ⊢m=n∪r→IJ⁡MH=D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈mifl=I0˙kMlkMl↔IJ⁡MH=D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈n∪rifl=I0˙kMlkMl
25 eleq2 ⊢m=N∖H→k∈m↔k∈N∖H
26 25 ifbid ⊢m=N∖H→ifk∈mifl=I0˙kMlkMl=ifk∈N∖Hifl=I0˙kMlkMl
27 26 ifeq2d ⊢m=N∖H→ifk=Hifl=I1˙0˙ifk∈mifl=I0˙kMlkMl=ifk=Hifl=I1˙0˙ifk∈N∖Hifl=I0˙kMlkMl
28 27 mpoeq3dv ⊢m=N∖H→k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈mifl=I0˙kMlkMl=k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈N∖Hifl=I0˙kMlkMl
29 28 fveq2d ⊢m=N∖H→D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈mifl=I0˙kMlkMl=D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈N∖Hifl=I0˙kMlkMl
30 29 eqeq2d ⊢m=N∖H→IJ⁡MH=D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈mifl=I0˙kMlkMl↔IJ⁡MH=D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈N∖Hifl=I0˙kMlkMl
31 1 2 3 4 5 6 maducoeval ⊢M∈B∧I∈N∧H∈N→IJ⁡MH=D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙kMl
32 31 3adant1l ⊢R∈CRing∧M∈B∧I∈N∧H∈N→IJ⁡MH=D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙kMl
33 noel ⊢¬k∈∅
34 iffalse ⊢¬k∈∅→ifk∈∅ifl=I0˙kMlkMl=kMl
35 33 34 mp1i ⊢k∈N∧l∈N→ifk∈∅ifl=I0˙kMlkMl=kMl
36 35 ifeq2d ⊢k∈N∧l∈N→ifk=Hifl=I1˙0˙ifk∈∅ifl=I0˙kMlkMl=ifk=Hifl=I1˙0˙kMl
37 36 mpoeq3ia ⊢k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈∅ifl=I0˙kMlkMl=k∈N,l∈N⟼ifk=Hifl=I1˙0˙kMl
38 37 fveq2i ⊢D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈∅ifl=I0˙kMlkMl=D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙kMl
39 32 38 eqtr4di ⊢R∈CRing∧M∈B∧I∈N∧H∈N→IJ⁡MH=D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈∅ifl=I0˙kMlkMl
40 eqid ⊢BaseR=BaseR
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˙∈BaseR
54 52 53 syl ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n∧l∈N→0˙∈BaseR
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∈BaseRN×N
57 elmapi ⊢M∈BaseRN×N→M:N×N⟶BaseR
58 55 56 57 3syl ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n→M:N×N⟶BaseR
59 58 adantr ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n∧l∈N→M:N×N⟶BaseR
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 fovcdmd ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n∧l∈N→rMl∈BaseR
66 54 65 ifcld ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n∧l∈N→ifl=I0˙rMl∈BaseR
67 40 5 ringidcl ⊢R∈Ring→1˙∈BaseR
68 52 67 syl ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n∧l∈N→1˙∈BaseR
69 68 54 ifcld ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n∧l∈N→ifl=I1˙0˙∈BaseR
70 54 3adant2 ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n∧k∈N∧l∈N→0˙∈BaseR
71 58 fovcdmda ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n∧k∈N∧l∈N→kMl∈BaseR
72 71 3impb ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n∧k∈N∧l∈N→kMl∈BaseR
73 70 72 ifcld ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n∧k∈N∧l∈N→ifl=I0˙kMl∈BaseR
74 73 72 ifcld ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n∧k∈N∧l∈N→ifk∈nifl=I0˙kMlkMl∈BaseR
75 simpl2 ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n→I∈N
76 58 62 75 fovcdmd ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n→rMI∈BaseR
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⟼ifk=rifl=I0˙rMl+RrMI⋅Rifl=I1˙0˙ifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl=D⁡k∈N,l∈N⟼ifk=rifl=I0˙rMlifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl
81 ifnot ⊢if¬l=IrMl0˙=ifl=I0˙rMl
82 81 eqcomi ⊢ifl=I0˙rMl=if¬l=IrMl0˙
83 82 a1i ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n∧l∈N→ifl=I0˙rMl=if¬l=IrMl0˙
84 ovif2 ⊢rMI⋅Rifl=I1˙0˙=ifl=IrMI⋅R1˙rMI⋅R0˙
85 76 adantr ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n∧l∈N→rMI∈BaseR
86 40 42 5 ringridm ⊢R∈Ring∧rMI∈BaseR→rMI⋅R1˙=rMI
87 52 85 86 syl2anc ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n∧l∈N→rMI⋅R1˙=rMI
88 87 adantr ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n∧l∈N∧l=I→rMI⋅R1˙=rMI
89 oveq2 ⊢l=I→rMl=rMI
90 89 adantl ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n∧l∈N∧l=I→rMl=rMI
91 88 90 eqtr4d ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n∧l∈N∧l=I→rMI⋅R1˙=rMl
92 91 ifeq1da ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n∧l∈N→ifl=IrMI⋅R1˙rMI⋅R0˙=ifl=IrMlrMI⋅R0˙
93 40 42 6 ringrz ⊢R∈Ring∧rMI∈BaseR→rMI⋅R0˙=0˙
94 52 85 93 syl2anc ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n∧l∈N→rMI⋅R0˙=0˙
95 94 ifeq2d ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n∧l∈N→ifl=IrMlrMI⋅R0˙=ifl=IrMl0˙
96 92 95 eqtrd ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n∧l∈N→ifl=IrMI⋅R1˙rMI⋅R0˙=ifl=IrMl0˙
97 84 96 eqtrid ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n∧l∈N→rMI⋅Rifl=I1˙0˙=ifl=IrMl0˙
98 83 97 oveq12d ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n∧l∈N→ifl=I0˙rMl+RrMI⋅Rifl=I1˙0˙=if¬l=IrMl0˙+Rifl=IrMl0˙
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∧rMl∈BaseR∧¬¬l=I∧l=I→if¬l=I∨l=IrMl0˙=if¬l=IrMl0˙+Rifl=IrMl0˙
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=IrMl0˙=if¬l=IrMl0˙+Rifl=IrMl0˙
107 pm2.1 ⊢¬l=I∨l=I
108 iftrue ⊢¬l=I∨l=I→if¬l=I∨l=IrMl0˙=rMl
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=IrMl0˙=rMl
110 98 106 109 3eqtr2d ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n∧l∈N→ifl=I0˙rMl+RrMI⋅Rifl=I1˙0˙=rMl
111 110 3adant2 ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n∧k∈N∧l∈N→ifl=I0˙rMl+RrMI⋅Rifl=I1˙0˙=rMl
112 oveq1 ⊢k=r→kMl=rMl
113 112 eqeq2d ⊢k=r→ifl=I0˙rMl+RrMI⋅Rifl=I1˙0˙=kMl↔ifl=I0˙rMl+RrMI⋅Rifl=I1˙0˙=rMl
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→ifl=I0˙rMl+RrMI⋅Rifl=I1˙0˙=kMl
115 114 imp ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n∧k∈N∧l∈N∧k=r→ifl=I0˙rMl+RrMI⋅Rifl=I1˙0˙=kMl
116 iftrue ⊢k=r→ifk=rifl=I0˙rMl+RrMI⋅Rifl=I1˙0˙ifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl=ifl=I0˙rMl+RrMI⋅Rifl=I1˙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→ifk=rifl=I0˙rMl+RrMI⋅Rifl=I1˙0˙ifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl=ifl=I0˙rMl+RrMI⋅Rifl=I1˙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→ifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl=ifk∈nifl=I0˙kMlkMl
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→ifk∈nifl=I0˙kMlkMl=kMl
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→ifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl=kMl
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→ifk=rifl=I0˙rMl+RrMI⋅Rifl=I1˙0˙ifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl=ifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl
135 iffalse ⊢¬k=r→ifk=rifl=I0˙rMl+RrMI⋅Rifl=I1˙0˙ifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl=ifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl
136 135 adantl ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n∧k∈N∧l∈N∧¬k=r→ifk=rifl=I0˙rMl+RrMI⋅Rifl=I1˙0˙ifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl=ifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl
137 134 136 pm2.61dan ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n∧k∈N∧l∈N→ifk=rifl=I0˙rMl+RrMI⋅Rifl=I1˙0˙ifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl=ifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl
138 137 mpoeq3dva ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n→k∈N,l∈N⟼ifk=rifl=I0˙rMl+RrMI⋅Rifl=I1˙0˙ifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl=k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl
139 138 fveq2d ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n→D⁡k∈N,l∈N⟼ifk=rifl=I0˙rMl+RrMI⋅Rifl=I1˙0˙ifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl=D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl
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→ifk=rifl=I0˙rMlifl=I1˙0˙=ifl=I1˙0˙
145 iftrue ⊢k=H→ifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl=ifl=I1˙0˙
146 145 adantl ⊢r≠H∧k=H→ifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl=ifl=I1˙0˙
147 146 ifeq2d ⊢r≠H∧k=H→ifk=rifl=I0˙rMlifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl=ifk=rifl=I0˙rMlifl=I1˙0˙
148 iftrue ⊢k=H→ifk=Hifl=I1˙0˙ifk∈n∪rifl=I0˙kMlkMl=ifl=I1˙0˙
149 148 adantl ⊢r≠H∧k=H→ifk=Hifl=I1˙0˙ifk∈n∪rifl=I0˙kMlkMl=ifl=I1˙0˙
150 144 147 149 3eqtr4d ⊢r≠H∧k=H→ifk=rifl=I0˙rMlifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl=ifk=Hifl=I1˙0˙ifk∈n∪rifl=I0˙kMlkMl
151 112 ifeq2d ⊢k=r→ifl=I0˙kMl=ifl=I0˙rMl
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→ifk∈n∪rifl=I0˙kMlkMl=ifl=I0˙kMl
158 iftrue ⊢k=r→ifk=rifl=I0˙rMlifk∈nifl=I0˙kMlkMl=ifl=I0˙rMl
159 151 157 158 3eqtr4rd ⊢k=r→ifk=rifl=I0˙rMlifk∈nifl=I0˙kMlkMl=ifk∈n∪rifl=I0˙kMlkMl
160 159 adantl ⊢r≠H∧¬k=H∧k=r→ifk=rifl=I0˙rMlifk∈nifl=I0˙kMlkMl=ifk∈n∪rifl=I0˙kMlkMl
161 iffalse ⊢¬k=r→ifk=rifl=I0˙rMlifk∈nifl=I0˙kMlkMl=ifk∈nifl=I0˙kMlkMl
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→ifk∈nifl=I0˙kMlkMl=ifk∈n∪rifl=I0˙kMlkMl
171 161 170 eqtrd ⊢¬k=r→ifk=rifl=I0˙rMlifk∈nifl=I0˙kMlkMl=ifk∈n∪rifl=I0˙kMlkMl
172 171 adantl ⊢r≠H∧¬k=H∧¬k=r→ifk=rifl=I0˙rMlifk∈nifl=I0˙kMlkMl=ifk∈n∪rifl=I0˙kMlkMl
173 160 172 pm2.61dan ⊢r≠H∧¬k=H→ifk=rifl=I0˙rMlifk∈nifl=I0˙kMlkMl=ifk∈n∪rifl=I0˙kMlkMl
174 iffalse ⊢¬k=H→ifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl=ifk∈nifl=I0˙kMlkMl
175 174 ifeq2d ⊢¬k=H→ifk=rifl=I0˙rMlifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl=ifk=rifl=I0˙rMlifk∈nifl=I0˙kMlkMl
176 175 adantl ⊢r≠H∧¬k=H→ifk=rifl=I0˙rMlifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl=ifk=rifl=I0˙rMlifk∈nifl=I0˙kMlkMl
177 iffalse ⊢¬k=H→ifk=Hifl=I1˙0˙ifk∈n∪rifl=I0˙kMlkMl=ifk∈n∪rifl=I0˙kMlkMl
178 177 adantl ⊢r≠H∧¬k=H→ifk=Hifl=I1˙0˙ifk∈n∪rifl=I0˙kMlkMl=ifk∈n∪rifl=I0˙kMlkMl
179 173 176 178 3eqtr4d ⊢r≠H∧¬k=H→ifk=rifl=I0˙rMlifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl=ifk=Hifl=I1˙0˙ifk∈n∪rifl=I0˙kMlkMl
180 150 179 pm2.61dan ⊢r≠H→ifk=rifl=I0˙rMlifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl=ifk=Hifl=I1˙0˙ifk∈n∪rifl=I0˙kMlkMl
181 180 mpoeq3dv ⊢r≠H→k∈N,l∈N⟼ifk=rifl=I0˙rMlifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl=k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈n∪rifl=I0˙kMlkMl
182 181 fveq2d ⊢r≠H→D⁡k∈N,l∈N⟼ifk=rifl=I0˙rMlifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl=D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈n∪rifl=I0˙kMlkMl
183 79 182 syl ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n→D⁡k∈N,l∈N⟼ifk=rifl=I0˙rMlifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl=D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈n∪rifl=I0˙kMlkMl
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⟼ifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl=D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈n∪rifl=I0˙kMlkMl
185 184 eqeq2d ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n→IJ⁡MH=D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl↔IJ⁡MH=D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈n∪rifl=I0˙kMlkMl
186 185 biimpd ⊢R∈CRing∧M∈B∧I∈N∧H∈N∧n⊆N∖H∧r∈N∖H∖n→IJ⁡MH=D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈nifl=I0˙kMlkMl→IJ⁡MH=D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈n∪rifl=I0˙kMlkMl
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→IJ⁡MH=D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈N∖Hifl=I0˙kMlkMl
191 iba ⊢k=H→l=I↔l=I∧k=H
192 191 ifbid ⊢k=H→ifl=I1˙0˙=ifl=I∧k=H1˙0˙
193 iftrue ⊢k=H→ifk=Hifl=I1˙0˙ifk∈N∖Hifl=I0˙kMlkMl=ifl=I1˙0˙
194 iftrue ⊢k=H∨l=I→ifk=H∨l=Iifl=I∧k=H1˙0˙kMl=ifl=I∧k=H1˙0˙
195 194 orcs ⊢k=H→ifk=H∨l=Iifl=I∧k=H1˙0˙kMl=ifl=I∧k=H1˙0˙
196 192 193 195 3eqtr4d ⊢k=H→ifk=Hifl=I1˙0˙ifk∈N∖Hifl=I0˙kMlkMl=ifk=H∨l=Iifl=I∧k=H1˙0˙kMl
197 196 adantl ⊢k∈N∧l∈N∧k=H→ifk=Hifl=I1˙0˙ifk∈N∖Hifl=I0˙kMlkMl=ifk=H∨l=Iifl=I∧k=H1˙0˙kMl
198 iffalse ⊢¬k=H→ifk=Hifl=I1˙0˙ifk∈N∖Hifl=I0˙kMlkMl=ifk∈N∖Hifl=I0˙kMlkMl
199 198 adantl ⊢k∈N∧l∈N∧¬k=H→ifk=Hifl=I1˙0˙ifk∈N∖Hifl=I0˙kMlkMl=ifk∈N∖Hifl=I0˙kMlkMl
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→ifk∈N∖Hifl=I0˙kMlkMl=ifl=I0˙kMl
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→ifl=I∧k=H1˙0˙=0˙
210 209 eqcomd ⊢¬k=H→0˙=ifl=I∧k=H1˙0˙
211 206 210 ifbieq1d ⊢¬k=H→ifl=I0˙kMl=ifk=H∨l=Iifl=I∧k=H1˙0˙kMl
212 211 adantl ⊢k∈N∧l∈N∧¬k=H→ifl=I0˙kMl=ifk=H∨l=Iifl=I∧k=H1˙0˙kMl
213 199 205 212 3eqtrd ⊢k∈N∧l∈N∧¬k=H→ifk=Hifl=I1˙0˙ifk∈N∖Hifl=I0˙kMlkMl=ifk=H∨l=Iifl=I∧k=H1˙0˙kMl
214 197 213 pm2.61dan ⊢k∈N∧l∈N→ifk=Hifl=I1˙0˙ifk∈N∖Hifl=I0˙kMlkMl=ifk=H∨l=Iifl=I∧k=H1˙0˙kMl
215 214 mpoeq3ia ⊢k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈N∖Hifl=I0˙kMlkMl=k∈N,l∈N⟼ifk=H∨l=Iifl=I∧k=H1˙0˙kMl
216 215 fveq2i ⊢D⁡k∈N,l∈N⟼ifk=Hifl=I1˙0˙ifk∈N∖Hifl=I0˙kMlkMl=D⁡k∈N,l∈N⟼ifk=H∨l=Iifl=I∧k=H1˙0˙kMl
217 190 216 eqtrdi ⊢R∈CRing∧M∈B∧I∈N∧H∈N→IJ⁡MH=D⁡k∈N,l∈N⟼ifk=H∨l=Iifl=I∧k=H1˙0˙kMl