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

Theorem mdetmul 20552
Description: Multiplicativity of the determinant function: the determinant of a matrix product of square matrices equals the product of their determinants. Proposition 4.15 in [Lang] p. 517. (Contributed by Stefan O'Rear, 16-Jul-2018.)
Hypotheses
Ref Expression
mdetmul.a 𝐴 = (𝑁 Mat 𝑅)
mdetmul.b 𝐵 = (Base‘𝐴)
mdetmul.d 𝐷 = (𝑁 maDet 𝑅)
mdetmul.t1 · = (.r𝑅)
mdetmul.t2 = (.r𝐴)
Assertion
Ref Expression
mdetmul ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → (𝐷‘(𝐹 𝐺)) = ((𝐷𝐹) · (𝐷𝐺)))

Proof of Theorem mdetmul
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mdetmul.a . . 3 𝐴 = (𝑁 Mat 𝑅)
2 mdetmul.b . . 3 𝐵 = (Base‘𝐴)
3 eqid 2724 . . 3 (Base‘𝑅) = (Base‘𝑅)
4 eqid 2724 . . 3 (0g𝑅) = (0g𝑅)
5 eqid 2724 . . 3 (1r𝑅) = (1r𝑅)
6 eqid 2724 . . 3 (+g𝑅) = (+g𝑅)
7 mdetmul.t1 . . 3 · = (.r𝑅)
81, 2matrcl 20341 . . . . 5 (𝐹𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
98simpld 477 . . . 4 (𝐹𝐵𝑁 ∈ Fin)
1093ad2ant2 1126 . . 3 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → 𝑁 ∈ Fin)
11 crngring 18679 . . . 4 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
12113ad2ant1 1125 . . 3 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → 𝑅 ∈ Ring)
13 mdetmul.d . . . . . . . 8 𝐷 = (𝑁 maDet 𝑅)
1413, 1, 2, 3mdetf 20524 . . . . . . 7 (𝑅 ∈ CRing → 𝐷:𝐵⟶(Base‘𝑅))
15143ad2ant1 1125 . . . . . 6 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → 𝐷:𝐵⟶(Base‘𝑅))
1615adantr 472 . . . . 5 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ 𝑎𝐵) → 𝐷:𝐵⟶(Base‘𝑅))
171matring 20372 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring)
1810, 12, 17syl2anc 696 . . . . . . 7 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → 𝐴 ∈ Ring)
1918adantr 472 . . . . . 6 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ 𝑎𝐵) → 𝐴 ∈ Ring)
20 simpr 479 . . . . . 6 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ 𝑎𝐵) → 𝑎𝐵)
21 simpl3 1208 . . . . . 6 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ 𝑎𝐵) → 𝐺𝐵)
22 mdetmul.t2 . . . . . . 7 = (.r𝐴)
232, 22ringcl 18682 . . . . . 6 ((𝐴 ∈ Ring ∧ 𝑎𝐵𝐺𝐵) → (𝑎 𝐺) ∈ 𝐵)
2419, 20, 21, 23syl3anc 1439 . . . . 5 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ 𝑎𝐵) → (𝑎 𝐺) ∈ 𝐵)
2516, 24ffvelrnd 6475 . . . 4 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ 𝑎𝐵) → (𝐷‘(𝑎 𝐺)) ∈ (Base‘𝑅))
26 eqid 2724 . . . 4 (𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺))) = (𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))
2725, 26fmptd 6500 . . 3 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → (𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺))):𝐵⟶(Base‘𝑅))
28 simp21 1225 . . . . . . 7 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑏𝐵)
29 oveq1 6772 . . . . . . . . 9 (𝑎 = 𝑏 → (𝑎 𝐺) = (𝑏 𝐺))
3029fveq2d 6308 . . . . . . . 8 (𝑎 = 𝑏 → (𝐷‘(𝑎 𝐺)) = (𝐷‘(𝑏 𝐺)))
31 fvex 6314 . . . . . . . 8 (𝐷‘(𝑏 𝐺)) ∈ V
3230, 26, 31fvmpt 6396 . . . . . . 7 (𝑏𝐵 → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (𝐷‘(𝑏 𝐺)))
3328, 32syl 17 . . . . . 6 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (𝐷‘(𝑏 𝐺)))
34 simp11 1222 . . . . . . 7 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑅 ∈ CRing)
3518adantr 472 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) → 𝐴 ∈ Ring)
36 simpr1 1210 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) → 𝑏𝐵)
37 simpl3 1208 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) → 𝐺𝐵)
382, 22ringcl 18682 . . . . . . . . 9 ((𝐴 ∈ Ring ∧ 𝑏𝐵𝐺𝐵) → (𝑏 𝐺) ∈ 𝐵)
3935, 36, 37, 38syl3anc 1439 . . . . . . . 8 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) → (𝑏 𝐺) ∈ 𝐵)
40393adant3 1124 . . . . . . 7 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → (𝑏 𝐺) ∈ 𝐵)
41 simp22 1226 . . . . . . 7 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑐𝑁)
42 simp23 1227 . . . . . . 7 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑑𝑁)
43 simp3l 1220 . . . . . . 7 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑐𝑑)
44 simpl3r 1265 . . . . . . . . . 10 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) ∧ 𝑎𝑁) → ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))
45 eqid 2724 . . . . . . . . . . . 12 𝑁 = 𝑁
46 oveq1 6772 . . . . . . . . . . . . 13 ((𝑐𝑏𝑒) = (𝑑𝑏𝑒) → ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)) = ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))
4746ralimi 3054 . . . . . . . . . . . 12 (∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒) → ∀𝑒𝑁 ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)) = ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))
48 mpteq12 4844 . . . . . . . . . . . 12 ((𝑁 = 𝑁 ∧ ∀𝑒𝑁 ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)) = ((𝑑𝑏𝑒) · (𝑒𝐺𝑎))) → (𝑒𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎))) = (𝑒𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎))))
4945, 47, 48sylancr 698 . . . . . . . . . . 11 (∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒) → (𝑒𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎))) = (𝑒𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎))))
5049oveq2d 6781 . . . . . . . . . 10 (∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒) → (𝑅 Σg (𝑒𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)))) = (𝑅 Σg (𝑒𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))))
5144, 50syl 17 . . . . . . . . 9 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) ∧ 𝑎𝑁) → (𝑅 Σg (𝑒𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)))) = (𝑅 Σg (𝑒𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))))
52 simp1 1128 . . . . . . . . . . . . . . 15 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → 𝑅 ∈ CRing)
53 eqid 2724 . . . . . . . . . . . . . . . . 17 (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)
541, 53matmulr 20367 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (.r𝐴))
5554, 22syl6eqr 2776 . . . . . . . . . . . . . . 15 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = )
5610, 52, 55syl2anc 696 . . . . . . . . . . . . . 14 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = )
5756ad2antrr 764 . . . . . . . . . . . . 13 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = )
5857oveqd 6782 . . . . . . . . . . . 12 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → (𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) = (𝑏 𝐺))
5958oveqd 6782 . . . . . . . . . . 11 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → (𝑐(𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺)𝑎) = (𝑐(𝑏 𝐺)𝑎))
60 simpll1 1231 . . . . . . . . . . . 12 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → 𝑅 ∈ CRing)
6110ad2antrr 764 . . . . . . . . . . . 12 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → 𝑁 ∈ Fin)
62 simplr1 1237 . . . . . . . . . . . . 13 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → 𝑏𝐵)
631, 3, 2matbas2i 20351 . . . . . . . . . . . . 13 (𝑏𝐵𝑏 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
6462, 63syl 17 . . . . . . . . . . . 12 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → 𝑏 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
651, 3, 2matbas2i 20351 . . . . . . . . . . . . . 14 (𝐺𝐵𝐺 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
66653ad2ant3 1127 . . . . . . . . . . . . 13 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → 𝐺 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
6766ad2antrr 764 . . . . . . . . . . . 12 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → 𝐺 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
68 simplr2 1239 . . . . . . . . . . . 12 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → 𝑐𝑁)
69 simpr 479 . . . . . . . . . . . 12 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → 𝑎𝑁)
7053, 3, 7, 60, 61, 61, 61, 64, 67, 68, 69mamufv 20316 . . . . . . . . . . 11 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → (𝑐(𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺)𝑎) = (𝑅 Σg (𝑒𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)))))
7159, 70eqtr3d 2760 . . . . . . . . . 10 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → (𝑐(𝑏 𝐺)𝑎) = (𝑅 Σg (𝑒𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)))))
72713adantl3 1154 . . . . . . . . 9 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) ∧ 𝑎𝑁) → (𝑐(𝑏 𝐺)𝑎) = (𝑅 Σg (𝑒𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)))))
7358oveqd 6782 . . . . . . . . . . 11 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → (𝑑(𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺)𝑎) = (𝑑(𝑏 𝐺)𝑎))
74 simplr3 1241 . . . . . . . . . . . 12 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → 𝑑𝑁)
7553, 3, 7, 60, 61, 61, 61, 64, 67, 74, 69mamufv 20316 . . . . . . . . . . 11 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → (𝑑(𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺)𝑎) = (𝑅 Σg (𝑒𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))))
7673, 75eqtr3d 2760 . . . . . . . . . 10 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → (𝑑(𝑏 𝐺)𝑎) = (𝑅 Σg (𝑒𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))))
77763adantl3 1154 . . . . . . . . 9 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) ∧ 𝑎𝑁) → (𝑑(𝑏 𝐺)𝑎) = (𝑅 Σg (𝑒𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))))
7851, 72, 773eqtr4d 2768 . . . . . . . 8 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) ∧ 𝑎𝑁) → (𝑐(𝑏 𝐺)𝑎) = (𝑑(𝑏 𝐺)𝑎))
7978ralrimiva 3068 . . . . . . 7 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → ∀𝑎𝑁 (𝑐(𝑏 𝐺)𝑎) = (𝑑(𝑏 𝐺)𝑎))
8013, 1, 2, 4, 34, 40, 41, 42, 43, 79mdetralt 20537 . . . . . 6 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → (𝐷‘(𝑏 𝐺)) = (0g𝑅))
8133, 80eqtrd 2758 . . . . 5 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (0g𝑅))
82813expia 1114 . . . 4 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) → ((𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒)) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (0g𝑅)))
8382ralrimivvva 3074 . . 3 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → ∀𝑏𝐵𝑐𝑁𝑑𝑁 ((𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒)) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (0g𝑅)))
84 simp11 1222 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑅 ∈ CRing)
8518adantr 472 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝐴 ∈ Ring)
86 simprll 821 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝑏𝐵)
87 simpl3 1208 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝐺𝐵)
8885, 86, 87, 38syl3anc 1439 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (𝑏 𝐺) ∈ 𝐵)
89883adant3 1124 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 𝐺) ∈ 𝐵)
90 simprlr 822 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝑐𝐵)
912, 22ringcl 18682 . . . . . . . . . . 11 ((𝐴 ∈ Ring ∧ 𝑐𝐵𝐺𝐵) → (𝑐 𝐺) ∈ 𝐵)
9285, 90, 87, 91syl3anc 1439 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (𝑐 𝐺) ∈ 𝐵)
93923adant3 1124 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑐 𝐺) ∈ 𝐵)
94 simprrl 823 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝑑𝐵)
952, 22ringcl 18682 . . . . . . . . . . 11 ((𝐴 ∈ Ring ∧ 𝑑𝐵𝐺𝐵) → (𝑑 𝐺) ∈ 𝐵)
9685, 94, 87, 95syl3anc 1439 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (𝑑 𝐺) ∈ 𝐵)
97963adant3 1124 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑑 𝐺) ∈ 𝐵)
98 simp2rr 1280 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑒𝑁)
99 simp31 1228 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))))
10099oveq1d 6780 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) = (((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
10112adantr 472 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝑅 ∈ Ring)
102 eqid 2724 . . . . . . . . . . . . 13 (𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩) = (𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)
103 snfi 8154 . . . . . . . . . . . . . 14 {𝑒} ∈ Fin
104103a1i 11 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → {𝑒} ∈ Fin)
10510adantr 472 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝑁 ∈ Fin)
1061, 3, 2matbas2i 20351 . . . . . . . . . . . . . . 15 (𝑐𝐵𝑐 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
10790, 106syl 17 . . . . . . . . . . . . . 14 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝑐 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
108 simprrr 824 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝑒𝑁)
109108snssd 4448 . . . . . . . . . . . . . . 15 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → {𝑒} ⊆ 𝑁)
110 xpss1 5236 . . . . . . . . . . . . . . 15 ({𝑒} ⊆ 𝑁 → ({𝑒} × 𝑁) ⊆ (𝑁 × 𝑁))
111109, 110syl 17 . . . . . . . . . . . . . 14 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ({𝑒} × 𝑁) ⊆ (𝑁 × 𝑁))
112 elmapssres 7999 . . . . . . . . . . . . . 14 ((𝑐 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)) ∧ ({𝑒} × 𝑁) ⊆ (𝑁 × 𝑁)) → (𝑐 ↾ ({𝑒} × 𝑁)) ∈ ((Base‘𝑅) ↑𝑚 ({𝑒} × 𝑁)))
113107, 111, 112syl2anc 696 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (𝑐 ↾ ({𝑒} × 𝑁)) ∈ ((Base‘𝑅) ↑𝑚 ({𝑒} × 𝑁)))
1141, 3, 2matbas2i 20351 . . . . . . . . . . . . . . 15 (𝑑𝐵𝑑 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
11594, 114syl 17 . . . . . . . . . . . . . 14 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝑑 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
116 elmapssres 7999 . . . . . . . . . . . . . 14 ((𝑑 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)) ∧ ({𝑒} × 𝑁) ⊆ (𝑁 × 𝑁)) → (𝑑 ↾ ({𝑒} × 𝑁)) ∈ ((Base‘𝑅) ↑𝑚 ({𝑒} × 𝑁)))
117115, 111, 116syl2anc 696 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (𝑑 ↾ ({𝑒} × 𝑁)) ∈ ((Base‘𝑅) ↑𝑚 ({𝑒} × 𝑁)))
11866adantr 472 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝐺 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
1193, 101, 102, 104, 105, 105, 6, 113, 117, 118mamudi 20332 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) = (((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) ∘𝑓 (+g𝑅)((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
1201193adant3 1124 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) = (((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) ∘𝑓 (+g𝑅)((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
121100, 120eqtrd 2758 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) = (((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) ∘𝑓 (+g𝑅)((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
12256adantr 472 . . . . . . . . . . . . . 14 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = )
123122oveqd 6782 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) = (𝑏 𝐺))
124123reseq1d 5502 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 𝐺) ↾ ({𝑒} × 𝑁)))
125 simpl1 1204 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝑅 ∈ CRing)
12686, 63syl 17 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝑏 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
12753, 102, 3, 125, 105, 105, 105, 109, 126, 118mamures 20319 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
128124, 127eqtr3d 2760 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑏 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
1291283adant3 1124 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
130122oveqd 6782 . . . . . . . . . . . . . 14 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (𝑐(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) = (𝑐 𝐺))
131130reseq1d 5502 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑐(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑐 𝐺) ↾ ({𝑒} × 𝑁)))
13253, 102, 3, 125, 105, 105, 105, 109, 107, 118mamures 20319 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑐(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
133131, 132eqtr3d 2760 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑐 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
134122oveqd 6782 . . . . . . . . . . . . . 14 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) = (𝑑 𝐺))
135134reseq1d 5502 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 𝐺) ↾ ({𝑒} × 𝑁)))
13653, 102, 3, 125, 105, 105, 105, 109, 115, 118mamures 20319 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
137135, 136eqtr3d 2760 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑑 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
138133, 137oveq12d 6783 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (((𝑐 𝐺) ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)((𝑑 𝐺) ↾ ({𝑒} × 𝑁))) = (((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) ∘𝑓 (+g𝑅)((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
1391383adant3 1124 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (((𝑐 𝐺) ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)((𝑑 𝐺) ↾ ({𝑒} × 𝑁))) = (((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) ∘𝑓 (+g𝑅)((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
140121, 129, 1393eqtr4d 2768 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 𝐺) ↾ ({𝑒} × 𝑁)) = (((𝑐 𝐺) ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)((𝑑 𝐺) ↾ ({𝑒} × 𝑁))))
141 simp32 1229 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
142141oveq1d 6780 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺) = ((𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
143123reseq1d 5502 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
144 eqid 2724 . . . . . . . . . . . . 13 (𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩) = (𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)
145 difssd 3846 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (𝑁 ∖ {𝑒}) ⊆ 𝑁)
14653, 144, 3, 125, 105, 105, 105, 145, 126, 118mamures 20319 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
147143, 146eqtr3d 2760 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑏 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
1481473adant3 1124 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
149130reseq1d 5502 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑐(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑐 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
15053, 144, 3, 125, 105, 105, 105, 145, 107, 118mamures 20319 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑐(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
151149, 150eqtr3d 2760 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑐 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
1521513adant3 1124 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑐 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
153142, 148, 1523eqtr4d 2768 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑐 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
154 simp33 1230 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
155154oveq1d 6780 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
156134reseq1d 5502 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
15753, 144, 3, 125, 105, 105, 105, 145, 115, 118mamures 20319 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
158156, 157eqtr3d 2760 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑑 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
1591583adant3 1124 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑑 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
160155, 148, 1593eqtr4d 2768 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
16113, 1, 2, 6, 84, 89, 93, 97, 98, 140, 153, 160mdetrlin 20531 . . . . . . . 8 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝐷‘(𝑏 𝐺)) = ((𝐷‘(𝑐 𝐺))(+g𝑅)(𝐷‘(𝑑 𝐺))))
16286, 32syl 17 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (𝐷‘(𝑏 𝐺)))
1631623adant3 1124 . . . . . . . 8 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (𝐷‘(𝑏 𝐺)))
164 oveq1 6772 . . . . . . . . . . . . 13 (𝑎 = 𝑐 → (𝑎 𝐺) = (𝑐 𝐺))
165164fveq2d 6308 . . . . . . . . . . . 12 (𝑎 = 𝑐 → (𝐷‘(𝑎 𝐺)) = (𝐷‘(𝑐 𝐺)))
166 fvex 6314 . . . . . . . . . . . 12 (𝐷‘(𝑐 𝐺)) ∈ V
167165, 26, 166fvmpt 6396 . . . . . . . . . . 11 (𝑐𝐵 → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑐) = (𝐷‘(𝑐 𝐺)))
16890, 167syl 17 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑐) = (𝐷‘(𝑐 𝐺)))
169 oveq1 6772 . . . . . . . . . . . . 13 (𝑎 = 𝑑 → (𝑎 𝐺) = (𝑑 𝐺))
170169fveq2d 6308 . . . . . . . . . . . 12 (𝑎 = 𝑑 → (𝐷‘(𝑎 𝐺)) = (𝐷‘(𝑑 𝐺)))
171 fvex 6314 . . . . . . . . . . . 12 (𝐷‘(𝑑 𝐺)) ∈ V
172170, 26, 171fvmpt 6396 . . . . . . . . . . 11 (𝑑𝐵 → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑) = (𝐷‘(𝑑 𝐺)))
17394, 172syl 17 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑) = (𝐷‘(𝑑 𝐺)))
174168, 173oveq12d 6783 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑐)(+g𝑅)((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑)) = ((𝐷‘(𝑐 𝐺))(+g𝑅)(𝐷‘(𝑑 𝐺))))
1751743adant3 1124 . . . . . . . 8 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑐)(+g𝑅)((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑)) = ((𝐷‘(𝑐 𝐺))(+g𝑅)(𝐷‘(𝑑 𝐺))))
176161, 163, 1753eqtr4d 2768 . . . . . . 7 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑐)(+g𝑅)((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑)))
1771763expia 1114 . . . . . 6 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑐)(+g𝑅)((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑))))
178177anassrs 683 . . . . 5 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝐵)) ∧ (𝑑𝐵𝑒𝑁)) → (((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑐)(+g𝑅)((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑))))
179178ralrimivva 3073 . . . 4 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝐵)) → ∀𝑑𝐵𝑒𝑁 (((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑐)(+g𝑅)((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑))))
180179ralrimivva 3073 . . 3 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → ∀𝑏𝐵𝑐𝐵𝑑𝐵𝑒𝑁 (((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑐)(+g𝑅)((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑))))
181 simp11 1222 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑅 ∈ CRing)
18218adantr 472 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → 𝐴 ∈ Ring)
183 simprll 821 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → 𝑏𝐵)
184 simpl3 1208 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → 𝐺𝐵)
185182, 183, 184, 38syl3anc 1439 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → (𝑏 𝐺) ∈ 𝐵)
1861853adant3 1124 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 𝐺) ∈ 𝐵)
187 simp2lr 1278 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑐 ∈ (Base‘𝑅))
188 simprrl 823 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → 𝑑𝐵)
189182, 188, 184, 95syl3anc 1439 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → (𝑑 𝐺) ∈ 𝐵)
1901893adant3 1124 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑑 𝐺) ∈ 𝐵)
191 simp2rr 1280 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑒𝑁)
192 simp3l 1220 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))))
193192oveq1d 6780 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) = (((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
19456adantr 472 . . . . . . . . . . . . . 14 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = )
195194oveqd 6782 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → (𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) = (𝑏 𝐺))
196195reseq1d 5502 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 𝐺) ↾ ({𝑒} × 𝑁)))
197 simpl1 1204 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → 𝑅 ∈ CRing)
19810adantr 472 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → 𝑁 ∈ Fin)
199 simprrr 824 . . . . . . . . . . . . . 14 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → 𝑒𝑁)
200199snssd 4448 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → {𝑒} ⊆ 𝑁)
201183, 63syl 17 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → 𝑏 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
20266adantr 472 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → 𝐺 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
20353, 102, 3, 197, 198, 198, 198, 200, 201, 202mamures 20319 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
204196, 203eqtr3d 2760 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑏 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
2052043adant3 1124 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
206194oveqd 6782 . . . . . . . . . . . . . . 15 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → (𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) = (𝑑 𝐺))
207206reseq1d 5502 . . . . . . . . . . . . . 14 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 𝐺) ↾ ({𝑒} × 𝑁)))
208188, 114syl 17 . . . . . . . . . . . . . . 15 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → 𝑑 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
20953, 102, 3, 197, 198, 198, 198, 200, 208, 202mamures 20319 . . . . . . . . . . . . . 14 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
210207, 209eqtr3d 2760 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑑 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
211210oveq2d 6781 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · ((𝑑 𝐺) ↾ ({𝑒} × 𝑁))) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
21212adantr 472 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → 𝑅 ∈ Ring)
213103a1i 11 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → {𝑒} ∈ Fin)
214 simprlr 822 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → 𝑐 ∈ (Base‘𝑅))
215200, 110syl 17 . . . . . . . . . . . . . 14 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → ({𝑒} × 𝑁) ⊆ (𝑁 × 𝑁))
216208, 215, 116syl2anc 696 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → (𝑑 ↾ ({𝑒} × 𝑁)) ∈ ((Base‘𝑅) ↑𝑚 ({𝑒} × 𝑁)))
2173, 212, 102, 213, 198, 198, 7, 214, 216, 202mamuvs1 20334 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → (((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
218211, 217eqtr4d 2761 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · ((𝑑 𝐺) ↾ ({𝑒} × 𝑁))) = (((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
2192183adant3 1124 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · ((𝑑 𝐺) ↾ ({𝑒} × 𝑁))) = (((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
220193, 205, 2193eqtr4d 2768 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 𝐺) ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · ((𝑑 𝐺) ↾ ({𝑒} × 𝑁))))
221 simp3r 1221 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
222221oveq1d 6780 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
223195reseq1d 5502 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
224 difssd 3846 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → (𝑁 ∖ {𝑒}) ⊆ 𝑁)
22553, 144, 3, 197, 198, 198, 198, 224, 201, 202mamures 20319 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
226223, 225eqtr3d 2760 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑏 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
2272263adant3 1124 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
228206reseq1d 5502 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
22953, 144, 3, 197, 198, 198, 198, 224, 208, 202mamures 20319 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
230228, 229eqtr3d 2760 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑑 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
2312303adant3 1124 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑑 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
232222, 227, 2313eqtr4d 2768 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
23313, 1, 2, 3, 7, 181, 186, 187, 190, 191, 220, 232mdetrsca 20532 . . . . . . . 8 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝐷‘(𝑏 𝐺)) = (𝑐 · (𝐷‘(𝑑 𝐺))))
234 simp2ll 1277 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑏𝐵)
235234, 32syl 17 . . . . . . . 8 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (𝐷‘(𝑏 𝐺)))
236 simp2rl 1279 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑑𝐵)
237172oveq2d 6781 . . . . . . . . 9 (𝑑𝐵 → (𝑐 · ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑)) = (𝑐 · (𝐷‘(𝑑 𝐺))))
238236, 237syl 17 . . . . . . . 8 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑐 · ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑)) = (𝑐 · (𝐷‘(𝑑 𝐺))))
239233, 235, 2383eqtr4d 2768 . . . . . . 7 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (𝑐 · ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑)))
2402393expia 1114 . . . . . 6 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → (((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (𝑐 · ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑))))
241240anassrs 683 . . . . 5 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐 ∈ (Base‘𝑅))) ∧ (𝑑𝐵𝑒𝑁)) → (((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (𝑐 · ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑))))
242241ralrimivva 3073 . . . 4 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐 ∈ (Base‘𝑅))) → ∀𝑑𝐵𝑒𝑁 (((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (𝑐 · ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑))))
243242ralrimivva 3073 . . 3 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → ∀𝑏𝐵𝑐 ∈ (Base‘𝑅)∀𝑑𝐵𝑒𝑁 (((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (𝑐 · ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑))))
244 simp2 1129 . . 3 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → 𝐹𝐵)
2451, 2, 3, 4, 5, 6, 7, 10, 12, 27, 83, 180, 243, 13, 52, 244mdetuni0 20550 . 2 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝐹) = (((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘(1r𝐴)) · (𝐷𝐹)))
246 oveq1 6772 . . . . 5 (𝑎 = 𝐹 → (𝑎 𝐺) = (𝐹 𝐺))
247246fveq2d 6308 . . . 4 (𝑎 = 𝐹 → (𝐷‘(𝑎 𝐺)) = (𝐷‘(𝐹 𝐺)))
248 fvex 6314 . . . 4 (𝐷‘(𝐹 𝐺)) ∈ V
249247, 26, 248fvmpt 6396 . . 3 (𝐹𝐵 → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝐹) = (𝐷‘(𝐹 𝐺)))
2502493ad2ant2 1126 . 2 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝐹) = (𝐷‘(𝐹 𝐺)))
251 eqid 2724 . . . . . . 7 (1r𝐴) = (1r𝐴)
2522, 251ringidcl 18689 . . . . . 6 (𝐴 ∈ Ring → (1r𝐴) ∈ 𝐵)
253 oveq1 6772 . . . . . . . 8 (𝑎 = (1r𝐴) → (𝑎 𝐺) = ((1r𝐴) 𝐺))
254253fveq2d 6308 . . . . . . 7 (𝑎 = (1r𝐴) → (𝐷‘(𝑎 𝐺)) = (𝐷‘((1r𝐴) 𝐺)))
255 fvex 6314 . . . . . . 7 (𝐷‘((1r𝐴) 𝐺)) ∈ V
256254, 26, 255fvmpt 6396 . . . . . 6 ((1r𝐴) ∈ 𝐵 → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘(1r𝐴)) = (𝐷‘((1r𝐴) 𝐺)))
25718, 252, 2563syl 18 . . . . 5 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘(1r𝐴)) = (𝐷‘((1r𝐴) 𝐺)))
258 simp3 1130 . . . . . . 7 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → 𝐺𝐵)
2592, 22, 251ringlidm 18692 . . . . . . 7 ((𝐴 ∈ Ring ∧ 𝐺𝐵) → ((1r𝐴) 𝐺) = 𝐺)
26018, 258, 259syl2anc 696 . . . . . 6 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → ((1r𝐴) 𝐺) = 𝐺)
261260fveq2d 6308 . . . . 5 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → (𝐷‘((1r𝐴) 𝐺)) = (𝐷𝐺))
262257, 261eqtrd 2758 . . . 4 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘(1r𝐴)) = (𝐷𝐺))
263262oveq1d 6780 . . 3 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → (((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘(1r𝐴)) · (𝐷𝐹)) = ((𝐷𝐺) · (𝐷𝐹)))
26415, 258ffvelrnd 6475 . . . 4 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → (𝐷𝐺) ∈ (Base‘𝑅))
26515, 244ffvelrnd 6475 . . . 4 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → (𝐷𝐹) ∈ (Base‘𝑅))
2663, 7crngcom 18683 . . . 4 ((𝑅 ∈ CRing ∧ (𝐷𝐺) ∈ (Base‘𝑅) ∧ (𝐷𝐹) ∈ (Base‘𝑅)) → ((𝐷𝐺) · (𝐷𝐹)) = ((𝐷𝐹) · (𝐷𝐺)))
26752, 264, 265, 266syl3anc 1439 . . 3 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → ((𝐷𝐺) · (𝐷𝐹)) = ((𝐷𝐹) · (𝐷𝐺)))
268263, 267eqtrd 2758 . 2 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → (((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘(1r𝐴)) · (𝐷𝐹)) = ((𝐷𝐹) · (𝐷𝐺)))
269245, 250, 2683eqtr3d 2766 1 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → (𝐷‘(𝐹 𝐺)) = ((𝐷𝐹) · (𝐷𝐺)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072   = wceq 1596  wcel 2103  wne 2896  wral 3014  Vcvv 3304  cdif 3677  wss 3680  {csn 4285  cotp 4293  cmpt 4837   × cxp 5216  cres 5220  wf 5997  cfv 6001  (class class class)co 6765  𝑓 cof 7012  𝑚 cmap 7974  Fincfn 8072  Basecbs 15980  +gcplusg 16064  .rcmulr 16065  0gc0g 16223   Σg cgsu 16224  1rcur 18622  Ringcrg 18668  CRingccrg 18669   maMul cmmul 20312   Mat cmat 20336   maDet cmdat 20513
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-rep 4879  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-inf2 8651  ax-cnex 10105  ax-resscn 10106  ax-1cn 10107  ax-icn 10108  ax-addcl 10109  ax-addrcl 10110  ax-mulcl 10111  ax-mulrcl 10112  ax-mulcom 10113  ax-addass 10114  ax-mulass 10115  ax-distr 10116  ax-i2m1 10117  ax-1ne0 10118  ax-1rid 10119  ax-rnegex 10120  ax-rrecex 10121  ax-cnre 10122  ax-pre-lttri 10123  ax-pre-lttrn 10124  ax-pre-ltadd 10125  ax-pre-mulgt0 10126  ax-addf 10128  ax-mulf 10129
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-xor 1578  df-tru 1599  df-fal 1602  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-reu 3021  df-rmo 3022  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-pss 3696  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-tp 4290  df-op 4292  df-ot 4294  df-uni 4545  df-int 4584  df-iun 4630  df-iin 4631  df-br 4761  df-opab 4821  df-mpt 4838  df-tr 4861  df-id 5128  df-eprel 5133  df-po 5139  df-so 5140  df-fr 5177  df-se 5178  df-we 5179  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-pred 5793  df-ord 5839  df-on 5840  df-lim 5841  df-suc 5842  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-isom 6010  df-riota 6726  df-ov 6768  df-oprab 6769  df-mpt2 6770  df-of 7014  df-om 7183  df-1st 7285  df-2nd 7286  df-supp 7416  df-tpos 7472  df-wrecs 7527  df-recs 7588  df-rdg 7626  df-1o 7680  df-2o 7681  df-oadd 7684  df-er 7862  df-map 7976  df-pm 7977  df-ixp 8026  df-en 8073  df-dom 8074  df-sdom 8075  df-fin 8076  df-fsupp 8392  df-sup 8464  df-oi 8531  df-card 8878  df-pnf 10189  df-mnf 10190  df-xr 10191  df-ltxr 10192  df-le 10193  df-sub 10381  df-neg 10382  df-div 10798  df-nn 11134  df-2 11192  df-3 11193  df-4 11194  df-5 11195  df-6 11196  df-7 11197  df-8 11198  df-9 11199  df-n0 11406  df-xnn0 11477  df-z 11491  df-dec 11607  df-uz 11801  df-rp 11947  df-fz 12441  df-fzo 12581  df-seq 12917  df-exp 12976  df-hash 13233  df-word 13406  df-lsw 13407  df-concat 13408  df-s1 13409  df-substr 13410  df-splice 13411  df-reverse 13412  df-s2 13714  df-struct 15982  df-ndx 15983  df-slot 15984  df-base 15986  df-sets 15987  df-ress 15988  df-plusg 16077  df-mulr 16078  df-starv 16079  df-sca 16080  df-vsca 16081  df-ip 16082  df-tset 16083  df-ple 16084  df-ds 16087  df-unif 16088  df-hom 16089  df-cco 16090  df-0g 16225  df-gsum 16226  df-prds 16231  df-pws 16233  df-mre 16369  df-mrc 16370  df-acs 16372  df-mgm 17364  df-sgrp 17406  df-mnd 17417  df-mhm 17457  df-submnd 17458  df-grp 17547  df-minusg 17548  df-sbg 17549  df-mulg 17663  df-subg 17713  df-ghm 17780  df-gim 17823  df-cntz 17871  df-oppg 17897  df-symg 17919  df-pmtr 17983  df-psgn 18032  df-evpm 18033  df-cmn 18316  df-abl 18317  df-mgp 18611  df-ur 18623  df-srg 18627  df-ring 18670  df-cring 18671  df-oppr 18744  df-dvdsr 18762  df-unit 18763  df-invr 18793  df-dvr 18804  df-rnghom 18838  df-drng 18872  df-subrg 18901  df-lmod 18988  df-lss 19056  df-sra 19295  df-rgmod 19296  df-cnfld 19870  df-zring 19942  df-zrh 19975  df-dsmm 20199  df-frlm 20214  df-mamu 20313  df-mat 20337  df-mdet 20514
This theorem is referenced by:  matunit  20607  cramerimplem3  20614  matunitlindflem2  33638
  Copyright terms: Public domain W3C validator