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	fovcdmda	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 𝑀 𝑏 ) ∈ 𝐾 )
61	60	3impb	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝑎 𝑀 𝑏 ) ∈ 𝐾 )
62	4 6 45 8 56 61 10	mdetr0	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝐿 , ( 0g ‘ 𝑅 ) , ( 𝑎 𝑀 𝑏 ) ) ) ) = ( 0g ‘ 𝑅 ) )
63	53 62	eqtrid	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ 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	ffvelcdmd	⊢ ( 𝜑 → ( 𝐽 ‘ 𝑀 ) ∈ 𝐵 )
83	1 6 3	matbas2i	⊢ ( ( 𝐽 ‘ 𝑀 ) ∈ 𝐵 → ( 𝐽 ‘ 𝑀 ) ∈ ( 𝐾 ↑m ( 𝑁 × 𝑁 ) ) )
84		elmapi	⊢ ( ( 𝐽 ‘ 𝑀 ) ∈ ( 𝐾 ↑m ( 𝑁 × 𝑁 ) ) → ( 𝐽 ‘ 𝑀 ) : ( 𝑁 × 𝑁 ) ⟶ 𝐾 )
85	82 83 84	3syl	⊢ ( 𝜑 → ( 𝐽 ‘ 𝑀 ) : ( 𝑁 × 𝑁 ) ⟶ 𝐾 )
86	85	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ 𝑏 ∈ 𝑑 ) → ( 𝐽 ‘ 𝑀 ) : ( 𝑁 × 𝑁 ) ⟶ 𝐾 )
87	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ 𝑏 ∈ 𝑑 ) → 𝐿 ∈ 𝑁 )
88	86 75 87	fovcdmd	⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ 𝑏 ∈ 𝑑 ) → ( 𝑏 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ∈ 𝐾 )
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	fovcdmd	⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → ( 𝑒 ( 𝐽 ‘ 𝑀 ) 𝐿 ) ∈ 𝐾 )
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	eqtrid	⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 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	eqtrid	⊢ ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) → ( ⦋ 𝑒 / 𝑖 ⦌ 𝑋 · 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	fovcdmda	⊢ ( ( ( 𝜑 ∧ ( 𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ ( 𝑁 ∖ 𝑑 ) ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 𝑀 𝑏 ) ∈ 𝐾 )
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 ( 𝑗 = 𝐿 , 𝑋 , ( 𝑗 𝑀 𝑖 ) ) ) ) )