Theorem madugsum 22074

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 5234	. . . . 5 ⊢ (𝑐 = ∅ → (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))) = (𝑏 ∈ ∅ ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))
2	1	oveq2d 7409	. . . 4 ⊢ (𝑐 = ∅ → (𝑅 Σg (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝑅 Σg (𝑏 ∈ ∅ ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))))
3		eleq2 2821	. . . . . . . 8 ⊢ (𝑐 = ∅ → (𝑏 ∈ 𝑐 ↔ 𝑏 ∈ ∅))
4	3	ifbid 4545	. . . . . . 7 ⊢ (𝑐 = ∅ → if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)))
5	4	ifeq1d 4541	. . . . . 6 ⊢ (𝑐 = ∅ → if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))
6	5	mpoeq3dv 7472	. . . . 5 ⊢ (𝑐 = ∅ → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))
7	6	fveq2d 6882	. . . 4 ⊢ (𝑐 = ∅ → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))
8	2, 7	eqeq12d 2747	. . 3 ⊢ (𝑐 = ∅ → ((𝑅 Σg (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) ↔ (𝑅 Σg (𝑏 ∈ ∅ ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))))
9		mpteq1 5234	. . . . 5 ⊢ (𝑐 = 𝑑 → (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))) = (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))
10	9	oveq2d 7409	. . . 4 ⊢ (𝑐 = 𝑑 → (𝑅 Σg (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))))
11		eleq2 2821	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → (𝑏 ∈ 𝑐 ↔ 𝑏 ∈ 𝑑))
12	11	ifbid 4545	. . . . . . 7 ⊢ (𝑐 = 𝑑 → if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)))
13	12	ifeq1d 4541	. . . . . 6 ⊢ (𝑐 = 𝑑 → if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))
14	13	mpoeq3dv 7472	. . . . 5 ⊢ (𝑐 = 𝑑 → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))
15	14	fveq2d 6882	. . . 4 ⊢ (𝑐 = 𝑑 → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))
16	10, 15	eqeq12d 2747	. . 3 ⊢ (𝑐 = 𝑑 → ((𝑅 Σg (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) ↔ (𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))))
17		mpteq1 5234	. . . . 5 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))) = (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))
18	17	oveq2d 7409	. . . 4 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → (𝑅 Σg (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝑅 Σg (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))))
19		eleq2 2821	. . . . . . . 8 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → (𝑏 ∈ 𝑐 ↔ 𝑏 ∈ (𝑑 ∪ {𝑒})))
20	19	ifbid 4545	. . . . . . 7 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)))
21	20	ifeq1d 4541	. . . . . 6 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))
22	21	mpoeq3dv 7472	. . . . 5 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))
23	22	fveq2d 6882	. . . 4 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))
24	18, 23	eqeq12d 2747	. . 3 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → ((𝑅 Σg (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) ↔ (𝑅 Σg (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))))
25		mpteq1 5234	. . . . 5 ⊢ (𝑐 = 𝑁 → (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))) = (𝑏 ∈ 𝑁 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))
26	25	oveq2d 7409	. . . 4 ⊢ (𝑐 = 𝑁 → (𝑅 Σg (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝑅 Σg (𝑏 ∈ 𝑁 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))))
27		eleq2 2821	. . . . . . . 8 ⊢ (𝑐 = 𝑁 → (𝑏 ∈ 𝑐 ↔ 𝑏 ∈ 𝑁))
28	27	ifbid 4545	. . . . . . 7 ⊢ (𝑐 = 𝑁 → if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)))
29	28	ifeq1d 4541	. . . . . 6 ⊢ (𝑐 = 𝑁 → if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))
30	29	mpoeq3dv 7472	. . . . 5 ⊢ (𝑐 = 𝑁 → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))
31	30	fveq2d 6882	. . . 4 ⊢ (𝑐 = 𝑁 → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))
32	26, 31	eqeq12d 2747	. . 3 ⊢ (𝑐 = 𝑁 → ((𝑅 Σg (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) ↔ (𝑅 Σg (𝑏 ∈ 𝑁 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))))
33		mpt0 6679	. . . . . 6 ⊢ (𝑏 ∈ ∅ ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))) = ∅
34	33	oveq2i 7404	. . . . 5 ⊢ (𝑅 Σg (𝑏 ∈ ∅ ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝑅 Σg ∅)
35		eqid 2731	. . . . . 6 ⊢ (0g‘𝑅) = (0g‘𝑅)
36	35	gsum0 18585	. . . . 5 ⊢ (𝑅 Σg ∅) = (0g‘𝑅)
37	34, 36	eqtri 2759	. . . 4 ⊢ (𝑅 Σg (𝑏 ∈ ∅ ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (0g‘𝑅)
38		noel 4326	. . . . . . . . 9 ⊢ ¬ 𝑏 ∈ ∅
39		iffalse 4531	. . . . . . . . 9 ⊢ (¬ 𝑏 ∈ ∅ → if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = (0g‘𝑅))
40	38, 39	mp1i 13	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = (0g‘𝑅))
41	40	ifeq1d 4541	. . . . . . 7 ⊢ ((𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, (0g‘𝑅), (𝑎𝑀𝑏)))
42	41	mpoeq3ia 7471	. . . . . 6 ⊢ (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (0g‘𝑅), (𝑎𝑀𝑏)))
43	42	fveq2i 6881	. . . . 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 21841	. . . . . . . 8 ⊢ (𝑀 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
51	47, 50	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
52	51	simpld 495	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ Fin)
53	48, 45, 49	matbas2i 21853	. . . . . . . . 9 ⊢ (𝑀 ∈ 𝐵 → 𝑀 ∈ (𝐾 ↑m (𝑁 × 𝑁)))
54		elmapi 8826	. . . . . . . . 9 ⊢ (𝑀 ∈ (𝐾 ↑m (𝑁 × 𝑁)) → 𝑀:(𝑁 × 𝑁)⟶𝐾)
55	47, 53, 54	3syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑀:(𝑁 × 𝑁)⟶𝐾)
56	55	fovcdmda 7561	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎𝑀𝑏) ∈ 𝐾)
57	56	3impb 1115	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (𝑎𝑀𝑏) ∈ 𝐾)
58		madugsum.l	. . . . . 6 ⊢ (𝜑 → 𝐿 ∈ 𝑁)
59	44, 45, 35, 46, 52, 57, 58	mdetr0 22036	. . . . 5 ⊢ (𝜑 → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (0g‘𝑅), (𝑎𝑀𝑏)))) = (0g‘𝑅))
60	43, 59	eqtrid 2783	. . . 4 ⊢ (𝜑 → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) = (0g‘𝑅))
61	37, 60	eqtr4id 2790	. . 3 ⊢ (𝜑 → (𝑅 Σg (𝑏 ∈ ∅ ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))
62		eqid 2731	. . . . . . 7 ⊢ (+g‘𝑅) = (+g‘𝑅)
63	46	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑅 ∈ CRing)
64		crngring 20026	. . . . . . . . 9 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
65	63, 64	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑅 ∈ Ring)
66		ringcmn 20056	. . . . . . . 8 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
67	65, 66	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑅 ∈ CMnd)
68	52	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑁 ∈ Fin)
69		simprl 769	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑑 ⊆ 𝑁)
70	68, 69	ssfid 9250	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑑 ∈ Fin)
71	65	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → 𝑅 ∈ Ring)
72	69	sselda 3978	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → 𝑏 ∈ 𝑁)
73		madugsum.x	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → 𝑋 ∈ 𝐾)
74	73	ralrimiva 3145	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐾)
75	74	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐾)
76		rspcsbela 4431	. . . . . . . . 9 ⊢ ((𝑏 ∈ 𝑁 ∧ ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐾) → ⦋𝑏 / 𝑖⦌𝑋 ∈ 𝐾)
77	72, 75, 76	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → ⦋𝑏 / 𝑖⦌𝑋 ∈ 𝐾)
78		maduf.j	. . . . . . . . . . . . . 14 ⊢ 𝐽 = (𝑁 maAdju 𝑅)
79	48, 78, 49	maduf 22072	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ CRing → 𝐽:𝐵⟶𝐵)
80	46, 79	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽:𝐵⟶𝐵)
81	80, 47	ffvelcdmd 7072	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐽‘𝑀) ∈ 𝐵)
82	48, 45, 49	matbas2i 21853	. . . . . . . . . . 11 ⊢ ((𝐽‘𝑀) ∈ 𝐵 → (𝐽‘𝑀) ∈ (𝐾 ↑m (𝑁 × 𝑁)))
83		elmapi 8826	. . . . . . . . . . 11 ⊢ ((𝐽‘𝑀) ∈ (𝐾 ↑m (𝑁 × 𝑁)) → (𝐽‘𝑀):(𝑁 × 𝑁)⟶𝐾)
84	81, 82, 83	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝐽‘𝑀):(𝑁 × 𝑁)⟶𝐾)
85	84	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → (𝐽‘𝑀):(𝑁 × 𝑁)⟶𝐾)
86	58	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → 𝐿 ∈ 𝑁)
87	85, 72, 86	fovcdmd 7562	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → (𝑏(𝐽‘𝑀)𝐿) ∈ 𝐾)
88		madugsum.t	. . . . . . . . 9 ⊢ · = (.r‘𝑅)
89	45, 88	ringcl 20031	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ ⦋𝑏 / 𝑖⦌𝑋 ∈ 𝐾 ∧ (𝑏(𝐽‘𝑀)𝐿) ∈ 𝐾) → (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)) ∈ 𝐾)
90	71, 77, 87, 89	syl3anc 1371	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)) ∈ 𝐾)
91		vex 3477	. . . . . . . 8 ⊢ 𝑒 ∈ V
92	91	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑒 ∈ V)
93		eldifn 4123	. . . . . . . 8 ⊢ (𝑒 ∈ (𝑁 ∖ 𝑑) → ¬ 𝑒 ∈ 𝑑)
94	93	ad2antll 727	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ¬ 𝑒 ∈ 𝑑)
95		eldifi 4122	. . . . . . . . . 10 ⊢ (𝑒 ∈ (𝑁 ∖ 𝑑) → 𝑒 ∈ 𝑁)
96	95	ad2antll 727	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑒 ∈ 𝑁)
97	74	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐾)
98		rspcsbela 4431	. . . . . . . . 9 ⊢ ((𝑒 ∈ 𝑁 ∧ ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐾) → ⦋𝑒 / 𝑖⦌𝑋 ∈ 𝐾)
99	96, 97, 98	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ⦋𝑒 / 𝑖⦌𝑋 ∈ 𝐾)
100	84	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝐽‘𝑀):(𝑁 × 𝑁)⟶𝐾)
101	58	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝐿 ∈ 𝑁)
102	100, 96, 101	fovcdmd 7562	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝑒(𝐽‘𝑀)𝐿) ∈ 𝐾)
103	45, 88	ringcl 20031	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ ⦋𝑒 / 𝑖⦌𝑋 ∈ 𝐾 ∧ (𝑒(𝐽‘𝑀)𝐿) ∈ 𝐾) → (⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿)) ∈ 𝐾)
104	65, 99, 102, 103	syl3anc 1371	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿)) ∈ 𝐾)
105		csbeq1 3892	. . . . . . . 8 ⊢ (𝑏 = 𝑒 → ⦋𝑏 / 𝑖⦌𝑋 = ⦋𝑒 / 𝑖⦌𝑋)
106		oveq1 7400	. . . . . . . 8 ⊢ (𝑏 = 𝑒 → (𝑏(𝐽‘𝑀)𝐿) = (𝑒(𝐽‘𝑀)𝐿))
107	105, 106	oveq12d 7411	. . . . . . 7 ⊢ (𝑏 = 𝑒 → (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)) = (⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿)))
108	45, 62, 67, 70, 90, 92, 94, 104, 107	gsumunsn 19787	. . . . . 6 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝑅 Σg (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = ((𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))))
109	108	adantr 481	. . . . 5 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ (𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))) → (𝑅 Σg (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = ((𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))))
110		oveq1 7400	. . . . . 6 ⊢ ((𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) → ((𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))) = ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))))
111	110	adantl 482	. . . . 5 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ (𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))) → ((𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))) = ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))))
112		elun 4144	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ (𝑑 ∪ {𝑒}) ↔ (𝑏 ∈ 𝑑 ∨ 𝑏 ∈ {𝑒}))
113		velsn 4638	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ {𝑒} ↔ 𝑏 = 𝑒)
114	113	orbi2i 911	. . . . . . . . . . . . . 14 ⊢ ((𝑏 ∈ 𝑑 ∨ 𝑏 ∈ {𝑒}) ↔ (𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒))
115	112, 114	bitri 274	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ (𝑑 ∪ {𝑒}) ↔ (𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒))
116		ifbi 4544	. . . . . . . . . . . . 13 ⊢ ((𝑏 ∈ (𝑑 ∪ {𝑒}) ↔ (𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒)) → if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = if((𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)))
117	115, 116	ax-mp 5	. . . . . . . . . . . 12 ⊢ if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = if((𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))
118		ringmnd 20024	. . . . . . . . . . . . . . 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 2113	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑒 → (𝑏 ∈ 𝑑 ↔ 𝑒 ∈ 𝑑))
125	124	biimpac 479	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 ∈ 𝑑 ∧ 𝑏 = 𝑒) → 𝑒 ∈ 𝑑)
126	94, 125	nsyl 140	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ¬ (𝑏 ∈ 𝑑 ∧ 𝑏 = 𝑒))
127	126	3ad2ant1 1133	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → ¬ (𝑏 ∈ 𝑑 ∧ 𝑏 = 𝑒))
128	45, 35, 62	mndifsplit 22067	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Mnd ∧ ⦋𝑏 / 𝑖⦌𝑋 ∈ 𝐾 ∧ ¬ (𝑏 ∈ 𝑑 ∧ 𝑏 = 𝑒)) → if((𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))))
129	120, 123, 127, 128	syl3anc 1371	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if((𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))))
130	117, 129	eqtrid 2783	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))))
131	105	adantl 482	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 = 𝑒) → ⦋𝑏 / 𝑖⦌𝑋 = ⦋𝑒 / 𝑖⦌𝑋)
132	131	ifeq1da 4553	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = if(𝑏 = 𝑒, ⦋𝑒 / 𝑖⦌𝑋, (0g‘𝑅)))
133		ovif2 7491	. . . . . . . . . . . . . . 15 ⊢ (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))) = if(𝑏 = 𝑒, (⦋𝑒 / 𝑖⦌𝑋 · (1r‘𝑅)), (⦋𝑒 / 𝑖⦌𝑋 · (0g‘𝑅)))
134		eqid 2731	. . . . . . . . . . . . . . . . . 18 ⊢ (1r‘𝑅) = (1r‘𝑅)
135	45, 88, 134	ringridm 20044	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Ring ∧ ⦋𝑒 / 𝑖⦌𝑋 ∈ 𝐾) → (⦋𝑒 / 𝑖⦌𝑋 · (1r‘𝑅)) = ⦋𝑒 / 𝑖⦌𝑋)
136	65, 99, 135	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (⦋𝑒 / 𝑖⦌𝑋 · (1r‘𝑅)) = ⦋𝑒 / 𝑖⦌𝑋)
137	45, 88, 35	ringrz 20065	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Ring ∧ ⦋𝑒 / 𝑖⦌𝑋 ∈ 𝐾) → (⦋𝑒 / 𝑖⦌𝑋 · (0g‘𝑅)) = (0g‘𝑅))
138	65, 99, 137	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (⦋𝑒 / 𝑖⦌𝑋 · (0g‘𝑅)) = (0g‘𝑅))
139	136, 138	ifeq12d 4543	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → if(𝑏 = 𝑒, (⦋𝑒 / 𝑖⦌𝑋 · (1r‘𝑅)), (⦋𝑒 / 𝑖⦌𝑋 · (0g‘𝑅))) = if(𝑏 = 𝑒, ⦋𝑒 / 𝑖⦌𝑋, (0g‘𝑅)))
140	133, 139	eqtrid 2783	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))) = if(𝑏 = 𝑒, ⦋𝑒 / 𝑖⦌𝑋, (0g‘𝑅)))
141	132, 140	eqtr4d 2774	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))))
142	141	oveq2d 7409	. . . . . . . . . . . 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 2771	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)))))
145	144	ifeq1d 4541	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)))), (𝑎𝑀𝑏)))
146	145	mpoeq3dva 7470	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)))), (𝑎𝑀𝑏))))
147	146	fveq2d 6882	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)))), (𝑎𝑀𝑏)))))
148	45, 35	ring0cl 20041	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Ring → (0g‘𝑅) ∈ 𝐾)
149	65, 148	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (0g‘𝑅) ∈ 𝐾)
150	149	3ad2ant1 1133	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (0g‘𝑅) ∈ 𝐾)
151	123, 150	ifcld 4568	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) ∈ 𝐾)
152	45, 134	ringidcl 20040	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ Ring → (1r‘𝑅) ∈ 𝐾)
153	65, 152	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (1r‘𝑅) ∈ 𝐾)
154	153, 149	ifcld 4568	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)) ∈ 𝐾)
155	45, 88	ringcl 20031	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Ring ∧ ⦋𝑒 / 𝑖⦌𝑋 ∈ 𝐾 ∧ if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)) ∈ 𝐾) → (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))) ∈ 𝐾)
156	65, 99, 154, 155	syl3anc 1371	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))) ∈ 𝐾)
157	156	3ad2ant1 1133	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))) ∈ 𝐾)
158	55	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑀:(𝑁 × 𝑁)⟶𝐾)
159	158	fovcdmda 7561	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎𝑀𝑏) ∈ 𝐾)
160	159	3impb 1115	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (𝑎𝑀𝑏) ∈ 𝐾)
161	44, 45, 62, 63, 68, 151, 157, 160, 101	mdetrlin2 22038	. . . . . . 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 22035	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))), (𝑎𝑀𝑏)))) = (⦋𝑒 / 𝑖⦌𝑋 · (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)), (𝑎𝑀𝑏))))))
164	47	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑀 ∈ 𝐵)
165	48, 44, 78, 49, 134, 35	maducoeval 22070	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) → (𝑒(𝐽‘𝑀)𝐿) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)), (𝑎𝑀𝑏)))))
166	164, 96, 101, 165	syl3anc 1371	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝑒(𝐽‘𝑀)𝐿) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)), (𝑎𝑀𝑏)))))
167	166	oveq2d 7409	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿)) = (⦋𝑒 / 𝑖⦌𝑋 · (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅)), (𝑎𝑀𝑏))))))
168	163, 167	eqtr4d 2774	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))), (𝑎𝑀𝑏)))) = (⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿)))
169	168	oveq2d 7409	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))(+g‘𝑅)(𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1r‘𝑅), (0g‘𝑅))), (𝑎𝑀𝑏))))) = ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))))
170	147, 161, 169	3eqtrrd 2776	. . . . . 6 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))
171	170	adantr 481	. . . . 5 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ (𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))) → ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))(+g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))
172	109, 111, 171	3eqtrd 2775	. . . 4 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ (𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))) → (𝑅 Σg (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))
173	172	ex 413	. . 3 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ((𝑅 Σg (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))) → (𝑅 Σg (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))))
174	8, 16, 24, 32, 61, 173, 52	findcard2d 9149	. 2 ⊢ (𝜑 → (𝑅 Σg (𝑏 ∈ 𝑁 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))))
175		nfcv 2902	. . . 4 ⊢ Ⅎ𝑏(𝑋 · (𝑖(𝐽‘𝑀)𝐿))
176		nfcsb1v 3914	. . . . 5 ⊢ Ⅎ𝑖⦋𝑏 / 𝑖⦌𝑋
177		nfcv 2902	. . . . 5 ⊢ Ⅎ𝑖 ·
178		nfcv 2902	. . . . 5 ⊢ Ⅎ𝑖(𝑏(𝐽‘𝑀)𝐿)
179	176, 177, 178	nfov 7423	. . . 4 ⊢ Ⅎ𝑖(⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))
180		csbeq1a 3903	. . . . 5 ⊢ (𝑖 = 𝑏 → 𝑋 = ⦋𝑏 / 𝑖⦌𝑋)
181		oveq1 7400	. . . . 5 ⊢ (𝑖 = 𝑏 → (𝑖(𝐽‘𝑀)𝐿) = (𝑏(𝐽‘𝑀)𝐿))
182	180, 181	oveq12d 7411	. . . 4 ⊢ (𝑖 = 𝑏 → (𝑋 · (𝑖(𝐽‘𝑀)𝐿)) = (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))
183	175, 179, 182	cbvmpt 5252	. . 3 ⊢ (𝑖 ∈ 𝑁 ↦ (𝑋 · (𝑖(𝐽‘𝑀)𝐿))) = (𝑏 ∈ 𝑁 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))
184	183	oveq2i 7404	. 2 ⊢ (𝑅 Σg (𝑖 ∈ 𝑁 ↦ (𝑋 · (𝑖(𝐽‘𝑀)𝐿)))) = (𝑅 Σg (𝑏 ∈ 𝑁 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))
185		nfcv 2902	. . . . 5 ⊢ Ⅎ𝑎if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖))
186		nfcv 2902	. . . . 5 ⊢ Ⅎ𝑏if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖))
187		nfcv 2902	. . . . 5 ⊢ Ⅎ𝑗if(𝑎 = 𝐿, ⦋𝑏 / 𝑖⦌𝑋, (𝑎𝑀𝑏))
188		nfv 1917	. . . . . 6 ⊢ Ⅎ𝑖 𝑎 = 𝐿
189		nfcv 2902	. . . . . 6 ⊢ Ⅎ𝑖(𝑎𝑀𝑏)
190	188, 176, 189	nfif 4552	. . . . 5 ⊢ Ⅎ𝑖if(𝑎 = 𝐿, ⦋𝑏 / 𝑖⦌𝑋, (𝑎𝑀𝑏))
191		eqeq1 2735	. . . . . . 7 ⊢ (𝑗 = 𝑎 → (𝑗 = 𝐿 ↔ 𝑎 = 𝐿))
192	191	adantr 481	. . . . . 6 ⊢ ((𝑗 = 𝑎 ∧ 𝑖 = 𝑏) → (𝑗 = 𝐿 ↔ 𝑎 = 𝐿))
193	180	adantl 482	. . . . . 6 ⊢ ((𝑗 = 𝑎 ∧ 𝑖 = 𝑏) → 𝑋 = ⦋𝑏 / 𝑖⦌𝑋)
194		oveq12 7402	. . . . . 6 ⊢ ((𝑗 = 𝑎 ∧ 𝑖 = 𝑏) → (𝑗𝑀𝑖) = (𝑎𝑀𝑏))
195	192, 193, 194	ifbieq12d 4550	. . . . 5 ⊢ ((𝑗 = 𝑎 ∧ 𝑖 = 𝑏) → if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖)) = if(𝑎 = 𝐿, ⦋𝑏 / 𝑖⦌𝑋, (𝑎𝑀𝑏)))
196	185, 186, 187, 190, 195	cbvmpo 7487	. . . 4 ⊢ (𝑗 ∈ 𝑁, 𝑖 ∈ 𝑁 ↦ if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, ⦋𝑏 / 𝑖⦌𝑋, (𝑎𝑀𝑏)))
197		iftrue 4528	. . . . . . . 8 ⊢ (𝑏 ∈ 𝑁 → if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)) = ⦋𝑏 / 𝑖⦌𝑋)
198	197	eqcomd 2737	. . . . . . 7 ⊢ (𝑏 ∈ 𝑁 → ⦋𝑏 / 𝑖⦌𝑋 = if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)))
199	198	adantl 482	. . . . . 6 ⊢ ((𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → ⦋𝑏 / 𝑖⦌𝑋 = if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)))
200	199	ifeq1d 4541	. . . . 5 ⊢ ((𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑎 = 𝐿, ⦋𝑏 / 𝑖⦌𝑋, (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))
201	200	mpoeq3ia 7471	. . . 4 ⊢ (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, ⦋𝑏 / 𝑖⦌𝑋, (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))
202	196, 201	eqtri 2759	. . 3 ⊢ (𝑗 ∈ 𝑁, 𝑖 ∈ 𝑁 ↦ if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏)))
203	202	fveq2i 6881	. 2 ⊢ (𝐷‘(𝑗 ∈ 𝑁, 𝑖 ∈ 𝑁 ↦ if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0g‘𝑅)), (𝑎𝑀𝑏))))
204	174, 184, 203	3eqtr4g 2796	1 ⊢ (𝜑 → (𝑅 Σg (𝑖 ∈ 𝑁 ↦ (𝑋 · (𝑖(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑗 ∈ 𝑁, 𝑖 ∈ 𝑁 ↦ if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖)))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  ∀wral 3060  Vcvv 3473  ⦋csb 3889   ∖ cdif 3941   ∪ cun 3942   ⊆ wss 3944  ∅c0 4318  ifcif 4522  {csn 4622   ↦ cmpt 5224   × cxp 5667  ⟶wf 6528  ‘cfv 6532  (class class class)co 7393   ∈ cmpo 7395   ↑_m cmap 8803  Fincfn 8922  Basecbs 17126  +_gcplusg 17179  ._rcmulr 17180  0_gc0g 17367   Σ_g cgsu 17368  Mndcmnd 18602  CMndccmn 19612  1_rcur 19963  Ringcrg 20014  CRingccrg 20015   Mat cmat 21836   maDet cmdat 22015   maAdju cmadu 22063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7708  ax-cnex 11148  ax-resscn 11149  ax-1cn 11150  ax-icn 11151  ax-addcl 11152  ax-addrcl 11153  ax-mulcl 11154  ax-mulrcl 11155  ax-mulcom 11156  ax-addass 11157  ax-mulass 11158  ax-distr 11159  ax-i2m1 11160  ax-1ne0 11161  ax-1rid 11162  ax-rnegex 11163  ax-rrecex 11164  ax-cnre 11165  ax-pre-lttri 11166  ax-pre-lttrn 11167  ax-pre-ltadd 11168  ax-pre-mulgt0 11169  ax-addf 11171  ax-mulf 11172

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-xor 1510  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-tp 4627  df-op 4629  df-ot 4631  df-uni 4902  df-int 4944  df-iun 4992  df-iin 4993  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6289  df-ord 6356  df-on 6357  df-lim 6358  df-suc 6359  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539  df-fv 6540  df-isom 6541  df-riota 7349  df-ov 7396  df-oprab 7397  df-mpo 7398  df-of 7653  df-om 7839  df-1st 7957  df-2nd 7958  df-supp 8129  df-tpos 8193  df-frecs 8248  df-wrecs 8279  df-recs 8353  df-rdg 8392  df-1o 8448  df-2o 8449  df-er 8686  df-map 8805  df-pm 8806  df-ixp 8875  df-en 8923  df-dom 8924  df-sdom 8925  df-fin 8926  df-fsupp 9345  df-sup 9419  df-oi 9487  df-card 9916  df-pnf 11232  df-mnf 11233  df-xr 11234  df-ltxr 11235  df-le 11236  df-sub 11428  df-neg 11429  df-div 11854  df-nn 12195  df-2 12257  df-3 12258  df-4 12259  df-5 12260  df-6 12261  df-7 12262  df-8 12263  df-9 12264  df-n0 12455  df-xnn0 12527  df-z 12541  df-dec 12660  df-uz 12805  df-rp 12957  df-fz 13467  df-fzo 13610  df-seq 13949  df-exp 14010  df-hash 14273  df-word 14447  df-lsw 14495  df-concat 14503  df-s1 14528  df-substr 14573  df-pfx 14603  df-splice 14682  df-reverse 14691  df-s2 14781  df-struct 17062  df-sets 17079  df-slot 17097  df-ndx 17109  df-base 17127  df-ress 17156  df-plusg 17192  df-mulr 17193  df-starv 17194  df-sca 17195  df-vsca 17196  df-ip 17197  df-tset 17198  df-ple 17199  df-ds 17201  df-unif 17202  df-hom 17203  df-cco 17204  df-0g 17369  df-gsum 17370  df-prds 17375  df-pws 17377  df-mre 17512  df-mrc 17513  df-acs 17515  df-mgm 18543  df-sgrp 18592  df-mnd 18603  df-mhm 18647  df-submnd 18648  df-efmnd 18725  df-grp 18797  df-minusg 18798  df-mulg 18923  df-subg 18975  df-ghm 19056  df-gim 19099  df-cntz 19147  df-oppg 19174  df-symg 19199  df-pmtr 19274  df-psgn 19323  df-cmn 19614  df-abl 19615  df-mgp 19947  df-ur 19964  df-ring 20016  df-cring 20017  df-oppr 20102  df-dvdsr 20123  df-unit 20124  df-invr 20154  df-dvr 20165  df-rnghom 20201  df-drng 20267  df-subrg 20310  df-sra 20734  df-rgmod 20735  df-cnfld 20879  df-zring 20952  df-zrh 20986  df-dsmm 21220  df-frlm 21235  df-mat 21837  df-mdet 22016  df-madu 22065

This theorem is referenced by:  madurid  22075  mdetlap1  32637