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 ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐷 ‘ ( 𝐹 ∙ 𝐺 ) ) = ( ( 𝐷 ‘ 𝐹 ) · ( 𝐷 ‘ 𝐺 ) ) )