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

Theorem mdetmul 20196
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 2609 . . 3 (Base‘𝑅) = (Base‘𝑅)
4 eqid 2609 . . 3 (0g𝑅) = (0g𝑅)
5 eqid 2609 . . 3 (1r𝑅) = (1r𝑅)
6 eqid 2609 . . 3 (+g𝑅) = (+g𝑅)
7 mdetmul.t1 . . 3 · = (.r𝑅)
81, 2matrcl 19985 . . . . 5 (𝐹𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
98simpld 473 . . . 4 (𝐹𝐵𝑁 ∈ Fin)
1093ad2ant2 1075 . . 3 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → 𝑁 ∈ Fin)
11 crngring 18330 . . . 4 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
12113ad2ant1 1074 . . 3 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → 𝑅 ∈ Ring)
13 mdetmul.d . . . . . . . 8 𝐷 = (𝑁 maDet 𝑅)
1413, 1, 2, 3mdetf 20168 . . . . . . 7 (𝑅 ∈ CRing → 𝐷:𝐵⟶(Base‘𝑅))
15143ad2ant1 1074 . . . . . 6 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → 𝐷:𝐵⟶(Base‘𝑅))
1615adantr 479 . . . . 5 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ 𝑎𝐵) → 𝐷:𝐵⟶(Base‘𝑅))
171matring 20016 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring)
1810, 12, 17syl2anc 690 . . . . . . 7 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → 𝐴 ∈ Ring)
1918adantr 479 . . . . . 6 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ 𝑎𝐵) → 𝐴 ∈ Ring)
20 simpr 475 . . . . . 6 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ 𝑎𝐵) → 𝑎𝐵)
21 simpl3 1058 . . . . . 6 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ 𝑎𝐵) → 𝐺𝐵)
22 mdetmul.t2 . . . . . . 7 = (.r𝐴)
232, 22ringcl 18333 . . . . . 6 ((𝐴 ∈ Ring ∧ 𝑎𝐵𝐺𝐵) → (𝑎 𝐺) ∈ 𝐵)
2419, 20, 21, 23syl3anc 1317 . . . . 5 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ 𝑎𝐵) → (𝑎 𝐺) ∈ 𝐵)
2516, 24ffvelrnd 6253 . . . 4 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ 𝑎𝐵) → (𝐷‘(𝑎 𝐺)) ∈ (Base‘𝑅))
26 eqid 2609 . . . 4 (𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺))) = (𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))
2725, 26fmptd 6277 . . 3 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → (𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺))):𝐵⟶(Base‘𝑅))
28 simp21 1086 . . . . . . 7 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑏𝐵)
29 oveq1 6534 . . . . . . . . 9 (𝑎 = 𝑏 → (𝑎 𝐺) = (𝑏 𝐺))
3029fveq2d 6092 . . . . . . . 8 (𝑎 = 𝑏 → (𝐷‘(𝑎 𝐺)) = (𝐷‘(𝑏 𝐺)))
31 fvex 6098 . . . . . . . 8 (𝐷‘(𝑏 𝐺)) ∈ V
3230, 26, 31fvmpt 6176 . . . . . . 7 (𝑏𝐵 → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (𝐷‘(𝑏 𝐺)))
3328, 32syl 17 . . . . . 6 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (𝐷‘(𝑏 𝐺)))
34 simp11 1083 . . . . . . 7 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑅 ∈ CRing)
3518adantr 479 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) → 𝐴 ∈ Ring)
36 simpr1 1059 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) → 𝑏𝐵)
37 simpl3 1058 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) → 𝐺𝐵)
382, 22ringcl 18333 . . . . . . . . 9 ((𝐴 ∈ Ring ∧ 𝑏𝐵𝐺𝐵) → (𝑏 𝐺) ∈ 𝐵)
3935, 36, 37, 38syl3anc 1317 . . . . . . . 8 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) → (𝑏 𝐺) ∈ 𝐵)
40393adant3 1073 . . . . . . 7 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → (𝑏 𝐺) ∈ 𝐵)
41 simp22 1087 . . . . . . 7 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑐𝑁)
42 simp23 1088 . . . . . . 7 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑑𝑁)
43 simp3l 1081 . . . . . . 7 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑐𝑑)
44 simpl3r 1109 . . . . . . . . . 10 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) ∧ 𝑎𝑁) → ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))
45 eqid 2609 . . . . . . . . . . . 12 𝑁 = 𝑁
46 oveq1 6534 . . . . . . . . . . . . 13 ((𝑐𝑏𝑒) = (𝑑𝑏𝑒) → ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)) = ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))
4746ralimi 2935 . . . . . . . . . . . 12 (∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒) → ∀𝑒𝑁 ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)) = ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))
48 mpteq12 4658 . . . . . . . . . . . 12 ((𝑁 = 𝑁 ∧ ∀𝑒𝑁 ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)) = ((𝑑𝑏𝑒) · (𝑒𝐺𝑎))) → (𝑒𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎))) = (𝑒𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎))))
4945, 47, 48sylancr 693 . . . . . . . . . . 11 (∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒) → (𝑒𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎))) = (𝑒𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎))))
5049oveq2d 6543 . . . . . . . . . 10 (∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒) → (𝑅 Σg (𝑒𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)))) = (𝑅 Σg (𝑒𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))))
5144, 50syl 17 . . . . . . . . 9 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) ∧ 𝑎𝑁) → (𝑅 Σg (𝑒𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)))) = (𝑅 Σg (𝑒𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))))
52 simp1 1053 . . . . . . . . . . . . . . 15 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → 𝑅 ∈ CRing)
53 eqid 2609 . . . . . . . . . . . . . . . . 17 (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)
541, 53matmulr 20011 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (.r𝐴))
5554, 22syl6eqr 2661 . . . . . . . . . . . . . . 15 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = )
5610, 52, 55syl2anc 690 . . . . . . . . . . . . . 14 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = )
5756ad2antrr 757 . . . . . . . . . . . . 13 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = )
5857oveqd 6544 . . . . . . . . . . . 12 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → (𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) = (𝑏 𝐺))
5958oveqd 6544 . . . . . . . . . . 11 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → (𝑐(𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺)𝑎) = (𝑐(𝑏 𝐺)𝑎))
60 simpll1 1092 . . . . . . . . . . . 12 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → 𝑅 ∈ CRing)
6110ad2antrr 757 . . . . . . . . . . . 12 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → 𝑁 ∈ Fin)
62 simplr1 1095 . . . . . . . . . . . . 13 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → 𝑏𝐵)
631, 3, 2matbas2i 19995 . . . . . . . . . . . . 13 (𝑏𝐵𝑏 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
6462, 63syl 17 . . . . . . . . . . . 12 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → 𝑏 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
651, 3, 2matbas2i 19995 . . . . . . . . . . . . . 14 (𝐺𝐵𝐺 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
66653ad2ant3 1076 . . . . . . . . . . . . 13 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → 𝐺 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
6766ad2antrr 757 . . . . . . . . . . . 12 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → 𝐺 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
68 simplr2 1096 . . . . . . . . . . . 12 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → 𝑐𝑁)
69 simpr 475 . . . . . . . . . . . 12 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → 𝑎𝑁)
7053, 3, 7, 60, 61, 61, 61, 64, 67, 68, 69mamufv 19960 . . . . . . . . . . 11 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → (𝑐(𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺)𝑎) = (𝑅 Σg (𝑒𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)))))
7159, 70eqtr3d 2645 . . . . . . . . . 10 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → (𝑐(𝑏 𝐺)𝑎) = (𝑅 Σg (𝑒𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)))))
72713adantl3 1211 . . . . . . . . 9 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) ∧ 𝑎𝑁) → (𝑐(𝑏 𝐺)𝑎) = (𝑅 Σg (𝑒𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)))))
7358oveqd 6544 . . . . . . . . . . 11 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → (𝑑(𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺)𝑎) = (𝑑(𝑏 𝐺)𝑎))
74 simplr3 1097 . . . . . . . . . . . 12 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → 𝑑𝑁)
7553, 3, 7, 60, 61, 61, 61, 64, 67, 74, 69mamufv 19960 . . . . . . . . . . 11 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → (𝑑(𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺)𝑎) = (𝑅 Σg (𝑒𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))))
7673, 75eqtr3d 2645 . . . . . . . . . 10 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) ∧ 𝑎𝑁) → (𝑑(𝑏 𝐺)𝑎) = (𝑅 Σg (𝑒𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))))
77763adantl3 1211 . . . . . . . . 9 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) ∧ 𝑎𝑁) → (𝑑(𝑏 𝐺)𝑎) = (𝑅 Σg (𝑒𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))))
7851, 72, 773eqtr4d 2653 . . . . . . . 8 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) ∧ 𝑎𝑁) → (𝑐(𝑏 𝐺)𝑎) = (𝑑(𝑏 𝐺)𝑎))
7978ralrimiva 2948 . . . . . . 7 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → ∀𝑎𝑁 (𝑐(𝑏 𝐺)𝑎) = (𝑑(𝑏 𝐺)𝑎))
8013, 1, 2, 4, 34, 40, 41, 42, 43, 79mdetralt 20181 . . . . . 6 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → (𝐷‘(𝑏 𝐺)) = (0g𝑅))
8133, 80eqtrd 2643 . . . . 5 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁) ∧ (𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (0g𝑅))
82813expia 1258 . . . 4 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝑁𝑑𝑁)) → ((𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒)) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (0g𝑅)))
8382ralrimivvva 2954 . . 3 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → ∀𝑏𝐵𝑐𝑁𝑑𝑁 ((𝑐𝑑 ∧ ∀𝑒𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒)) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (0g𝑅)))
84 simp11 1083 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑅 ∈ CRing)
8518adantr 479 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝐴 ∈ Ring)
86 simprll 797 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝑏𝐵)
87 simpl3 1058 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝐺𝐵)
8885, 86, 87, 38syl3anc 1317 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (𝑏 𝐺) ∈ 𝐵)
89883adant3 1073 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 𝐺) ∈ 𝐵)
90 simprlr 798 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝑐𝐵)
912, 22ringcl 18333 . . . . . . . . . . 11 ((𝐴 ∈ Ring ∧ 𝑐𝐵𝐺𝐵) → (𝑐 𝐺) ∈ 𝐵)
9285, 90, 87, 91syl3anc 1317 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (𝑐 𝐺) ∈ 𝐵)
93923adant3 1073 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑐 𝐺) ∈ 𝐵)
94 simprrl 799 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝑑𝐵)
952, 22ringcl 18333 . . . . . . . . . . 11 ((𝐴 ∈ Ring ∧ 𝑑𝐵𝐺𝐵) → (𝑑 𝐺) ∈ 𝐵)
9685, 94, 87, 95syl3anc 1317 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (𝑑 𝐺) ∈ 𝐵)
97963adant3 1073 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑑 𝐺) ∈ 𝐵)
98 simp2rr 1123 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑒𝑁)
99 simp31 1089 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))))
10099oveq1d 6542 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) = (((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
10112adantr 479 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝑅 ∈ Ring)
102 eqid 2609 . . . . . . . . . . . . 13 (𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩) = (𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)
103 snfi 7901 . . . . . . . . . . . . . 14 {𝑒} ∈ Fin
104103a1i 11 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → {𝑒} ∈ Fin)
10510adantr 479 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝑁 ∈ Fin)
1061, 3, 2matbas2i 19995 . . . . . . . . . . . . . . 15 (𝑐𝐵𝑐 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
10790, 106syl 17 . . . . . . . . . . . . . 14 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝑐 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
108 simprrr 800 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝑒𝑁)
109108snssd 4280 . . . . . . . . . . . . . . 15 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → {𝑒} ⊆ 𝑁)
110 xpss1 5140 . . . . . . . . . . . . . . 15 ({𝑒} ⊆ 𝑁 → ({𝑒} × 𝑁) ⊆ (𝑁 × 𝑁))
111109, 110syl 17 . . . . . . . . . . . . . 14 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ({𝑒} × 𝑁) ⊆ (𝑁 × 𝑁))
112 elmapssres 7746 . . . . . . . . . . . . . 14 ((𝑐 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)) ∧ ({𝑒} × 𝑁) ⊆ (𝑁 × 𝑁)) → (𝑐 ↾ ({𝑒} × 𝑁)) ∈ ((Base‘𝑅) ↑𝑚 ({𝑒} × 𝑁)))
113107, 111, 112syl2anc 690 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (𝑐 ↾ ({𝑒} × 𝑁)) ∈ ((Base‘𝑅) ↑𝑚 ({𝑒} × 𝑁)))
1141, 3, 2matbas2i 19995 . . . . . . . . . . . . . . 15 (𝑑𝐵𝑑 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
11594, 114syl 17 . . . . . . . . . . . . . 14 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝑑 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
116 elmapssres 7746 . . . . . . . . . . . . . 14 ((𝑑 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)) ∧ ({𝑒} × 𝑁) ⊆ (𝑁 × 𝑁)) → (𝑑 ↾ ({𝑒} × 𝑁)) ∈ ((Base‘𝑅) ↑𝑚 ({𝑒} × 𝑁)))
117115, 111, 116syl2anc 690 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (𝑑 ↾ ({𝑒} × 𝑁)) ∈ ((Base‘𝑅) ↑𝑚 ({𝑒} × 𝑁)))
11866adantr 479 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝐺 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
1193, 101, 102, 104, 105, 105, 6, 113, 117, 118mamudi 19976 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) = (((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) ∘𝑓 (+g𝑅)((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
1201193adant3 1073 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) = (((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) ∘𝑓 (+g𝑅)((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
121100, 120eqtrd 2643 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) = (((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) ∘𝑓 (+g𝑅)((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
12256adantr 479 . . . . . . . . . . . . . 14 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = )
123122oveqd 6544 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) = (𝑏 𝐺))
124123reseq1d 5303 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 𝐺) ↾ ({𝑒} × 𝑁)))
125 simpl1 1056 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝑅 ∈ CRing)
12686, 63syl 17 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → 𝑏 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
12753, 102, 3, 125, 105, 105, 105, 109, 126, 118mamures 19963 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
128124, 127eqtr3d 2645 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑏 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
1291283adant3 1073 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
130122oveqd 6544 . . . . . . . . . . . . . 14 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (𝑐(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) = (𝑐 𝐺))
131130reseq1d 5303 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑐(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑐 𝐺) ↾ ({𝑒} × 𝑁)))
13253, 102, 3, 125, 105, 105, 105, 109, 107, 118mamures 19963 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑐(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
133131, 132eqtr3d 2645 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑐 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
134122oveqd 6544 . . . . . . . . . . . . . 14 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) = (𝑑 𝐺))
135134reseq1d 5303 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 𝐺) ↾ ({𝑒} × 𝑁)))
13653, 102, 3, 125, 105, 105, 105, 109, 115, 118mamures 19963 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
137135, 136eqtr3d 2645 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑑 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
138133, 137oveq12d 6545 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (((𝑐 𝐺) ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)((𝑑 𝐺) ↾ ({𝑒} × 𝑁))) = (((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) ∘𝑓 (+g𝑅)((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
1391383adant3 1073 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (((𝑐 𝐺) ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)((𝑑 𝐺) ↾ ({𝑒} × 𝑁))) = (((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) ∘𝑓 (+g𝑅)((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
140121, 129, 1393eqtr4d 2653 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 𝐺) ↾ ({𝑒} × 𝑁)) = (((𝑐 𝐺) ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)((𝑑 𝐺) ↾ ({𝑒} × 𝑁))))
141 simp32 1090 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
142141oveq1d 6542 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺) = ((𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
143123reseq1d 5303 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
144 eqid 2609 . . . . . . . . . . . . 13 (𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩) = (𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)
145 difssd 3699 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (𝑁 ∖ {𝑒}) ⊆ 𝑁)
14653, 144, 3, 125, 105, 105, 105, 145, 126, 118mamures 19963 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
147143, 146eqtr3d 2645 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑏 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
1481473adant3 1073 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
149130reseq1d 5303 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑐(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑐 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
15053, 144, 3, 125, 105, 105, 105, 145, 107, 118mamures 19963 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑐(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
151149, 150eqtr3d 2645 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑐 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
1521513adant3 1073 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑐 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
153142, 148, 1523eqtr4d 2653 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑐 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
154 simp33 1091 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
155154oveq1d 6542 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
156134reseq1d 5303 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
15753, 144, 3, 125, 105, 105, 105, 145, 115, 118mamures 19963 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
158156, 157eqtr3d 2645 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑑 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
1591583adant3 1073 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑑 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
160155, 148, 1593eqtr4d 2653 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
16113, 1, 2, 6, 84, 89, 93, 97, 98, 140, 153, 160mdetrlin 20175 . . . . . . . 8 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝐷‘(𝑏 𝐺)) = ((𝐷‘(𝑐 𝐺))(+g𝑅)(𝐷‘(𝑑 𝐺))))
16286, 32syl 17 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (𝐷‘(𝑏 𝐺)))
1631623adant3 1073 . . . . . . . 8 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (𝐷‘(𝑏 𝐺)))
164 oveq1 6534 . . . . . . . . . . . . 13 (𝑎 = 𝑐 → (𝑎 𝐺) = (𝑐 𝐺))
165164fveq2d 6092 . . . . . . . . . . . 12 (𝑎 = 𝑐 → (𝐷‘(𝑎 𝐺)) = (𝐷‘(𝑐 𝐺)))
166 fvex 6098 . . . . . . . . . . . 12 (𝐷‘(𝑐 𝐺)) ∈ V
167165, 26, 166fvmpt 6176 . . . . . . . . . . 11 (𝑐𝐵 → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑐) = (𝐷‘(𝑐 𝐺)))
16890, 167syl 17 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑐) = (𝐷‘(𝑐 𝐺)))
169 oveq1 6534 . . . . . . . . . . . . 13 (𝑎 = 𝑑 → (𝑎 𝐺) = (𝑑 𝐺))
170169fveq2d 6092 . . . . . . . . . . . 12 (𝑎 = 𝑑 → (𝐷‘(𝑎 𝐺)) = (𝐷‘(𝑑 𝐺)))
171 fvex 6098 . . . . . . . . . . . 12 (𝐷‘(𝑑 𝐺)) ∈ V
172170, 26, 171fvmpt 6176 . . . . . . . . . . 11 (𝑑𝐵 → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑) = (𝐷‘(𝑑 𝐺)))
17394, 172syl 17 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑) = (𝐷‘(𝑑 𝐺)))
174168, 173oveq12d 6545 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑐)(+g𝑅)((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑)) = ((𝐷‘(𝑐 𝐺))(+g𝑅)(𝐷‘(𝑑 𝐺))))
1751743adant3 1073 . . . . . . . 8 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑐)(+g𝑅)((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑)) = ((𝐷‘(𝑐 𝐺))(+g𝑅)(𝐷‘(𝑑 𝐺))))
176161, 163, 1753eqtr4d 2653 . . . . . . 7 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑐)(+g𝑅)((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑)))
1771763expia 1258 . . . . . 6 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐𝐵) ∧ (𝑑𝐵𝑒𝑁))) → (((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑐)(+g𝑅)((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑))))
178177anassrs 677 . . . . 5 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝐵)) ∧ (𝑑𝐵𝑒𝑁)) → (((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑐)(+g𝑅)((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑))))
179178ralrimivva 2953 . . . 4 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐𝐵)) → ∀𝑑𝐵𝑒𝑁 (((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑐)(+g𝑅)((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑))))
180179ralrimivva 2953 . . 3 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → ∀𝑏𝐵𝑐𝐵𝑑𝐵𝑒𝑁 (((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘𝑓 (+g𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑐)(+g𝑅)((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑))))
181 simp11 1083 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑅 ∈ CRing)
18218adantr 479 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → 𝐴 ∈ Ring)
183 simprll 797 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → 𝑏𝐵)
184 simpl3 1058 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → 𝐺𝐵)
185182, 183, 184, 38syl3anc 1317 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → (𝑏 𝐺) ∈ 𝐵)
1861853adant3 1073 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 𝐺) ∈ 𝐵)
187 simp2lr 1121 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑐 ∈ (Base‘𝑅))
188 simprrl 799 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → 𝑑𝐵)
189182, 188, 184, 95syl3anc 1317 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → (𝑑 𝐺) ∈ 𝐵)
1901893adant3 1073 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑑 𝐺) ∈ 𝐵)
191 simp2rr 1123 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑒𝑁)
192 simp3l 1081 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))))
193192oveq1d 6542 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) = (((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
19456adantr 479 . . . . . . . . . . . . . 14 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = )
195194oveqd 6544 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → (𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) = (𝑏 𝐺))
196195reseq1d 5303 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 𝐺) ↾ ({𝑒} × 𝑁)))
197 simpl1 1056 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → 𝑅 ∈ CRing)
19810adantr 479 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → 𝑁 ∈ Fin)
199 simprrr 800 . . . . . . . . . . . . . 14 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → 𝑒𝑁)
200199snssd 4280 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → {𝑒} ⊆ 𝑁)
201183, 63syl 17 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → 𝑏 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
20266adantr 479 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → 𝐺 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
20353, 102, 3, 197, 198, 198, 198, 200, 201, 202mamures 19963 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
204196, 203eqtr3d 2645 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑏 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
2052043adant3 1073 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
206194oveqd 6544 . . . . . . . . . . . . . . 15 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → (𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) = (𝑑 𝐺))
207206reseq1d 5303 . . . . . . . . . . . . . 14 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 𝐺) ↾ ({𝑒} × 𝑁)))
208188, 114syl 17 . . . . . . . . . . . . . . 15 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → 𝑑 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
20953, 102, 3, 197, 198, 198, 198, 200, 208, 202mamures 19963 . . . . . . . . . . . . . 14 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
210207, 209eqtr3d 2645 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑑 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
211210oveq2d 6543 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · ((𝑑 𝐺) ↾ ({𝑒} × 𝑁))) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
21212adantr 479 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → 𝑅 ∈ Ring)
213103a1i 11 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → {𝑒} ∈ Fin)
214 simprlr 798 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → 𝑐 ∈ (Base‘𝑅))
215200, 110syl 17 . . . . . . . . . . . . . 14 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → ({𝑒} × 𝑁) ⊆ (𝑁 × 𝑁))
216208, 215, 116syl2anc 690 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → (𝑑 ↾ ({𝑒} × 𝑁)) ∈ ((Base‘𝑅) ↑𝑚 ({𝑒} × 𝑁)))
2173, 212, 102, 213, 198, 198, 7, 214, 216, 202mamuvs1 19978 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → (((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
218211, 217eqtr4d 2646 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · ((𝑑 𝐺) ↾ ({𝑒} × 𝑁))) = (((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
2192183adant3 1073 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · ((𝑑 𝐺) ↾ ({𝑒} × 𝑁))) = (((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
220193, 205, 2193eqtr4d 2653 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 𝐺) ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · ((𝑑 𝐺) ↾ ({𝑒} × 𝑁))))
221 simp3r 1082 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
222221oveq1d 6542 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
223195reseq1d 5303 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
224 difssd 3699 . . . . . . . . . . . . 13 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → (𝑁 ∖ {𝑒}) ⊆ 𝑁)
22553, 144, 3, 197, 198, 198, 198, 224, 201, 202mamures 19963 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
226223, 225eqtr3d 2645 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑏 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
2272263adant3 1073 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
228206reseq1d 5303 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
22953, 144, 3, 197, 198, 198, 198, 224, 208, 202mamures 19963 . . . . . . . . . . . 12 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
230228, 229eqtr3d 2645 . . . . . . . . . . 11 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → ((𝑑 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
2312303adant3 1073 . . . . . . . . . 10 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑑 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
232222, 227, 2313eqtr4d 2653 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
23313, 1, 2, 3, 7, 181, 186, 187, 190, 191, 220, 232mdetrsca 20176 . . . . . . . 8 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝐷‘(𝑏 𝐺)) = (𝑐 · (𝐷‘(𝑑 𝐺))))
234 simp2ll 1120 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑏𝐵)
235234, 32syl 17 . . . . . . . 8 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (𝐷‘(𝑏 𝐺)))
236 simp2rl 1122 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑑𝐵)
237172oveq2d 6543 . . . . . . . . 9 (𝑑𝐵 → (𝑐 · ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑)) = (𝑐 · (𝐷‘(𝑑 𝐺))))
238236, 237syl 17 . . . . . . . 8 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑐 · ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑)) = (𝑐 · (𝐷‘(𝑑 𝐺))))
239233, 235, 2383eqtr4d 2653 . . . . . . 7 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (𝑐 · ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑)))
2402393expia 1258 . . . . . 6 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ ((𝑏𝐵𝑐 ∈ (Base‘𝑅)) ∧ (𝑑𝐵𝑒𝑁))) → (((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (𝑐 · ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑))))
241240anassrs 677 . . . . 5 ((((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐 ∈ (Base‘𝑅))) ∧ (𝑑𝐵𝑒𝑁)) → (((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (𝑐 · ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑))))
242241ralrimivva 2953 . . . 4 (((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) ∧ (𝑏𝐵𝑐 ∈ (Base‘𝑅))) → ∀𝑑𝐵𝑒𝑁 (((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (𝑐 · ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑))))
243242ralrimivva 2953 . . 3 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → ∀𝑏𝐵𝑐 ∈ (Base‘𝑅)∀𝑑𝐵𝑒𝑁 (((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘𝑓 · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑏) = (𝑐 · ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝑑))))
244 simp2 1054 . . 3 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → 𝐹𝐵)
2451, 2, 3, 4, 5, 6, 7, 10, 12, 27, 83, 180, 243, 13, 52, 244mdetuni0 20194 . 2 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝐹) = (((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘(1r𝐴)) · (𝐷𝐹)))
246 oveq1 6534 . . . . 5 (𝑎 = 𝐹 → (𝑎 𝐺) = (𝐹 𝐺))
247246fveq2d 6092 . . . 4 (𝑎 = 𝐹 → (𝐷‘(𝑎 𝐺)) = (𝐷‘(𝐹 𝐺)))
248 fvex 6098 . . . 4 (𝐷‘(𝐹 𝐺)) ∈ V
249247, 26, 248fvmpt 6176 . . 3 (𝐹𝐵 → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝐹) = (𝐷‘(𝐹 𝐺)))
2502493ad2ant2 1075 . 2 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘𝐹) = (𝐷‘(𝐹 𝐺)))
251 eqid 2609 . . . . . . 7 (1r𝐴) = (1r𝐴)
2522, 251ringidcl 18340 . . . . . 6 (𝐴 ∈ Ring → (1r𝐴) ∈ 𝐵)
253 oveq1 6534 . . . . . . . 8 (𝑎 = (1r𝐴) → (𝑎 𝐺) = ((1r𝐴) 𝐺))
254253fveq2d 6092 . . . . . . 7 (𝑎 = (1r𝐴) → (𝐷‘(𝑎 𝐺)) = (𝐷‘((1r𝐴) 𝐺)))
255 fvex 6098 . . . . . . 7 (𝐷‘((1r𝐴) 𝐺)) ∈ V
256254, 26, 255fvmpt 6176 . . . . . 6 ((1r𝐴) ∈ 𝐵 → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘(1r𝐴)) = (𝐷‘((1r𝐴) 𝐺)))
25718, 252, 2563syl 18 . . . . 5 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘(1r𝐴)) = (𝐷‘((1r𝐴) 𝐺)))
258 simp3 1055 . . . . . . 7 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → 𝐺𝐵)
2592, 22, 251ringlidm 18343 . . . . . . 7 ((𝐴 ∈ Ring ∧ 𝐺𝐵) → ((1r𝐴) 𝐺) = 𝐺)
26018, 258, 259syl2anc 690 . . . . . 6 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → ((1r𝐴) 𝐺) = 𝐺)
261260fveq2d 6092 . . . . 5 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → (𝐷‘((1r𝐴) 𝐺)) = (𝐷𝐺))
262257, 261eqtrd 2643 . . . 4 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → ((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘(1r𝐴)) = (𝐷𝐺))
263262oveq1d 6542 . . 3 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → (((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘(1r𝐴)) · (𝐷𝐹)) = ((𝐷𝐺) · (𝐷𝐹)))
26415, 258ffvelrnd 6253 . . . 4 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → (𝐷𝐺) ∈ (Base‘𝑅))
26515, 244ffvelrnd 6253 . . . 4 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → (𝐷𝐹) ∈ (Base‘𝑅))
2663, 7crngcom 18334 . . . 4 ((𝑅 ∈ CRing ∧ (𝐷𝐺) ∈ (Base‘𝑅) ∧ (𝐷𝐹) ∈ (Base‘𝑅)) → ((𝐷𝐺) · (𝐷𝐹)) = ((𝐷𝐹) · (𝐷𝐺)))
26752, 264, 265, 266syl3anc 1317 . . 3 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → ((𝐷𝐺) · (𝐷𝐹)) = ((𝐷𝐹) · (𝐷𝐺)))
268263, 267eqtrd 2643 . 2 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → (((𝑎𝐵 ↦ (𝐷‘(𝑎 𝐺)))‘(1r𝐴)) · (𝐷𝐹)) = ((𝐷𝐹) · (𝐷𝐺)))
269245, 250, 2683eqtr3d 2651 1 ((𝑅 ∈ CRing ∧ 𝐹𝐵𝐺𝐵) → (𝐷‘(𝐹 𝐺)) = ((𝐷𝐹) · (𝐷𝐺)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030   = wceq 1474  wcel 1976  wne 2779  wral 2895  Vcvv 3172  cdif 3536  wss 3539  {csn 4124  cotp 4132  cmpt 4637   × cxp 5026  cres 5030  wf 5786  cfv 5790  (class class class)co 6527  𝑓 cof 6771  𝑚 cmap 7722  Fincfn 7819  Basecbs 15644  +gcplusg 15717  .rcmulr 15718  0gc0g 15872   Σg cgsu 15873  1rcur 18273  Ringcrg 18319  CRingccrg 18320   maMul cmmul 19956   Mat cmat 19980   maDet cmdat 20157
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-inf2 8399  ax-cnex 9849  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870  ax-addf 9872  ax-mulf 9873
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-xor 1456  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-ot 4133  df-uni 4367  df-int 4405  df-iun 4451  df-iin 4452  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-of 6773  df-om 6936  df-1st 7037  df-2nd 7038  df-supp 7161  df-tpos 7217  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-1o 7425  df-2o 7426  df-oadd 7429  df-er 7607  df-map 7724  df-pm 7725  df-ixp 7773  df-en 7820  df-dom 7821  df-sdom 7822  df-fin 7823  df-fsupp 8137  df-sup 8209  df-oi 8276  df-card 8626  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121  df-div 10537  df-nn 10871  df-2 10929  df-3 10930  df-4 10931  df-5 10932  df-6 10933  df-7 10934  df-8 10935  df-9 10936  df-n0 11143  df-z 11214  df-dec 11329  df-uz 11523  df-rp 11668  df-fz 12156  df-fzo 12293  df-seq 12622  df-exp 12681  df-hash 12938  df-word 13103  df-lsw 13104  df-concat 13105  df-s1 13106  df-substr 13107  df-splice 13108  df-reverse 13109  df-s2 13393  df-struct 15646  df-ndx 15647  df-slot 15648  df-base 15649  df-sets 15650  df-ress 15651  df-plusg 15730  df-mulr 15731  df-starv 15732  df-sca 15733  df-vsca 15734  df-ip 15735  df-tset 15736  df-ple 15737  df-ds 15740  df-unif 15741  df-hom 15742  df-cco 15743  df-0g 15874  df-gsum 15875  df-prds 15880  df-pws 15882  df-mre 16018  df-mrc 16019  df-acs 16021  df-mgm 17014  df-sgrp 17056  df-mnd 17067  df-mhm 17107  df-submnd 17108  df-grp 17197  df-minusg 17198  df-sbg 17199  df-mulg 17313  df-subg 17363  df-ghm 17430  df-gim 17473  df-cntz 17522  df-oppg 17548  df-symg 17570  df-pmtr 17634  df-psgn 17683  df-evpm 17684  df-cmn 17967  df-abl 17968  df-mgp 18262  df-ur 18274  df-srg 18278  df-ring 18321  df-cring 18322  df-oppr 18395  df-dvdsr 18413  df-unit 18414  df-invr 18444  df-dvr 18455  df-rnghom 18487  df-drng 18521  df-subrg 18550  df-lmod 18637  df-lss 18703  df-sra 18942  df-rgmod 18943  df-cnfld 19517  df-zring 19587  df-zrh 19619  df-dsmm 19843  df-frlm 19858  df-mamu 19957  df-mat 19981  df-mdet 20158
This theorem is referenced by:  matunit  20251  cramerimplem3  20258  matunitlindflem2  32400
  Copyright terms: Public domain W3C validator