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

 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 𝑅)
Assertion
Ref Expression
madugsum (𝜑 → (𝑅 Σg (𝑖𝑁 ↦ (𝑋 · (𝑖(𝐽𝑀)𝐿)))) = (𝐷‘(𝑗𝑁, 𝑖𝑁 ↦ if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖)))))
Distinct variable groups:   𝑖,𝑁,𝑗   𝑅,𝑖,𝑗   𝐵,𝑖,𝑗   𝜑,𝑖,𝑗   𝑖,𝐽   𝑖,𝐾,𝑗   𝑖,𝑀,𝑗   𝑗,𝑋   · ,𝑖   𝑖,𝐿,𝑗
Allowed substitution hints:   𝐴(𝑖,𝑗)   𝐷(𝑖,𝑗)   · (𝑗)   𝐽(𝑗)   𝑋(𝑖)

Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mpteq1 5151 . . . . 5 (𝑐 = ∅ → (𝑏𝑐 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿))) = (𝑏 ∈ ∅ ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿))))
21oveq2d 7166 . . . 4 (𝑐 = ∅ → (𝑅 Σg (𝑏𝑐 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))) = (𝑅 Σg (𝑏 ∈ ∅ ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))))
3 eleq2 2906 . . . . . . . 8 (𝑐 = ∅ → (𝑏𝑐𝑏 ∈ ∅))
43ifbid 4492 . . . . . . 7 (𝑐 = ∅ → if(𝑏𝑐, 𝑏 / 𝑖𝑋, (0g𝑅)) = if(𝑏 ∈ ∅, 𝑏 / 𝑖𝑋, (0g𝑅)))
54ifeq1d 4488 . . . . . 6 (𝑐 = ∅ → if(𝑎 = 𝐿, if(𝑏𝑐, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, if(𝑏 ∈ ∅, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)))
65mpoeq3dv 7227 . . . . 5 (𝑐 = ∅ → (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑐, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏))) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏))))
76fveq2d 6673 . . . 4 (𝑐 = ∅ → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑐, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)))))
82, 7eqeq12d 2842 . . 3 (𝑐 = ∅ → ((𝑅 Σg (𝑏𝑐 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑐, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)))) ↔ (𝑅 Σg (𝑏 ∈ ∅ ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏))))))
9 mpteq1 5151 . . . . 5 (𝑐 = 𝑑 → (𝑏𝑐 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿))) = (𝑏𝑑 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿))))
109oveq2d 7166 . . . 4 (𝑐 = 𝑑 → (𝑅 Σg (𝑏𝑐 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))) = (𝑅 Σg (𝑏𝑑 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))))
11 eleq2 2906 . . . . . . . 8 (𝑐 = 𝑑 → (𝑏𝑐𝑏𝑑))
1211ifbid 4492 . . . . . . 7 (𝑐 = 𝑑 → if(𝑏𝑐, 𝑏 / 𝑖𝑋, (0g𝑅)) = if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅)))
1312ifeq1d 4488 . . . . . 6 (𝑐 = 𝑑 → if(𝑎 = 𝐿, if(𝑏𝑐, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)))
1413mpoeq3dv 7227 . . . . 5 (𝑐 = 𝑑 → (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑐, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏))) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏))))
1514fveq2d 6673 . . . 4 (𝑐 = 𝑑 → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑐, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)))))
1610, 15eqeq12d 2842 . . 3 (𝑐 = 𝑑 → ((𝑅 Σg (𝑏𝑐 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑐, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)))) ↔ (𝑅 Σg (𝑏𝑑 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏))))))
17 mpteq1 5151 . . . . 5 (𝑐 = (𝑑 ∪ {𝑒}) → (𝑏𝑐 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿))) = (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿))))
1817oveq2d 7166 . . . 4 (𝑐 = (𝑑 ∪ {𝑒}) → (𝑅 Σg (𝑏𝑐 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))) = (𝑅 Σg (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))))
19 eleq2 2906 . . . . . . . 8 (𝑐 = (𝑑 ∪ {𝑒}) → (𝑏𝑐𝑏 ∈ (𝑑 ∪ {𝑒})))
2019ifbid 4492 . . . . . . 7 (𝑐 = (𝑑 ∪ {𝑒}) → if(𝑏𝑐, 𝑏 / 𝑖𝑋, (0g𝑅)) = if(𝑏 ∈ (𝑑 ∪ {𝑒}), 𝑏 / 𝑖𝑋, (0g𝑅)))
2120ifeq1d 4488 . . . . . 6 (𝑐 = (𝑑 ∪ {𝑒}) → if(𝑎 = 𝐿, if(𝑏𝑐, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)))
2221mpoeq3dv 7227 . . . . 5 (𝑐 = (𝑑 ∪ {𝑒}) → (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑐, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏))) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏))))
2322fveq2d 6673 . . . 4 (𝑐 = (𝑑 ∪ {𝑒}) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑐, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)))))
2418, 23eqeq12d 2842 . . 3 (𝑐 = (𝑑 ∪ {𝑒}) → ((𝑅 Σg (𝑏𝑐 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑐, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)))) ↔ (𝑅 Σg (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏))))))
25 mpteq1 5151 . . . . 5 (𝑐 = 𝑁 → (𝑏𝑐 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿))) = (𝑏𝑁 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿))))
2625oveq2d 7166 . . . 4 (𝑐 = 𝑁 → (𝑅 Σg (𝑏𝑐 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))) = (𝑅 Σg (𝑏𝑁 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))))
27 eleq2 2906 . . . . . . . 8 (𝑐 = 𝑁 → (𝑏𝑐𝑏𝑁))
2827ifbid 4492 . . . . . . 7 (𝑐 = 𝑁 → if(𝑏𝑐, 𝑏 / 𝑖𝑋, (0g𝑅)) = if(𝑏𝑁, 𝑏 / 𝑖𝑋, (0g𝑅)))
2928ifeq1d 4488 . . . . . 6 (𝑐 = 𝑁 → if(𝑎 = 𝐿, if(𝑏𝑐, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, if(𝑏𝑁, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)))
3029mpoeq3dv 7227 . . . . 5 (𝑐 = 𝑁 → (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑐, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏))) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑁, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏))))
3130fveq2d 6673 . . . 4 (𝑐 = 𝑁 → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑐, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑁, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)))))
3226, 31eqeq12d 2842 . . 3 (𝑐 = 𝑁 → ((𝑅 Σg (𝑏𝑐 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑐, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)))) ↔ (𝑅 Σg (𝑏𝑁 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑁, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏))))))
33 noel 4300 . . . . . . . . 9 ¬ 𝑏 ∈ ∅
34 iffalse 4479 . . . . . . . . 9 𝑏 ∈ ∅ → if(𝑏 ∈ ∅, 𝑏 / 𝑖𝑋, (0g𝑅)) = (0g𝑅))
3533, 34mp1i 13 . . . . . . . 8 ((𝑎𝑁𝑏𝑁) → if(𝑏 ∈ ∅, 𝑏 / 𝑖𝑋, (0g𝑅)) = (0g𝑅))
3635ifeq1d 4488 . . . . . . 7 ((𝑎𝑁𝑏𝑁) → if(𝑎 = 𝐿, if(𝑏 ∈ ∅, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, (0g𝑅), (𝑎𝑀𝑏)))
3736mpoeq3ia 7226 . . . . . 6 (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏))) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, (0g𝑅), (𝑎𝑀𝑏)))
3837fveq2i 6672 . . . . 5 (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, (0g𝑅), (𝑎𝑀𝑏))))
39 madugsum.d . . . . . 6 𝐷 = (𝑁 maDet 𝑅)
40 madugsum.k . . . . . 6 𝐾 = (Base‘𝑅)
41 eqid 2826 . . . . . 6 (0g𝑅) = (0g𝑅)
42 madugsum.r . . . . . 6 (𝜑𝑅 ∈ CRing)
43 madugsum.m . . . . . . . 8 (𝜑𝑀𝐵)
44 maduf.a . . . . . . . . 9 𝐴 = (𝑁 Mat 𝑅)
45 maduf.b . . . . . . . . 9 𝐵 = (Base‘𝐴)
4644, 45matrcl 20956 . . . . . . . 8 (𝑀𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
4743, 46syl 17 . . . . . . 7 (𝜑 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
4847simpld 495 . . . . . 6 (𝜑𝑁 ∈ Fin)
4944, 40, 45matbas2i 20966 . . . . . . . . 9 (𝑀𝐵𝑀 ∈ (𝐾m (𝑁 × 𝑁)))
50 elmapi 8423 . . . . . . . . 9 (𝑀 ∈ (𝐾m (𝑁 × 𝑁)) → 𝑀:(𝑁 × 𝑁)⟶𝐾)
5143, 49, 503syl 18 . . . . . . . 8 (𝜑𝑀:(𝑁 × 𝑁)⟶𝐾)
5251fovrnda 7313 . . . . . . 7 ((𝜑 ∧ (𝑎𝑁𝑏𝑁)) → (𝑎𝑀𝑏) ∈ 𝐾)
53523impb 1109 . . . . . 6 ((𝜑𝑎𝑁𝑏𝑁) → (𝑎𝑀𝑏) ∈ 𝐾)
54 madugsum.l . . . . . 6 (𝜑𝐿𝑁)
5539, 40, 41, 42, 48, 53, 54mdetr0 21149 . . . . 5 (𝜑 → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, (0g𝑅), (𝑎𝑀𝑏)))) = (0g𝑅))
5638, 55syl5eq 2873 . . . 4 (𝜑 → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)))) = (0g𝑅))
57 mpt0 6489 . . . . . 6 (𝑏 ∈ ∅ ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿))) = ∅
5857oveq2i 7161 . . . . 5 (𝑅 Σg (𝑏 ∈ ∅ ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))) = (𝑅 Σg ∅)
5941gsum0 17889 . . . . 5 (𝑅 Σg ∅) = (0g𝑅)
6058, 59eqtri 2849 . . . 4 (𝑅 Σg (𝑏 ∈ ∅ ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))) = (0g𝑅)
6156, 60syl6reqr 2880 . . 3 (𝜑 → (𝑅 Σg (𝑏 ∈ ∅ ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ ∅, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)))))
62 eqid 2826 . . . . . . 7 (+g𝑅) = (+g𝑅)
6342adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → 𝑅 ∈ CRing)
64 crngring 19244 . . . . . . . . 9 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
6563, 64syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → 𝑅 ∈ Ring)
66 ringcmn 19267 . . . . . . . 8 (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
6765, 66syl 17 . . . . . . 7 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → 𝑅 ∈ CMnd)
6848adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → 𝑁 ∈ Fin)
69 simprl 767 . . . . . . . 8 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → 𝑑𝑁)
7068, 69ssfid 8735 . . . . . . 7 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → 𝑑 ∈ Fin)
7165adantr 481 . . . . . . . 8 (((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) ∧ 𝑏𝑑) → 𝑅 ∈ Ring)
7269sselda 3971 . . . . . . . . 9 (((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) ∧ 𝑏𝑑) → 𝑏𝑁)
73 madugsum.x . . . . . . . . . . 11 ((𝜑𝑖𝑁) → 𝑋𝐾)
7473ralrimiva 3187 . . . . . . . . . 10 (𝜑 → ∀𝑖𝑁 𝑋𝐾)
7574ad2antrr 722 . . . . . . . . 9 (((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) ∧ 𝑏𝑑) → ∀𝑖𝑁 𝑋𝐾)
76 rspcsbela 4391 . . . . . . . . 9 ((𝑏𝑁 ∧ ∀𝑖𝑁 𝑋𝐾) → 𝑏 / 𝑖𝑋𝐾)
7772, 75, 76syl2anc 584 . . . . . . . 8 (((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) ∧ 𝑏𝑑) → 𝑏 / 𝑖𝑋𝐾)
78 maduf.j . . . . . . . . . . . . . 14 𝐽 = (𝑁 maAdju 𝑅)
7944, 78, 45maduf 21185 . . . . . . . . . . . . 13 (𝑅 ∈ CRing → 𝐽:𝐵𝐵)
8042, 79syl 17 . . . . . . . . . . . 12 (𝜑𝐽:𝐵𝐵)
8180, 43ffvelrnd 6850 . . . . . . . . . . 11 (𝜑 → (𝐽𝑀) ∈ 𝐵)
8244, 40, 45matbas2i 20966 . . . . . . . . . . 11 ((𝐽𝑀) ∈ 𝐵 → (𝐽𝑀) ∈ (𝐾m (𝑁 × 𝑁)))
83 elmapi 8423 . . . . . . . . . . 11 ((𝐽𝑀) ∈ (𝐾m (𝑁 × 𝑁)) → (𝐽𝑀):(𝑁 × 𝑁)⟶𝐾)
8481, 82, 833syl 18 . . . . . . . . . 10 (𝜑 → (𝐽𝑀):(𝑁 × 𝑁)⟶𝐾)
8584ad2antrr 722 . . . . . . . . 9 (((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) ∧ 𝑏𝑑) → (𝐽𝑀):(𝑁 × 𝑁)⟶𝐾)
8654ad2antrr 722 . . . . . . . . 9 (((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) ∧ 𝑏𝑑) → 𝐿𝑁)
8785, 72, 86fovrnd 7314 . . . . . . . 8 (((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) ∧ 𝑏𝑑) → (𝑏(𝐽𝑀)𝐿) ∈ 𝐾)
88 madugsum.t . . . . . . . . 9 · = (.r𝑅)
8940, 88ringcl 19247 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝑏 / 𝑖𝑋𝐾 ∧ (𝑏(𝐽𝑀)𝐿) ∈ 𝐾) → (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)) ∈ 𝐾)
9071, 77, 87, 89syl3anc 1365 . . . . . . 7 (((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) ∧ 𝑏𝑑) → (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)) ∈ 𝐾)
91 vex 3503 . . . . . . . 8 𝑒 ∈ V
9291a1i 11 . . . . . . 7 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → 𝑒 ∈ V)
93 eldifn 4108 . . . . . . . 8 (𝑒 ∈ (𝑁𝑑) → ¬ 𝑒𝑑)
9493ad2antll 725 . . . . . . 7 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → ¬ 𝑒𝑑)
95 eldifi 4107 . . . . . . . . . 10 (𝑒 ∈ (𝑁𝑑) → 𝑒𝑁)
9695ad2antll 725 . . . . . . . . 9 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → 𝑒𝑁)
9774adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → ∀𝑖𝑁 𝑋𝐾)
98 rspcsbela 4391 . . . . . . . . 9 ((𝑒𝑁 ∧ ∀𝑖𝑁 𝑋𝐾) → 𝑒 / 𝑖𝑋𝐾)
9996, 97, 98syl2anc 584 . . . . . . . 8 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → 𝑒 / 𝑖𝑋𝐾)
10084adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → (𝐽𝑀):(𝑁 × 𝑁)⟶𝐾)
10154adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → 𝐿𝑁)
102100, 96, 101fovrnd 7314 . . . . . . . 8 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → (𝑒(𝐽𝑀)𝐿) ∈ 𝐾)
10340, 88ringcl 19247 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝑒 / 𝑖𝑋𝐾 ∧ (𝑒(𝐽𝑀)𝐿) ∈ 𝐾) → (𝑒 / 𝑖𝑋 · (𝑒(𝐽𝑀)𝐿)) ∈ 𝐾)
10465, 99, 102, 103syl3anc 1365 . . . . . . 7 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → (𝑒 / 𝑖𝑋 · (𝑒(𝐽𝑀)𝐿)) ∈ 𝐾)
105 csbeq1 3890 . . . . . . . 8 (𝑏 = 𝑒𝑏 / 𝑖𝑋 = 𝑒 / 𝑖𝑋)
106 oveq1 7157 . . . . . . . 8 (𝑏 = 𝑒 → (𝑏(𝐽𝑀)𝐿) = (𝑒(𝐽𝑀)𝐿))
107105, 106oveq12d 7168 . . . . . . 7 (𝑏 = 𝑒 → (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)) = (𝑒 / 𝑖𝑋 · (𝑒(𝐽𝑀)𝐿)))
10840, 62, 67, 70, 90, 92, 94, 104, 107gsumunsn 19016 . . . . . 6 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → (𝑅 Σg (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))) = ((𝑅 Σg (𝑏𝑑 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿))))(+g𝑅)(𝑒 / 𝑖𝑋 · (𝑒(𝐽𝑀)𝐿))))
109108adantr 481 . . . . 5 (((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) ∧ (𝑅 Σg (𝑏𝑑 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏))))) → (𝑅 Σg (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))) = ((𝑅 Σg (𝑏𝑑 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿))))(+g𝑅)(𝑒 / 𝑖𝑋 · (𝑒(𝐽𝑀)𝐿))))
110 oveq1 7157 . . . . . 6 ((𝑅 Σg (𝑏𝑑 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)))) → ((𝑅 Σg (𝑏𝑑 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿))))(+g𝑅)(𝑒 / 𝑖𝑋 · (𝑒(𝐽𝑀)𝐿))) = ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏))))(+g𝑅)(𝑒 / 𝑖𝑋 · (𝑒(𝐽𝑀)𝐿))))
111110adantl 482 . . . . 5 (((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) ∧ (𝑅 Σg (𝑏𝑑 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏))))) → ((𝑅 Σg (𝑏𝑑 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿))))(+g𝑅)(𝑒 / 𝑖𝑋 · (𝑒(𝐽𝑀)𝐿))) = ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏))))(+g𝑅)(𝑒 / 𝑖𝑋 · (𝑒(𝐽𝑀)𝐿))))
112 elun 4129 . . . . . . . . . . . . . 14 (𝑏 ∈ (𝑑 ∪ {𝑒}) ↔ (𝑏𝑑𝑏 ∈ {𝑒}))
113 velsn 4580 . . . . . . . . . . . . . . 15 (𝑏 ∈ {𝑒} ↔ 𝑏 = 𝑒)
114113orbi2i 908 . . . . . . . . . . . . . 14 ((𝑏𝑑𝑏 ∈ {𝑒}) ↔ (𝑏𝑑𝑏 = 𝑒))
115112, 114bitri 276 . . . . . . . . . . . . 13 (𝑏 ∈ (𝑑 ∪ {𝑒}) ↔ (𝑏𝑑𝑏 = 𝑒))
116 ifbi 4491 . . . . . . . . . . . . 13 ((𝑏 ∈ (𝑑 ∪ {𝑒}) ↔ (𝑏𝑑𝑏 = 𝑒)) → if(𝑏 ∈ (𝑑 ∪ {𝑒}), 𝑏 / 𝑖𝑋, (0g𝑅)) = if((𝑏𝑑𝑏 = 𝑒), 𝑏 / 𝑖𝑋, (0g𝑅)))
117115, 116ax-mp 5 . . . . . . . . . . . 12 if(𝑏 ∈ (𝑑 ∪ {𝑒}), 𝑏 / 𝑖𝑋, (0g𝑅)) = if((𝑏𝑑𝑏 = 𝑒), 𝑏 / 𝑖𝑋, (0g𝑅))
118 ringmnd 19242 . . . . . . . . . . . . . . 15 (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
11965, 118syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → 𝑅 ∈ Mnd)
1201193ad2ant1 1127 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) ∧ 𝑎𝑁𝑏𝑁) → 𝑅 ∈ Mnd)
121 simp3 1132 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) ∧ 𝑎𝑁𝑏𝑁) → 𝑏𝑁)
122973ad2ant1 1127 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) ∧ 𝑎𝑁𝑏𝑁) → ∀𝑖𝑁 𝑋𝐾)
123121, 122, 76syl2anc 584 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) ∧ 𝑎𝑁𝑏𝑁) → 𝑏 / 𝑖𝑋𝐾)
124 elequ1 2114 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑒 → (𝑏𝑑𝑒𝑑))
125124biimpac 479 . . . . . . . . . . . . . . 15 ((𝑏𝑑𝑏 = 𝑒) → 𝑒𝑑)
12694, 125nsyl 142 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → ¬ (𝑏𝑑𝑏 = 𝑒))
1271263ad2ant1 1127 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) ∧ 𝑎𝑁𝑏𝑁) → ¬ (𝑏𝑑𝑏 = 𝑒))
12840, 41, 62mndifsplit 21180 . . . . . . . . . . . . 13 ((𝑅 ∈ Mnd ∧ 𝑏 / 𝑖𝑋𝐾 ∧ ¬ (𝑏𝑑𝑏 = 𝑒)) → if((𝑏𝑑𝑏 = 𝑒), 𝑏 / 𝑖𝑋, (0g𝑅)) = (if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅))(+g𝑅)if(𝑏 = 𝑒, 𝑏 / 𝑖𝑋, (0g𝑅))))
129120, 123, 127, 128syl3anc 1365 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) ∧ 𝑎𝑁𝑏𝑁) → if((𝑏𝑑𝑏 = 𝑒), 𝑏 / 𝑖𝑋, (0g𝑅)) = (if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅))(+g𝑅)if(𝑏 = 𝑒, 𝑏 / 𝑖𝑋, (0g𝑅))))
130117, 129syl5eq 2873 . . . . . . . . . . 11 (((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) ∧ 𝑎𝑁𝑏𝑁) → if(𝑏 ∈ (𝑑 ∪ {𝑒}), 𝑏 / 𝑖𝑋, (0g𝑅)) = (if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅))(+g𝑅)if(𝑏 = 𝑒, 𝑏 / 𝑖𝑋, (0g𝑅))))
131105adantl 482 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) ∧ 𝑏 = 𝑒) → 𝑏 / 𝑖𝑋 = 𝑒 / 𝑖𝑋)
132131ifeq1da 4500 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → if(𝑏 = 𝑒, 𝑏 / 𝑖𝑋, (0g𝑅)) = if(𝑏 = 𝑒, 𝑒 / 𝑖𝑋, (0g𝑅)))
133 ovif2 7246 . . . . . . . . . . . . . . 15 (𝑒 / 𝑖𝑋 · if(𝑏 = 𝑒, (1r𝑅), (0g𝑅))) = if(𝑏 = 𝑒, (𝑒 / 𝑖𝑋 · (1r𝑅)), (𝑒 / 𝑖𝑋 · (0g𝑅)))
134 eqid 2826 . . . . . . . . . . . . . . . . . 18 (1r𝑅) = (1r𝑅)
13540, 88, 134ringridm 19258 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ Ring ∧ 𝑒 / 𝑖𝑋𝐾) → (𝑒 / 𝑖𝑋 · (1r𝑅)) = 𝑒 / 𝑖𝑋)
13665, 99, 135syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → (𝑒 / 𝑖𝑋 · (1r𝑅)) = 𝑒 / 𝑖𝑋)
13740, 88, 41ringrz 19274 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ Ring ∧ 𝑒 / 𝑖𝑋𝐾) → (𝑒 / 𝑖𝑋 · (0g𝑅)) = (0g𝑅))
13865, 99, 137syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → (𝑒 / 𝑖𝑋 · (0g𝑅)) = (0g𝑅))
139136, 138ifeq12d 4490 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → if(𝑏 = 𝑒, (𝑒 / 𝑖𝑋 · (1r𝑅)), (𝑒 / 𝑖𝑋 · (0g𝑅))) = if(𝑏 = 𝑒, 𝑒 / 𝑖𝑋, (0g𝑅)))
140133, 139syl5eq 2873 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → (𝑒 / 𝑖𝑋 · if(𝑏 = 𝑒, (1r𝑅), (0g𝑅))) = if(𝑏 = 𝑒, 𝑒 / 𝑖𝑋, (0g𝑅)))
141132, 140eqtr4d 2864 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → if(𝑏 = 𝑒, 𝑏 / 𝑖𝑋, (0g𝑅)) = (𝑒 / 𝑖𝑋 · if(𝑏 = 𝑒, (1r𝑅), (0g𝑅))))
142141oveq2d 7166 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → (if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅))(+g𝑅)if(𝑏 = 𝑒, 𝑏 / 𝑖𝑋, (0g𝑅))) = (if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅))(+g𝑅)(𝑒 / 𝑖𝑋 · if(𝑏 = 𝑒, (1r𝑅), (0g𝑅)))))
1431423ad2ant1 1127 . . . . . . . . . . 11 (((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) ∧ 𝑎𝑁𝑏𝑁) → (if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅))(+g𝑅)if(𝑏 = 𝑒, 𝑏 / 𝑖𝑋, (0g𝑅))) = (if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅))(+g𝑅)(𝑒 / 𝑖𝑋 · if(𝑏 = 𝑒, (1r𝑅), (0g𝑅)))))
144130, 143eqtrd 2861 . . . . . . . . . 10 (((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) ∧ 𝑎𝑁𝑏𝑁) → if(𝑏 ∈ (𝑑 ∪ {𝑒}), 𝑏 / 𝑖𝑋, (0g𝑅)) = (if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅))(+g𝑅)(𝑒 / 𝑖𝑋 · if(𝑏 = 𝑒, (1r𝑅), (0g𝑅)))))
145144ifeq1d 4488 . . . . . . . . 9 (((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) ∧ 𝑎𝑁𝑏𝑁) → if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, (if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅))(+g𝑅)(𝑒 / 𝑖𝑋 · if(𝑏 = 𝑒, (1r𝑅), (0g𝑅)))), (𝑎𝑀𝑏)))
146145mpoeq3dva 7225 . . . . . . . 8 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏))) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, (if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅))(+g𝑅)(𝑒 / 𝑖𝑋 · if(𝑏 = 𝑒, (1r𝑅), (0g𝑅)))), (𝑎𝑀𝑏))))
147146fveq2d 6673 . . . . . . 7 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, (if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅))(+g𝑅)(𝑒 / 𝑖𝑋 · if(𝑏 = 𝑒, (1r𝑅), (0g𝑅)))), (𝑎𝑀𝑏)))))
14840, 41ring0cl 19255 . . . . . . . . . . 11 (𝑅 ∈ Ring → (0g𝑅) ∈ 𝐾)
14965, 148syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → (0g𝑅) ∈ 𝐾)
1501493ad2ant1 1127 . . . . . . . . 9 (((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) ∧ 𝑎𝑁𝑏𝑁) → (0g𝑅) ∈ 𝐾)
151123, 150ifcld 4515 . . . . . . . 8 (((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) ∧ 𝑎𝑁𝑏𝑁) → if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅)) ∈ 𝐾)
15240, 134ringidcl 19254 . . . . . . . . . . . 12 (𝑅 ∈ Ring → (1r𝑅) ∈ 𝐾)
15365, 152syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → (1r𝑅) ∈ 𝐾)
154153, 149ifcld 4515 . . . . . . . . . 10 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → if(𝑏 = 𝑒, (1r𝑅), (0g𝑅)) ∈ 𝐾)
15540, 88ringcl 19247 . . . . . . . . . 10 ((𝑅 ∈ Ring ∧ 𝑒 / 𝑖𝑋𝐾 ∧ if(𝑏 = 𝑒, (1r𝑅), (0g𝑅)) ∈ 𝐾) → (𝑒 / 𝑖𝑋 · if(𝑏 = 𝑒, (1r𝑅), (0g𝑅))) ∈ 𝐾)
15665, 99, 154, 155syl3anc 1365 . . . . . . . . 9 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → (𝑒 / 𝑖𝑋 · if(𝑏 = 𝑒, (1r𝑅), (0g𝑅))) ∈ 𝐾)
1571563ad2ant1 1127 . . . . . . . 8 (((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) ∧ 𝑎𝑁𝑏𝑁) → (𝑒 / 𝑖𝑋 · if(𝑏 = 𝑒, (1r𝑅), (0g𝑅))) ∈ 𝐾)
15851adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → 𝑀:(𝑁 × 𝑁)⟶𝐾)
159158fovrnda 7313 . . . . . . . . 9 (((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) ∧ (𝑎𝑁𝑏𝑁)) → (𝑎𝑀𝑏) ∈ 𝐾)
1601593impb 1109 . . . . . . . 8 (((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) ∧ 𝑎𝑁𝑏𝑁) → (𝑎𝑀𝑏) ∈ 𝐾)
16139, 40, 62, 63, 68, 151, 157, 160, 101mdetrlin2 21151 . . . . . . 7 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, (if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅))(+g𝑅)(𝑒 / 𝑖𝑋 · if(𝑏 = 𝑒, (1r𝑅), (0g𝑅)))), (𝑎𝑀𝑏)))) = ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏))))(+g𝑅)(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, (𝑒 / 𝑖𝑋 · if(𝑏 = 𝑒, (1r𝑅), (0g𝑅))), (𝑎𝑀𝑏))))))
1621543ad2ant1 1127 . . . . . . . . . 10 (((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) ∧ 𝑎𝑁𝑏𝑁) → if(𝑏 = 𝑒, (1r𝑅), (0g𝑅)) ∈ 𝐾)
16339, 40, 88, 63, 68, 162, 160, 99, 101mdetrsca2 21148 . . . . . . . . 9 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, (𝑒 / 𝑖𝑋 · if(𝑏 = 𝑒, (1r𝑅), (0g𝑅))), (𝑎𝑀𝑏)))) = (𝑒 / 𝑖𝑋 · (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 = 𝑒, (1r𝑅), (0g𝑅)), (𝑎𝑀𝑏))))))
16443adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → 𝑀𝐵)
16544, 39, 78, 45, 134, 41maducoeval 21183 . . . . . . . . . . 11 ((𝑀𝐵𝑒𝑁𝐿𝑁) → (𝑒(𝐽𝑀)𝐿) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 = 𝑒, (1r𝑅), (0g𝑅)), (𝑎𝑀𝑏)))))
166164, 96, 101, 165syl3anc 1365 . . . . . . . . . 10 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → (𝑒(𝐽𝑀)𝐿) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 = 𝑒, (1r𝑅), (0g𝑅)), (𝑎𝑀𝑏)))))
167166oveq2d 7166 . . . . . . . . 9 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → (𝑒 / 𝑖𝑋 · (𝑒(𝐽𝑀)𝐿)) = (𝑒 / 𝑖𝑋 · (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 = 𝑒, (1r𝑅), (0g𝑅)), (𝑎𝑀𝑏))))))
168163, 167eqtr4d 2864 . . . . . . . 8 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, (𝑒 / 𝑖𝑋 · if(𝑏 = 𝑒, (1r𝑅), (0g𝑅))), (𝑎𝑀𝑏)))) = (𝑒 / 𝑖𝑋 · (𝑒(𝐽𝑀)𝐿)))
169168oveq2d 7166 . . . . . . 7 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏))))(+g𝑅)(𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, (𝑒 / 𝑖𝑋 · if(𝑏 = 𝑒, (1r𝑅), (0g𝑅))), (𝑎𝑀𝑏))))) = ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏))))(+g𝑅)(𝑒 / 𝑖𝑋 · (𝑒(𝐽𝑀)𝐿))))
170147, 161, 1693eqtrrd 2866 . . . . . 6 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏))))(+g𝑅)(𝑒 / 𝑖𝑋 · (𝑒(𝐽𝑀)𝐿))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)))))
171170adantr 481 . . . . 5 (((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) ∧ (𝑅 Σg (𝑏𝑑 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏))))) → ((𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏))))(+g𝑅)(𝑒 / 𝑖𝑋 · (𝑒(𝐽𝑀)𝐿))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)))))
172109, 111, 1713eqtrd 2865 . . . 4 (((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) ∧ (𝑅 Σg (𝑏𝑑 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏))))) → (𝑅 Σg (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)))))
173172ex 413 . . 3 ((𝜑 ∧ (𝑑𝑁𝑒 ∈ (𝑁𝑑))) → ((𝑅 Σg (𝑏𝑑 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑑, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)))) → (𝑅 Σg (𝑏 ∈ (𝑑 ∪ {𝑒}) ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏 ∈ (𝑑 ∪ {𝑒}), 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏))))))
1748, 16, 24, 32, 61, 173, 48findcard2d 8754 . 2 (𝜑 → (𝑅 Σg (𝑏𝑁 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑁, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)))))
175 nfcv 2982 . . . 4 𝑏(𝑋 · (𝑖(𝐽𝑀)𝐿))
176 nfcsb1v 3911 . . . . 5 𝑖𝑏 / 𝑖𝑋
177 nfcv 2982 . . . . 5 𝑖 ·
178 nfcv 2982 . . . . 5 𝑖(𝑏(𝐽𝑀)𝐿)
179176, 177, 178nfov 7180 . . . 4 𝑖(𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿))
180 csbeq1a 3901 . . . . 5 (𝑖 = 𝑏𝑋 = 𝑏 / 𝑖𝑋)
181 oveq1 7157 . . . . 5 (𝑖 = 𝑏 → (𝑖(𝐽𝑀)𝐿) = (𝑏(𝐽𝑀)𝐿))
182180, 181oveq12d 7168 . . . 4 (𝑖 = 𝑏 → (𝑋 · (𝑖(𝐽𝑀)𝐿)) = (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))
183175, 179, 182cbvmpt 5164 . . 3 (𝑖𝑁 ↦ (𝑋 · (𝑖(𝐽𝑀)𝐿))) = (𝑏𝑁 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿)))
184183oveq2i 7161 . 2 (𝑅 Σg (𝑖𝑁 ↦ (𝑋 · (𝑖(𝐽𝑀)𝐿)))) = (𝑅 Σg (𝑏𝑁 ↦ (𝑏 / 𝑖𝑋 · (𝑏(𝐽𝑀)𝐿))))
185 nfcv 2982 . . . . 5 𝑎if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖))
186 nfcv 2982 . . . . 5 𝑏if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖))
187 nfcv 2982 . . . . 5 𝑗if(𝑎 = 𝐿, 𝑏 / 𝑖𝑋, (𝑎𝑀𝑏))
188 nfv 1908 . . . . . 6 𝑖 𝑎 = 𝐿
189 nfcv 2982 . . . . . 6 𝑖(𝑎𝑀𝑏)
190188, 176, 189nfif 4499 . . . . 5 𝑖if(𝑎 = 𝐿, 𝑏 / 𝑖𝑋, (𝑎𝑀𝑏))
191 eqeq1 2830 . . . . . . 7 (𝑗 = 𝑎 → (𝑗 = 𝐿𝑎 = 𝐿))
192191adantr 481 . . . . . 6 ((𝑗 = 𝑎𝑖 = 𝑏) → (𝑗 = 𝐿𝑎 = 𝐿))
193180adantl 482 . . . . . 6 ((𝑗 = 𝑎𝑖 = 𝑏) → 𝑋 = 𝑏 / 𝑖𝑋)
194 oveq12 7159 . . . . . 6 ((𝑗 = 𝑎𝑖 = 𝑏) → (𝑗𝑀𝑖) = (𝑎𝑀𝑏))
195192, 193, 194ifbieq12d 4497 . . . . 5 ((𝑗 = 𝑎𝑖 = 𝑏) → if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖)) = if(𝑎 = 𝐿, 𝑏 / 𝑖𝑋, (𝑎𝑀𝑏)))
196185, 186, 187, 190, 195cbvmpo 7242 . . . 4 (𝑗𝑁, 𝑖𝑁 ↦ if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖))) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, 𝑏 / 𝑖𝑋, (𝑎𝑀𝑏)))
197 iftrue 4476 . . . . . . . 8 (𝑏𝑁 → if(𝑏𝑁, 𝑏 / 𝑖𝑋, (0g𝑅)) = 𝑏 / 𝑖𝑋)
198197eqcomd 2832 . . . . . . 7 (𝑏𝑁𝑏 / 𝑖𝑋 = if(𝑏𝑁, 𝑏 / 𝑖𝑋, (0g𝑅)))
199198adantl 482 . . . . . 6 ((𝑎𝑁𝑏𝑁) → 𝑏 / 𝑖𝑋 = if(𝑏𝑁, 𝑏 / 𝑖𝑋, (0g𝑅)))
200199ifeq1d 4488 . . . . 5 ((𝑎𝑁𝑏𝑁) → if(𝑎 = 𝐿, 𝑏 / 𝑖𝑋, (𝑎𝑀𝑏)) = if(𝑎 = 𝐿, if(𝑏𝑁, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)))
201200mpoeq3ia 7226 . . . 4 (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, 𝑏 / 𝑖𝑋, (𝑎𝑀𝑏))) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑁, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)))
202196, 201eqtri 2849 . . 3 (𝑗𝑁, 𝑖𝑁 ↦ if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖))) = (𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑁, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏)))
203202fveq2i 6672 . 2 (𝐷‘(𝑗𝑁, 𝑖𝑁 ↦ if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖)))) = (𝐷‘(𝑎𝑁, 𝑏𝑁 ↦ if(𝑎 = 𝐿, if(𝑏𝑁, 𝑏 / 𝑖𝑋, (0g𝑅)), (𝑎𝑀𝑏))))
204174, 184, 2033eqtr4g 2886 1 (𝜑 → (𝑅 Σg (𝑖𝑁 ↦ (𝑋 · (𝑖(𝐽𝑀)𝐿)))) = (𝐷‘(𝑗𝑁, 𝑖𝑁 ↦ if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖)))))