Metamath Proof Explorer

Theorem mdetmul

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)

Ref Expression
Hypotheses mdetmul.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
mdetmul.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
mdetmul.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
mdetmul.t1 ⊢ · = ( .r ‘ 𝑅 )
mdetmul.t2 ⊢ ∙ = ( .r ‘ 𝐴 )
Assertion mdetmul ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐷 ‘ ( 𝐹 ∙ 𝐺 ) ) = ( ( 𝐷 ‘ 𝐹 ) · ( 𝐷 ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 mdetmul.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 mdetmul.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 mdetmul.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
4 mdetmul.t1 ⊢ · = ( .r ‘ 𝑅 )
5 mdetmul.t2 ⊢ ∙ = ( .r ‘ 𝐴 )
6 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
8 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
9 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
10 1 2 matrcl ⊢ ( 𝐹 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
11 10 simpld ⊢ ( 𝐹 ∈ 𝐵 → 𝑁 ∈ Fin )
12 11 3ad2ant2 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝑁 ∈ Fin )
13 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
14 13 3ad2ant1 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝑅 ∈ Ring )
15 3 1 2 6 mdetf ⊢ ( 𝑅 ∈ CRing → 𝐷 : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
16 15 3ad2ant1 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐷 : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
17 16 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) → 𝐷 : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
18 1 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
19 12 14 18 syl2anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐴 ∈ Ring )
20 19 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) → 𝐴 ∈ Ring )
21 simpr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) → 𝑎 ∈ 𝐵 )
22 simpl3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) → 𝐺 ∈ 𝐵 )
23 2 5 ringcl ⊢ ( ( 𝐴 ∈ Ring ∧ 𝑎 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝑎 ∙ 𝐺 ) ∈ 𝐵 )
24 20 21 22 23 syl3anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) → ( 𝑎 ∙ 𝐺 ) ∈ 𝐵 )
25 17 24 ffvelcdmd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ) → ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ∈ ( Base ‘ 𝑅 ) )
26 25 fmpttd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
27 simp21 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) ) → 𝑏 ∈ 𝐵 )
28 fvoveq1 ⊢ ( 𝑎 = 𝑏 → ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) = ( 𝐷 ‘ ( 𝑏 ∙ 𝐺 ) ) )
29 eqid ⊢ ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) = ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) )
30 fvex ⊢ ( 𝐷 ‘ ( 𝑏 ∙ 𝐺 ) ) ∈ V
31 28 29 30 fvmpt ⊢ ( 𝑏 ∈ 𝐵 → ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑏 ) = ( 𝐷 ‘ ( 𝑏 ∙ 𝐺 ) ) )
32 27 31 syl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑏 ) = ( 𝐷 ‘ ( 𝑏 ∙ 𝐺 ) ) )
33 simp11 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) ) → 𝑅 ∈ CRing )
34 19 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ) → 𝐴 ∈ Ring )
35 simpr1 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ) → 𝑏 ∈ 𝐵 )
36 simpl3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ) → 𝐺 ∈ 𝐵 )
37 2 5 ringcl ⊢ ( ( 𝐴 ∈ Ring ∧ 𝑏 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝑏 ∙ 𝐺 ) ∈ 𝐵 )
38 34 35 36 37 syl3anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ) → ( 𝑏 ∙ 𝐺 ) ∈ 𝐵 )
39 38 3adant3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) ) → ( 𝑏 ∙ 𝐺 ) ∈ 𝐵 )
40 simp22 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) ) → 𝑐 ∈ 𝑁 )
41 simp23 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) ) → 𝑑 ∈ 𝑁 )
42 simp3l ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) ) → 𝑐 ≠ 𝑑 )
43 simpl3r ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) ) ∧ 𝑎 ∈ 𝑁 ) → ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) )
44 eqid ⊢ 𝑁 = 𝑁
45 oveq1 ⊢ ( ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) → ( ( 𝑐 𝑏 𝑒 ) · ( 𝑒 𝐺 𝑎 ) ) = ( ( 𝑑 𝑏 𝑒 ) · ( 𝑒 𝐺 𝑎 ) ) )
46 45 ralimi ⊢ ( ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) → ∀ 𝑒 ∈ 𝑁 ( ( 𝑐 𝑏 𝑒 ) · ( 𝑒 𝐺 𝑎 ) ) = ( ( 𝑑 𝑏 𝑒 ) · ( 𝑒 𝐺 𝑎 ) ) )
47 mpteq12 ⊢ ( ( 𝑁 = 𝑁 ∧ ∀ 𝑒 ∈ 𝑁 ( ( 𝑐 𝑏 𝑒 ) · ( 𝑒 𝐺 𝑎 ) ) = ( ( 𝑑 𝑏 𝑒 ) · ( 𝑒 𝐺 𝑎 ) ) ) → ( 𝑒 ∈ 𝑁 ↦ ( ( 𝑐 𝑏 𝑒 ) · ( 𝑒 𝐺 𝑎 ) ) ) = ( 𝑒 ∈ 𝑁 ↦ ( ( 𝑑 𝑏 𝑒 ) · ( 𝑒 𝐺 𝑎 ) ) ) )
48 44 46 47 sylancr ⊢ ( ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) → ( 𝑒 ∈ 𝑁 ↦ ( ( 𝑐 𝑏 𝑒 ) · ( 𝑒 𝐺 𝑎 ) ) ) = ( 𝑒 ∈ 𝑁 ↦ ( ( 𝑑 𝑏 𝑒 ) · ( 𝑒 𝐺 𝑎 ) ) ) )
49 48 oveq2d ⊢ ( ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) → ( 𝑅 Σg ( 𝑒 ∈ 𝑁 ↦ ( ( 𝑐 𝑏 𝑒 ) · ( 𝑒 𝐺 𝑎 ) ) ) ) = ( 𝑅 Σg ( 𝑒 ∈ 𝑁 ↦ ( ( 𝑑 𝑏 𝑒 ) · ( 𝑒 𝐺 𝑎 ) ) ) ) )
50 43 49 syl ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) ) ∧ 𝑎 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑒 ∈ 𝑁 ↦ ( ( 𝑐 𝑏 𝑒 ) · ( 𝑒 𝐺 𝑎 ) ) ) ) = ( 𝑅 Σg ( 𝑒 ∈ 𝑁 ↦ ( ( 𝑑 𝑏 𝑒 ) · ( 𝑒 𝐺 𝑎 ) ) ) ) )
51 simp1 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝑅 ∈ CRing )
52 eqid ⊢ ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ )
53 1 52 matmulr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( .r ‘ 𝐴 ) )
54 53 5 eqtr4di ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ∙ )
55 12 51 54 syl2anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ∙ )
56 55 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ∙ )
57 56 oveqd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( 𝑏 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝐺 ) = ( 𝑏 ∙ 𝐺 ) )
58 57 oveqd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( 𝑐 ( 𝑏 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝐺 ) 𝑎 ) = ( 𝑐 ( 𝑏 ∙ 𝐺 ) 𝑎 ) )
59 simpll1 ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ) ∧ 𝑎 ∈ 𝑁 ) → 𝑅 ∈ CRing )
60 12 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ) ∧ 𝑎 ∈ 𝑁 ) → 𝑁 ∈ Fin )
61 simplr1 ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ) ∧ 𝑎 ∈ 𝑁 ) → 𝑏 ∈ 𝐵 )
62 1 6 2 matbas2i ⊢ ( 𝑏 ∈ 𝐵 → 𝑏 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
63 61 62 syl ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ) ∧ 𝑎 ∈ 𝑁 ) → 𝑏 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
64 1 6 2 matbas2i ⊢ ( 𝐺 ∈ 𝐵 → 𝐺 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
65 64 3ad2ant3 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐺 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
66 65 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ) ∧ 𝑎 ∈ 𝑁 ) → 𝐺 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
67 simplr2 ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ) ∧ 𝑎 ∈ 𝑁 ) → 𝑐 ∈ 𝑁 )
68 simpr ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ) ∧ 𝑎 ∈ 𝑁 ) → 𝑎 ∈ 𝑁 )
69 52 6 4 59 60 60 60 63 66 67 68 mamufv ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( 𝑐 ( 𝑏 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝐺 ) 𝑎 ) = ( 𝑅 Σg ( 𝑒 ∈ 𝑁 ↦ ( ( 𝑐 𝑏 𝑒 ) · ( 𝑒 𝐺 𝑎 ) ) ) ) )
70 58 69 eqtr3d ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( 𝑐 ( 𝑏 ∙ 𝐺 ) 𝑎 ) = ( 𝑅 Σg ( 𝑒 ∈ 𝑁 ↦ ( ( 𝑐 𝑏 𝑒 ) · ( 𝑒 𝐺 𝑎 ) ) ) ) )
71 70 3adantl3 ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) ) ∧ 𝑎 ∈ 𝑁 ) → ( 𝑐 ( 𝑏 ∙ 𝐺 ) 𝑎 ) = ( 𝑅 Σg ( 𝑒 ∈ 𝑁 ↦ ( ( 𝑐 𝑏 𝑒 ) · ( 𝑒 𝐺 𝑎 ) ) ) ) )
72 57 oveqd ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( 𝑑 ( 𝑏 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝐺 ) 𝑎 ) = ( 𝑑 ( 𝑏 ∙ 𝐺 ) 𝑎 ) )
73 simplr3 ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ) ∧ 𝑎 ∈ 𝑁 ) → 𝑑 ∈ 𝑁 )
74 52 6 4 59 60 60 60 63 66 73 68 mamufv ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( 𝑑 ( 𝑏 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝐺 ) 𝑎 ) = ( 𝑅 Σg ( 𝑒 ∈ 𝑁 ↦ ( ( 𝑑 𝑏 𝑒 ) · ( 𝑒 𝐺 𝑎 ) ) ) ) )
75 72 74 eqtr3d ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ) ∧ 𝑎 ∈ 𝑁 ) → ( 𝑑 ( 𝑏 ∙ 𝐺 ) 𝑎 ) = ( 𝑅 Σg ( 𝑒 ∈ 𝑁 ↦ ( ( 𝑑 𝑏 𝑒 ) · ( 𝑒 𝐺 𝑎 ) ) ) ) )
76 75 3adantl3 ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) ) ∧ 𝑎 ∈ 𝑁 ) → ( 𝑑 ( 𝑏 ∙ 𝐺 ) 𝑎 ) = ( 𝑅 Σg ( 𝑒 ∈ 𝑁 ↦ ( ( 𝑑 𝑏 𝑒 ) · ( 𝑒 𝐺 𝑎 ) ) ) ) )
77 50 71 76 3eqtr4d ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) ) ∧ 𝑎 ∈ 𝑁 ) → ( 𝑐 ( 𝑏 ∙ 𝐺 ) 𝑎 ) = ( 𝑑 ( 𝑏 ∙ 𝐺 ) 𝑎 ) )
78 77 ralrimiva ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) ) → ∀ 𝑎 ∈ 𝑁 ( 𝑐 ( 𝑏 ∙ 𝐺 ) 𝑎 ) = ( 𝑑 ( 𝑏 ∙ 𝐺 ) 𝑎 ) )
79 3 1 2 7 33 39 40 41 42 78 mdetralt ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) ) → ( 𝐷 ‘ ( 𝑏 ∙ 𝐺 ) ) = ( 0g ‘ 𝑅 ) )
80 32 79 eqtrd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ∧ ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑏 ) = ( 0g ‘ 𝑅 ) )
81 80 3expia ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁 ) ) → ( ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑏 ) = ( 0g ‘ 𝑅 ) ) )
82 81 ralrimivvva ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝑁 ∀ 𝑑 ∈ 𝑁 ( ( 𝑐 ≠ 𝑑 ∧ ∀ 𝑒 ∈ 𝑁 ( 𝑐 𝑏 𝑒 ) = ( 𝑑 𝑏 𝑒 ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑏 ) = ( 0g ‘ 𝑅 ) ) )
83 simp11 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → 𝑅 ∈ CRing )
84 19 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝐴 ∈ Ring )
85 simprll ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝑏 ∈ 𝐵 )
86 simpl3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝐺 ∈ 𝐵 )
87 84 85 86 37 syl3anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( 𝑏 ∙ 𝐺 ) ∈ 𝐵 )
88 87 3adant3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( 𝑏 ∙ 𝐺 ) ∈ 𝐵 )
89 simprlr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝑐 ∈ 𝐵 )
90 2 5 ringcl ⊢ ( ( 𝐴 ∈ Ring ∧ 𝑐 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝑐 ∙ 𝐺 ) ∈ 𝐵 )
91 84 89 86 90 syl3anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( 𝑐 ∙ 𝐺 ) ∈ 𝐵 )
92 91 3adant3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( 𝑐 ∙ 𝐺 ) ∈ 𝐵 )
93 simprrl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝑑 ∈ 𝐵 )
94 2 5 ringcl ⊢ ( ( 𝐴 ∈ Ring ∧ 𝑑 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝑑 ∙ 𝐺 ) ∈ 𝐵 )
95 84 93 86 94 syl3anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( 𝑑 ∙ 𝐺 ) ∈ 𝐵 )
96 95 3adant3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( 𝑑 ∙ 𝐺 ) ∈ 𝐵 )
97 simp2rr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → 𝑒 ∈ 𝑁 )
98 simp31 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) )
99 98 oveq1d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) = ( ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
100 14 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝑅 ∈ Ring )
101 eqid ⊢ ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) = ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ )
102 snfi ⊢ { 𝑒 } ∈ Fin
103 102 a1i ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → { 𝑒 } ∈ Fin )
104 12 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝑁 ∈ Fin )
105 1 6 2 matbas2i ⊢ ( 𝑐 ∈ 𝐵 → 𝑐 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
106 89 105 syl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝑐 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
107 simprrr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝑒 ∈ 𝑁 )
108 107 snssd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → { 𝑒 } ⊆ 𝑁 )
109 xpss1 ⊢ ( { 𝑒 } ⊆ 𝑁 → ( { 𝑒 } × 𝑁 ) ⊆ ( 𝑁 × 𝑁 ) )
110 108 109 syl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( { 𝑒 } × 𝑁 ) ⊆ ( 𝑁 × 𝑁 ) )
111 elmapssres ⊢ ( ( 𝑐 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ ( { 𝑒 } × 𝑁 ) ⊆ ( 𝑁 × 𝑁 ) ) → ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( { 𝑒 } × 𝑁 ) ) )
112 106 110 111 syl2anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( { 𝑒 } × 𝑁 ) ) )
113 1 6 2 matbas2i ⊢ ( 𝑑 ∈ 𝐵 → 𝑑 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
114 93 113 syl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝑑 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
115 elmapssres ⊢ ( ( 𝑑 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ∧ ( { 𝑒 } × 𝑁 ) ⊆ ( 𝑁 × 𝑁 ) ) → ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( { 𝑒 } × 𝑁 ) ) )
116 114 110 115 syl2anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( { 𝑒 } × 𝑁 ) ) )
117 65 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝐺 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
118 6 100 101 103 104 104 9 112 116 117 mamudi ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) = ( ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ∘f ( +g ‘ 𝑅 ) ( ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ) )
119 118 3adant3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) = ( ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ∘f ( +g ‘ 𝑅 ) ( ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ) )
120 99 119 eqtrd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) = ( ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ∘f ( +g ‘ 𝑅 ) ( ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ) )
121 55 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ∙ )
122 121 oveqd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( 𝑏 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝐺 ) = ( 𝑏 ∙ 𝐺 ) )
123 122 reseq1d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑏 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑏 ∙ 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) )
124 simpl1 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝑅 ∈ CRing )
125 85 62 syl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝑏 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
126 52 101 6 124 104 104 104 108 125 117 mamures ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑏 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
127 123 126 eqtr3d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑏 ∙ 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
128 127 3adant3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( 𝑏 ∙ 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
129 121 oveqd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( 𝑐 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝐺 ) = ( 𝑐 ∙ 𝐺 ) )
130 129 reseq1d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑐 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ∙ 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) )
131 52 101 6 124 104 104 104 108 106 117 mamures ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑐 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
132 130 131 eqtr3d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑐 ∙ 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
133 121 oveqd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( 𝑑 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝐺 ) = ( 𝑑 ∙ 𝐺 ) )
134 133 reseq1d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑑 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑑 ∙ 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) )
135 52 101 6 124 104 104 104 108 114 117 mamures ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑑 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
136 134 135 eqtr3d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑑 ∙ 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
137 132 136 oveq12d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( ( 𝑐 ∙ 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( ( 𝑑 ∙ 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) ) = ( ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ∘f ( +g ‘ 𝑅 ) ( ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ) )
138 137 3adant3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( ( 𝑐 ∙ 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( ( 𝑑 ∙ 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) ) = ( ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ∘f ( +g ‘ 𝑅 ) ( ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ) )
139 120 128 138 3eqtr4d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( 𝑏 ∙ 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( 𝑐 ∙ 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( ( 𝑑 ∙ 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) ) )
140 simp32 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) )
141 140 oveq1d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ( 𝑅 maMul ⟨ ( 𝑁 ∖ { 𝑒 } ) , 𝑁 , 𝑁 ⟩ ) 𝐺 ) = ( ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ( 𝑅 maMul ⟨ ( 𝑁 ∖ { 𝑒 } ) , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
142 122 reseq1d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑏 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( ( 𝑏 ∙ 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) )
143 eqid ⊢ ( 𝑅 maMul ⟨ ( 𝑁 ∖ { 𝑒 } ) , 𝑁 , 𝑁 ⟩ ) = ( 𝑅 maMul ⟨ ( 𝑁 ∖ { 𝑒 } ) , 𝑁 , 𝑁 ⟩ )
144 difssd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( 𝑁 ∖ { 𝑒 } ) ⊆ 𝑁 )
145 52 143 6 124 104 104 104 144 125 117 mamures ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑏 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ( 𝑅 maMul ⟨ ( 𝑁 ∖ { 𝑒 } ) , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
146 142 145 eqtr3d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑏 ∙ 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ( 𝑅 maMul ⟨ ( 𝑁 ∖ { 𝑒 } ) , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
147 146 3adant3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( 𝑏 ∙ 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ( 𝑅 maMul ⟨ ( 𝑁 ∖ { 𝑒 } ) , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
148 129 reseq1d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑐 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( ( 𝑐 ∙ 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) )
149 52 143 6 124 104 104 104 144 106 117 mamures ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑐 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ( 𝑅 maMul ⟨ ( 𝑁 ∖ { 𝑒 } ) , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
150 148 149 eqtr3d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑐 ∙ 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ( 𝑅 maMul ⟨ ( 𝑁 ∖ { 𝑒 } ) , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
151 150 3adant3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( 𝑐 ∙ 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ( 𝑅 maMul ⟨ ( 𝑁 ∖ { 𝑒 } ) , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
152 141 147 151 3eqtr4d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( 𝑏 ∙ 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( ( 𝑐 ∙ 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) )
153 simp33 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) )
154 153 oveq1d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ( 𝑅 maMul ⟨ ( 𝑁 ∖ { 𝑒 } ) , 𝑁 , 𝑁 ⟩ ) 𝐺 ) = ( ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ( 𝑅 maMul ⟨ ( 𝑁 ∖ { 𝑒 } ) , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
155 133 reseq1d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑑 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( ( 𝑑 ∙ 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) )
156 52 143 6 124 104 104 104 144 114 117 mamures ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑑 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ( 𝑅 maMul ⟨ ( 𝑁 ∖ { 𝑒 } ) , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
157 155 156 eqtr3d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑑 ∙ 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ( 𝑅 maMul ⟨ ( 𝑁 ∖ { 𝑒 } ) , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
158 157 3adant3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( 𝑑 ∙ 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ( 𝑅 maMul ⟨ ( 𝑁 ∖ { 𝑒 } ) , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
159 154 147 158 3eqtr4d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( 𝑏 ∙ 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( ( 𝑑 ∙ 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) )
160 3 1 2 9 83 88 92 96 97 139 152 159 mdetrlin ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( 𝐷 ‘ ( 𝑏 ∙ 𝐺 ) ) = ( ( 𝐷 ‘ ( 𝑐 ∙ 𝐺 ) ) ( +g ‘ 𝑅 ) ( 𝐷 ‘ ( 𝑑 ∙ 𝐺 ) ) ) )
161 85 31 syl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑏 ) = ( 𝐷 ‘ ( 𝑏 ∙ 𝐺 ) ) )
162 161 3adant3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑏 ) = ( 𝐷 ‘ ( 𝑏 ∙ 𝐺 ) ) )
163 fvoveq1 ⊢ ( 𝑎 = 𝑐 → ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) = ( 𝐷 ‘ ( 𝑐 ∙ 𝐺 ) ) )
164 fvex ⊢ ( 𝐷 ‘ ( 𝑐 ∙ 𝐺 ) ) ∈ V
165 163 29 164 fvmpt ⊢ ( 𝑐 ∈ 𝐵 → ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑐 ) = ( 𝐷 ‘ ( 𝑐 ∙ 𝐺 ) ) )
166 89 165 syl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑐 ) = ( 𝐷 ‘ ( 𝑐 ∙ 𝐺 ) ) )
167 fvoveq1 ⊢ ( 𝑎 = 𝑑 → ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) = ( 𝐷 ‘ ( 𝑑 ∙ 𝐺 ) ) )
168 fvex ⊢ ( 𝐷 ‘ ( 𝑑 ∙ 𝐺 ) ) ∈ V
169 167 29 168 fvmpt ⊢ ( 𝑑 ∈ 𝐵 → ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑑 ) = ( 𝐷 ‘ ( 𝑑 ∙ 𝐺 ) ) )
170 93 169 syl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑑 ) = ( 𝐷 ‘ ( 𝑑 ∙ 𝐺 ) ) )
171 166 170 oveq12d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑐 ) ( +g ‘ 𝑅 ) ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑑 ) ) = ( ( 𝐷 ‘ ( 𝑐 ∙ 𝐺 ) ) ( +g ‘ 𝑅 ) ( 𝐷 ‘ ( 𝑑 ∙ 𝐺 ) ) ) )
172 171 3adant3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑐 ) ( +g ‘ 𝑅 ) ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑑 ) ) = ( ( 𝐷 ‘ ( 𝑐 ∙ 𝐺 ) ) ( +g ‘ 𝑅 ) ( 𝐷 ‘ ( 𝑑 ∙ 𝐺 ) ) ) )
173 160 162 172 3eqtr4d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑏 ) = ( ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑐 ) ( +g ‘ 𝑅 ) ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑑 ) ) )
174 173 3expia ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑏 ) = ( ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑐 ) ( +g ‘ 𝑅 ) ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑑 ) ) ) )
175 174 anassrs ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) → ( ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑏 ) = ( ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑐 ) ( +g ‘ 𝑅 ) ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑑 ) ) ) )
176 175 ralrimivva ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ∀ 𝑑 ∈ 𝐵 ∀ 𝑒 ∈ 𝑁 ( ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑏 ) = ( ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑐 ) ( +g ‘ 𝑅 ) ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑑 ) ) ) )
177 176 ralrimivva ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ∀ 𝑑 ∈ 𝐵 ∀ 𝑒 ∈ 𝑁 ( ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑐 ↾ ( { 𝑒 } × 𝑁 ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑐 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑏 ) = ( ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑐 ) ( +g ‘ 𝑅 ) ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑑 ) ) ) )
178 simp11 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → 𝑅 ∈ CRing )
179 19 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝐴 ∈ Ring )
180 simprll ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝑏 ∈ 𝐵 )
181 simpl3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝐺 ∈ 𝐵 )
182 179 180 181 37 syl3anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( 𝑏 ∙ 𝐺 ) ∈ 𝐵 )
183 182 3adant3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( 𝑏 ∙ 𝐺 ) ∈ 𝐵 )
184 simp2lr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → 𝑐 ∈ ( Base ‘ 𝑅 ) )
185 simprrl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝑑 ∈ 𝐵 )
186 179 185 181 94 syl3anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( 𝑑 ∙ 𝐺 ) ∈ 𝐵 )
187 186 3adant3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( 𝑑 ∙ 𝐺 ) ∈ 𝐵 )
188 simp2rr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → 𝑒 ∈ 𝑁 )
189 simp3l ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) )
190 189 oveq1d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) = ( ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
191 55 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ∙ )
192 191 oveqd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( 𝑏 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝐺 ) = ( 𝑏 ∙ 𝐺 ) )
193 192 reseq1d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑏 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑏 ∙ 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) )
194 simpl1 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝑅 ∈ CRing )
195 12 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝑁 ∈ Fin )
196 simprrr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝑒 ∈ 𝑁 )
197 196 snssd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → { 𝑒 } ⊆ 𝑁 )
198 180 62 syl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝑏 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
199 65 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝐺 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
200 52 101 6 194 195 195 195 197 198 199 mamures ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑏 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
201 193 200 eqtr3d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑏 ∙ 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
202 201 3adant3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( 𝑏 ∙ 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
203 191 oveqd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( 𝑑 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝐺 ) = ( 𝑑 ∙ 𝐺 ) )
204 203 reseq1d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑑 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑑 ∙ 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) )
205 185 113 syl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝑑 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
206 52 101 6 194 195 195 195 197 205 199 mamures ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑑 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
207 204 206 eqtr3d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑑 ∙ 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
208 207 oveq2d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( ( 𝑑 ∙ 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ) )
209 14 adantr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝑅 ∈ Ring )
210 102 a1i ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → { 𝑒 } ∈ Fin )
211 simprlr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → 𝑐 ∈ ( Base ‘ 𝑅 ) )
212 197 109 syl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( { 𝑒 } × 𝑁 ) ⊆ ( 𝑁 × 𝑁 ) )
213 205 212 115 syl2anc ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m ( { 𝑒 } × 𝑁 ) ) )
214 6 209 101 210 195 195 4 211 213 199 mamuvs1 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ) )
215 208 214 eqtr4d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( ( 𝑑 ∙ 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) ) = ( ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
216 215 3adant3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( ( 𝑑 ∙ 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) ) = ( ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ( 𝑅 maMul ⟨ { 𝑒 } , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
217 190 202 216 3eqtr4d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( 𝑏 ∙ 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( ( 𝑑 ∙ 𝐺 ) ↾ ( { 𝑒 } × 𝑁 ) ) ) )
218 simp3r ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) )
219 218 oveq1d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ( 𝑅 maMul ⟨ ( 𝑁 ∖ { 𝑒 } ) , 𝑁 , 𝑁 ⟩ ) 𝐺 ) = ( ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ( 𝑅 maMul ⟨ ( 𝑁 ∖ { 𝑒 } ) , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
220 192 reseq1d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑏 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( ( 𝑏 ∙ 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) )
221 difssd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( 𝑁 ∖ { 𝑒 } ) ⊆ 𝑁 )
222 52 143 6 194 195 195 195 221 198 199 mamures ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑏 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ( 𝑅 maMul ⟨ ( 𝑁 ∖ { 𝑒 } ) , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
223 220 222 eqtr3d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑏 ∙ 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ( 𝑅 maMul ⟨ ( 𝑁 ∖ { 𝑒 } ) , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
224 223 3adant3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( 𝑏 ∙ 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ( 𝑅 maMul ⟨ ( 𝑁 ∖ { 𝑒 } ) , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
225 203 reseq1d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑑 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( ( 𝑑 ∙ 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) )
226 52 143 6 194 195 195 195 221 205 199 mamures ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑑 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ( 𝑅 maMul ⟨ ( 𝑁 ∖ { 𝑒 } ) , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
227 225 226 eqtr3d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( 𝑑 ∙ 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ( 𝑅 maMul ⟨ ( 𝑁 ∖ { 𝑒 } ) , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
228 227 3adant3 ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( 𝑑 ∙ 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ( 𝑅 maMul ⟨ ( 𝑁 ∖ { 𝑒 } ) , 𝑁 , 𝑁 ⟩ ) 𝐺 ) )
229 219 224 228 3eqtr4d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( 𝑏 ∙ 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( ( 𝑑 ∙ 𝐺 ) ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) )
230 3 1 2 6 4 178 183 184 187 188 217 229 mdetrsca ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( 𝐷 ‘ ( 𝑏 ∙ 𝐺 ) ) = ( 𝑐 · ( 𝐷 ‘ ( 𝑑 ∙ 𝐺 ) ) ) )
231 simp2ll ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → 𝑏 ∈ 𝐵 )
232 231 31 syl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑏 ) = ( 𝐷 ‘ ( 𝑏 ∙ 𝐺 ) ) )
233 simp2rl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → 𝑑 ∈ 𝐵 )
234 169 oveq2d ⊢ ( 𝑑 ∈ 𝐵 → ( 𝑐 · ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑑 ) ) = ( 𝑐 · ( 𝐷 ‘ ( 𝑑 ∙ 𝐺 ) ) ) )
235 233 234 syl ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( 𝑐 · ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑑 ) ) = ( 𝑐 · ( 𝐷 ‘ ( 𝑑 ∙ 𝐺 ) ) ) )
236 230 232 235 3eqtr4d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ∧ ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑏 ) = ( 𝑐 · ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑑 ) ) )
237 236 3expia ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) ) → ( ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑏 ) = ( 𝑐 · ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑑 ) ) ) )
238 237 anassrs ⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁 ) ) → ( ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑏 ) = ( 𝑐 · ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑑 ) ) ) )
239 238 ralrimivva ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ) → ∀ 𝑑 ∈ 𝐵 ∀ 𝑒 ∈ 𝑁 ( ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑏 ) = ( 𝑐 · ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑑 ) ) ) )
240 239 ralrimivva ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ ( Base ‘ 𝑅 ) ∀ 𝑑 ∈ 𝐵 ∀ 𝑒 ∈ 𝑁 ( ( ( 𝑏 ↾ ( { 𝑒 } × 𝑁 ) ) = ( ( ( { 𝑒 } × 𝑁 ) × { 𝑐 } ) ∘f · ( 𝑑 ↾ ( { 𝑒 } × 𝑁 ) ) ) ∧ ( 𝑏 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) = ( 𝑑 ↾ ( ( 𝑁 ∖ { 𝑒 } ) × 𝑁 ) ) ) → ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑏 ) = ( 𝑐 · ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝑑 ) ) ) )
241 simp2 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐹 ∈ 𝐵 )
242 1 2 6 7 8 9 4 12 14 26 82 177 240 3 51 241 mdetuni0 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝐹 ) = ( ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐷 ‘ 𝐹 ) ) )
243 fvoveq1 ⊢ ( 𝑎 = 𝐹 → ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) = ( 𝐷 ‘ ( 𝐹 ∙ 𝐺 ) ) )
244 fvex ⊢ ( 𝐷 ‘ ( 𝐹 ∙ 𝐺 ) ) ∈ V
245 243 29 244 fvmpt ⊢ ( 𝐹 ∈ 𝐵 → ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝐹 ) = ( 𝐷 ‘ ( 𝐹 ∙ 𝐺 ) ) )
246 245 3ad2ant2 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ 𝐹 ) = ( 𝐷 ‘ ( 𝐹 ∙ 𝐺 ) ) )
247 eqid ⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
248 2 247 ringidcl ⊢ ( 𝐴 ∈ Ring → ( 1r ‘ 𝐴 ) ∈ 𝐵 )
249 fvoveq1 ⊢ ( 𝑎 = ( 1r ‘ 𝐴 ) → ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) = ( 𝐷 ‘ ( ( 1r ‘ 𝐴 ) ∙ 𝐺 ) ) )
250 fvex ⊢ ( 𝐷 ‘ ( ( 1r ‘ 𝐴 ) ∙ 𝐺 ) ) ∈ V
251 249 29 250 fvmpt ⊢ ( ( 1r ‘ 𝐴 ) ∈ 𝐵 → ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ ( 1r ‘ 𝐴 ) ) = ( 𝐷 ‘ ( ( 1r ‘ 𝐴 ) ∙ 𝐺 ) ) )
252 19 248 251 3syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ ( 1r ‘ 𝐴 ) ) = ( 𝐷 ‘ ( ( 1r ‘ 𝐴 ) ∙ 𝐺 ) ) )
253 simp3 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐺 ∈ 𝐵 )
254 2 5 247 ringlidm ⊢ ( ( 𝐴 ∈ Ring ∧ 𝐺 ∈ 𝐵 ) → ( ( 1r ‘ 𝐴 ) ∙ 𝐺 ) = 𝐺 )
255 19 253 254 syl2anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( ( 1r ‘ 𝐴 ) ∙ 𝐺 ) = 𝐺 )
256 255 fveq2d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐷 ‘ ( ( 1r ‘ 𝐴 ) ∙ 𝐺 ) ) = ( 𝐷 ‘ 𝐺 ) )
257 252 256 eqtrd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ ( 1r ‘ 𝐴 ) ) = ( 𝐷 ‘ 𝐺 ) )
258 257 oveq1d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐷 ‘ 𝐹 ) ) = ( ( 𝐷 ‘ 𝐺 ) · ( 𝐷 ‘ 𝐹 ) ) )
259 16 253 ffvelcdmd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐷 ‘ 𝐺 ) ∈ ( Base ‘ 𝑅 ) )
260 16 241 ffvelcdmd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐷 ‘ 𝐹 ) ∈ ( Base ‘ 𝑅 ) )
261 6 4 crngcom ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝐷 ‘ 𝐺 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐷 ‘ 𝐹 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐷 ‘ 𝐺 ) · ( 𝐷 ‘ 𝐹 ) ) = ( ( 𝐷 ‘ 𝐹 ) · ( 𝐷 ‘ 𝐺 ) ) )
262 51 259 260 261 syl3anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝐺 ) · ( 𝐷 ‘ 𝐹 ) ) = ( ( 𝐷 ‘ 𝐹 ) · ( 𝐷 ‘ 𝐺 ) ) )
263 258 262 eqtrd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( ( ( 𝑎 ∈ 𝐵 ↦ ( 𝐷 ‘ ( 𝑎 ∙ 𝐺 ) ) ) ‘ ( 1r ‘ 𝐴 ) ) · ( 𝐷 ‘ 𝐹 ) ) = ( ( 𝐷 ‘ 𝐹 ) · ( 𝐷 ‘ 𝐺 ) ) )
264 242 246 263 3eqtr3d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐷 ‘ ( 𝐹 ∙ 𝐺 ) ) = ( ( 𝐷 ‘ 𝐹 ) · ( 𝐷 ‘ 𝐺 ) ) )