This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem maducoeval2

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

Ref Expression
Hypotheses madufval.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
madufval.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
madufval.j ⊢ 𝐽 = ( 𝑁 maAdju 𝑅 )
madufval.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
madufval.o ⊢ 1 = ( 1r ‘ 𝑅 )
madufval.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion maducoeval2 ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝐼 ∈ 𝑁 ∧ 𝐻 ∈ 𝑁 ) → ( 𝐼 ( 𝐽 ‘ 𝑀 ) 𝐻 ) = ( 𝐷 ‘ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( ( 𝑘 = 𝐻 ∨ 𝑙 = 𝐼 ) , if ( ( 𝑙 = 𝐼 ∧ 𝑘 = 𝐻 ) , 1 , 0 ) , ( 𝑘 𝑀 𝑙 ) ) ) ) )

Proof

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