Theorem madugsum 22866

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 5194	. . . . 5 ⊢ (𝑐 = ∅ → (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))) = (𝑏 ∈ ∅ ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))
2	1	oveq2d 7430	. . . 4 ⊢ (𝑐 = ∅ → (𝑅 Σg (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝑅 Σg (𝑏 ∈ ∅ ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))))
3		eleq2 2849	. . . . . . . 8 ⊢ (𝑐 = ∅ → (𝑏 ∈ 𝑐 ↔ 𝑏 ∈ ∅))
4	3	ifbid 4506	. . . . . . 7 ⊢ (𝑐 = ∅ → if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)))
5	4	ifeq1d 4502	. . . . . 6 ⊢ (𝑐 = ∅ → if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))
6	5	mpoeq3dv 7493	. . . . 5 ⊢ (𝑐 = ∅ → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))
7	6	fveq2d 6883	. . . 4 ⊢ (𝑐 = ∅ → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))
8	2, 7	eqeq12d 2776	. . 3 ⊢ (𝑐 = ∅ → ((𝑅 Σg (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) ↔ (𝑅 Σg (𝑏 ∈ ∅ ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))))
9		mpteq1 5194	. . . . 5 ⊢ (𝑐 = 𝑑 → (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))) = (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))
10	9	oveq2d 7430	. . . 4 ⊢ (𝑐 = 𝑑 → (𝑅 Σg (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))))
11		eleq2 2849	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → (𝑏 ∈ 𝑐 ↔ 𝑏 ∈ 𝑑))
12	11	ifbid 4506	. . . . . . 7 ⊢ (𝑐 = 𝑑 → if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)))
13	12	ifeq1d 4502	. . . . . 6 ⊢ (𝑐 = 𝑑 → if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))
14	13	mpoeq3dv 7493	. . . . 5 ⊢ (𝑐 = 𝑑 → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))
15	14	fveq2d 6883	. . . 4 ⊢ (𝑐 = 𝑑 → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))
16	10, 15	eqeq12d 2776	. . 3 ⊢ (𝑐 = 𝑑 → ((𝑅 Σg (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) ↔ (𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))))
17		mpteq1 5194	. . . . 5 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))) = (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))
18	17	oveq2d 7430	. . . 4 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → (𝑅 Σg (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝑅 Σg (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))))
19		eleq2 2849	. . . . . . . 8 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → (𝑏 ∈ 𝑐 ↔ 𝑏 ∈ (𝑑 ∪ {𝑒})))
20	19	ifbid 4506	. . . . . . 7 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)))
21	20	ifeq1d 4502	. . . . . 6 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))
22	21	mpoeq3dv 7493	. . . . 5 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))
23	22	fveq2d 6883	. . . 4 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))
24	18, 23	eqeq12d 2776	. . 3 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → ((𝑅 Σg (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) ↔ (𝑅 Σg (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))))
25		mpteq1 5194	. . . . 5 ⊢ (𝑐 = 𝑁 → (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))) = (𝑏 ∈ 𝑁 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))
26	25	oveq2d 7430	. . . 4 ⊢ (𝑐 = 𝑁 → (𝑅 Σg (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝑅 Σg (𝑏 ∈ 𝑁 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))))
27		eleq2 2849	. . . . . . . 8 ⊢ (𝑐 = 𝑁 → (𝑏 ∈ 𝑐 ↔ 𝑏 ∈ 𝑁))
28	27	ifbid 4506	. . . . . . 7 ⊢ (𝑐 = 𝑁 → if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)))
29	28	ifeq1d 4502	. . . . . 6 ⊢ (𝑐 = 𝑁 → if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))
30	29	mpoeq3dv 7493	. . . . 5 ⊢ (𝑐 = 𝑁 → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))
31	30	fveq2d 6883	. . . 4 ⊢ (𝑐 = 𝑁 → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))
32	26, 31	eqeq12d 2776	. . 3 ⊢ (𝑐 = 𝑁 → ((𝑅 Σg (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) ↔ (𝑅 Σg (𝑏 ∈ 𝑁 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))))
33		mpt0 6675	. . . . . 6 ⊢ (𝑏 ∈ ∅ ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))) = ∅
34	33	oveq2i 7425	. . . . 5 ⊢ (𝑅 Σg (𝑏 ∈ ∅ ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝑅 Σg ∅)
35		eqid 2760	. . . . . 6 ⊢ (0g‘𝑅) = (0g‘𝑅)
36	35	gsum0 18787	. . . . 5 ⊢ (𝑅 Σg ∅) = (0g‘𝑅)
37	34, 36	eqtri 2783	. . . 4 ⊢ (𝑅 Σg (𝑏 ∈ ∅ ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (0g‘𝑅)
38		noel 4284	. . . . . . . . 9 ⊢ ¬ 𝑏 ∈ ∅
39		iffalse 4491	. . . . . . . . 9 ⊢ (¬ 𝑏 ∈ ∅ → if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = (0g‘𝑅))
40	38, 39	mp1i 14	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = (0g‘𝑅))
41	40	ifeq1d 4502	. . . . . . 7 ⊢ ((𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, (0g‘𝑅), (𝑎𝑀𝑏)))
42	41	mpoeq3ia 7492	. . . . . 6 ⊢ (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (0g‘𝑅), (𝑎𝑀𝑏)))
43	42	fveq2i 6882	. . . . 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 22635	. . . . . . . 8 ⊢ (𝑀 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
51	47, 50	syl 18	. . . . . . 7 ⊢ (𝜑 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
52	51	simpld 500	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ Fin)
53	48, 45, 49	matbas2i 22645	. . . . . . . . 9 ⊢ (𝑀 ∈ 𝐵 → 𝑀 ∈ (𝐾 ↑m (𝑁 × 𝑁)))
54		elmapi 8849	. . . . . . . . 9 ⊢ (𝑀 ∈ (𝐾 ↑m (𝑁 × 𝑁)) → 𝑀:(𝑁 × 𝑁)⟶𝐾)
55	47, 53, 54	3syl 19	. . . . . . . 8 ⊢ (𝜑 → 𝑀:(𝑁 × 𝑁)⟶𝐾)
56	55	fovcdmda 7586	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎𝑀𝑏) ∈ 𝐾)
57	56	3impb 1132	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (𝑎𝑀𝑏) ∈ 𝐾)
58		madugsum.l	. . . . . 6 ⊢ (𝜑 → 𝐿 ∈ 𝑁)
59	44, 45, 35, 46, 52, 57, 58	mdetr0 22828	. . . . 5 ⊢ (𝜑 → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (0g‘𝑅), (𝑎𝑀𝑏)))) = (0g‘𝑅))
60	43, 59	eqtrid 2807	. . . 4 ⊢ (𝜑 → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) = (0g‘𝑅))
61	37, 60	eqtr4id 2814	. . 3 ⊢ (𝜑 → (𝑅 Σg (𝑏 ∈ ∅ ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))
62		eqid 2760	. . . . . . 7 ⊢ (+g‘𝑅) = (+g‘𝑅)
63	46	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑅 ∈ CRing)
64		crngring 20385	. . . . . . . . 9 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
65	63, 64	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑅 ∈ Ring)
66		ringcmn 20424	. . . . . . . 8 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
67	65, 66	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑅 ∈ CMnd)
68	52	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑁 ∈ Fin)
69		simprl 783	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑑 ⊆ 𝑁)
70	68, 69	ssfid 9240	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑑 ∈ Fin)
71	65	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → 𝑅 ∈ Ring)
72	69	sselda 3931	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → 𝑏 ∈ 𝑁)
73		madugsum.x	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → 𝑋 ∈ 𝐾)
74	73	ralrimiva 3154	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐾)
75	74	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐾)
76		rspcsbela 4396	. . . . . . . . 9 ⊢ ((𝑏 ∈ 𝑁 ∧ ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐾) → ⦋𝑏 / 𝑖⦌𝑋 ∈ 𝐾)
77	72, 75, 76	syl2anc 596	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → ⦋𝑏 / 𝑖⦌𝑋 ∈ 𝐾)
78		maduf.j	. . . . . . . . . . . . . 14 ⊢ 𝐽 = (𝑁 maAdju 𝑅)
79	48, 78, 49	maduf 22864	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ CRing → 𝐽:𝐵⟶𝐵)
80	46, 79	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽:𝐵⟶𝐵)
81	80, 47	ffvelcdmd 7079	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐽‘𝑀) ∈ 𝐵)
82	48, 45, 49	matbas2i 22645	. . . . . . . . . . 11 ⊢ ((𝐽‘𝑀) ∈ 𝐵 → (𝐽‘𝑀) ∈ (𝐾 ↑m (𝑁 × 𝑁)))
83		elmapi 8849	. . . . . . . . . . 11 ⊢ ((𝐽‘𝑀) ∈ (𝐾 ↑m (𝑁 × 𝑁)) → (𝐽‘𝑀):(𝑁 × 𝑁)⟶𝐾)
84	81, 82, 83	3syl 19	. . . . . . . . . 10 ⊢ (𝜑 → (𝐽‘𝑀):(𝑁 × 𝑁)⟶𝐾)
85	84	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → (𝐽‘𝑀):(𝑁 × 𝑁)⟶𝐾)
86	58	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → 𝐿 ∈ 𝑁)
87	85, 72, 86	fovcdmd 7587	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → (𝑏(𝐽‘𝑀)𝐿) ∈ 𝐾)
88		madugsum.t	. . . . . . . . 9 ⊢ · = (.r‘𝑅)
89	45, 88	ringcl 20390	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ ⦋𝑏 / 𝑖⦌𝑋 ∈ 𝐾 ∧ (𝑏(𝐽‘𝑀)𝐿) ∈ 𝐾) → (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)) ∈ 𝐾)
90	71, 77, 87, 89	syl3anc 1398	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)) ∈ 𝐾)
91		vex 3454	. . . . . . . 8 ⊢ 𝑒 ∈ V
92	91	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑒 ∈ V)
93		eldifn 4079	. . . . . . . 8 ⊢ (𝑒 ∈ (𝑁 ∖ 𝑑) → ¬ 𝑒 ∈ 𝑑)
94	93	ad2antll 742	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ¬ 𝑒 ∈ 𝑑)
95		eldifi 4078	. . . . . . . . . 10 ⊢ (𝑒 ∈ (𝑁 ∖ 𝑑) → 𝑒 ∈ 𝑁)
96	95	ad2antll 742	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑒 ∈ 𝑁)
97	74	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐾)
98		rspcsbela 4396	. . . . . . . . 9 ⊢ ((𝑒 ∈ 𝑁 ∧ ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐾) → ⦋𝑒 / 𝑖⦌𝑋 ∈ 𝐾)
99	96, 97, 98	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ⦋𝑒 / 𝑖⦌𝑋 ∈ 𝐾)
100	84	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝐽‘𝑀):(𝑁 × 𝑁)⟶𝐾)
101	58	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝐿 ∈ 𝑁)
102	100, 96, 101	fovcdmd 7587	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝑒(𝐽‘𝑀)𝐿) ∈ 𝐾)
103	45, 88	ringcl 20390	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ ⦋𝑒 / 𝑖⦌𝑋 ∈ 𝐾 ∧ (𝑒(𝐽‘𝑀)𝐿) ∈ 𝐾) → (⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿)) ∈ 𝐾)
104	65, 99, 102, 103	syl3anc 1398	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿)) ∈ 𝐾)
105		csbeq1 3850	. . . . . . . 8 ⊢ (𝑏 = 𝑒 → ⦋𝑏 / 𝑖⦌𝑋 = ⦋𝑒 / 𝑖⦌𝑋)
106		oveq1 7421	. . . . . . . 8 ⊢ (𝑏 = 𝑒 → (𝑏(𝐽‘𝑀)𝐿) = (𝑒(𝐽‘𝑀)𝐿))
107	105, 106	oveq12d 7432	. . . . . . 7 ⊢ (𝑏 = 𝑒 → (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)) = (⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿)))
108	45, 62, 67, 70, 90, 92, 94, 104, 107	gsumunsn 20088	. . . . . 6 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝑅 Σg (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = ((𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))))
109	108	adantr 486	. . . . 5 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ (𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))) → (𝑅 Σg (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = ((𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))))
110		oveq1 7421	. . . . . 6 ⊢ ((𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) → ((𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))) = ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))))
111	110	adantl 487	. . . . 5 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ (𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))) → ((𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))) = ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))))
112		elun 4100	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ (𝑑 ∪ {𝑒}) ↔ (𝑏 ∈ 𝑑 ∨ 𝑏 ∈ {𝑒}))
113		velsn 4600	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ {𝑒} ↔ 𝑏 = 𝑒)
114	113	orbi2i 926	. . . . . . . . . . . . . 14 ⊢ ((𝑏 ∈ 𝑑 ∨ 𝑏 ∈ {𝑒}) ↔ (𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒))
115	112, 114	bitri 278	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ (𝑑 ∪ {𝑒}) ↔ (𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒))
116		ifbi 4505	. . . . . . . . . . . . 13 ⊢ ((𝑏 ∈ (𝑑 ∪ {𝑒}) ↔ (𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒)) → if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = if((𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)))
117	115, 116	ax-mp 5	. . . . . . . . . . . 12 ⊢ if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = if((𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))
118		ringmnd 20383	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
119	65, 118	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑅 ∈ Mnd)
120	119	3ad2ant1 1151	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝑅 ∈ Mnd)
121		simp3 1156	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝑏 ∈ 𝑁)
122	97	3ad2ant1 1151	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐾)
123	121, 122, 76	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → ⦋𝑏 / 𝑖⦌𝑋 ∈ 𝐾)
124		elequ1 2152	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑒 → (𝑏 ∈ 𝑑 ↔ 𝑒 ∈ 𝑑))
125	124	biimpac 484	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 ∈ 𝑑 ∧ 𝑏 = 𝑒) → 𝑒 ∈ 𝑑)
126	94, 125	nsyl 141	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ¬ (𝑏 ∈ 𝑑 ∧ 𝑏 = 𝑒))
127	126	3ad2ant1 1151	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → ¬ (𝑏 ∈ 𝑑 ∧ 𝑏 = 𝑒))
128	45, 35, 62	mndifsplit 22859	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Mnd ∧ ⦋𝑏 / 𝑖⦌𝑋 ∈ 𝐾 ∧ ¬ (𝑏 ∈ 𝑑 ∧ 𝑏 = 𝑒)) → if((𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))))
129	120, 123, 127, 128	syl3anc 1398	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if((𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))))
130	117, 129	eqtrid 2807	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))))
131	105	adantl 487	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 = 𝑒) → ⦋𝑏 / 𝑖⦌𝑋 = ⦋𝑒 / 𝑖⦌𝑋)
132	131	ifeq1da 4514	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = if(𝑏 = 𝑒, ⦋𝑒 / 𝑖⦌𝑋, (0g‘𝑅)))
133		ovif2 7513	. . . . . . . . . . . . . . 15 ⊢ (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))) = if(𝑏 = 𝑒, (⦋𝑒 / 𝑖⦌𝑋 · (1r‘𝑅)), (⦋𝑒 / 𝑖⦌𝑋 · (0g‘𝑅)))
134		eqid 2760	. . . . . . . . . . . . . . . . . 18 ⊢ (1r‘𝑅) = (1r‘𝑅)
135	45, 88, 134	ringridm 20412	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Ring ∧ ⦋𝑒 / 𝑖⦌𝑋 ∈ 𝐾) → (⦋𝑒 / 𝑖⦌𝑋 · (1r‘𝑅)) = ⦋𝑒 / 𝑖⦌𝑋)
136	65, 99, 135	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (⦋𝑒 / 𝑖⦌𝑋 · (1r‘𝑅)) = ⦋𝑒 / 𝑖⦌𝑋)
137	45, 88, 35	ringrz 20437	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Ring ∧ ⦋𝑒 / 𝑖⦌𝑋 ∈ 𝐾) → (⦋𝑒 / 𝑖⦌𝑋 · (0g‘𝑅)) = (0g‘𝑅))
138	65, 99, 137	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (⦋𝑒 / 𝑖⦌𝑋 · (0g‘𝑅)) = (0g‘𝑅))
139	136, 138	ifeq12d 4504	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → if(𝑏 = 𝑒, (⦋𝑒 / 𝑖⦌𝑋 · (1r‘𝑅)), (⦋𝑒 / 𝑖⦌𝑋 · (0g‘𝑅))) = if(𝑏 = 𝑒, ⦋𝑒 / 𝑖⦌𝑋, (0g‘𝑅)))
140	133, 139	eqtrid 2807	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))) = if(𝑏 = 𝑒, ⦋𝑒 / 𝑖⦌𝑋, (0g‘𝑅)))
141	132, 140	eqtr4d 2798	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))))
142	141	oveq2d 7430	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))) = (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)))))
143	142	3ad2ant1 1151	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))) = (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)))))
144	130, 143	eqtrd 2795	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)))))
145	144	ifeq1d 4502	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)))), (𝑎𝑀𝑏)))
146	145	mpoeq3dva 7491	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)))), (𝑎𝑀𝑏))))
147	146	fveq2d 6883	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)))), (𝑎𝑀𝑏)))))
148	45, 35	ring0cl 20409	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Ring → (0g‘𝑅) ∈ 𝐾)
149	65, 148	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (0g‘𝑅) ∈ 𝐾)
150	149	3ad2ant1 1151	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (0g‘𝑅) ∈ 𝐾)
151	123, 150	ifcld 4529	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) ∈ 𝐾)
152	45, 134	ringidcl 20407	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ Ring → (1r‘𝑅) ∈ 𝐾)
153	65, 152	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (1r‘𝑅) ∈ 𝐾)
154	153, 149	ifcld 4529	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)) ∈ 𝐾)
155	45, 88	ringcl 20390	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Ring ∧ ⦋𝑒 / 𝑖⦌𝑋 ∈ 𝐾 ∧ if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)) ∈ 𝐾) → (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))) ∈ 𝐾)
156	65, 99, 154, 155	syl3anc 1398	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))) ∈ 𝐾)
157	156	3ad2ant1 1151	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))) ∈ 𝐾)
158	55	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑀:(𝑁 × 𝑁)⟶𝐾)
159	158	fovcdmda 7586	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎𝑀𝑏) ∈ 𝐾)
160	159	3impb 1132	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (𝑎𝑀𝑏) ∈ 𝐾)
161	44, 45, 62, 63, 68, 151, 157, 160, 101	mdetrlin2 22830	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)))), (𝑎𝑀𝑏)))) = ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))(+g‘𝑅)(𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))), (𝑎𝑀𝑏))))))
162	154	3ad2ant1 1151	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)) ∈ 𝐾)
163	44, 45, 88, 63, 68, 162, 160, 99, 101	mdetrsca2 22827	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))), (𝑎𝑀𝑏)))) = (⦋𝑒 / 𝑖⦌𝑋 · (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)), (𝑎𝑀𝑏))))))
164	47	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑀 ∈ 𝐵)
165	48, 44, 78, 49, 134, 35	maducoeval 22862	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) → (𝑒(𝐽‘𝑀)𝐿) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)), (𝑎𝑀𝑏)))))
166	164, 96, 101, 165	syl3anc 1398	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝑒(𝐽‘𝑀)𝐿) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)), (𝑎𝑀𝑏)))))
167	166	oveq2d 7430	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿)) = (⦋𝑒 / 𝑖⦌𝑋 · (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)), (𝑎𝑀𝑏))))))
168	163, 167	eqtr4d 2798	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))), (𝑎𝑀𝑏)))) = (⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿)))
169	168	oveq2d 7430	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))(+g‘𝑅)(𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))), (𝑎𝑀𝑏))))) = ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))))
170	147, 161, 169	3eqtrrd 2800	. . . . . 6 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))
171	170	adantr 486	. . . . 5 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ (𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))) → ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))
172	109, 111, 171	3eqtrd 2799	. . . 4 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ (𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))) → (𝑅 Σg (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))
173	172	ex 418	. . 3 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ((𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) → (𝑅 Σg (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))))
174	8, 16, 24, 32, 61, 173, 52	findcard2d 9162	. 2 ⊢ (𝜑 → (𝑅 Σg (𝑏 ∈ 𝑁 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))
175		nfcv 2922	. . . 4 ⊢ Ⅎ𝑏(𝑋 · (𝑖(𝐽‘𝑀)𝐿))
176		nfcsb1v 3871	. . . . 5 ⊢ Ⅎ𝑖⦋𝑏 / 𝑖⦌𝑋
177		nfcv 2922	. . . . 5 ⊢ Ⅎ𝑖 ·
178		nfcv 2922	. . . . 5 ⊢ Ⅎ𝑖(𝑏(𝐽‘𝑀)𝐿)
179	176, 177, 178	nfov 7444	. . . 4 ⊢ Ⅎ𝑖(⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))
180		csbeq1a 3861	. . . . 5 ⊢ (𝑖 = 𝑏 → 𝑋 = ⦋𝑏 / 𝑖⦌𝑋)
181		oveq1 7421	. . . . 5 ⊢ (𝑖 = 𝑏 → (𝑖(𝐽‘𝑀)𝐿) = (𝑏(𝐽‘𝑀)𝐿))
182	180, 181	oveq12d 7432	. . . 4 ⊢ (𝑖 = 𝑏 → (𝑋 · (𝑖(𝐽‘𝑀)𝐿)) = (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))
183	175, 179, 182	cbvmpt 5207	. . 3 ⊢ (𝑖 ∈ 𝑁 ↦ (𝑋 · (𝑖(𝐽‘𝑀)𝐿))) = (𝑏 ∈ 𝑁 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))
184	183	oveq2i 7425	. 2 ⊢ (𝑅 Σg (𝑖 ∈ 𝑁 ↦ (𝑋 · (𝑖(𝐽‘𝑀)𝐿)))) = (𝑅 Σg (𝑏 ∈ 𝑁 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))
185		nfcv 2922	. . . . 5 ⊢ Ⅎ𝑎if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖))
186		nfcv 2922	. . . . 5 ⊢ Ⅎ𝑏if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖))
187		nfcv 2922	. . . . 5 ⊢ Ⅎ𝑗if(𝑎 = 𝐿, ⦋𝑏 / 𝑖⦌𝑋, (𝑎𝑀𝑏))
188		nfv 1947	. . . . . 6 ⊢ Ⅎ𝑖 𝑎 = 𝐿
189		nfcv 2922	. . . . . 6 ⊢ Ⅎ𝑖(𝑎𝑀𝑏)
190	188, 176, 189	nfif 4513	. . . . 5 ⊢ Ⅎ𝑖if(𝑎 = 𝐿, ⦋𝑏 / 𝑖⦌𝑋, (𝑎𝑀𝑏))
191		eqeq1 2764	. . . . . . 7 ⊢ (𝑗 = 𝑎 → (𝑗 = 𝐿 ↔ 𝑎 = 𝐿))
192	191	adantr 486	. . . . . 6 ⊢ ((𝑗 = 𝑎 ∧ 𝑖 = 𝑏) → (𝑗 = 𝐿 ↔ 𝑎 = 𝐿))
193	180	adantl 487	. . . . . 6 ⊢ ((𝑗 = 𝑎 ∧ 𝑖 = 𝑏) → 𝑋 = ⦋𝑏 / 𝑖⦌𝑋)
194		oveq12 7423	. . . . . 6 ⊢ ((𝑗 = 𝑎 ∧ 𝑖 = 𝑏) → (𝑗𝑀𝑖) = (𝑎𝑀𝑏))
195	192, 193, 194	ifbieq12d 4511	. . . . 5 ⊢ ((𝑗 = 𝑎 ∧ 𝑖 = 𝑏) → if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖)) = if(𝑎 = 𝐿, ⦋𝑏 / 𝑖⦌𝑋, (𝑎𝑀𝑏)))
196	185, 186, 187, 190, 195	cbvmpo 7508	. . . 4 ⊢ (𝑗 ∈ 𝑁, 𝑖 ∈ 𝑁 ↦ if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, ⦋𝑏 / 𝑖⦌𝑋, (𝑎𝑀𝑏)))
197		iftrue 4488	. . . . . . . 8 ⊢ (𝑏 ∈ 𝑁 → if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = ⦋𝑏 / 𝑖⦌𝑋)
198	197	eqcomd 2766	. . . . . . 7 ⊢ (𝑏 ∈ 𝑁 → ⦋𝑏 / 𝑖⦌𝑋 = if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)))
199	198	adantl 487	. . . . . 6 ⊢ ((𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → ⦋𝑏 / 𝑖⦌𝑋 = if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)))
200	199	ifeq1d 4502	. . . . 5 ⊢ ((𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑎 = 𝐿, ⦋𝑏 / 𝑖⦌𝑋, (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))
201	200	mpoeq3ia 7492	. . . 4 ⊢ (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, ⦋𝑏 / 𝑖⦌𝑋, (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))
202	196, 201	eqtri 2783	. . 3 ⊢ (𝑗 ∈ 𝑁, 𝑖 ∈ 𝑁 ↦ if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))
203	202	fveq2i 6882	. 2 ⊢ (𝐷‘(𝑗 ∈ 𝑁, 𝑖 ∈ 𝑁 ↦ if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))
204	174, 184, 203	3eqtr4g 2820	1 ⊢ (𝜑 → (𝑅 Σg (𝑖 ∈ 𝑁 ↦ (𝑋 · (𝑖(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑗 ∈ 𝑁, 𝑖 ∈ 𝑁 ↦ if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖)))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ∀wral 3076  Vcvv 3450  ⦋csb 3847   ∖ cdif 3896   ∪ cun 3897   ⊆ wss 3899  ∅c0 4279  ifcif 4482  {csn 4584   ↦ cmpt 5186   × cxp 5653  ⟶wf 6529  ‘cfv 6533  (class class class)co 7414   ∈ cmpo 7416   ↑_m cmap 8827  Fincfn 8953  Basecbs 17302  +_gcplusg 17343  ._rcmulr 17344  0_gc0g 17525   Σ_g cgsu 17526  Mndcmnd 18837  CMndccmn 19908  1_rcur 20321  Ringcrg 20373  CRingccrg 20374   Mat cmat 22630   maDet cmdat 22807   maAdju cmadu 22855

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737  ax-cnex 11181  ax-resscn 11182  ax-1cn 11183  ax-icn 11184  ax-addcl 11185  ax-addrcl 11186  ax-mulcl 11187  ax-mulrcl 11188  ax-mulcom 11189  ax-addass 11190  ax-mulass 11191  ax-distr 11192  ax-i2m1 11193  ax-1ne0 11194  ax-1rid 11195  ax-rnegex 11196  ax-rrecex 11197  ax-cnre 11198  ax-pre-lttri 11199  ax-pre-lttrn 11200  ax-pre-ltadd 11201  ax-pre-mulgt0 11202  ax-addf 11204  ax-mulf 11205

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-xor 1542  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-ot 4593  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7371  df-ov 7417  df-oprab 7418  df-mpo 7419  df-of 7679  df-om 7864  df-1st 7987  df-2nd 7988  df-supp 8160  df-tpos 8225  df-frecs 8281  df-wrecs 8312  df-recs 8361  df-rdg 8400  df-1o 8456  df-2o 8457  df-er 8697  df-map 8829  df-pm 8830  df-ixp 8906  df-en 8954  df-dom 8955  df-sdom 8956  df-fin 8957  df-fsupp 9333  df-sup 9413  df-oi 9483  df-card 9945  df-pnf 11270  df-mnf 11271  df-xr 11272  df-ltxr 11273  df-le 11274  df-sub 11468  df-neg 11469  df-div 11897  df-nn 12259  df-2 12328  df-3 12329  df-4 12330  df-5 12331  df-6 12332  df-7 12333  df-8 12334  df-9 12335  df-n0 12530  df-xnn0 12603  df-z 12617  df-dec 12738  df-uz 12889  df-rp 13044  df-fz 13563  df-fzo 13711  df-seq 14067  df-exp 14127  df-hash 14396  df-word 14580  df-lsw 14629  df-concat 14637  df-s1 14664  df-substr 14710  df-pfx 14742  df-splice 14820  df-reverse 14829  df-s2 14920  df-struct 17240  df-sets 17257  df-slot 17275  df-ndx 17287  df-base 17303  df-ress 17324  df-plusg 17356  df-mulr 17357  df-starv 17358  df-sca 17359  df-vsca 17360  df-ip 17361  df-tset 17362  df-ple 17363  df-ds 17365  df-unif 17366  df-hom 17367  df-cco 17368  df-0g 17527  df-gsum 17528  df-prds 17533  df-pws 17535  df-mre 17671  df-mrc 17672  df-acs 17674  df-mgm 18731  df-sgrp 18822  df-mnd 18838  df-mhm 18892  df-submnd 18893  df-efmnd 18979  df-grp 19061  df-minusg 19062  df-mulg 19192  df-subg 19247  df-ghm 19342  df-gim 19387  df-cntz 19445  df-oppg 19474  df-symg 19498  df-pmtr 19570  df-psgn 19619  df-cmn 19910  df-abl 19911  df-mgp 20275  df-rng 20289  df-ur 20322  df-ring 20375  df-cring 20376  df-oppr 20479  df-dvdsr 20499  df-unit 20500  df-invr 20530  df-dvr 20543  df-rhm 20614  df-subrng 20709  df-subrg 20733  df-drng 20893  df-sra 21358  df-rgmod 21359  df-cnfld 21587  df-zring 21661  df-zrh 21717  df-dsmm 21946  df-frlm 21961  df-mat 22631  df-mdet 22808  df-madu 22857

This theorem is used by:  madurid  22867  mdetlap1  34337