Metamath Proof Explorer

Theorem madugsum

Description: The determinant of a matrix with a row L consisting of the same element X is the sum of the elements of the L -th column of the adjunct of the matrix multiplied with X . (Contributed by Stefan O'Rear, 16-Jul-2018)

Ref Expression
Hypotheses maduf.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
maduf.j ⊢ 𝐽 = ( 𝑁 maAdju 𝑅 )
maduf.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
madugsum.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
madugsum.t ⊢ · = ( .r ‘ 𝑅 )
madugsum.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
madugsum.m ⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
madugsum.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
madugsum.x ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → 𝑋 ∈ 𝐾 )
madugsum.l ⊢ ( 𝜑 → 𝐿 ∈ 𝑁 )
Assertion madugsum ( 𝜑 → ( 𝑅 Σg ( 𝑖 ∈ 𝑁 ↦ ( 𝑋 · ( 𝑖 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) = ( 𝐷 ‘ ( 𝑗 ∈ 𝑁 , 𝑖 ∈ 𝑁 ↦ if ( 𝑗 = 𝐿 , 𝑋 , ( 𝑗 𝑀 𝑖 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 maduf.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 maduf.j ⊢ 𝐽 = ( 𝑁 maAdju 𝑅 )
3 maduf.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
4 madugsum.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
5 madugsum.t ⊢ · = ( .r ‘ 𝑅 )
6 madugsum.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
7 madugsum.m ⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
8 madugsum.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
9 madugsum.x ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → 𝑋 ∈ 𝐾 )
10 madugsum.l ⊢ ( 𝜑 → 𝐿 ∈ 𝑁 )
11 mpteq1 ⊢ ( 𝑐 = ∅ → ( 𝑏 ∈ 𝑐 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) = ( 𝑏 ∈ ∅ ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) )
12 11 oveq2d ⊢ ( 𝑐 = ∅ → ( 𝑅 Σg ( 𝑏 ∈ 𝑐 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) = ( 𝑅 Σg ( 𝑏 ∈ ∅ ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) )
13 eleq2 ⊢ ( 𝑐 = ∅ → ( 𝑏 ∈ 𝑐 ↔ 𝑏 ∈ ∅ ) )
14 13 ifbid ⊢ ( 𝑐 = ∅ → if ( 𝑏 ∈ 𝑐 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) = if ( 𝑏 ∈ ∅ , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) )
15 14 ifeq1d ⊢ ( 𝑐 = ∅ → if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑐 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) = if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ ∅ , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) )
16 15 mpoeq3dv ⊢ ( 𝑐 = ∅ → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑐 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ ∅ , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) )
17 16 fveq2d ⊢ ( 𝑐 = ∅ → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑐 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ ∅ , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) )
18 12 17 eqeq12d ⊢ ( 𝑐 = ∅ → ( ( 𝑅 Σg ( 𝑏 ∈ 𝑐 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑐 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) ↔ ( 𝑅 Σg ( 𝑏 ∈ ∅ ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ ∅ , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) ) )
19 mpteq1 ⊢ ( 𝑐 = 𝑑 → ( 𝑏 ∈ 𝑐 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) = ( 𝑏 ∈ 𝑑 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) )
20 19 oveq2d ⊢ ( 𝑐 = 𝑑 → ( 𝑅 Σg ( 𝑏 ∈ 𝑐 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) = ( 𝑅 Σg ( 𝑏 ∈ 𝑑 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) )
21 eleq2 ⊢ ( 𝑐 = 𝑑 → ( 𝑏 ∈ 𝑐 ↔ 𝑏 ∈ 𝑑 ) )
22 21 ifbid ⊢ ( 𝑐 = 𝑑 → if ( 𝑏 ∈ 𝑐 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) = if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) )
23 22 ifeq1d ⊢ ( 𝑐 = 𝑑 → if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑐 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) = if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) )
24 23 mpoeq3dv ⊢ ( 𝑐 = 𝑑 → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑐 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) )
25 24 fveq2d ⊢ ( 𝑐 = 𝑑 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑐 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) )
26 20 25 eqeq12d ⊢ ( 𝑐 = 𝑑 → ( ( 𝑅 Σg ( 𝑏 ∈ 𝑐 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑐 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) ↔ ( 𝑅 Σg ( 𝑏 ∈ 𝑑 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) ) )
27 mpteq1 ⊢ ( 𝑐 = ( 𝑑 ∪ { 𝑒 } ) → ( 𝑏 ∈ 𝑐 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) = ( 𝑏 ∈ ( 𝑑 ∪ { 𝑒 } ) ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) )
28 27 oveq2d ⊢ ( 𝑐 = ( 𝑑 ∪ { 𝑒 } ) → ( 𝑅 Σg ( 𝑏 ∈ 𝑐 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) = ( 𝑅 Σg ( 𝑏 ∈ ( 𝑑 ∪ { 𝑒 } ) ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) )
29 eleq2 ⊢ ( 𝑐 = ( 𝑑 ∪ { 𝑒 } ) → ( 𝑏 ∈ 𝑐 ↔ 𝑏 ∈ ( 𝑑 ∪ { 𝑒 } ) ) )
30 29 ifbid ⊢ ( 𝑐 = ( 𝑑 ∪ { 𝑒 } ) → if ( 𝑏 ∈ 𝑐 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) = if ( 𝑏 ∈ ( 𝑑 ∪ { 𝑒 } ) , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) )
31 30 ifeq1d ⊢ ( 𝑐 = ( 𝑑 ∪ { 𝑒 } ) → if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑐 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) = if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ ( 𝑑 ∪ { 𝑒 } ) , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) )
32 31 mpoeq3dv ⊢ ( 𝑐 = ( 𝑑 ∪ { 𝑒 } ) → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑐 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ ( 𝑑 ∪ { 𝑒 } ) , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) )
33 32 fveq2d ⊢ ( 𝑐 = ( 𝑑 ∪ { 𝑒 } ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑐 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ ( 𝑑 ∪ { 𝑒 } ) , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) )
34 28 33 eqeq12d ⊢ ( 𝑐 = ( 𝑑 ∪ { 𝑒 } ) → ( ( 𝑅 Σg ( 𝑏 ∈ 𝑐 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑐 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) ↔ ( 𝑅 Σg ( 𝑏 ∈ ( 𝑑 ∪ { 𝑒 } ) ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ ( 𝑑 ∪ { 𝑒 } ) , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) ) )
35 mpteq1 ⊢ ( 𝑐 = 𝑁 → ( 𝑏 ∈ 𝑐 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) = ( 𝑏 ∈ 𝑁 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) )
36 35 oveq2d ⊢ ( 𝑐 = 𝑁 → ( 𝑅 Σg ( 𝑏 ∈ 𝑐 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) = ( 𝑅 Σg ( 𝑏 ∈ 𝑁 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) )
37 eleq2 ⊢ ( 𝑐 = 𝑁 → ( 𝑏 ∈ 𝑐 ↔ 𝑏 ∈ 𝑁 ) )
38 37 ifbid ⊢ ( 𝑐 = 𝑁 → if ( 𝑏 ∈ 𝑐 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) = if ( 𝑏 ∈ 𝑁 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) )
39 38 ifeq1d ⊢ ( 𝑐 = 𝑁 → if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑐 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) = if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑁 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) )
40 39 mpoeq3dv ⊢ ( 𝑐 = 𝑁 → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑐 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑁 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) )
41 40 fveq2d ⊢ ( 𝑐 = 𝑁 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑐 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑁 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) )
42 36 41 eqeq12d ⊢ ( 𝑐 = 𝑁 → ( ( 𝑅 Σg ( 𝑏 ∈ 𝑐 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑐 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) ↔ ( 𝑅 Σg ( 𝑏 ∈ 𝑁 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑁 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) ) )
43 mpt0 ⊢ ( 𝑏 ∈ ∅ ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) = ∅
44 43 oveq2i ⊢ ( 𝑅 Σg ( 𝑏 ∈ ∅ ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) = ( 𝑅 Σg ∅ )
45 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
46 45 gsum0 ⊢ ( 𝑅 Σg ∅ ) = ( 0g ‘ 𝑅 )
47 44 46 eqtri ⊢ ( 𝑅 Σg ( 𝑏 ∈ ∅ ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) = ( 0g ‘ 𝑅 )
48 noel ⊢ ¬ 𝑏 ∈ ∅
49 iffalse ⊢ ( ¬ 𝑏 ∈ ∅ → if ( 𝑏 ∈ ∅ , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
50 48 49 mp1i ⊢ ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → if ( 𝑏 ∈ ∅ , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
51 50 ifeq1d ⊢ ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ ∅ , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) = if ( 𝑎 = 𝐿 , ( 0g ‘ 𝑅 ) , ( 𝑎 𝑀 𝑏 ) ) )
52 51 mpoeq3ia ⊢ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ ∅ , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , ( 0g ‘ 𝑅 ) , ( 𝑎 𝑀 𝑏 ) ) )
53 52 fveq2i ⊢ ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ ∅ , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , ( 0g ‘ 𝑅 ) , ( 𝑎 𝑀 𝑏 ) ) ) )
54 1 3 matrcl ⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
55 7 54 syl ⊢ ( 𝜑 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
56 55 simpld ⊢ ( 𝜑 → 𝑁 ∈ Fin )
57 1 6 3 matbas2i ⊢ ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( 𝐾 ↑m ( 𝑁 × 𝑁 ) ) )
58 elmapi ⊢ ( 𝑀 ∈ ( 𝐾 ↑m ( 𝑁 × 𝑁 ) ) → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ 𝐾 )
59 7 57 58 3syl ⊢ ( 𝜑 → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ 𝐾 )
60 59 fovrnda ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 𝑀 𝑏 ) ∈ 𝐾 )
61 60 3impb ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝑎 𝑀 𝑏 ) ∈ 𝐾 )
62 4 6 45 8 56 61 10 mdetr0 ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , ( 0g ‘ 𝑅 ) , ( 𝑎 𝑀 𝑏 ) ) ) ) = ( 0g ‘ 𝑅 ) )
63 53 62 syl5eq ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ ∅ , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) = ( 0g ‘ 𝑅 ) )
64 47 63 eqtr4id ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑏 ∈ ∅ ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ ∅ , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) )
65 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
66 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → 𝑅 ∈ CRing )
67 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
68 66 67 syl ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → 𝑅 ∈ Ring )
69 ringcmn ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
70 68 69 syl ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → 𝑅 ∈ CMnd )
71 56 adantr ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → 𝑁 ∈ Fin )
72 simprl ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → 𝑑 ⊆ 𝑁 )
73 71 72 ssfid ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → 𝑑 ∈ Fin )
74 68 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ 𝑏 ∈ 𝑑 ) → 𝑅 ∈ Ring )
75 72 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ 𝑏 ∈ 𝑑 ) → 𝑏 ∈ 𝑁 )
76 9 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝑁 𝑋 ∈ 𝐾 )
77 76 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ 𝑏 ∈ 𝑑 ) → ∀ 𝑖 ∈ 𝑁 𝑋 ∈ 𝐾 )
78 rspcsbela ⊢ ( ( 𝑏 ∈ 𝑁 ∧ ∀ 𝑖 ∈ 𝑁 𝑋 ∈ 𝐾 ) → ⦋ 𝑏 / 𝑖 ⦌ 𝑋 ∈ 𝐾 )
79 75 77 78 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ 𝑏 ∈ 𝑑 ) → ⦋ 𝑏 / 𝑖 ⦌ 𝑋 ∈ 𝐾 )
80 1 2 3 maduf ⊢ ( 𝑅 ∈ CRing → 𝐽 : 𝐵 ⟶ 𝐵 )
81 8 80 syl ⊢ ( 𝜑 → 𝐽 : 𝐵 ⟶ 𝐵 )
82 81 7 ffvelrnd ⊢ ( 𝜑 → ( 𝐽 ‘ 𝑀 ) ∈ 𝐵 )
83 1 6 3 matbas2i ⊢ ( ( 𝐽 ‘ 𝑀 ) ∈ 𝐵 → ( 𝐽 ‘ 𝑀 ) ∈ ( 𝐾 ↑m ( 𝑁 × 𝑁 ) ) )
84 elmapi ⊢ ( ( 𝐽 ‘ 𝑀 ) ∈ ( 𝐾 ↑m ( 𝑁 × 𝑁 ) ) → ( 𝐽 ‘ 𝑀 ) : ( 𝑁 × 𝑁 ) ⟶ 𝐾 )
85 82 83 84 3syl ⊢ ( 𝜑 → ( 𝐽 ‘ 𝑀 ) : ( 𝑁 × 𝑁 ) ⟶ 𝐾 )
86 85 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ 𝑏 ∈ 𝑑 ) → ( 𝐽 ‘ 𝑀 ) : ( 𝑁 × 𝑁 ) ⟶ 𝐾 )
87 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ 𝑏 ∈ 𝑑 ) → 𝐿 ∈ 𝑁 )
88 86 75 87 fovrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ 𝑏 ∈ 𝑑 ) → ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ∈ 𝐾 )
89 6 5 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ⦋ 𝑏 / 𝑖 ⦌ 𝑋 ∈ 𝐾 ∧ ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ∈ 𝐾 ) → ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ∈ 𝐾 )
90 74 79 88 89 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ 𝑏 ∈ 𝑑 ) → ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ∈ 𝐾 )
91 vex ⊢ 𝑒 ∈ V
92 91 a1i ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → 𝑒 ∈ V )
93 eldifn ⊢ ( 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) → ¬ 𝑒 ∈ 𝑑 )
94 93 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → ¬ 𝑒 ∈ 𝑑 )
95 eldifi ⊢ ( 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) → 𝑒 ∈ 𝑁 )
96 95 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → 𝑒 ∈ 𝑁 )
97 76 adantr ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → ∀ 𝑖 ∈ 𝑁 𝑋 ∈ 𝐾 )
98 rspcsbela ⊢ ( ( 𝑒 ∈ 𝑁 ∧ ∀ 𝑖 ∈ 𝑁 𝑋 ∈ 𝐾 ) → ⦋ 𝑒 / 𝑖 ⦌ 𝑋 ∈ 𝐾 )
99 96 97 98 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → ⦋ 𝑒 / 𝑖 ⦌ 𝑋 ∈ 𝐾 )
100 85 adantr ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → ( 𝐽 ‘ 𝑀 ) : ( 𝑁 × 𝑁 ) ⟶ 𝐾 )
101 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → 𝐿 ∈ 𝑁 )
102 100 96 101 fovrnd ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → ( 𝑒 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ∈ 𝐾 )
103 6 5 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ⦋ 𝑒 / 𝑖 ⦌ 𝑋 ∈ 𝐾 ∧ ( 𝑒 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ∈ 𝐾 ) → ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · ( 𝑒 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ∈ 𝐾 )
104 68 99 102 103 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · ( 𝑒 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ∈ 𝐾 )
105 csbeq1 ⊢ ( 𝑏 = 𝑒 → ⦋ 𝑏 / 𝑖 ⦌ 𝑋 = ⦋ 𝑒 / 𝑖 ⦌ 𝑋 )
106 oveq1 ⊢ ( 𝑏 = 𝑒 → ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) = ( 𝑒 ( 𝐽 ‘ 𝑀 ) 𝐿 ) )
107 105 106 oveq12d ⊢ ( 𝑏 = 𝑒 → ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) = ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · ( 𝑒 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) )
108 6 65 70 73 90 92 94 104 107 gsumunsn ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → ( 𝑅 Σg ( 𝑏 ∈ ( 𝑑 ∪ { 𝑒 } ) ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) = ( ( 𝑅 Σg ( 𝑏 ∈ 𝑑 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) ( +g ‘ 𝑅 ) ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · ( 𝑒 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) )
109 108 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ ( 𝑅 Σg ( 𝑏 ∈ 𝑑 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) ) → ( 𝑅 Σg ( 𝑏 ∈ ( 𝑑 ∪ { 𝑒 } ) ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) = ( ( 𝑅 Σg ( 𝑏 ∈ 𝑑 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) ( +g ‘ 𝑅 ) ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · ( 𝑒 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) )
110 oveq1 ⊢ ( ( 𝑅 Σg ( 𝑏 ∈ 𝑑 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) → ( ( 𝑅 Σg ( 𝑏 ∈ 𝑑 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) ( +g ‘ 𝑅 ) ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · ( 𝑒 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) = ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) ( +g ‘ 𝑅 ) ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · ( 𝑒 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) )
111 110 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ ( 𝑅 Σg ( 𝑏 ∈ 𝑑 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) ) → ( ( 𝑅 Σg ( 𝑏 ∈ 𝑑 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) ( +g ‘ 𝑅 ) ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · ( 𝑒 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) = ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) ( +g ‘ 𝑅 ) ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · ( 𝑒 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) )
112 elun ⊢ ( 𝑏 ∈ ( 𝑑 ∪ { 𝑒 } ) ↔ ( 𝑏 ∈ 𝑑 ∨ 𝑏 ∈ { 𝑒 } ) )
113 velsn ⊢ ( 𝑏 ∈ { 𝑒 } ↔ 𝑏 = 𝑒 )
114 113 orbi2i ⊢ ( ( 𝑏 ∈ 𝑑 ∨ 𝑏 ∈ { 𝑒 } ) ↔ ( 𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒 ) )
115 112 114 bitri ⊢ ( 𝑏 ∈ ( 𝑑 ∪ { 𝑒 } ) ↔ ( 𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒 ) )
116 ifbi ⊢ ( ( 𝑏 ∈ ( 𝑑 ∪ { 𝑒 } ) ↔ ( 𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒 ) ) → if ( 𝑏 ∈ ( 𝑑 ∪ { 𝑒 } ) , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) = if ( ( 𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒 ) , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) )
117 115 116 ax-mp ⊢ if ( 𝑏 ∈ ( 𝑑 ∪ { 𝑒 } ) , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) = if ( ( 𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒 ) , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) )
118 ringmnd ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
119 68 118 syl ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → 𝑅 ∈ Mnd )
120 119 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑅 ∈ Mnd )
121 simp3 ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑏 ∈ 𝑁 )
122 97 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ∀ 𝑖 ∈ 𝑁 𝑋 ∈ 𝐾 )
123 121 122 78 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ⦋ 𝑏 / 𝑖 ⦌ 𝑋 ∈ 𝐾 )
124 elequ1 ⊢ ( 𝑏 = 𝑒 → ( 𝑏 ∈ 𝑑 ↔ 𝑒 ∈ 𝑑 ) )
125 124 biimpac ⊢ ( ( 𝑏 ∈ 𝑑 ∧ 𝑏 = 𝑒 ) → 𝑒 ∈ 𝑑 )
126 94 125 nsyl ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → ¬ ( 𝑏 ∈ 𝑑 ∧ 𝑏 = 𝑒 ) )
127 126 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ¬ ( 𝑏 ∈ 𝑑 ∧ 𝑏 = 𝑒 ) )
128 6 45 65 mndifsplit ⊢ ( ( 𝑅 ∈ Mnd ∧ ⦋ 𝑏 / 𝑖 ⦌ 𝑋 ∈ 𝐾 ∧ ¬ ( 𝑏 ∈ 𝑑 ∧ 𝑏 = 𝑒 ) ) → if ( ( 𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒 ) , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) = ( if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) ( +g ‘ 𝑅 ) if ( 𝑏 = 𝑒 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) ) )
129 120 123 127 128 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → if ( ( 𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒 ) , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) = ( if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) ( +g ‘ 𝑅 ) if ( 𝑏 = 𝑒 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) ) )
130 117 129 syl5eq ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → if ( 𝑏 ∈ ( 𝑑 ∪ { 𝑒 } ) , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) = ( if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) ( +g ‘ 𝑅 ) if ( 𝑏 = 𝑒 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) ) )
131 105 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ 𝑏 = 𝑒 ) → ⦋ 𝑏 / 𝑖 ⦌ 𝑋 = ⦋ 𝑒 / 𝑖 ⦌ 𝑋 )
132 131 ifeq1da ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → if ( 𝑏 = 𝑒 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) = if ( 𝑏 = 𝑒 , ⦋ 𝑒 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) )
133 ovif2 ⊢ ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · if ( 𝑏 = 𝑒 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = if ( 𝑏 = 𝑒 , ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · ( 1r ‘ 𝑅 ) ) , ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · ( 0g ‘ 𝑅 ) ) )
134 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
135 6 5 134 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ ⦋ 𝑒 / 𝑖 ⦌ 𝑋 ∈ 𝐾 ) → ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · ( 1r ‘ 𝑅 ) ) = ⦋ 𝑒 / 𝑖 ⦌ 𝑋 )
136 68 99 135 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · ( 1r ‘ 𝑅 ) ) = ⦋ 𝑒 / 𝑖 ⦌ 𝑋 )
137 6 5 45 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ ⦋ 𝑒 / 𝑖 ⦌ 𝑋 ∈ 𝐾 ) → ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
138 68 99 137 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
139 136 138 ifeq12d ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → if ( 𝑏 = 𝑒 , ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · ( 1r ‘ 𝑅 ) ) , ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · ( 0g ‘ 𝑅 ) ) ) = if ( 𝑏 = 𝑒 , ⦋ 𝑒 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) )
140 133 139 syl5eq ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · if ( 𝑏 = 𝑒 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = if ( 𝑏 = 𝑒 , ⦋ 𝑒 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) )
141 132 140 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → if ( 𝑏 = 𝑒 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) = ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · if ( 𝑏 = 𝑒 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
142 141 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → ( if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) ( +g ‘ 𝑅 ) if ( 𝑏 = 𝑒 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) ) = ( if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) ( +g ‘ 𝑅 ) ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · if ( 𝑏 = 𝑒 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) )
143 142 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) ( +g ‘ 𝑅 ) if ( 𝑏 = 𝑒 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) ) = ( if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) ( +g ‘ 𝑅 ) ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · if ( 𝑏 = 𝑒 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) )
144 130 143 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → if ( 𝑏 ∈ ( 𝑑 ∪ { 𝑒 } ) , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) = ( if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) ( +g ‘ 𝑅 ) ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · if ( 𝑏 = 𝑒 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) )
145 144 ifeq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ ( 𝑑 ∪ { 𝑒 } ) , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) = if ( 𝑎 = 𝐿 , ( if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) ( +g ‘ 𝑅 ) ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · if ( 𝑏 = 𝑒 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) , ( 𝑎 𝑀 𝑏 ) ) )
146 145 mpoeq3dva ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ ( 𝑑 ∪ { 𝑒 } ) , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , ( if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) ( +g ‘ 𝑅 ) ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · if ( 𝑏 = 𝑒 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) , ( 𝑎 𝑀 𝑏 ) ) ) )
147 146 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ ( 𝑑 ∪ { 𝑒 } ) , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , ( if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) ( +g ‘ 𝑅 ) ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · if ( 𝑏 = 𝑒 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) )
148 6 45 ring0cl ⊢ ( 𝑅 ∈ Ring → ( 0g ‘ 𝑅 ) ∈ 𝐾 )
149 68 148 syl ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → ( 0g ‘ 𝑅 ) ∈ 𝐾 )
150 149 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 0g ‘ 𝑅 ) ∈ 𝐾 )
151 123 150 ifcld ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) ∈ 𝐾 )
152 6 134 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐾 )
153 68 152 syl ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → ( 1r ‘ 𝑅 ) ∈ 𝐾 )
154 153 149 ifcld ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → if ( 𝑏 = 𝑒 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ 𝐾 )
155 6 5 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ⦋ 𝑒 / 𝑖 ⦌ 𝑋 ∈ 𝐾 ∧ if ( 𝑏 = 𝑒 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ 𝐾 ) → ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · if ( 𝑏 = 𝑒 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ 𝐾 )
156 68 99 154 155 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · if ( 𝑏 = 𝑒 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ 𝐾 )
157 156 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · if ( 𝑏 = 𝑒 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ 𝐾 )
158 59 adantr ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ 𝐾 )
159 158 fovrnda ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 𝑀 𝑏 ) ∈ 𝐾 )
160 159 3impb ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝑎 𝑀 𝑏 ) ∈ 𝐾 )
161 4 6 65 66 71 151 157 160 101 mdetrlin2 ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , ( if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) ( +g ‘ 𝑅 ) ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · if ( 𝑏 = 𝑒 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) = ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) ( +g ‘ 𝑅 ) ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · if ( 𝑏 = 𝑒 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) ) )
162 154 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → if ( 𝑏 = 𝑒 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ 𝐾 )
163 4 6 5 66 71 162 160 99 101 mdetrsca2 ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · if ( 𝑏 = 𝑒 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) = ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 = 𝑒 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) ) )
164 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → 𝑀 ∈ 𝐵 )
165 1 4 2 3 134 45 maducoeval ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → ( 𝑒 ( 𝐽 ‘ 𝑀 ) 𝐿 ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 = 𝑒 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) )
166 164 96 101 165 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → ( 𝑒 ( 𝐽 ‘ 𝑀 ) 𝐿 ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 = 𝑒 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) )
167 166 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · ( 𝑒 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) = ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 = 𝑒 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) ) )
168 163 167 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · if ( 𝑏 = 𝑒 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) = ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · ( 𝑒 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) )
169 168 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) ( +g ‘ 𝑅 ) ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · if ( 𝑏 = 𝑒 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) ) = ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) ( +g ‘ 𝑅 ) ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · ( 𝑒 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) )
170 147 161 169 3eqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) ( +g ‘ 𝑅 ) ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · ( 𝑒 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ ( 𝑑 ∪ { 𝑒 } ) , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) )
171 170 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ ( 𝑅 Σg ( 𝑏 ∈ 𝑑 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) ) → ( ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) ( +g ‘ 𝑅 ) ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · ( 𝑒 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ ( 𝑑 ∪ { 𝑒 } ) , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) )
172 109 111 171 3eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ ( 𝑅 Σg ( 𝑏 ∈ 𝑑 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) ) → ( 𝑅 Σg ( 𝑏 ∈ ( 𝑑 ∪ { 𝑒 } ) ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ ( 𝑑 ∪ { 𝑒 } ) , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) )
173 172 ex ⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → ( ( 𝑅 Σg ( 𝑏 ∈ 𝑑 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑑 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) → ( 𝑅 Σg ( 𝑏 ∈ ( 𝑑 ∪ { 𝑒 } ) ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ ( 𝑑 ∪ { 𝑒 } ) , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) ) )
174 18 26 34 42 64 173 56 findcard2d ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑏 ∈ 𝑁 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑁 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) ) )
175 nfcv ⊢ Ⅎ 𝑏 ( 𝑋 · ( 𝑖 ( 𝐽 ‘ 𝑀 ) 𝐿 ) )
176 nfcsb1v ⊢ Ⅎ 𝑖 ⦋ 𝑏 / 𝑖 ⦌ 𝑋
177 nfcv ⊢ Ⅎ 𝑖 ·
178 nfcv ⊢ Ⅎ 𝑖 ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 )
179 176 177 178 nfov ⊢ Ⅎ 𝑖 ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) )
180 csbeq1a ⊢ ( 𝑖 = 𝑏 → 𝑋 = ⦋ 𝑏 / 𝑖 ⦌ 𝑋 )
181 oveq1 ⊢ ( 𝑖 = 𝑏 → ( 𝑖 ( 𝐽 ‘ 𝑀 ) 𝐿 ) = ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) )
182 180 181 oveq12d ⊢ ( 𝑖 = 𝑏 → ( 𝑋 · ( 𝑖 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) = ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) )
183 175 179 182 cbvmpt ⊢ ( 𝑖 ∈ 𝑁 ↦ ( 𝑋 · ( 𝑖 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) = ( 𝑏 ∈ 𝑁 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) )
184 183 oveq2i ⊢ ( 𝑅 Σg ( 𝑖 ∈ 𝑁 ↦ ( 𝑋 · ( 𝑖 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) = ( 𝑅 Σg ( 𝑏 ∈ 𝑁 ↦ ( ⦋ 𝑏 / 𝑖 ⦌ 𝑋 · ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) )
185 nfcv ⊢ Ⅎ 𝑎 if ( 𝑗 = 𝐿 , 𝑋 , ( 𝑗 𝑀 𝑖 ) )
186 nfcv ⊢ Ⅎ 𝑏 if ( 𝑗 = 𝐿 , 𝑋 , ( 𝑗 𝑀 𝑖 ) )
187 nfcv ⊢ Ⅎ 𝑗 if ( 𝑎 = 𝐿 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 𝑎 𝑀 𝑏 ) )
188 nfv ⊢ Ⅎ 𝑖 𝑎 = 𝐿
189 nfcv ⊢ Ⅎ 𝑖 ( 𝑎 𝑀 𝑏 )
190 188 176 189 nfif ⊢ Ⅎ 𝑖 if ( 𝑎 = 𝐿 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 𝑎 𝑀 𝑏 ) )
191 eqeq1 ⊢ ( 𝑗 = 𝑎 → ( 𝑗 = 𝐿 ↔ 𝑎 = 𝐿 ) )
192 191 adantr ⊢ ( ( 𝑗 = 𝑎 ∧ 𝑖 = 𝑏 ) → ( 𝑗 = 𝐿 ↔ 𝑎 = 𝐿 ) )
193 180 adantl ⊢ ( ( 𝑗 = 𝑎 ∧ 𝑖 = 𝑏 ) → 𝑋 = ⦋ 𝑏 / 𝑖 ⦌ 𝑋 )
194 oveq12 ⊢ ( ( 𝑗 = 𝑎 ∧ 𝑖 = 𝑏 ) → ( 𝑗 𝑀 𝑖 ) = ( 𝑎 𝑀 𝑏 ) )
195 192 193 194 ifbieq12d ⊢ ( ( 𝑗 = 𝑎 ∧ 𝑖 = 𝑏 ) → if ( 𝑗 = 𝐿 , 𝑋 , ( 𝑗 𝑀 𝑖 ) ) = if ( 𝑎 = 𝐿 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 𝑎 𝑀 𝑏 ) ) )
196 185 186 187 190 195 cbvmpo ⊢ ( 𝑗 ∈ 𝑁 , 𝑖 ∈ 𝑁 ↦ if ( 𝑗 = 𝐿 , 𝑋 , ( 𝑗 𝑀 𝑖 ) ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 𝑎 𝑀 𝑏 ) ) )
197 iftrue ⊢ ( 𝑏 ∈ 𝑁 → if ( 𝑏 ∈ 𝑁 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) = ⦋ 𝑏 / 𝑖 ⦌ 𝑋 )
198 197 eqcomd ⊢ ( 𝑏 ∈ 𝑁 → ⦋ 𝑏 / 𝑖 ⦌ 𝑋 = if ( 𝑏 ∈ 𝑁 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) )
199 198 adantl ⊢ ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ⦋ 𝑏 / 𝑖 ⦌ 𝑋 = if ( 𝑏 ∈ 𝑁 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) )
200 199 ifeq1d ⊢ ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → if ( 𝑎 = 𝐿 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 𝑎 𝑀 𝑏 ) ) = if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑁 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) )
201 200 mpoeq3ia ⊢ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 𝑎 𝑀 𝑏 ) ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑁 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) )
202 196 201 eqtri ⊢ ( 𝑗 ∈ 𝑁 , 𝑖 ∈ 𝑁 ↦ if ( 𝑗 = 𝐿 , 𝑋 , ( 𝑗 𝑀 𝑖 ) ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑁 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) )
203 202 fveq2i ⊢ ( 𝐷 ‘ ( 𝑗 ∈ 𝑁 , 𝑖 ∈ 𝑁 ↦ if ( 𝑗 = 𝐿 , 𝑋 , ( 𝑗 𝑀 𝑖 ) ) ) ) = ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , if ( 𝑏 ∈ 𝑁 , ⦋ 𝑏 / 𝑖 ⦌ 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 𝑎 𝑀 𝑏 ) ) ) )
204 174 184 203 3eqtr4g ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑖 ∈ 𝑁 ↦ ( 𝑋 · ( 𝑖 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ) ) ) = ( 𝐷 ‘ ( 𝑗 ∈ 𝑁 , 𝑖 ∈ 𝑁 ↦ if ( 𝑗 = 𝐿 , 𝑋 , ( 𝑗 𝑀 𝑖 ) ) ) ) )