madugsum - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > madugsum		Structured version Visualization version GIF version

Theorem madugsum 22500

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 7421	. . . 4 ⊢ (𝑐 = ∅ → (𝑅 Σ_g (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝑅 Σ_g (𝑏 ∈ ∅ ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))))
3		eleq2 2816	. . . . . . . 8 ⊢ (𝑐 = ∅ → (𝑏 ∈ 𝑐 ↔ 𝑏 ∈ ∅))
4	3	ifbid 4546	. . . . . . 7 ⊢ (𝑐 = ∅ → if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)) = if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)))
5	4	ifeq1d 4542	. . . . . 6 ⊢ (𝑐 = ∅ → if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)))
6	5	mpoeq3dv 7484	. . . . 5 ⊢ (𝑐 = ∅ → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏))))
7	6	fveq2d 6889	. . . 4 ⊢ (𝑐 = ∅ → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)))))
8	2, 7	eqeq12d 2742	. . 3 ⊢ (𝑐 = ∅ → ((𝑅 Σ_g (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)))) ↔ (𝑅 Σ_g (𝑏 ∈ ∅ ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏))))))
9		mpteq1 5234	. . . . 5 ⊢ (𝑐 = 𝑑 → (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))) = (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))
10	9	oveq2d 7421	. . . 4 ⊢ (𝑐 = 𝑑 → (𝑅 Σ_g (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝑅 Σ_g (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))))
11		eleq2 2816	. . . . . . . 8 ⊢ (𝑐 = 𝑑 → (𝑏 ∈ 𝑐 ↔ 𝑏 ∈ 𝑑))
12	11	ifbid 4546	. . . . . . 7 ⊢ (𝑐 = 𝑑 → if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)) = if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)))
13	12	ifeq1d 4542	. . . . . 6 ⊢ (𝑐 = 𝑑 → if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)))
14	13	mpoeq3dv 7484	. . . . 5 ⊢ (𝑐 = 𝑑 → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏))))
15	14	fveq2d 6889	. . . 4 ⊢ (𝑐 = 𝑑 → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)))))
16	10, 15	eqeq12d 2742	. . 3 ⊢ (𝑐 = 𝑑 → ((𝑅 Σ_g (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)))) ↔ (𝑅 Σ_g (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏))))))
17		mpteq1 5234	. . . . 5 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))) = (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))
18	17	oveq2d 7421	. . . 4 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → (𝑅 Σ_g (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝑅 Σ_g (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))))
19		eleq2 2816	. . . . . . . 8 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → (𝑏 ∈ 𝑐 ↔ 𝑏 ∈ (𝑑 ∪ {𝑒})))
20	19	ifbid 4546	. . . . . . 7 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)) = if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)))
21	20	ifeq1d 4542	. . . . . 6 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)))
22	21	mpoeq3dv 7484	. . . . 5 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏))))
23	22	fveq2d 6889	. . . 4 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)))))
24	18, 23	eqeq12d 2742	. . 3 ⊢ (𝑐 = (𝑑 ∪ {𝑒}) → ((𝑅 Σ_g (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)))) ↔ (𝑅 Σ_g (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏))))))
25		mpteq1 5234	. . . . 5 ⊢ (𝑐 = 𝑁 → (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))) = (𝑏 ∈ 𝑁 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))
26	25	oveq2d 7421	. . . 4 ⊢ (𝑐 = 𝑁 → (𝑅 Σ_g (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝑅 Σ_g (𝑏 ∈ 𝑁 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))))
27		eleq2 2816	. . . . . . . 8 ⊢ (𝑐 = 𝑁 → (𝑏 ∈ 𝑐 ↔ 𝑏 ∈ 𝑁))
28	27	ifbid 4546	. . . . . . 7 ⊢ (𝑐 = 𝑁 → if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)) = if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)))
29	28	ifeq1d 4542	. . . . . 6 ⊢ (𝑐 = 𝑁 → if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)))
30	29	mpoeq3dv 7484	. . . . 5 ⊢ (𝑐 = 𝑁 → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏))))
31	30	fveq2d 6889	. . . 4 ⊢ (𝑐 = 𝑁 → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)))))
32	26, 31	eqeq12d 2742	. . 3 ⊢ (𝑐 = 𝑁 → ((𝑅 Σ_g (𝑏 ∈ 𝑐 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑐, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)))) ↔ (𝑅 Σ_g (𝑏 ∈ 𝑁 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏))))))
33		mpt0 6686	. . . . . 6 ⊢ (𝑏 ∈ ∅ ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))) = ∅
34	33	oveq2i 7416	. . . . 5 ⊢ (𝑅 Σ_g (𝑏 ∈ ∅ ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝑅 Σ_g ∅)
35		eqid 2726	. . . . . 6 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
36	35	gsum0 18617	. . . . 5 ⊢ (𝑅 Σ_g ∅) = (0_g‘𝑅)
37	34, 36	eqtri 2754	. . . 4 ⊢ (𝑅 Σ_g (𝑏 ∈ ∅ ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (0_g‘𝑅)
38		noel 4325	. . . . . . . . 9 ⊢ ¬ 𝑏 ∈ ∅
39		iffalse 4532	. . . . . . . . 9 ⊢ (¬ 𝑏 ∈ ∅ → if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)) = (0_g‘𝑅))
40	38, 39	mp1i 13	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)) = (0_g‘𝑅))
41	40	ifeq1d 4542	. . . . . . 7 ⊢ ((𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, (0_g‘𝑅), (𝑎𝑀𝑏)))
42	41	mpoeq3ia 7483	. . . . . 6 ⊢ (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (0_g‘𝑅), (𝑎𝑀𝑏)))
43	42	fveq2i 6888	. . . . 5 ⊢ (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (0_g‘𝑅), (𝑎𝑀𝑏))))
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 22267	. . . . . . . 8 ⊢ (𝑀 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
51	47, 50	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
52	51	simpld 494	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ Fin)
53	48, 45, 49	matbas2i 22279	. . . . . . . . 9 ⊢ (𝑀 ∈ 𝐵 → 𝑀 ∈ (𝐾 ↑_m (𝑁 × 𝑁)))
54		elmapi 8845	. . . . . . . . 9 ⊢ (𝑀 ∈ (𝐾 ↑_m (𝑁 × 𝑁)) → 𝑀:(𝑁 × 𝑁)⟶𝐾)
55	47, 53, 54	3syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑀:(𝑁 × 𝑁)⟶𝐾)
56	55	fovcdmda 7575	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎𝑀𝑏) ∈ 𝐾)
57	56	3impb 1112	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (𝑎𝑀𝑏) ∈ 𝐾)
58		madugsum.l	. . . . . 6 ⊢ (𝜑 → 𝐿 ∈ 𝑁)
59	44, 45, 35, 46, 52, 57, 58	mdetr0 22462	. . . . 5 ⊢ (𝜑 → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (0_g‘𝑅), (𝑎𝑀𝑏)))) = (0_g‘𝑅))
60	43, 59	eqtrid 2778	. . . 4 ⊢ (𝜑 → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)))) = (0_g‘𝑅))
61	37, 60	eqtr4id 2785	. . 3 ⊢ (𝜑 → (𝑅 Σ_g (𝑏 ∈ ∅ ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)))))
62		eqid 2726	. . . . . . 7 ⊢ (+_g‘𝑅) = (+_g‘𝑅)
63	46	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑅 ∈ CRing)
64		crngring 20150	. . . . . . . . 9 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
65	63, 64	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑅 ∈ Ring)
66		ringcmn 20181	. . . . . . . 8 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
67	65, 66	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑅 ∈ CMnd)
68	52	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑁 ∈ Fin)
69		simprl 768	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑑 ⊆ 𝑁)
70	68, 69	ssfid 9269	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑑 ∈ Fin)
71	65	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → 𝑅 ∈ Ring)
72	69	sselda 3977	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → 𝑏 ∈ 𝑁)
73		madugsum.x	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → 𝑋 ∈ 𝐾)
74	73	ralrimiva 3140	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐾)
75	74	ad2antrr 723	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐾)
76		rspcsbela 4430	. . . . . . . . 9 ⊢ ((𝑏 ∈ 𝑁 ∧ ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐾) → ⦋𝑏 / 𝑖⦌𝑋 ∈ 𝐾)
77	72, 75, 76	syl2anc 583	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → ⦋𝑏 / 𝑖⦌𝑋 ∈ 𝐾)
78		maduf.j	. . . . . . . . . . . . . 14 ⊢ 𝐽 = (𝑁 maAdju 𝑅)
79	48, 78, 49	maduf 22498	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ CRing → 𝐽:𝐵⟶𝐵)
80	46, 79	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽:𝐵⟶𝐵)
81	80, 47	ffvelcdmd 7081	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐽‘𝑀) ∈ 𝐵)
82	48, 45, 49	matbas2i 22279	. . . . . . . . . . 11 ⊢ ((𝐽‘𝑀) ∈ 𝐵 → (𝐽‘𝑀) ∈ (𝐾 ↑_m (𝑁 × 𝑁)))
83		elmapi 8845	. . . . . . . . . . 11 ⊢ ((𝐽‘𝑀) ∈ (𝐾 ↑_m (𝑁 × 𝑁)) → (𝐽‘𝑀):(𝑁 × 𝑁)⟶𝐾)
84	81, 82, 83	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝐽‘𝑀):(𝑁 × 𝑁)⟶𝐾)
85	84	ad2antrr 723	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → (𝐽‘𝑀):(𝑁 × 𝑁)⟶𝐾)
86	58	ad2antrr 723	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → 𝐿 ∈ 𝑁)
87	85, 72, 86	fovcdmd 7576	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → (𝑏(𝐽‘𝑀)𝐿) ∈ 𝐾)
88		madugsum.t	. . . . . . . . 9 ⊢ · = (._r‘𝑅)
89	45, 88	ringcl 20155	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ ⦋𝑏 / 𝑖⦌𝑋 ∈ 𝐾 ∧ (𝑏(𝐽‘𝑀)𝐿) ∈ 𝐾) → (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)) ∈ 𝐾)
90	71, 77, 87, 89	syl3anc 1368	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 ∈ 𝑑) → (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)) ∈ 𝐾)
91		vex 3472	. . . . . . . 8 ⊢ 𝑒 ∈ V
92	91	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑒 ∈ V)
93		eldifn 4122	. . . . . . . 8 ⊢ (𝑒 ∈ (𝑁 ∖ 𝑑) → ¬ 𝑒 ∈ 𝑑)
94	93	ad2antll 726	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ¬ 𝑒 ∈ 𝑑)
95		eldifi 4121	. . . . . . . . . 10 ⊢ (𝑒 ∈ (𝑁 ∖ 𝑑) → 𝑒 ∈ 𝑁)
96	95	ad2antll 726	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑒 ∈ 𝑁)
97	74	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐾)
98		rspcsbela 4430	. . . . . . . . 9 ⊢ ((𝑒 ∈ 𝑁 ∧ ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐾) → ⦋𝑒 / 𝑖⦌𝑋 ∈ 𝐾)
99	96, 97, 98	syl2anc 583	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ⦋𝑒 / 𝑖⦌𝑋 ∈ 𝐾)
100	84	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝐽‘𝑀):(𝑁 × 𝑁)⟶𝐾)
101	58	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝐿 ∈ 𝑁)
102	100, 96, 101	fovcdmd 7576	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝑒(𝐽‘𝑀)𝐿) ∈ 𝐾)
103	45, 88	ringcl 20155	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ ⦋𝑒 / 𝑖⦌𝑋 ∈ 𝐾 ∧ (𝑒(𝐽‘𝑀)𝐿) ∈ 𝐾) → (⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿)) ∈ 𝐾)
104	65, 99, 102, 103	syl3anc 1368	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿)) ∈ 𝐾)
105		csbeq1 3891	. . . . . . . 8 ⊢ (𝑏 = 𝑒 → ⦋𝑏 / 𝑖⦌𝑋 = ⦋𝑒 / 𝑖⦌𝑋)
106		oveq1 7412	. . . . . . . 8 ⊢ (𝑏 = 𝑒 → (𝑏(𝐽‘𝑀)𝐿) = (𝑒(𝐽‘𝑀)𝐿))
107	105, 106	oveq12d 7423	. . . . . . 7 ⊢ (𝑏 = 𝑒 → (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)) = (⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿)))
108	45, 62, 67, 70, 90, 92, 94, 104, 107	gsumunsn 19880	. . . . . 6 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝑅 Σ_g (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = ((𝑅 Σ_g (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))(+_g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))))
109	108	adantr 480	. . . . 5 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ (𝑅 Σ_g (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏))))) → (𝑅 Σ_g (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = ((𝑅 Σ_g (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))(+_g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))))
110		oveq1 7412	. . . . . 6 ⊢ ((𝑅 Σ_g (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)))) → ((𝑅 Σ_g (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))(+_g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))) = ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏))))(+_g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))))
111	110	adantl 481	. . . . 5 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ (𝑅 Σ_g (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏))))) → ((𝑅 Σ_g (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))(+_g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))) = ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏))))(+_g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))))
112		elun 4143	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ (𝑑 ∪ {𝑒}) ↔ (𝑏 ∈ 𝑑 ∨ 𝑏 ∈ {𝑒}))
113		velsn 4639	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ {𝑒} ↔ 𝑏 = 𝑒)
114	113	orbi2i 909	. . . . . . . . . . . . . 14 ⊢ ((𝑏 ∈ 𝑑 ∨ 𝑏 ∈ {𝑒}) ↔ (𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒))
115	112, 114	bitri 275	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ (𝑑 ∪ {𝑒}) ↔ (𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒))
116		ifbi 4545	. . . . . . . . . . . . 13 ⊢ ((𝑏 ∈ (𝑑 ∪ {𝑒}) ↔ (𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒)) → if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)) = if((𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒), ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)))
117	115, 116	ax-mp 5	. . . . . . . . . . . 12 ⊢ if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)) = if((𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒), ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅))
118		ringmnd 20148	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
119	65, 118	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑅 ∈ Mnd)
120	119	3ad2ant1 1130	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝑅 ∈ Mnd)
121		simp3 1135	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝑏 ∈ 𝑁)
122	97	3ad2ant1 1130	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐾)
123	121, 122, 76	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → ⦋𝑏 / 𝑖⦌𝑋 ∈ 𝐾)
124		elequ1 2105	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑒 → (𝑏 ∈ 𝑑 ↔ 𝑒 ∈ 𝑑))
125	124	biimpac 478	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 ∈ 𝑑 ∧ 𝑏 = 𝑒) → 𝑒 ∈ 𝑑)
126	94, 125	nsyl 140	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ¬ (𝑏 ∈ 𝑑 ∧ 𝑏 = 𝑒))
127	126	3ad2ant1 1130	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → ¬ (𝑏 ∈ 𝑑 ∧ 𝑏 = 𝑒))
128	45, 35, 62	mndifsplit 22493	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Mnd ∧ ⦋𝑏 / 𝑖⦌𝑋 ∈ 𝐾 ∧ ¬ (𝑏 ∈ 𝑑 ∧ 𝑏 = 𝑒)) → if((𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒), ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)) = (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅))(+_g‘𝑅)if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅))))
129	120, 123, 127, 128	syl3anc 1368	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if((𝑏 ∈ 𝑑 ∨ 𝑏 = 𝑒), ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)) = (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅))(+_g‘𝑅)if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅))))
130	117, 129	eqtrid 2778	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)) = (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅))(+_g‘𝑅)if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅))))
131	105	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑏 = 𝑒) → ⦋𝑏 / 𝑖⦌𝑋 = ⦋𝑒 / 𝑖⦌𝑋)
132	131	ifeq1da 4554	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)) = if(𝑏 = 𝑒, ⦋𝑒 / 𝑖⦌𝑋, (0_g‘𝑅)))
133		ovif2 7503	. . . . . . . . . . . . . . 15 ⊢ (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1_r‘𝑅), (0_g‘𝑅))) = if(𝑏 = 𝑒, (⦋𝑒 / 𝑖⦌𝑋 · (1_r‘𝑅)), (⦋𝑒 / 𝑖⦌𝑋 · (0_g‘𝑅)))
134		eqid 2726	. . . . . . . . . . . . . . . . . 18 ⊢ (1_r‘𝑅) = (1_r‘𝑅)
135	45, 88, 134	ringridm 20169	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Ring ∧ ⦋𝑒 / 𝑖⦌𝑋 ∈ 𝐾) → (⦋𝑒 / 𝑖⦌𝑋 · (1_r‘𝑅)) = ⦋𝑒 / 𝑖⦌𝑋)
136	65, 99, 135	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (⦋𝑒 / 𝑖⦌𝑋 · (1_r‘𝑅)) = ⦋𝑒 / 𝑖⦌𝑋)
137	45, 88, 35	ringrz 20193	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Ring ∧ ⦋𝑒 / 𝑖⦌𝑋 ∈ 𝐾) → (⦋𝑒 / 𝑖⦌𝑋 · (0_g‘𝑅)) = (0_g‘𝑅))
138	65, 99, 137	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (⦋𝑒 / 𝑖⦌𝑋 · (0_g‘𝑅)) = (0_g‘𝑅))
139	136, 138	ifeq12d 4544	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → if(𝑏 = 𝑒, (⦋𝑒 / 𝑖⦌𝑋 · (1_r‘𝑅)), (⦋𝑒 / 𝑖⦌𝑋 · (0_g‘𝑅))) = if(𝑏 = 𝑒, ⦋𝑒 / 𝑖⦌𝑋, (0_g‘𝑅)))
140	133, 139	eqtrid 2778	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1_r‘𝑅), (0_g‘𝑅))) = if(𝑏 = 𝑒, ⦋𝑒 / 𝑖⦌𝑋, (0_g‘𝑅)))
141	132, 140	eqtr4d 2769	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)) = (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1_r‘𝑅), (0_g‘𝑅))))
142	141	oveq2d 7421	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅))(+_g‘𝑅)if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅))) = (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅))(+_g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1_r‘𝑅), (0_g‘𝑅)))))
143	142	3ad2ant1 1130	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅))(+_g‘𝑅)if(𝑏 = 𝑒, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅))) = (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅))(+_g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1_r‘𝑅), (0_g‘𝑅)))))
144	130, 143	eqtrd 2766	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)) = (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅))(+_g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1_r‘𝑅), (0_g‘𝑅)))))
145	144	ifeq1d 4542	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅))(+_g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1_r‘𝑅), (0_g‘𝑅)))), (𝑎𝑀𝑏)))
146	145	mpoeq3dva 7482	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅))(+_g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1_r‘𝑅), (0_g‘𝑅)))), (𝑎𝑀𝑏))))
147	146	fveq2d 6889	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅))(+_g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1_r‘𝑅), (0_g‘𝑅)))), (𝑎𝑀𝑏)))))
148	45, 35	ring0cl 20166	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Ring → (0_g‘𝑅) ∈ 𝐾)
149	65, 148	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (0_g‘𝑅) ∈ 𝐾)
150	149	3ad2ant1 1130	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (0_g‘𝑅) ∈ 𝐾)
151	123, 150	ifcld 4569	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)) ∈ 𝐾)
152	45, 134	ringidcl 20165	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ Ring → (1_r‘𝑅) ∈ 𝐾)
153	65, 152	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (1_r‘𝑅) ∈ 𝐾)
154	153, 149	ifcld 4569	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → if(𝑏 = 𝑒, (1_r‘𝑅), (0_g‘𝑅)) ∈ 𝐾)
155	45, 88	ringcl 20155	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Ring ∧ ⦋𝑒 / 𝑖⦌𝑋 ∈ 𝐾 ∧ if(𝑏 = 𝑒, (1_r‘𝑅), (0_g‘𝑅)) ∈ 𝐾) → (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1_r‘𝑅), (0_g‘𝑅))) ∈ 𝐾)
156	65, 99, 154, 155	syl3anc 1368	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1_r‘𝑅), (0_g‘𝑅))) ∈ 𝐾)
157	156	3ad2ant1 1130	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1_r‘𝑅), (0_g‘𝑅))) ∈ 𝐾)
158	55	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑀:(𝑁 × 𝑁)⟶𝐾)
159	158	fovcdmda 7575	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎𝑀𝑏) ∈ 𝐾)
160	159	3impb 1112	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (𝑎𝑀𝑏) ∈ 𝐾)
161	44, 45, 62, 63, 68, 151, 157, 160, 101	mdetrlin2 22464	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅))(+_g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1_r‘𝑅), (0_g‘𝑅)))), (𝑎𝑀𝑏)))) = ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏))))(+_g‘𝑅)(𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1_r‘𝑅), (0_g‘𝑅))), (𝑎𝑀𝑏))))))
162	154	3ad2ant1 1130	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑏 = 𝑒, (1_r‘𝑅), (0_g‘𝑅)) ∈ 𝐾)
163	44, 45, 88, 63, 68, 162, 160, 99, 101	mdetrsca2 22461	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1_r‘𝑅), (0_g‘𝑅))), (𝑎𝑀𝑏)))) = (⦋𝑒 / 𝑖⦌𝑋 · (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 = 𝑒, (1_r‘𝑅), (0_g‘𝑅)), (𝑎𝑀𝑏))))))
164	47	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → 𝑀 ∈ 𝐵)
165	48, 44, 78, 49, 134, 35	maducoeval 22496	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) → (𝑒(𝐽‘𝑀)𝐿) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 = 𝑒, (1_r‘𝑅), (0_g‘𝑅)), (𝑎𝑀𝑏)))))
166	164, 96, 101, 165	syl3anc 1368	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝑒(𝐽‘𝑀)𝐿) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 = 𝑒, (1_r‘𝑅), (0_g‘𝑅)), (𝑎𝑀𝑏)))))
167	166	oveq2d 7421	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿)) = (⦋𝑒 / 𝑖⦌𝑋 · (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 = 𝑒, (1_r‘𝑅), (0_g‘𝑅)), (𝑎𝑀𝑏))))))
168	163, 167	eqtr4d 2769	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1_r‘𝑅), (0_g‘𝑅))), (𝑎𝑀𝑏)))) = (⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿)))
169	168	oveq2d 7421	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏))))(+_g‘𝑅)(𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, (⦋𝑒 / 𝑖⦌𝑋 · if(𝑏 = 𝑒, (1_r‘𝑅), (0_g‘𝑅))), (𝑎𝑀𝑏))))) = ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏))))(+_g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))))
170	147, 161, 169	3eqtrrd 2771	. . . . . 6 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏))))(+_g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)))))
171	170	adantr 480	. . . . 5 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ (𝑅 Σ_g (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏))))) → ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏))))(+_g‘𝑅)(⦋𝑒 / 𝑖⦌𝑋 · (𝑒(𝐽‘𝑀)𝐿))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)))))
172	109, 111, 171	3eqtrd 2770	. . . 4 ⊢ (((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) ∧ (𝑅 Σ_g (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏))))) → (𝑅 Σ_g (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)))))
173	172	ex 412	. . 3 ⊢ ((𝜑 ∧ (𝑑 ⊆ 𝑁 ∧ 𝑒 ∈ (𝑁 ∖ 𝑑))) → ((𝑅 Σ_g (𝑏 ∈ 𝑑 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑑, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)))) → (𝑅 Σ_g (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏))))))
174	8, 16, 24, 32, 61, 173, 52	findcard2d 9168	. 2 ⊢ (𝜑 → (𝑅 Σ_g (𝑏 ∈ 𝑁 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)))))
175		nfcv 2897	. . . 4 ⊢ Ⅎ𝑏(𝑋 · (𝑖(𝐽‘𝑀)𝐿))
176		nfcsb1v 3913	. . . . 5 ⊢ Ⅎ𝑖⦋𝑏 / 𝑖⦌𝑋
177		nfcv 2897	. . . . 5 ⊢ Ⅎ𝑖 ·
178		nfcv 2897	. . . . 5 ⊢ Ⅎ𝑖(𝑏(𝐽‘𝑀)𝐿)
179	176, 177, 178	nfov 7435	. . . 4 ⊢ Ⅎ𝑖(⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))
180		csbeq1a 3902	. . . . 5 ⊢ (𝑖 = 𝑏 → 𝑋 = ⦋𝑏 / 𝑖⦌𝑋)
181		oveq1 7412	. . . . 5 ⊢ (𝑖 = 𝑏 → (𝑖(𝐽‘𝑀)𝐿) = (𝑏(𝐽‘𝑀)𝐿))
182	180, 181	oveq12d 7423	. . . 4 ⊢ (𝑖 = 𝑏 → (𝑋 · (𝑖(𝐽‘𝑀)𝐿)) = (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))
183	175, 179, 182	cbvmpt 5252	. . 3 ⊢ (𝑖 ∈ 𝑁 ↦ (𝑋 · (𝑖(𝐽‘𝑀)𝐿))) = (𝑏 ∈ 𝑁 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿)))
184	183	oveq2i 7416	. 2 ⊢ (𝑅 Σ_g (𝑖 ∈ 𝑁 ↦ (𝑋 · (𝑖(𝐽‘𝑀)𝐿)))) = (𝑅 Σ_g (𝑏 ∈ 𝑁 ↦ (⦋𝑏 / 𝑖⦌𝑋 · (𝑏(𝐽‘𝑀)𝐿))))
185		nfcv 2897	. . . . 5 ⊢ Ⅎ𝑎if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖))
186		nfcv 2897	. . . . 5 ⊢ Ⅎ𝑏if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖))
187		nfcv 2897	. . . . 5 ⊢ Ⅎ𝑗if(𝑎 = 𝐿, ⦋𝑏 / 𝑖⦌𝑋, (𝑎𝑀𝑏))
188		nfv 1909	. . . . . 6 ⊢ Ⅎ𝑖 𝑎 = 𝐿
189		nfcv 2897	. . . . . 6 ⊢ Ⅎ𝑖(𝑎𝑀𝑏)
190	188, 176, 189	nfif 4553	. . . . 5 ⊢ Ⅎ𝑖if(𝑎 = 𝐿, ⦋𝑏 / 𝑖⦌𝑋, (𝑎𝑀𝑏))
191		eqeq1 2730	. . . . . . 7 ⊢ (𝑗 = 𝑎 → (𝑗 = 𝐿 ↔ 𝑎 = 𝐿))
192	191	adantr 480	. . . . . 6 ⊢ ((𝑗 = 𝑎 ∧ 𝑖 = 𝑏) → (𝑗 = 𝐿 ↔ 𝑎 = 𝐿))
193	180	adantl 481	. . . . . 6 ⊢ ((𝑗 = 𝑎 ∧ 𝑖 = 𝑏) → 𝑋 = ⦋𝑏 / 𝑖⦌𝑋)
194		oveq12 7414	. . . . . 6 ⊢ ((𝑗 = 𝑎 ∧ 𝑖 = 𝑏) → (𝑗𝑀𝑖) = (𝑎𝑀𝑏))
195	192, 193, 194	ifbieq12d 4551	. . . . 5 ⊢ ((𝑗 = 𝑎 ∧ 𝑖 = 𝑏) → if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖)) = if(𝑎 = 𝐿, ⦋𝑏 / 𝑖⦌𝑋, (𝑎𝑀𝑏)))
196	185, 186, 187, 190, 195	cbvmpo 7499	. . . 4 ⊢ (𝑗 ∈ 𝑁, 𝑖 ∈ 𝑁 ↦ if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, ⦋𝑏 / 𝑖⦌𝑋, (𝑎𝑀𝑏)))
197		iftrue 4529	. . . . . . . 8 ⊢ (𝑏 ∈ 𝑁 → if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)) = ⦋𝑏 / 𝑖⦌𝑋)
198	197	eqcomd 2732	. . . . . . 7 ⊢ (𝑏 ∈ 𝑁 → ⦋𝑏 / 𝑖⦌𝑋 = if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)))
199	198	adantl 481	. . . . . 6 ⊢ ((𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → ⦋𝑏 / 𝑖⦌𝑋 = if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)))
200	199	ifeq1d 4542	. . . . 5 ⊢ ((𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → if(𝑎 = 𝐿, ⦋𝑏 / 𝑖⦌𝑋, (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)))
201	200	mpoeq3ia 7483	. . . 4 ⊢ (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, ⦋𝑏 / 𝑖⦌𝑋, (𝑎𝑀𝑏))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)))
202	196, 201	eqtri 2754	. . 3 ⊢ (𝑗 ∈ 𝑁, 𝑖 ∈ 𝑁 ↦ if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖))) = (𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏)))
203	202	fveq2i 6888	. 2 ⊢ (𝐷‘(𝑗 ∈ 𝑁, 𝑖 ∈ 𝑁 ↦ if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖)))) = (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ 𝑁, ⦋𝑏 / 𝑖⦌𝑋, (0_g‘𝑅)), (𝑎𝑀𝑏))))
204	174, 184, 203	3eqtr4g 2791	1 ⊢ (𝜑 → (𝑅 Σ_g (𝑖 ∈ 𝑁 ↦ (𝑋 · (𝑖(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑗 ∈ 𝑁, 𝑖 ∈ 𝑁 ↦ if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 844 ∧ w3a 1084 = wceq 1533 ∈ wcel 2098 ∀wral 3055 Vcvv 3468 ⦋csb 3888 ∖ cdif 3940 ∪ cun 3941 ⊆ wss 3943 ∅c0 4317 ifcif 4523 {csn 4623 ↦ cmpt 5224 × cxp 5667 ⟶wf 6533 ‘cfv 6537 (class class class)co 7405 ∈ cmpo 7407 ↑_m cmap 8822 Fincfn 8941 Basecbs 17153 +_gcplusg 17206 ._rcmulr 17207 0_gc0g 17394 Σ_g cgsu 17395 Mndcmnd 18667 CMndccmn 19700 1_rcur 20086 Ringcrg 20138 CRingccrg 20139 Mat cmat 22262 maDet cmdat 22441 maAdju cmadu 22489

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2697 ax-rep 5278 ax-sep 5292 ax-nul 5299 ax-pow 5356 ax-pr 5420 ax-un 7722 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189 ax-addf 11191 ax-mulf 11192

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-xor 1505 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2704 df-cleq 2718 df-clel 2804 df-nfc 2879 df-ne 2935 df-nel 3041 df-ral 3056 df-rex 3065 df-rmo 3370 df-reu 3371 df-rab 3427 df-v 3470 df-sbc 3773 df-csb 3889 df-dif 3946 df-un 3948 df-in 3950 df-ss 3960 df-pss 3962 df-nul 4318 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-tp 4628 df-op 4630 df-ot 4632 df-uni 4903 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 6294 df-ord 6361 df-on 6362 df-lim 6363 df-suc 6364 df-iota 6489 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-of 7667 df-om 7853 df-1st 7974 df-2nd 7975 df-supp 8147 df-tpos 8212 df-frecs 8267 df-wrecs 8298 df-recs 8372 df-rdg 8411 df-1o 8467 df-2o 8468 df-er 8705 df-map 8824 df-pm 8825 df-ixp 8894 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-fsupp 9364 df-sup 9439 df-oi 9507 df-card 9936 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-sub 11450 df-neg 11451 df-div 11876 df-nn 12217 df-2 12279 df-3 12280 df-4 12281 df-5 12282 df-6 12283 df-7 12284 df-8 12285 df-9 12286 df-n0 12477 df-xnn0 12549 df-z 12563 df-dec 12682 df-uz 12827 df-rp 12981 df-fz 13491 df-fzo 13634 df-seq 13973 df-exp 14033 df-hash 14296 df-word 14471 df-lsw 14519 df-concat 14527 df-s1 14552 df-substr 14597 df-pfx 14627 df-splice 14706 df-reverse 14715 df-s2 14805 df-struct 17089 df-sets 17106 df-slot 17124 df-ndx 17136 df-base 17154 df-ress 17183 df-plusg 17219 df-mulr 17220 df-starv 17221 df-sca 17222 df-vsca 17223 df-ip 17224 df-tset 17225 df-ple 17226 df-ds 17228 df-unif 17229 df-hom 17230 df-cco 17231 df-0g 17396 df-gsum 17397 df-prds 17402 df-pws 17404 df-mre 17539 df-mrc 17540 df-acs 17542 df-mgm 18573 df-sgrp 18652 df-mnd 18668 df-mhm 18713 df-submnd 18714 df-efmnd 18794 df-grp 18866 df-minusg 18867 df-mulg 18996 df-subg 19050 df-ghm 19139 df-gim 19184 df-cntz 19233 df-oppg 19262 df-symg 19287 df-pmtr 19362 df-psgn 19411 df-cmn 19702 df-abl 19703 df-mgp 20040 df-rng 20058 df-ur 20087 df-ring 20140 df-cring 20141 df-oppr 20236 df-dvdsr 20259 df-unit 20260 df-invr 20290 df-dvr 20303 df-rhm 20374 df-subrng 20446 df-subrg 20471 df-drng 20589 df-sra 21021 df-rgmod 21022 df-cnfld 21241 df-zring 21334 df-zrh 21390 df-dsmm 21627 df-frlm 21642 df-mat 22263 df-mdet 22442 df-madu 22491

This theorem is referenced by: madurid 22501 mdetlap1 33336

W3C validator