mdetmul - Metamath Proof Explorer

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

Theorem mdetmul 22650

Description: Multiplicativity of the determinant function: the determinant of a matrix product of square matrices equals the product of their determinants. Proposition 4.15 in [Lang] p. 517. (Contributed by Stefan O'Rear, 16-Jul-2018.)

**Hypotheses**
Ref	Expression
mdetmul.a	⊢ 𝐴 = (𝑁 Mat 𝑅)
mdetmul.b	⊢ 𝐵 = (Base‘𝐴)
mdetmul.d	⊢ 𝐷 = (𝑁 maDet 𝑅)
mdetmul.t1	⊢ · = (._r‘𝑅)
mdetmul.t2	⊢ ∙ = (._r‘𝐴)

**Assertion**
Ref	Expression
mdetmul	⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐷‘(𝐹 ∙ 𝐺)) = ((𝐷‘𝐹) · (𝐷‘𝐺)))

Proof of Theorem mdetmul Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 are mutually distinct and distinct from all other variables.

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1537 ∈ wcel 2108 ≠ wne 2946 ∀wral 3067 Vcvv 3488 ∖ cdif 3973 ⊆ wss 3976 {csn 4648 ⟨cotp 4656 ↦ cmpt 5249 × cxp 5698 ↾ cres 5702 ⟶wf 6569 ‘cfv 6573 (class class class)co 7448 ∘_f cof 7712 ↑_m cmap 8884 Fincfn 9003 Basecbs 17258 +_gcplusg 17311 ._rcmulr 17312 0_gc0g 17499 Σ_g cgsu 17500 1_rcur 20208 Ringcrg 20260 CRingccrg 20261 maMul cmmul 22415 Mat cmat 22432 maDet cmdat 22611

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 ax-cnex 11240 ax-resscn 11241 ax-1cn 11242 ax-icn 11243 ax-addcl 11244 ax-addrcl 11245 ax-mulcl 11246 ax-mulrcl 11247 ax-mulcom 11248 ax-addass 11249 ax-mulass 11250 ax-distr 11251 ax-i2m1 11252 ax-1ne0 11253 ax-1rid 11254 ax-rnegex 11255 ax-rrecex 11256 ax-cnre 11257 ax-pre-lttri 11258 ax-pre-lttrn 11259 ax-pre-ltadd 11260 ax-pre-mulgt0 11261 ax-addf 11263 ax-mulf 11264

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-xor 1509 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-tp 4653 df-op 4655 df-ot 4657 df-uni 4932 df-int 4971 df-iun 5017 df-iin 5018 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-se 5653 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-pred 6332 df-ord 6398 df-on 6399 df-lim 6400 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-isom 6582 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-of 7714 df-om 7904 df-1st 8030 df-2nd 8031 df-supp 8202 df-tpos 8267 df-frecs 8322 df-wrecs 8353 df-recs 8427 df-rdg 8466 df-1o 8522 df-2o 8523 df-er 8763 df-map 8886 df-pm 8887 df-ixp 8956 df-en 9004 df-dom 9005 df-sdom 9006 df-fin 9007 df-fsupp 9432 df-sup 9511 df-oi 9579 df-card 10008 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11522 df-neg 11523 df-div 11948 df-nn 12294 df-2 12356 df-3 12357 df-4 12358 df-5 12359 df-6 12360 df-7 12361 df-8 12362 df-9 12363 df-n0 12554 df-xnn0 12626 df-z 12640 df-dec 12759 df-uz 12904 df-rp 13058 df-fz 13568 df-fzo 13712 df-seq 14053 df-exp 14113 df-hash 14380 df-word 14563 df-lsw 14611 df-concat 14619 df-s1 14644 df-substr 14689 df-pfx 14719 df-splice 14798 df-reverse 14807 df-s2 14897 df-struct 17194 df-sets 17211 df-slot 17229 df-ndx 17241 df-base 17259 df-ress 17288 df-plusg 17324 df-mulr 17325 df-starv 17326 df-sca 17327 df-vsca 17328 df-ip 17329 df-tset 17330 df-ple 17331 df-ds 17333 df-unif 17334 df-hom 17335 df-cco 17336 df-0g 17501 df-gsum 17502 df-prds 17507 df-pws 17509 df-mre 17644 df-mrc 17645 df-acs 17647 df-mgm 18678 df-sgrp 18757 df-mnd 18773 df-mhm 18818 df-submnd 18819 df-efmnd 18904 df-grp 18976 df-minusg 18977 df-sbg 18978 df-mulg 19108 df-subg 19163 df-ghm 19253 df-gim 19299 df-cntz 19357 df-oppg 19386 df-symg 19411 df-pmtr 19484 df-psgn 19533 df-evpm 19534 df-cmn 19824 df-abl 19825 df-mgp 20162 df-rng 20180 df-ur 20209 df-srg 20214 df-ring 20262 df-cring 20263 df-oppr 20360 df-dvdsr 20383 df-unit 20384 df-invr 20414 df-dvr 20427 df-rhm 20498 df-subrng 20572 df-subrg 20597 df-drng 20753 df-lmod 20882 df-lss 20953 df-sra 21195 df-rgmod 21196 df-cnfld 21388 df-zring 21481 df-zrh 21537 df-dsmm 21775 df-frlm 21790 df-mamu 22416 df-mat 22433 df-mdet 22612

This theorem is referenced by: matunit 22705 cramerimplem3 22712 matunitlindflem2 37577

W3C validator