Theorem madugsum 22563

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

Hypotheses

Ref	Expression
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

Ref	Expression
madugsum	⊢ (𝜑 → (𝑅 Σg (𝑖 ∈ 𝑁 ↦ (𝑋 · (𝑖(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑗 ∈ 𝑁, 𝑖 ∈ 𝑁 ↦ if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖)))))

Distinct variable groups:   𝑖,𝑁,𝑗   𝑅,𝑖,𝑗   𝐵,𝑖,𝑗   𝜑,𝑖,𝑗   𝑖,𝐽   𝑖,𝐾,𝑗   𝑖,𝑀,𝑗   𝑗,𝑋   · ,𝑖   𝑖,𝐿,𝑗

Allowed substitution hints:   𝐴(𝑖,𝑗)   𝐷(𝑖,𝑗)   · (𝑗)   𝐽(𝑗)   𝑋(𝑖)

Proof of Theorem madugsum

Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mpteq1 5191	. . . . 5 ⊢ (𝑐 = ∅ → (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))) = (𝑏 ∈ ∅ ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))
2	1	oveq2d 7385	. . . 4 ⊢ (𝑐 = ∅ → (𝑅 Σg (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝑅 Σg (𝑏 ∈ ∅ ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))))
3		eleq2 2817	. . . . . . . 8 ⊢ (𝑐 = ∅ → (𝑏 ∈ 𝑐 ↔ 𝑏 ∈ ∅))
4	3	ifbid 4508	. . . . . . 7 ⊢ (𝑐 = ∅ → if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)))
5	4	ifeq1d 4504	. . . . . 6 ⊢ (𝑐 = ∅ → if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))
6	5	mpoeq3dv 7448	. . . . 5 ⊢ (𝑐 = ∅ → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))
7	6	fveq2d 6844	. . . 4 ⊢ (𝑐 = ∅ → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))
8	2, 7	eqeq12d 2745	. . 3 ⊢ (𝑐 = ∅ → ((𝑅 Σg (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) ↔ (𝑅 Σg (𝑏 ∈ ∅ ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))))
9		mpteq1 5191	. . . . 5 ⊢ (𝑐 = 𝑑 → (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))) = (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))
10	9	oveq2d 7385	. . . 4 ⊢ (𝑐 = 𝑑 → (𝑅 Σg (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))))
11		eleq2 2817	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → (𝑏 ∈ 𝑐 ↔ 𝑏 ∈ 𝑑))
12	11	ifbid 4508	. . . . . . 7 ⊢ (𝑐 = 𝑑 → if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)))
13	12	ifeq1d 4504	. . . . . 6 ⊢ (𝑐 = 𝑑 → if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))
14	13	mpoeq3dv 7448	. . . . 5 ⊢ (𝑐 = 𝑑 → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))
15	14	fveq2d 6844	. . . 4 ⊢ (𝑐 = 𝑑 → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))
16	10, 15	eqeq12d 2745	. . 3 ⊢ (𝑐 = 𝑑 → ((𝑅 Σg (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) ↔ (𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))))
17		mpteq1 5191	. . . . 5 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))) = (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))
18	17	oveq2d 7385	. . . 4 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → (𝑅 Σg (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝑅 Σg (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))))
19		eleq2 2817	. . . . . . . 8 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → (𝑏 ∈ 𝑐 ↔ 𝑏 ∈ (𝑑 ∪ {𝑒})))
20	19	ifbid 4508	. . . . . . 7 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)))
21	20	ifeq1d 4504	. . . . . 6 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))
22	21	mpoeq3dv 7448	. . . . 5 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))
23	22	fveq2d 6844	. . . 4 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))
24	18, 23	eqeq12d 2745	. . 3 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → ((𝑅 Σg (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) ↔ (𝑅 Σg (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))))
25		mpteq1 5191	. . . . 5 ⊢ (𝑐 = 𝑁 → (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))) = (𝑏 ∈ 𝑁 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))
26	25	oveq2d 7385	. . . 4 ⊢ (𝑐 = 𝑁 → (𝑅 Σg (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝑅 Σg (𝑏 ∈ 𝑁 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))))
27		eleq2 2817	. . . . . . . 8 ⊢ (𝑐 = 𝑁 → (𝑏 ∈ 𝑐 ↔ 𝑏 ∈ 𝑁))
28	27	ifbid 4508	. . . . . . 7 ⊢ (𝑐 = 𝑁 → if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)))
29	28	ifeq1d 4504	. . . . . 6 ⊢ (𝑐 = 𝑁 → if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))
30	29	mpoeq3dv 7448	. . . . 5 ⊢ (𝑐 = 𝑁 → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))
31	30	fveq2d 6844	. . . 4 ⊢ (𝑐 = 𝑁 → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))
32	26, 31	eqeq12d 2745	. . 3 ⊢ (𝑐 = 𝑁 → ((𝑅 Σg (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) ↔ (𝑅 Σg (𝑏 ∈ 𝑁 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))))
33		mpt0 6642	. . . . . 6 ⊢ (𝑏 ∈ ∅ ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))) = ∅
34	33	oveq2i 7380	. . . . 5 ⊢ (𝑅 Σg (𝑏 ∈ ∅ ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝑅 Σg ∅)
35		eqid 2729	. . . . . 6 ⊢ (0g‘𝑅) = (0g‘𝑅)
36	35	gsum0 18593	. . . . 5 ⊢ (𝑅 Σg ∅) = (0g‘𝑅)
37	34, 36	eqtri 2752	. . . 4 ⊢ (𝑅 Σg (𝑏 ∈ ∅ ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (0g‘𝑅)
38		noel 4297	. . . . . . . . 9 ⊢ ¬ 𝑏 ∈ ∅
39		iffalse 4493	. . . . . . . . 9 ⊢ (¬ 𝑏 ∈ ∅ → if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = (0g‘𝑅))
40	38, 39	mp1i 13	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = (0g‘𝑅))
41	40	ifeq1d 4504	. . . . . . 7 ⊢ ((𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, (0g‘𝑅), (𝑎𝑀𝑏)))
42	41	mpoeq3ia 7447	. . . . . 6 ⊢ (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (0g‘𝑅), (𝑎𝑀𝑏)))
43	42	fveq2i 6843	. . . . 5 ⊢ (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (0g‘𝑅), (𝑎𝑀𝑏))))
44		madugsum.d	. . . . . 6 ⊢ 𝐷 = (𝑁 maDet 𝑅)
45		madugsum.k	. . . . . 6 ⊢ 𝐾 = (Base‘𝑅)
46		madugsum.r	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ CRing)
47		madugsum.m	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ 𝐵)
48		maduf.a	. . . . . . . . 9 ⊢ 𝐴 = (𝑁 Mat 𝑅)
49		maduf.b	. . . . . . . . 9 ⊢ 𝐵 = (Base‘𝐴)
50	48, 49	matrcl 22332	. . . . . . . 8 ⊢ (𝑀 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
51	47, 50	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
52	51	simpld 494	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ Fin)
53	48, 45, 49	matbas2i 22342	. . . . . . . . 9 ⊢ (𝑀 ∈ 𝐵 → 𝑀 ∈ (𝐾 ↑m (𝑁 × 𝑁)))
54		elmapi 8799	. . . . . . . . 9 ⊢ (𝑀 ∈ (𝐾 ↑m (𝑁 × 𝑁)) → 𝑀:(𝑁 × 𝑁)⟶𝐾)
55	47, 53, 54	3syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑀:(𝑁 × 𝑁)⟶𝐾)
56	55	fovcdmda 7540	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎𝑀𝑏) ∈ 𝐾)
57	56	3impb 1114	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (𝑎𝑀𝑏) ∈ 𝐾)
58		madugsum.l	. . . . . 6 ⊢ (𝜑 → 𝐿 ∈ 𝑁)
59	44, 45, 35, 46, 52, 57, 58	mdetr0 22525	. . . . 5 ⊢ (𝜑 → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (0g‘𝑅), (𝑎𝑀𝑏)))) = (0g‘𝑅))
60	43, 59	eqtrid 2776	. . . 4 ⊢ (𝜑 → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) = (0g‘𝑅))
61	37, 60	eqtr4id 2783	. . 3 ⊢ (𝜑 → (𝑅 Σg (𝑏 ∈ ∅ ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))
62		eqid 2729	. . . . . . 7 ⊢ (+g‘𝑅) = (+g‘𝑅)
63	46	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑅 ∈ CRing)
64		crngring 20165	. . . . . . . . 9 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
65	63, 64	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑅 ∈ Ring)
66		ringcmn 20202	. . . . . . . 8 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
67	65, 66	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑅 ∈ CMnd)
68	52	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑁 ∈ Fin)
69		simprl 770	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑑 ⊆ 𝑁)
70	68, 69	ssfid 9188	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑑 ∈ Fin)
71	65	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → 𝑅 ∈ Ring)
72	69	sselda 3943	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → 𝑏 ∈ 𝑁)
73		madugsum.x	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → 𝑋 ∈ 𝐾)
74	73	ralrimiva 3125	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐾)
75	74	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐾)
76		rspcsbela 4397	. . . . . . . . 9 ⊢ ((𝑏 ∈ 𝑁 ∧ ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐾) → ⦋𝑏 / 𝑖⦌𝑋 ∈ 𝐾)
77	72, 75, 76	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → ⦋𝑏 / 𝑖⦌𝑋 ∈ 𝐾)
78		maduf.j	. . . . . . . . . . . . . 14 ⊢ 𝐽 = (𝑁 maAdju 𝑅)
79	48, 78, 49	maduf 22561	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ CRing → 𝐽:𝐵⟶𝐵)
80	46, 79	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽:𝐵⟶𝐵)
81	80, 47	ffvelcdmd 7039	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐽‘𝑀) ∈ 𝐵)
82	48, 45, 49	matbas2i 22342	. . . . . . . . . . 11 ⊢ ((𝐽‘𝑀) ∈ 𝐵 → (𝐽‘𝑀) ∈ (𝐾 ↑m (𝑁 × 𝑁)))
83		elmapi 8799	. . . . . . . . . . 11 ⊢ ((𝐽‘𝑀) ∈ (𝐾 ↑m (𝑁 × 𝑁)) → (𝐽‘𝑀):(𝑁 × 𝑁)⟶𝐾)
84	81, 82, 83	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝐽‘𝑀):(𝑁 × 𝑁)⟶𝐾)
85	84	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → (𝐽‘𝑀):(𝑁 × 𝑁)⟶𝐾)
86	58	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → 𝐿 ∈ 𝑁)
87	85, 72, 86	fovcdmd 7541	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → (𝑏(𝐽‘𝑀)𝐿) ∈ 𝐾)
88		madugsum.t	. . . . . . . . 9 ⊢ · = (.r‘𝑅)
89	45, 88	ringcl 20170	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ ⦋𝑏 / 𝑖⦌𝑋 ∈ 𝐾 ∧ (𝑏(𝐽‘𝑀)𝐿) ∈ 𝐾) → (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)) ∈ 𝐾)
90	71, 77, 87, 89	syl3anc 1373	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)) ∈ 𝐾)
91		vex 3448	. . . . . . . 8 ⊢ 𝑒 ∈ V
92	91	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑒 ∈ V)
93		eldifn 4091	. . . . . . . 8 ⊢ (𝑒 ∈ (𝑁 ∖ 𝑑) → ¬ 𝑒 ∈ 𝑑)
94	93	ad2antll 729	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ¬ 𝑒 ∈ 𝑑)
95		eldifi 4090	. . . . . . . . . 10 ⊢ (𝑒 ∈ (𝑁 ∖ 𝑑) → 𝑒 ∈ 𝑁)
96	95	ad2antll 729	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑒 ∈ 𝑁)
97	74	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐾)
98		rspcsbela 4397	. . . . . . . . 9 ⊢ ((𝑒 ∈ 𝑁 ∧ ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐾) → ⦋𝑒 / 𝑖⦌𝑋 ∈ 𝐾)
99	96, 97, 98	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ⦋𝑒 / 𝑖⦌𝑋 ∈ 𝐾)
100	84	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝐽‘𝑀):(𝑁 × 𝑁)⟶𝐾)
101	58	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝐿 ∈ 𝑁)
102	100, 96, 101	fovcdmd 7541	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝑒(𝐽‘𝑀)𝐿) ∈ 𝐾)
103	45, 88	ringcl 20170	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ ⦋𝑒 / 𝑖⦌𝑋 ∈ 𝐾 ∧ (𝑒(𝐽‘𝑀)𝐿) ∈ 𝐾) → (⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿)) ∈ 𝐾)
104	65, 99, 102, 103	syl3anc 1373	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿)) ∈ 𝐾)
105		csbeq1 3862	. . . . . . . 8 ⊢ (𝑏 = 𝑒 → ⦋𝑏 / 𝑖⦌𝑋 = ⦋𝑒 / 𝑖⦌𝑋)
106		oveq1 7376	. . . . . . . 8 ⊢ (𝑏 = 𝑒 → (𝑏(𝐽‘𝑀)𝐿) = (𝑒(𝐽‘𝑀)𝐿))
107	105, 106	oveq12d 7387	. . . . . . 7 ⊢ (𝑏 = 𝑒 → (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)) = (⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿)))
108	45, 62, 67, 70, 90, 92, 94, 104, 107	gsumunsn 19874	. . . . . 6 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝑅 Σg (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = ((𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))))
109	108	adantr 480	. . . . 5 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ (𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))) → (𝑅 Σg (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = ((𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))))
110		oveq1 7376	. . . . . 6 ⊢ ((𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) → ((𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))) = ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))))
111	110	adantl 481	. . . . 5 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ (𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))) → ((𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))) = ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))))
112		elun 4112	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ (𝑑 ∪ {𝑒}) ↔ (𝑏 ∈ 𝑑 ∨ 𝑏 ∈ {𝑒}))
113		velsn 4601	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ {𝑒} ↔ 𝑏 = 𝑒)
114	113	orbi2i 912	. . . . . . . . . . . . . 14 ⊢ ((𝑏 ∈ 𝑑 ∨ 𝑏 ∈ {𝑒}) ↔ (𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒))
115	112, 114	bitri 275	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ (𝑑 ∪ {𝑒}) ↔ (𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒))
116		ifbi 4507	. . . . . . . . . . . . 13 ⊢ ((𝑏 ∈ (𝑑 ∪ {𝑒}) ↔ (𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒)) → if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = if((𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)))
117	115, 116	ax-mp 5	. . . . . . . . . . . 12 ⊢ if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = if((𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))
118		ringmnd 20163	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
119	65, 118	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑅 ∈ Mnd)
120	119	3ad2ant1 1133	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝑅 ∈ Mnd)
121		simp3 1138	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝑏 ∈ 𝑁)
122	97	3ad2ant1 1133	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐾)
123	121, 122, 76	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → ⦋𝑏 / 𝑖⦌𝑋 ∈ 𝐾)
124		elequ1 2116	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑒 → (𝑏 ∈ 𝑑 ↔ 𝑒 ∈ 𝑑))
125	124	biimpac 478	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 ∈ 𝑑 ∧ 𝑏 = 𝑒) → 𝑒 ∈ 𝑑)
126	94, 125	nsyl 140	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ¬ (𝑏 ∈ 𝑑 ∧ 𝑏 = 𝑒))
127	126	3ad2ant1 1133	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → ¬ (𝑏 ∈ 𝑑 ∧ 𝑏 = 𝑒))
128	45, 35, 62	mndifsplit 22556	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Mnd ∧ ⦋𝑏 / 𝑖⦌𝑋 ∈ 𝐾 ∧ ¬ (𝑏 ∈ 𝑑 ∧ 𝑏 = 𝑒)) → if((𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))))
129	120, 123, 127, 128	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if((𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))))
130	117, 129	eqtrid 2776	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))))
131	105	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 = 𝑒) → ⦋𝑏 / 𝑖⦌𝑋 = ⦋𝑒 / 𝑖⦌𝑋)
132	131	ifeq1da 4516	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = if(𝑏 = 𝑒, ⦋𝑒 / 𝑖⦌𝑋, (0g‘𝑅)))
133		ovif2 7468	. . . . . . . . . . . . . . 15 ⊢ (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))) = if(𝑏 = 𝑒, (⦋𝑒 / 𝑖⦌𝑋 · (1r‘𝑅)), (⦋𝑒 / 𝑖⦌𝑋 · (0g‘𝑅)))
134		eqid 2729	. . . . . . . . . . . . . . . . . 18 ⊢ (1r‘𝑅) = (1r‘𝑅)
135	45, 88, 134	ringridm 20190	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Ring ∧ ⦋𝑒 / 𝑖⦌𝑋 ∈ 𝐾) → (⦋𝑒 / 𝑖⦌𝑋 · (1r‘𝑅)) = ⦋𝑒 / 𝑖⦌𝑋)
136	65, 99, 135	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (⦋𝑒 / 𝑖⦌𝑋 · (1r‘𝑅)) = ⦋𝑒 / 𝑖⦌𝑋)
137	45, 88, 35	ringrz 20214	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Ring ∧ ⦋𝑒 / 𝑖⦌𝑋 ∈ 𝐾) → (⦋𝑒 / 𝑖⦌𝑋 · (0g‘𝑅)) = (0g‘𝑅))
138	65, 99, 137	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (⦋𝑒 / 𝑖⦌𝑋 · (0g‘𝑅)) = (0g‘𝑅))
139	136, 138	ifeq12d 4506	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → if(𝑏 = 𝑒, (⦋𝑒 / 𝑖⦌𝑋 · (1r‘𝑅)), (⦋𝑒 / 𝑖⦌𝑋 · (0g‘𝑅))) = if(𝑏 = 𝑒, ⦋𝑒 / 𝑖⦌𝑋, (0g‘𝑅)))
140	133, 139	eqtrid 2776	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))) = if(𝑏 = 𝑒, ⦋𝑒 / 𝑖⦌𝑋, (0g‘𝑅)))
141	132, 140	eqtr4d 2767	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))))
142	141	oveq2d 7385	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))) = (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)))))
143	142	3ad2ant1 1133	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))) = (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)))))
144	130, 143	eqtrd 2764	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)))))
145	144	ifeq1d 4504	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)))), (𝑎𝑀𝑏)))
146	145	mpoeq3dva 7446	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)))), (𝑎𝑀𝑏))))
147	146	fveq2d 6844	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)))), (𝑎𝑀𝑏)))))
148	45, 35	ring0cl 20187	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Ring → (0g‘𝑅) ∈ 𝐾)
149	65, 148	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (0g‘𝑅) ∈ 𝐾)
150	149	3ad2ant1 1133	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (0g‘𝑅) ∈ 𝐾)
151	123, 150	ifcld 4531	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) ∈ 𝐾)
152	45, 134	ringidcl 20185	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ Ring → (1r‘𝑅) ∈ 𝐾)
153	65, 152	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (1r‘𝑅) ∈ 𝐾)
154	153, 149	ifcld 4531	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)) ∈ 𝐾)
155	45, 88	ringcl 20170	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Ring ∧ ⦋𝑒 / 𝑖⦌𝑋 ∈ 𝐾 ∧ if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)) ∈ 𝐾) → (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))) ∈ 𝐾)
156	65, 99, 154, 155	syl3anc 1373	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))) ∈ 𝐾)
157	156	3ad2ant1 1133	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))) ∈ 𝐾)
158	55	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑀:(𝑁 × 𝑁)⟶𝐾)
159	158	fovcdmda 7540	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎𝑀𝑏) ∈ 𝐾)
160	159	3impb 1114	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (𝑎𝑀𝑏) ∈ 𝐾)
161	44, 45, 62, 63, 68, 151, 157, 160, 101	mdetrlin2 22527	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)))), (𝑎𝑀𝑏)))) = ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))(+g‘𝑅)(𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))), (𝑎𝑀𝑏))))))
162	154	3ad2ant1 1133	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)) ∈ 𝐾)
163	44, 45, 88, 63, 68, 162, 160, 99, 101	mdetrsca2 22524	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))), (𝑎𝑀𝑏)))) = (⦋𝑒 / 𝑖⦌𝑋 · (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)), (𝑎𝑀𝑏))))))
164	47	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑀 ∈ 𝐵)
165	48, 44, 78, 49, 134, 35	maducoeval 22559	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) → (𝑒(𝐽‘𝑀)𝐿) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)), (𝑎𝑀𝑏)))))
166	164, 96, 101, 165	syl3anc 1373	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝑒(𝐽‘𝑀)𝐿) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)), (𝑎𝑀𝑏)))))
167	166	oveq2d 7385	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿)) = (⦋𝑒 / 𝑖⦌𝑋 · (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)), (𝑎𝑀𝑏))))))
168	163, 167	eqtr4d 2767	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))), (𝑎𝑀𝑏)))) = (⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿)))
169	168	oveq2d 7385	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))(+g‘𝑅)(𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))), (𝑎𝑀𝑏))))) = ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))))
170	147, 161, 169	3eqtrrd 2769	. . . . . 6 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))
171	170	adantr 480	. . . . 5 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ (𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))) → ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))
172	109, 111, 171	3eqtrd 2768	. . . 4 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ (𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))) → (𝑅 Σg (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))
173	172	ex 412	. . 3 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ((𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) → (𝑅 Σg (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))))
174	8, 16, 24, 32, 61, 173, 52	findcard2d 9107	. 2 ⊢ (𝜑 → (𝑅 Σg (𝑏 ∈ 𝑁 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))
175		nfcv 2891	. . . 4 ⊢ Ⅎ𝑏(𝑋 · (𝑖(𝐽‘𝑀)𝐿))
176		nfcsb1v 3883	. . . . 5 ⊢ Ⅎ𝑖⦋𝑏 / 𝑖⦌𝑋
177		nfcv 2891	. . . . 5 ⊢ Ⅎ𝑖 ·
178		nfcv 2891	. . . . 5 ⊢ Ⅎ𝑖(𝑏(𝐽‘𝑀)𝐿)
179	176, 177, 178	nfov 7399	. . . 4 ⊢ Ⅎ𝑖(⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))
180		csbeq1a 3873	. . . . 5 ⊢ (𝑖 = 𝑏 → 𝑋 = ⦋𝑏 / 𝑖⦌𝑋)
181		oveq1 7376	. . . . 5 ⊢ (𝑖 = 𝑏 → (𝑖(𝐽‘𝑀)𝐿) = (𝑏(𝐽‘𝑀)𝐿))
182	180, 181	oveq12d 7387	. . . 4 ⊢ (𝑖 = 𝑏 → (𝑋 · (𝑖(𝐽‘𝑀)𝐿)) = (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))
183	175, 179, 182	cbvmpt 5204	. . 3 ⊢ (𝑖 ∈ 𝑁 ↦ (𝑋 · (𝑖(𝐽‘𝑀)𝐿))) = (𝑏 ∈ 𝑁 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))
184	183	oveq2i 7380	. 2 ⊢ (𝑅 Σg (𝑖 ∈ 𝑁 ↦ (𝑋 · (𝑖(𝐽‘𝑀)𝐿)))) = (𝑅 Σg (𝑏 ∈ 𝑁 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))
185		nfcv 2891	. . . . 5 ⊢ Ⅎ𝑎if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖))
186		nfcv 2891	. . . . 5 ⊢ Ⅎ𝑏if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖))
187		nfcv 2891	. . . . 5 ⊢ Ⅎ𝑗if(𝑎 = 𝐿, ⦋𝑏 / 𝑖⦌𝑋, (𝑎𝑀𝑏))
188		nfv 1914	. . . . . 6 ⊢ Ⅎ𝑖 𝑎 = 𝐿
189		nfcv 2891	. . . . . 6 ⊢ Ⅎ𝑖(𝑎𝑀𝑏)
190	188, 176, 189	nfif 4515	. . . . 5 ⊢ Ⅎ𝑖if(𝑎 = 𝐿, ⦋𝑏 / 𝑖⦌𝑋, (𝑎𝑀𝑏))
191		eqeq1 2733	. . . . . . 7 ⊢ (𝑗 = 𝑎 → (𝑗 = 𝐿 ↔ 𝑎 = 𝐿))
192	191	adantr 480	. . . . . 6 ⊢ ((𝑗 = 𝑎 ∧ 𝑖 = 𝑏) → (𝑗 = 𝐿 ↔ 𝑎 = 𝐿))
193	180	adantl 481	. . . . . 6 ⊢ ((𝑗 = 𝑎 ∧ 𝑖 = 𝑏) → 𝑋 = ⦋𝑏 / 𝑖⦌𝑋)
194		oveq12 7378	. . . . . 6 ⊢ ((𝑗 = 𝑎 ∧ 𝑖 = 𝑏) → (𝑗𝑀𝑖) = (𝑎𝑀𝑏))
195	192, 193, 194	ifbieq12d 4513	. . . . 5 ⊢ ((𝑗 = 𝑎 ∧ 𝑖 = 𝑏) → if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖)) = if(𝑎 = 𝐿, ⦋𝑏 / 𝑖⦌𝑋, (𝑎𝑀𝑏)))
196	185, 186, 187, 190, 195	cbvmpo 7463	. . . 4 ⊢ (𝑗 ∈ 𝑁, 𝑖 ∈ 𝑁 ↦ if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, ⦋𝑏 / 𝑖⦌𝑋, (𝑎𝑀𝑏)))
197		iftrue 4490	. . . . . . . 8 ⊢ (𝑏 ∈ 𝑁 → if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = ⦋𝑏 / 𝑖⦌𝑋)
198	197	eqcomd 2735	. . . . . . 7 ⊢ (𝑏 ∈ 𝑁 → ⦋𝑏 / 𝑖⦌𝑋 = if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)))
199	198	adantl 481	. . . . . 6 ⊢ ((𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → ⦋𝑏 / 𝑖⦌𝑋 = if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)))
200	199	ifeq1d 4504	. . . . 5 ⊢ ((𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑎 = 𝐿, ⦋𝑏 / 𝑖⦌𝑋, (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))
201	200	mpoeq3ia 7447	. . . 4 ⊢ (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, ⦋𝑏 / 𝑖⦌𝑋, (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))
202	196, 201	eqtri 2752	. . 3 ⊢ (𝑗 ∈ 𝑁, 𝑖 ∈ 𝑁 ↦ if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))
203	202	fveq2i 6843	. 2 ⊢ (𝐷‘(𝑗 ∈ 𝑁, 𝑖 ∈ 𝑁 ↦ if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))
204	174, 184, 203	3eqtr4g 2789	1 ⊢ (𝜑 → (𝑅 Σg (𝑖 ∈ 𝑁 ↦ (𝑋 · (𝑖(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑗 ∈ 𝑁, 𝑖 ∈ 𝑁 ↦ if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖)))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ∀wral 3044  Vcvv 3444  ⦋csb 3859   ∖ cdif 3908   ∪ cun 3909   ⊆ wss 3911  ∅c0 4292  ifcif 4484  {csn 4585   ↦ cmpt 5183   × cxp 5629  ⟶wf 6495  ‘cfv 6499  (class class class)co 7369   ∈ cmpo 7371   ↑_m cmap 8776  Fincfn 8895  Basecbs 17155  +_gcplusg 17196  ._rcmulr 17197  0_gc0g 17378   Σ_g cgsu 17379  Mndcmnd 18643  CMndccmn 19694  1_rcur 20101  Ringcrg 20153  CRingccrg 20154   Mat cmat 22327   maDet cmdat 22504   maAdju cmadu 22552

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5229  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-cnex 11100  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120  ax-pre-mulgt0 11121  ax-addf 11123  ax-mulf 11124

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-xor 1512  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-ot 4594  df-uni 4868  df-int 4907  df-iun 4953  df-iin 4954  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-isom 6508  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-of 7633  df-om 7823  df-1st 7947  df-2nd 7948  df-supp 8117  df-tpos 8182  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-1o 8411  df-2o 8412  df-er 8648  df-map 8778  df-pm 8779  df-ixp 8848  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-fsupp 9289  df-sup 9369  df-oi 9439  df-card 9868  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-sub 11383  df-neg 11384  df-div 11812  df-nn 12163  df-2 12225  df-3 12226  df-4 12227  df-5 12228  df-6 12229  df-7 12230  df-8 12231  df-9 12232  df-n0 12419  df-xnn0 12492  df-z 12506  df-dec 12626  df-uz 12770  df-rp 12928  df-fz 13445  df-fzo 13592  df-seq 13943  df-exp 14003  df-hash 14272  df-word 14455  df-lsw 14504  df-concat 14512  df-s1 14537  df-substr 14582  df-pfx 14612  df-splice 14691  df-reverse 14700  df-s2 14790  df-struct 17093  df-sets 17110  df-slot 17128  df-ndx 17140  df-base 17156  df-ress 17177  df-plusg 17209  df-mulr 17210  df-starv 17211  df-sca 17212  df-vsca 17213  df-ip 17214  df-tset 17215  df-ple 17216  df-ds 17218  df-unif 17219  df-hom 17220  df-cco 17221  df-0g 17380  df-gsum 17381  df-prds 17386  df-pws 17388  df-mre 17523  df-mrc 17524  df-acs 17526  df-mgm 18549  df-sgrp 18628  df-mnd 18644  df-mhm 18692  df-submnd 18693  df-efmnd 18778  df-grp 18850  df-minusg 18851  df-mulg 18982  df-subg 19037  df-ghm 19127  df-gim 19173  df-cntz 19231  df-oppg 19260  df-symg 19284  df-pmtr 19356  df-psgn 19405  df-cmn 19696  df-abl 19697  df-mgp 20061  df-rng 20073  df-ur 20102  df-ring 20155  df-cring 20156  df-oppr 20257  df-dvdsr 20277  df-unit 20278  df-invr 20308  df-dvr 20321  df-rhm 20392  df-subrng 20466  df-subrg 20490  df-drng 20651  df-sra 21112  df-rgmod 21113  df-cnfld 21297  df-zring 21389  df-zrh 21445  df-dsmm 21674  df-frlm 21689  df-mat 22328  df-mdet 22505  df-madu 22554

This theorem is referenced by:  madurid  22564  mdetlap1  33809