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

Theorem mdetuni0 21230
Description: Lemma for mdetuni 21231. (Contributed by SO, 15-Jul-2018.)
Hypotheses
Ref Expression
mdetuni.a 𝐴 = (𝑁 Mat 𝑅)
mdetuni.b 𝐵 = (Base‘𝐴)
mdetuni.k 𝐾 = (Base‘𝑅)
mdetuni.0g 0 = (0g𝑅)
mdetuni.1r 1 = (1r𝑅)
mdetuni.pg + = (+g𝑅)
mdetuni.tg · = (.r𝑅)
mdetuni.n (𝜑𝑁 ∈ Fin)
mdetuni.r (𝜑𝑅 ∈ Ring)
mdetuni.ff (𝜑𝐷:𝐵𝐾)
mdetuni.al (𝜑 → ∀𝑥𝐵𝑦𝑁𝑧𝑁 ((𝑦𝑧 ∧ ∀𝑤𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷𝑥) = 0 ))
mdetuni.li (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = ((𝐷𝑦) + (𝐷𝑧))))
mdetuni.sc (𝜑 → ∀𝑥𝐵𝑦𝐾𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = (𝑦 · (𝐷𝑧))))
mdetuni.e 𝐸 = (𝑁 maDet 𝑅)
mdetuni.cr (𝜑𝑅 ∈ CRing)
mdetuni.f (𝜑𝐹𝐵)
Assertion
Ref Expression
mdetuni0 (𝜑 → (𝐷𝐹) = ((𝐷‘(1r𝐴)) · (𝐸𝐹)))
Distinct variable groups:   𝜑,𝑥,𝑦,𝑧,𝑤   𝑥,𝐵,𝑦,𝑧,𝑤   𝑥,𝐾,𝑦,𝑧,𝑤   𝑥,𝑁,𝑦,𝑧,𝑤   𝑥,𝐷,𝑦,𝑧,𝑤   𝑥, · ,𝑦,𝑧,𝑤   𝑥, + ,𝑦,𝑧,𝑤   𝑥, 0 ,𝑦,𝑧,𝑤   𝑥, 1 ,𝑦,𝑧,𝑤   𝑥,𝑅,𝑦,𝑧,𝑤   𝑥,𝐴,𝑦,𝑧,𝑤   𝑥,𝐸,𝑦,𝑧,𝑤   𝑥,𝐹,𝑦,𝑧,𝑤

Proof of Theorem mdetuni0
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mdetuni.a . . . . 5 𝐴 = (𝑁 Mat 𝑅)
2 mdetuni.b . . . . 5 𝐵 = (Base‘𝐴)
3 mdetuni.k . . . . 5 𝐾 = (Base‘𝑅)
4 mdetuni.0g . . . . 5 0 = (0g𝑅)
5 mdetuni.1r . . . . 5 1 = (1r𝑅)
6 mdetuni.pg . . . . 5 + = (+g𝑅)
7 mdetuni.tg . . . . 5 · = (.r𝑅)
8 mdetuni.n . . . . 5 (𝜑𝑁 ∈ Fin)
9 mdetuni.r . . . . 5 (𝜑𝑅 ∈ Ring)
10 ringgrp 19299 . . . . . . . . 9 (𝑅 ∈ Ring → 𝑅 ∈ Grp)
119, 10syl 17 . . . . . . . 8 (𝜑𝑅 ∈ Grp)
1211adantr 484 . . . . . . 7 ((𝜑𝑎𝐵) → 𝑅 ∈ Grp)
13 mdetuni.ff . . . . . . . 8 (𝜑𝐷:𝐵𝐾)
1413ffvelrnda 6832 . . . . . . 7 ((𝜑𝑎𝐵) → (𝐷𝑎) ∈ 𝐾)
159adantr 484 . . . . . . . 8 ((𝜑𝑎𝐵) → 𝑅 ∈ Ring)
168, 9jca 515 . . . . . . . . . . 11 (𝜑 → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
171matring 21052 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring)
18 eqid 2801 . . . . . . . . . . . 12 (1r𝐴) = (1r𝐴)
192, 18ringidcl 19318 . . . . . . . . . . 11 (𝐴 ∈ Ring → (1r𝐴) ∈ 𝐵)
2016, 17, 193syl 18 . . . . . . . . . 10 (𝜑 → (1r𝐴) ∈ 𝐵)
2113, 20ffvelrnd 6833 . . . . . . . . 9 (𝜑 → (𝐷‘(1r𝐴)) ∈ 𝐾)
2221adantr 484 . . . . . . . 8 ((𝜑𝑎𝐵) → (𝐷‘(1r𝐴)) ∈ 𝐾)
23 mdetuni.cr . . . . . . . . . 10 (𝜑𝑅 ∈ CRing)
24 mdetuni.e . . . . . . . . . . 11 𝐸 = (𝑁 maDet 𝑅)
2524, 1, 2, 3mdetf 21204 . . . . . . . . . 10 (𝑅 ∈ CRing → 𝐸:𝐵𝐾)
2623, 25syl 17 . . . . . . . . 9 (𝜑𝐸:𝐵𝐾)
2726ffvelrnda 6832 . . . . . . . 8 ((𝜑𝑎𝐵) → (𝐸𝑎) ∈ 𝐾)
283, 7ringcl 19311 . . . . . . . 8 ((𝑅 ∈ Ring ∧ (𝐷‘(1r𝐴)) ∈ 𝐾 ∧ (𝐸𝑎) ∈ 𝐾) → ((𝐷‘(1r𝐴)) · (𝐸𝑎)) ∈ 𝐾)
2915, 22, 27, 28syl3anc 1368 . . . . . . 7 ((𝜑𝑎𝐵) → ((𝐷‘(1r𝐴)) · (𝐸𝑎)) ∈ 𝐾)
30 eqid 2801 . . . . . . . 8 (-g𝑅) = (-g𝑅)
313, 30grpsubcl 18175 . . . . . . 7 ((𝑅 ∈ Grp ∧ (𝐷𝑎) ∈ 𝐾 ∧ ((𝐷‘(1r𝐴)) · (𝐸𝑎)) ∈ 𝐾) → ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))) ∈ 𝐾)
3212, 14, 29, 31syl3anc 1368 . . . . . 6 ((𝜑𝑎𝐵) → ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))) ∈ 𝐾)
3332fmpttd 6860 . . . . 5 (𝜑 → (𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎)))):𝐵𝐾)
34 simpr1 1191 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) → 𝑏𝐵)
35 fveq2 6649 . . . . . . . . . . . 12 (𝑎 = 𝑏 → (𝐷𝑎) = (𝐷𝑏))
36 fveq2 6649 . . . . . . . . . . . . 13 (𝑎 = 𝑏 → (𝐸𝑎) = (𝐸𝑏))
3736oveq2d 7155 . . . . . . . . . . . 12 (𝑎 = 𝑏 → ((𝐷‘(1r𝐴)) · (𝐸𝑎)) = ((𝐷‘(1r𝐴)) · (𝐸𝑏)))
3835, 37oveq12d 7157 . . . . . . . . . . 11 (𝑎 = 𝑏 → ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))) = ((𝐷𝑏)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑏))))
39 eqid 2801 . . . . . . . . . . 11 (𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎)))) = (𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))
40 ovex 7172 . . . . . . . . . . 11 ((𝐷𝑏)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑏))) ∈ V
4138, 39, 40fvmpt 6749 . . . . . . . . . 10 (𝑏𝐵 → ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑏) = ((𝐷𝑏)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑏))))
4234, 41syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) → ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑏) = ((𝐷𝑏)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑏))))
43423adant3 1129 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑏) = ((𝐷𝑏)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑏))))
44 simp1 1133 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝜑)
45 simp21 1203 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑏𝐵)
46 simp3r 1199 . . . . . . . . . . 11 ((𝜑 ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))
47 oveq2 7147 . . . . . . . . . . . . 13 (𝑒 = 𝑤 → (𝑐𝑏𝑒) = (𝑐𝑏𝑤))
48 oveq2 7147 . . . . . . . . . . . . 13 (𝑒 = 𝑤 → (𝑑𝑏𝑒) = (𝑑𝑏𝑤))
4947, 48eqeq12d 2817 . . . . . . . . . . . 12 (𝑒 = 𝑤 → ((𝑐𝑏𝑒) = (𝑑𝑏𝑒) ↔ (𝑐𝑏𝑤) = (𝑑𝑏𝑤)))
5049cbvralvw 3399 . . . . . . . . . . 11 (∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒) ↔ ∀𝑤𝑁 (𝑐𝑏𝑤) = (𝑑𝑏𝑤))
5146, 50sylib 221 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → ∀𝑤𝑁 (𝑐𝑏𝑤) = (𝑑𝑏𝑤))
52 simp22 1204 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑐𝑁)
53 simp23 1205 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑑𝑁)
54 simp3l 1198 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑐𝑑)
55 mdetuni.al . . . . . . . . . . 11 (𝜑 → ∀𝑥𝐵𝑦𝑁𝑧𝑁 ((𝑦𝑧 ∧ ∀𝑤𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷𝑥) = 0 ))
56 mdetuni.li . . . . . . . . . . 11 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = ((𝐷𝑦) + (𝐷𝑧))))
57 mdetuni.sc . . . . . . . . . . 11 (𝜑 → ∀𝑥𝐵𝑦𝐾𝑧𝐵𝑤𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷𝑥) = (𝑦 · (𝐷𝑧))))
581, 2, 3, 4, 5, 6, 7, 8, 9, 13, 55, 56, 57mdetunilem1 21221 . . . . . . . . . 10 (((𝜑𝑏𝐵 ∧ ∀𝑤𝑁 (𝑐𝑏𝑤) = (𝑑𝑏𝑤)) ∧ (𝑐𝑁𝑑𝑁𝑐𝑑)) → (𝐷𝑏) = 0 )
5944, 45, 51, 52, 53, 54, 58syl33anc 1382 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → (𝐷𝑏) = 0 )
60233ad2ant1 1130 . . . . . . . . . . 11 ((𝜑 ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑅 ∈ CRing)
6124, 1, 2, 4, 60, 45, 52, 53, 54, 46mdetralt 21217 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → (𝐸𝑏) = 0 )
6261oveq2d 7155 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → ((𝐷‘(1r𝐴)) · (𝐸𝑏)) = ((𝐷‘(1r𝐴)) · 0 ))
6359, 62oveq12d 7157 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → ((𝐷𝑏)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑏))) = ( 0 (-g𝑅)((𝐷‘(1r𝐴)) · 0 )))
643, 7, 4ringrz 19338 . . . . . . . . . . . 12 ((𝑅 ∈ Ring ∧ (𝐷‘(1r𝐴)) ∈ 𝐾) → ((𝐷‘(1r𝐴)) · 0 ) = 0 )
659, 21, 64syl2anc 587 . . . . . . . . . . 11 (𝜑 → ((𝐷‘(1r𝐴)) · 0 ) = 0 )
6665oveq2d 7155 . . . . . . . . . 10 (𝜑 → ( 0 (-g𝑅)((𝐷‘(1r𝐴)) · 0 )) = ( 0 (-g𝑅) 0 ))
673, 4grpidcl 18127 . . . . . . . . . . 11 (𝑅 ∈ Grp → 0𝐾)
683, 4, 30grpsubid 18179 . . . . . . . . . . 11 ((𝑅 ∈ Grp ∧ 0𝐾) → ( 0 (-g𝑅) 0 ) = 0 )
6911, 67, 68syl2anc2 588 . . . . . . . . . 10 (𝜑 → ( 0 (-g𝑅) 0 ) = 0 )
7066, 69eqtrd 2836 . . . . . . . . 9 (𝜑 → ( 0 (-g𝑅)((𝐷‘(1r𝐴)) · 0 )) = 0 )
71703ad2ant1 1130 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → ( 0 (-g𝑅)((𝐷‘(1r𝐴)) · 0 )) = 0 )
7243, 63, 713eqtrd 2840 . . . . . . 7 ((𝜑 ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑏) = 0 )
73723expia 1118 . . . . . 6 ((𝜑 ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) → ((𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒)) → ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑏) = 0 ))
7473ralrimivvva 3160 . . . . 5 (𝜑 → ∀𝑏𝐵𝑐𝑁𝑑𝑁 ((𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒)) → ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑏) = 0 ))
75 simp1 1133 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f + (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝜑)
76 simp2ll 1237 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f + (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑏𝐵)
77 simp2lr 1238 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f + (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑐𝐵)
78 simp2rl 1239 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f + (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑑𝐵)
79 simp2rr 1240 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f + (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑒𝑁)
80 simp31 1206 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f + (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f + (𝑑 ↾ ({𝑒} × 𝑁))))
81 simp32 1207 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f + (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
82 simp33 1208 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f + (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
831, 2, 3, 4, 5, 6, 7, 8, 9, 13, 55, 56, 57mdetunilem3 21223 . . . . . . . . . . . 12 (((𝜑𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁 ∧ (𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f + (𝑑 ↾ ({𝑒} × 𝑁)))) ∧ ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝐷𝑏) = ((𝐷𝑐) + (𝐷𝑑)))
8475, 76, 77, 78, 79, 80, 81, 82, 83syl332anc 1398 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f + (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝐷𝑏) = ((𝐷𝑐) + (𝐷𝑑)))
85233ad2ant1 1130 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f + (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑅 ∈ CRing)
8624, 1, 2, 6, 85, 76, 77, 78, 79, 80, 81, 82mdetrlin 21211 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f + (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝐸𝑏) = ((𝐸𝑐) + (𝐸𝑑)))
8786oveq2d 7155 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f + (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝐷‘(1r𝐴)) · (𝐸𝑏)) = ((𝐷‘(1r𝐴)) · ((𝐸𝑐) + (𝐸𝑑))))
8884, 87oveq12d 7157 . . . . . . . . . 10 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f + (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝐷𝑏)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑏))) = (((𝐷𝑐) + (𝐷𝑑))(-g𝑅)((𝐷‘(1r𝐴)) · ((𝐸𝑐) + (𝐸𝑑)))))
89 simprll 778 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝑏𝐵)
9089, 41syl 17 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑏) = ((𝐷𝑏)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑏))))
91903adant3 1129 . . . . . . . . . 10 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f + (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑏) = ((𝐷𝑏)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑏))))
92 simprlr 779 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝑐𝐵)
93 fveq2 6649 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑐 → (𝐷𝑎) = (𝐷𝑐))
94 fveq2 6649 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑐 → (𝐸𝑎) = (𝐸𝑐))
9594oveq2d 7155 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑐 → ((𝐷‘(1r𝐴)) · (𝐸𝑎)) = ((𝐷‘(1r𝐴)) · (𝐸𝑐)))
9693, 95oveq12d 7157 . . . . . . . . . . . . . . 15 (𝑎 = 𝑐 → ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))) = ((𝐷𝑐)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑐))))
97 ovex 7172 . . . . . . . . . . . . . . 15 ((𝐷𝑐)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑐))) ∈ V
9896, 39, 97fvmpt 6749 . . . . . . . . . . . . . 14 (𝑐𝐵 → ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑐) = ((𝐷𝑐)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑐))))
9992, 98syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑐) = ((𝐷𝑐)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑐))))
100 simprrl 780 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝑑𝐵)
101 fveq2 6649 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑑 → (𝐷𝑎) = (𝐷𝑑))
102 fveq2 6649 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑑 → (𝐸𝑎) = (𝐸𝑑))
103102oveq2d 7155 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑑 → ((𝐷‘(1r𝐴)) · (𝐸𝑎)) = ((𝐷‘(1r𝐴)) · (𝐸𝑑)))
104101, 103oveq12d 7157 . . . . . . . . . . . . . . 15 (𝑎 = 𝑑 → ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))) = ((𝐷𝑑)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑑))))
105 ovex 7172 . . . . . . . . . . . . . . 15 ((𝐷𝑑)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑑))) ∈ V
106104, 39, 105fvmpt 6749 . . . . . . . . . . . . . 14 (𝑑𝐵 → ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑑) = ((𝐷𝑑)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑑))))
107100, 106syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑑) = ((𝐷𝑑)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑑))))
10899, 107oveq12d 7157 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑐) + ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑑)) = (((𝐷𝑐)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑐))) + ((𝐷𝑑)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑑)))))
109 ringabl 19330 . . . . . . . . . . . . . . 15 (𝑅 ∈ Ring → 𝑅 ∈ Abel)
1109, 109syl 17 . . . . . . . . . . . . . 14 (𝜑𝑅 ∈ Abel)
111110adantr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝑅 ∈ Abel)
11213adantr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝐷:𝐵𝐾)
113112, 92ffvelrnd 6833 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (𝐷𝑐) ∈ 𝐾)
114112, 100ffvelrnd 6833 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (𝐷𝑑) ∈ 𝐾)
1159adantr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝑅 ∈ Ring)
11621adantr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (𝐷‘(1r𝐴)) ∈ 𝐾)
11726adantr 484 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝐸:𝐵𝐾)
118117, 92ffvelrnd 6833 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (𝐸𝑐) ∈ 𝐾)
1193, 7ringcl 19311 . . . . . . . . . . . . . 14 ((𝑅 ∈ Ring ∧ (𝐷‘(1r𝐴)) ∈ 𝐾 ∧ (𝐸𝑐) ∈ 𝐾) → ((𝐷‘(1r𝐴)) · (𝐸𝑐)) ∈ 𝐾)
120115, 116, 118, 119syl3anc 1368 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝐷‘(1r𝐴)) · (𝐸𝑐)) ∈ 𝐾)
121117, 100ffvelrnd 6833 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (𝐸𝑑) ∈ 𝐾)
1223, 7ringcl 19311 . . . . . . . . . . . . . 14 ((𝑅 ∈ Ring ∧ (𝐷‘(1r𝐴)) ∈ 𝐾 ∧ (𝐸𝑑) ∈ 𝐾) → ((𝐷‘(1r𝐴)) · (𝐸𝑑)) ∈ 𝐾)
123115, 116, 121, 122syl3anc 1368 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝐷‘(1r𝐴)) · (𝐸𝑑)) ∈ 𝐾)
1243, 6, 30ablsub4 18930 . . . . . . . . . . . . 13 ((𝑅 ∈ Abel ∧ ((𝐷𝑐) ∈ 𝐾 ∧ (𝐷𝑑) ∈ 𝐾) ∧ (((𝐷‘(1r𝐴)) · (𝐸𝑐)) ∈ 𝐾 ∧ ((𝐷‘(1r𝐴)) · (𝐸𝑑)) ∈ 𝐾)) → (((𝐷𝑐) + (𝐷𝑑))(-g𝑅)(((𝐷‘(1r𝐴)) · (𝐸𝑐)) + ((𝐷‘(1r𝐴)) · (𝐸𝑑)))) = (((𝐷𝑐)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑐))) + ((𝐷𝑑)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑑)))))
125111, 113, 114, 120, 123, 124syl122anc 1376 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (((𝐷𝑐) + (𝐷𝑑))(-g𝑅)(((𝐷‘(1r𝐴)) · (𝐸𝑐)) + ((𝐷‘(1r𝐴)) · (𝐸𝑑)))) = (((𝐷𝑐)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑐))) + ((𝐷𝑑)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑑)))))
1263, 6, 7ringdi 19316 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ ((𝐷‘(1r𝐴)) ∈ 𝐾 ∧ (𝐸𝑐) ∈ 𝐾 ∧ (𝐸𝑑) ∈ 𝐾)) → ((𝐷‘(1r𝐴)) · ((𝐸𝑐) + (𝐸𝑑))) = (((𝐷‘(1r𝐴)) · (𝐸𝑐)) + ((𝐷‘(1r𝐴)) · (𝐸𝑑))))
127115, 116, 118, 121, 126syl13anc 1369 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝐷‘(1r𝐴)) · ((𝐸𝑐) + (𝐸𝑑))) = (((𝐷‘(1r𝐴)) · (𝐸𝑐)) + ((𝐷‘(1r𝐴)) · (𝐸𝑑))))
128127eqcomd 2807 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (((𝐷‘(1r𝐴)) · (𝐸𝑐)) + ((𝐷‘(1r𝐴)) · (𝐸𝑑))) = ((𝐷‘(1r𝐴)) · ((𝐸𝑐) + (𝐸𝑑))))
129128oveq2d 7155 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (((𝐷𝑐) + (𝐷𝑑))(-g𝑅)(((𝐷‘(1r𝐴)) · (𝐸𝑐)) + ((𝐷‘(1r𝐴)) · (𝐸𝑑)))) = (((𝐷𝑐) + (𝐷𝑑))(-g𝑅)((𝐷‘(1r𝐴)) · ((𝐸𝑐) + (𝐸𝑑)))))
130108, 125, 1293eqtr2d 2842 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑐) + ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑑)) = (((𝐷𝑐) + (𝐷𝑑))(-g𝑅)((𝐷‘(1r𝐴)) · ((𝐸𝑐) + (𝐸𝑑)))))
1311303adant3 1129 . . . . . . . . . 10 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f + (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑐) + ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑑)) = (((𝐷𝑐) + (𝐷𝑑))(-g𝑅)((𝐷‘(1r𝐴)) · ((𝐸𝑐) + (𝐸𝑑)))))
13288, 91, 1313eqtr4d 2846 . . . . . . . . 9 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f + (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑏) = (((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑐) + ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑑)))
1331323expia 1118 . . . . . . . 8 ((𝜑 ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f + (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑏) = (((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑐) + ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑑))))
134133anassrs 471 . . . . . . 7 (((𝜑 ∧ (𝑏𝐵𝑐𝐵)) ∧ (𝑑𝐵𝑒𝑁)) → (((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f + (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑏) = (((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑐) + ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑑))))
135134ralrimivva 3159 . . . . . 6 ((𝜑 ∧ (𝑏𝐵𝑐𝐵)) → ∀𝑑𝐵𝑒𝑁 (((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f + (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑏) = (((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑐) + ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑑))))
136135ralrimivva 3159 . . . . 5 (𝜑 → ∀𝑏𝐵𝑐𝐵𝑑𝐵𝑒𝑁 (((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f + (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑏) = (((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑐) + ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑑))))
137 simp1 1133 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝜑)
138 simp2ll 1237 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑏𝐵)
139 simp2lr 1238 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑐𝐾)
140 simp2rl 1239 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑑𝐵)
141 simp2rr 1240 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑒𝑁)
142 simp3l 1198 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))))
143 simp3r 1199 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
1441, 2, 3, 4, 5, 6, 7, 8, 9, 13, 55, 56, 57mdetunilem4 21224 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑏𝐵𝑐𝐾𝑑𝐵) ∧ (𝑒𝑁 ∧ (𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝐷𝑏) = (𝑐 · (𝐷𝑑)))
145137, 138, 139, 140, 141, 142, 143, 144syl133anc 1390 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝐷𝑏) = (𝑐 · (𝐷𝑑)))
146233ad2ant1 1130 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑅 ∈ CRing)
14724, 1, 2, 3, 7, 146, 138, 139, 140, 141, 142, 143mdetrsca 21212 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝐸𝑏) = (𝑐 · (𝐸𝑑)))
148147oveq2d 7155 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝐷‘(1r𝐴)) · (𝐸𝑏)) = ((𝐷‘(1r𝐴)) · (𝑐 · (𝐸𝑑))))
149145, 148oveq12d 7157 . . . . . . . . . 10 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝐷𝑏)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑏))) = ((𝑐 · (𝐷𝑑))(-g𝑅)((𝐷‘(1r𝐴)) · (𝑐 · (𝐸𝑑)))))
150 simprll 778 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁))) → 𝑏𝐵)
151150, 41syl 17 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑏) = ((𝐷𝑏)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑏))))
1521513adant3 1129 . . . . . . . . . 10 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑏) = ((𝐷𝑏)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑏))))
153 simprrl 780 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁))) → 𝑑𝐵)
154153, 106syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑑) = ((𝐷𝑑)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑑))))
155154oveq2d 7155 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁))) → (𝑐 · ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑑)) = (𝑐 · ((𝐷𝑑)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑑)))))
1569adantr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁))) → 𝑅 ∈ Ring)
157 simprlr 779 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁))) → 𝑐𝐾)
15813adantr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁))) → 𝐷:𝐵𝐾)
159158, 153ffvelrnd 6833 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁))) → (𝐷𝑑) ∈ 𝐾)
16021adantr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁))) → (𝐷‘(1r𝐴)) ∈ 𝐾)
16126adantr 484 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁))) → 𝐸:𝐵𝐾)
162161, 153ffvelrnd 6833 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁))) → (𝐸𝑑) ∈ 𝐾)
163156, 160, 162, 122syl3anc 1368 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁))) → ((𝐷‘(1r𝐴)) · (𝐸𝑑)) ∈ 𝐾)
1643, 7, 30, 156, 157, 159, 163ringsubdi 19349 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁))) → (𝑐 · ((𝐷𝑑)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑑)))) = ((𝑐 · (𝐷𝑑))(-g𝑅)(𝑐 · ((𝐷‘(1r𝐴)) · (𝐸𝑑)))))
165 eqid 2801 . . . . . . . . . . . . . . . . 17 (mulGrp‘𝑅) = (mulGrp‘𝑅)
166165crngmgp 19302 . . . . . . . . . . . . . . . 16 (𝑅 ∈ CRing → (mulGrp‘𝑅) ∈ CMnd)
16723, 166syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (mulGrp‘𝑅) ∈ CMnd)
168167adantr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁))) → (mulGrp‘𝑅) ∈ CMnd)
169165, 3mgpbas 19242 . . . . . . . . . . . . . . 15 𝐾 = (Base‘(mulGrp‘𝑅))
170165, 7mgpplusg 19240 . . . . . . . . . . . . . . 15 · = (+g‘(mulGrp‘𝑅))
171169, 170cmn12 18923 . . . . . . . . . . . . . 14 (((mulGrp‘𝑅) ∈ CMnd ∧ (𝑐𝐾 ∧ (𝐷‘(1r𝐴)) ∈ 𝐾 ∧ (𝐸𝑑) ∈ 𝐾)) → (𝑐 · ((𝐷‘(1r𝐴)) · (𝐸𝑑))) = ((𝐷‘(1r𝐴)) · (𝑐 · (𝐸𝑑))))
172168, 157, 160, 162, 171syl13anc 1369 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁))) → (𝑐 · ((𝐷‘(1r𝐴)) · (𝐸𝑑))) = ((𝐷‘(1r𝐴)) · (𝑐 · (𝐸𝑑))))
173172oveq2d 7155 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑐 · (𝐷𝑑))(-g𝑅)(𝑐 · ((𝐷‘(1r𝐴)) · (𝐸𝑑)))) = ((𝑐 · (𝐷𝑑))(-g𝑅)((𝐷‘(1r𝐴)) · (𝑐 · (𝐸𝑑)))))
174155, 164, 1733eqtrd 2840 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁))) → (𝑐 · ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑑)) = ((𝑐 · (𝐷𝑑))(-g𝑅)((𝐷‘(1r𝐴)) · (𝑐 · (𝐸𝑑)))))
1751743adant3 1129 . . . . . . . . . 10 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑐 · ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑑)) = ((𝑐 · (𝐷𝑑))(-g𝑅)((𝐷‘(1r𝐴)) · (𝑐 · (𝐸𝑑)))))
176149, 152, 1753eqtr4d 2846 . . . . . . . . 9 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑏) = (𝑐 · ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑑)))
1771763expia 1118 . . . . . . . 8 ((𝜑 ∧ ((𝑏𝐵𝑐𝐾) ∧ (𝑑𝐵𝑒𝑁))) → (((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑏) = (𝑐 · ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑑))))
178177anassrs 471 . . . . . . 7 (((𝜑 ∧ (𝑏𝐵𝑐𝐾)) ∧ (𝑑𝐵𝑒𝑁)) → (((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑏) = (𝑐 · ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑑))))
179178ralrimivva 3159 . . . . . 6 ((𝜑 ∧ (𝑏𝐵𝑐𝐾)) → ∀𝑑𝐵𝑒𝑁 (((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑏) = (𝑐 · ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑑))))
180179ralrimivva 3159 . . . . 5 (𝜑 → ∀𝑏𝐵𝑐𝐾𝑑𝐵𝑒𝑁 (((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑏) = (𝑐 · ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑑))))
181 eqidd 2802 . . . . . 6 (𝜑 → (𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎)))) = (𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎)))))
182 fveq2 6649 . . . . . . . 8 (𝑎 = (1r𝐴) → (𝐷𝑎) = (𝐷‘(1r𝐴)))
183 fveq2 6649 . . . . . . . . 9 (𝑎 = (1r𝐴) → (𝐸𝑎) = (𝐸‘(1r𝐴)))
184183oveq2d 7155 . . . . . . . 8 (𝑎 = (1r𝐴) → ((𝐷‘(1r𝐴)) · (𝐸𝑎)) = ((𝐷‘(1r𝐴)) · (𝐸‘(1r𝐴))))
185182, 184oveq12d 7157 . . . . . . 7 (𝑎 = (1r𝐴) → ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))) = ((𝐷‘(1r𝐴))(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸‘(1r𝐴)))))
18624, 1, 18, 5mdet1 21210 . . . . . . . . . . . 12 ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) → (𝐸‘(1r𝐴)) = 1 )
18723, 8, 186syl2anc 587 . . . . . . . . . . 11 (𝜑 → (𝐸‘(1r𝐴)) = 1 )
188187oveq2d 7155 . . . . . . . . . 10 (𝜑 → ((𝐷‘(1r𝐴)) · (𝐸‘(1r𝐴))) = ((𝐷‘(1r𝐴)) · 1 ))
1893, 7, 5ringridm 19322 . . . . . . . . . . 11 ((𝑅 ∈ Ring ∧ (𝐷‘(1r𝐴)) ∈ 𝐾) → ((𝐷‘(1r𝐴)) · 1 ) = (𝐷‘(1r𝐴)))
1909, 21, 189syl2anc 587 . . . . . . . . . 10 (𝜑 → ((𝐷‘(1r𝐴)) · 1 ) = (𝐷‘(1r𝐴)))
191188, 190eqtrd 2836 . . . . . . . . 9 (𝜑 → ((𝐷‘(1r𝐴)) · (𝐸‘(1r𝐴))) = (𝐷‘(1r𝐴)))
192191oveq2d 7155 . . . . . . . 8 (𝜑 → ((𝐷‘(1r𝐴))(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸‘(1r𝐴)))) = ((𝐷‘(1r𝐴))(-g𝑅)(𝐷‘(1r𝐴))))
1933, 4, 30grpsubid 18179 . . . . . . . . 9 ((𝑅 ∈ Grp ∧ (𝐷‘(1r𝐴)) ∈ 𝐾) → ((𝐷‘(1r𝐴))(-g𝑅)(𝐷‘(1r𝐴))) = 0 )
19411, 21, 193syl2anc 587 . . . . . . . 8 (𝜑 → ((𝐷‘(1r𝐴))(-g𝑅)(𝐷‘(1r𝐴))) = 0 )
195192, 194eqtrd 2836 . . . . . . 7 (𝜑 → ((𝐷‘(1r𝐴))(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸‘(1r𝐴)))) = 0 )
196185, 195sylan9eqr 2858 . . . . . 6 ((𝜑𝑎 = (1r𝐴)) → ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))) = 0 )
1974fvexi 6663 . . . . . . 7 0 ∈ V
198197a1i 11 . . . . . 6 (𝜑0 ∈ V)
199181, 196, 20, 198fvmptd 6756 . . . . 5 (𝜑 → ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘(1r𝐴)) = 0 )
200 eqid 2801 . . . . 5 {𝑏 ∣ ∀𝑐𝐵𝑑 ∈ (𝑁m 𝑁)(∀𝑒𝑏 (𝑐𝑒) = if(𝑒𝑑, 1 , 0 ) → ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑐) = 0 )} = {𝑏 ∣ ∀𝑐𝐵𝑑 ∈ (𝑁m 𝑁)(∀𝑒𝑏 (𝑐𝑒) = if(𝑒𝑑, 1 , 0 ) → ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝑐) = 0 )}
2011, 2, 3, 4, 5, 6, 7, 8, 9, 33, 74, 136, 180, 199, 200mdetunilem9 21229 . . . 4 (𝜑 → (𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎)))) = (𝐵 × { 0 }))
202201fveq1d 6651 . . 3 (𝜑 → ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝐹) = ((𝐵 × { 0 })‘𝐹))
203 fveq2 6649 . . . . . 6 (𝑎 = 𝐹 → (𝐷𝑎) = (𝐷𝐹))
204 fveq2 6649 . . . . . . 7 (𝑎 = 𝐹 → (𝐸𝑎) = (𝐸𝐹))
205204oveq2d 7155 . . . . . 6 (𝑎 = 𝐹 → ((𝐷‘(1r𝐴)) · (𝐸𝑎)) = ((𝐷‘(1r𝐴)) · (𝐸𝐹)))
206203, 205oveq12d 7157 . . . . 5 (𝑎 = 𝐹 → ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))) = ((𝐷𝐹)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝐹))))
207206adantl 485 . . . 4 ((𝜑𝑎 = 𝐹) → ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))) = ((𝐷𝐹)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝐹))))
208 mdetuni.f . . . 4 (𝜑𝐹𝐵)
209 ovexd 7174 . . . 4 (𝜑 → ((𝐷𝐹)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝐹))) ∈ V)
210181, 207, 208, 209fvmptd 6756 . . 3 (𝜑 → ((𝑎𝐵 ↦ ((𝐷𝑎)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝑎))))‘𝐹) = ((𝐷𝐹)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝐹))))
211197fvconst2 6947 . . . 4 (𝐹𝐵 → ((𝐵 × { 0 })‘𝐹) = 0 )
212208, 211syl 17 . . 3 (𝜑 → ((𝐵 × { 0 })‘𝐹) = 0 )
213202, 210, 2123eqtr3d 2844 . 2 (𝜑 → ((𝐷𝐹)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝐹))) = 0 )
21413, 208ffvelrnd 6833 . . 3 (𝜑 → (𝐷𝐹) ∈ 𝐾)
21526, 208ffvelrnd 6833 . . . 4 (𝜑 → (𝐸𝐹) ∈ 𝐾)
2163, 7ringcl 19311 . . . 4 ((𝑅 ∈ Ring ∧ (𝐷‘(1r𝐴)) ∈ 𝐾 ∧ (𝐸𝐹) ∈ 𝐾) → ((𝐷‘(1r𝐴)) · (𝐸𝐹)) ∈ 𝐾)
2179, 21, 215, 216syl3anc 1368 . . 3 (𝜑 → ((𝐷‘(1r𝐴)) · (𝐸𝐹)) ∈ 𝐾)
2183, 4, 30grpsubeq0 18181 . . 3 ((𝑅 ∈ Grp ∧ (𝐷𝐹) ∈ 𝐾 ∧ ((𝐷‘(1r𝐴)) · (𝐸𝐹)) ∈ 𝐾) → (((𝐷𝐹)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝐹))) = 0 ↔ (𝐷𝐹) = ((𝐷‘(1r𝐴)) · (𝐸𝐹))))
21911, 214, 217, 218syl3anc 1368 . 2 (𝜑 → (((𝐷𝐹)(-g𝑅)((𝐷‘(1r𝐴)) · (𝐸𝐹))) = 0 ↔ (𝐷𝐹) = ((𝐷‘(1r𝐴)) · (𝐸𝐹))))
220213, 219mpbid 235 1 (𝜑 → (𝐷𝐹) = ((𝐷‘(1r𝐴)) · (𝐸𝐹)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2112  {cab 2779  wne 2990  wral 3109  Vcvv 3444  cdif 3881  ifcif 4428  {csn 4528  cmpt 5113   × cxp 5521  cres 5525  wf 6324  cfv 6328  (class class class)co 7139  f cof 7391  m cmap 8393  Fincfn 8496  Basecbs 16479  +gcplusg 16561  .rcmulr 16562  0gc0g 16709  Grpcgrp 18099  -gcsg 18101  CMndccmn 18902  Abelcabl 18903  mulGrpcmgp 19236  1rcur 19248  Ringcrg 19294  CRingccrg 19295   Mat cmat 21016   maDet cmdat 21193
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607  ax-addf 10609  ax-mulf 10610
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-xor 1503  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-ot 4537  df-uni 4804  df-int 4842  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-of 7393  df-om 7565  df-1st 7675  df-2nd 7676  df-supp 7818  df-tpos 7879  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-2o 8090  df-oadd 8093  df-er 8276  df-map 8395  df-pm 8396  df-ixp 8449  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fsupp 8822  df-sup 8894  df-oi 8962  df-card 9356  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-div 11291  df-nn 11630  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-xnn0 11960  df-z 11974  df-dec 12091  df-uz 12236  df-rp 12382  df-fz 12890  df-fzo 13033  df-seq 13369  df-exp 13430  df-hash 13691  df-word 13862  df-lsw 13910  df-concat 13918  df-s1 13945  df-substr 13998  df-pfx 14028  df-splice 14107  df-reverse 14116  df-s2 14205  df-struct 16481  df-ndx 16482  df-slot 16483  df-base 16485  df-sets 16486  df-ress 16487  df-plusg 16574  df-mulr 16575  df-starv 16576  df-sca 16577  df-vsca 16578  df-ip 16579  df-tset 16580  df-ple 16581  df-ds 16583  df-unif 16584  df-hom 16585  df-cco 16586  df-0g 16711  df-gsum 16712  df-prds 16717  df-pws 16719  df-mre 16853  df-mrc 16854  df-acs 16856  df-mgm 17848  df-sgrp 17897  df-mnd 17908  df-mhm 17952  df-submnd 17953  df-efmnd 18030  df-grp 18102  df-minusg 18103  df-sbg 18104  df-mulg 18221  df-subg 18272  df-ghm 18352  df-gim 18395  df-cntz 18443  df-oppg 18470  df-symg 18492  df-pmtr 18566  df-psgn 18615  df-evpm 18616  df-cmn 18904  df-abl 18905  df-mgp 19237  df-ur 19249  df-srg 19253  df-ring 19296  df-cring 19297  df-oppr 19373  df-dvdsr 19391  df-unit 19392  df-invr 19422  df-dvr 19433  df-rnghom 19467  df-drng 19501  df-subrg 19530  df-lmod 19633  df-lss 19701  df-sra 19941  df-rgmod 19942  df-cnfld 20096  df-zring 20168  df-zrh 20201  df-dsmm 20425  df-frlm 20440  df-mamu 20995  df-mat 21017  df-mdet 21194
This theorem is referenced by:  mdetuni  21231  mdetmul  21232
  Copyright terms: Public domain W3C validator