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 syl6bb ⊢ ¬ 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