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 22759

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 2761	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
4		eqid 2761	. . 3 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
5		eqid 2761	. . 3 ⊢ (1_r‘𝑅) = (1_r‘𝑅)
6		eqid 2761	. . 3 ⊢ (+_g‘𝑅) = (+_g‘𝑅)
7		mdetmul.t1	. . 3 ⊢ · = (._r‘𝑅)
8	1, 2	matrcl 22548	. . . . 5 ⊢ (𝐹 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
9	8	simpld 499	. . . 4 ⊢ (𝐹 ∈ 𝐵 → 𝑁 ∈ Fin)
10	9	3ad2ant2 1150	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝑁 ∈ Fin)
11		crngring 20326	. . . 4 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
12	11	3ad2ant1 1149	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝑅 ∈ Ring)
13		mdetmul.d	. . . . . . . 8 ⊢ 𝐷 = (𝑁 maDet 𝑅)
14	13, 1, 2, 3	mdetf 22731	. . . . . . 7 ⊢ (𝑅 ∈ CRing → 𝐷:𝐵⟶(Base‘𝑅))
15	14	3ad2ant1 1149	. . . . . 6 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐷:𝐵⟶(Base‘𝑅))
16	15	adantr 485	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) → 𝐷:𝐵⟶(Base‘𝑅))
17	1	matring 22579	. . . . . . . 8 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring)
18	10, 12, 17	syl2anc 595	. . . . . . 7 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐴 ∈ Ring)
19	18	adantr 485	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) → 𝐴 ∈ Ring)
20		simpr 489	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) → 𝑎 ∈ 𝐵)
21		simpl3 1210	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) → 𝐺 ∈ 𝐵)
22		mdetmul.t2	. . . . . . 7 ⊢ ∙ = (._r‘𝐴)
23	2, 22	ringcl 20331	. . . . . 6 ⊢ ((𝐴 ∈ Ring ∧ 𝑎 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑎 ∙ 𝐺) ∈ 𝐵)
24	19, 20, 21, 23	syl3anc 1396	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) → (𝑎 ∙ 𝐺) ∈ 𝐵)
25	16, 24	ffvelcdmd 7080	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) → (𝐷‘(𝑎 ∙ 𝐺)) ∈ (Base‘𝑅))
26	25	fmpttd 7110	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺))):𝐵⟶(Base‘𝑅))
27		simp21 1223	. . . . . . 7 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑏 ∈ 𝐵)
28		fvoveq1 7433	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → (𝐷‘(𝑎 ∙ 𝐺)) = (𝐷‘(𝑏 ∙ 𝐺)))
29		eqid 2761	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺))) = (𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))
30		fvex 6894	. . . . . . . 8 ⊢ (𝐷‘(𝑏 ∙ 𝐺)) ∈ V
31	28, 29, 30	fvmpt 6989	. . . . . . 7 ⊢ (𝑏 ∈ 𝐵 → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝐷‘(𝑏 ∙ 𝐺)))
32	27, 31	syl 18	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝐷‘(𝑏 ∙ 𝐺)))
33		simp11 1220	. . . . . . 7 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑅 ∈ CRing)
34	18	adantr 485	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) → 𝐴 ∈ Ring)
35		simpr1 1211	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) → 𝑏 ∈ 𝐵)
36		simpl3 1210	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) → 𝐺 ∈ 𝐵)
37	2, 22	ringcl 20331	. . . . . . . . 9 ⊢ ((𝐴 ∈ Ring ∧ 𝑏 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑏 ∙ 𝐺) ∈ 𝐵)
38	34, 35, 36, 37	syl3anc 1396	. . . . . . . 8 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) → (𝑏 ∙ 𝐺) ∈ 𝐵)
39	38	3adant3 1148	. . . . . . 7 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → (𝑏 ∙ 𝐺) ∈ 𝐵)
40		simp22 1224	. . . . . . 7 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑐 ∈ 𝑁)
41		simp23 1225	. . . . . . 7 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑑 ∈ 𝑁)
42		simp3l 1218	. . . . . . 7 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑐 ≠ 𝑑)
43		simpl3r 1246	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) ∧ 𝑎 ∈ 𝑁) → ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))
44		eqid 2761	. . . . . . . . . . . 12 ⊢ 𝑁 = 𝑁
45		oveq1 7417	. . . . . . . . . . . . 13 ⊢ ((𝑐𝑏𝑒) = (𝑑𝑏𝑒) → ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)) = ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))
46	45	ralimi 3100	. . . . . . . . . . . 12 ⊢ (∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒) → ∀𝑒 ∈ 𝑁 ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)) = ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))
47		mpteq12 5198	. . . . . . . . . . . 12 ⊢ ((𝑁 = 𝑁 ∧ ∀𝑒 ∈ 𝑁 ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)) = ((𝑑𝑏𝑒) · (𝑒𝐺𝑎))) → (𝑒 ∈ 𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎))) = (𝑒 ∈ 𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎))))
48	44, 46, 47	sylancr 598	. . . . . . . . . . 11 ⊢ (∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒) → (𝑒 ∈ 𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎))) = (𝑒 ∈ 𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎))))
49	48	oveq2d 7426	. . . . . . . . . 10 ⊢ (∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒) → (𝑅 Σ_g (𝑒 ∈ 𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)))) = (𝑅 Σ_g (𝑒 ∈ 𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))))
50	43, 49	syl 18	. . . . . . . . 9 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) ∧ 𝑎 ∈ 𝑁) → (𝑅 Σ_g (𝑒 ∈ 𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)))) = (𝑅 Σ_g (𝑒 ∈ 𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))))
51		simp1 1152	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝑅 ∈ CRing)
52		eqid 2761	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)
53	1, 52	matmulr 22574	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (._r‘𝐴))
54	53, 22	eqtr4di 2814	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = ∙ )
55	10, 51, 54	syl2anc 595	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = ∙ )
56	55	ad2antrr 738	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = ∙ )
57	56	oveqd 7427	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) = (𝑏 ∙ 𝐺))
58	57	oveqd 7427	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑐(𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺)𝑎) = (𝑐(𝑏 ∙ 𝐺)𝑎))
59		simpll1 1229	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝑅 ∈ CRing)
60	10	ad2antrr 738	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝑁 ∈ Fin)
61		simplr1 1232	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝑏 ∈ 𝐵)
62	1, 3, 2	matbas2i 22558	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ 𝐵 → 𝑏 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
63	61, 62	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝑏 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
64	1, 3, 2	matbas2i 22558	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ 𝐵 → 𝐺 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
65	64	3ad2ant3 1151	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐺 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
66	65	ad2antrr 738	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝐺 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
67		simplr2 1233	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝑐 ∈ 𝑁)
68		simpr 489	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝑎 ∈ 𝑁)
69	52, 3, 7, 59, 60, 60, 60, 63, 66, 67, 68	mamufv 22530	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑐(𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺)𝑎) = (𝑅 Σ_g (𝑒 ∈ 𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)))))
70	58, 69	eqtr3d 2798	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑐(𝑏 ∙ 𝐺)𝑎) = (𝑅 Σ_g (𝑒 ∈ 𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)))))
71	70	3adantl3 1185	. . . . . . . . 9 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) ∧ 𝑎 ∈ 𝑁) → (𝑐(𝑏 ∙ 𝐺)𝑎) = (𝑅 Σ_g (𝑒 ∈ 𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)))))
72	57	oveqd 7427	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑑(𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺)𝑎) = (𝑑(𝑏 ∙ 𝐺)𝑎))
73		simplr3 1234	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝑑 ∈ 𝑁)
74	52, 3, 7, 59, 60, 60, 60, 63, 66, 73, 68	mamufv 22530	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑑(𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺)𝑎) = (𝑅 Σ_g (𝑒 ∈ 𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))))
75	72, 74	eqtr3d 2798	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑑(𝑏 ∙ 𝐺)𝑎) = (𝑅 Σ_g (𝑒 ∈ 𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))))
76	75	3adantl3 1185	. . . . . . . . 9 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) ∧ 𝑎 ∈ 𝑁) → (𝑑(𝑏 ∙ 𝐺)𝑎) = (𝑅 Σ_g (𝑒 ∈ 𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))))
77	50, 71, 76	3eqtr4d 2806	. . . . . . . 8 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) ∧ 𝑎 ∈ 𝑁) → (𝑐(𝑏 ∙ 𝐺)𝑎) = (𝑑(𝑏 ∙ 𝐺)𝑎))
78	77	ralrimiva 3155	. . . . . . 7 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → ∀𝑎 ∈ 𝑁 (𝑐(𝑏 ∙ 𝐺)𝑎) = (𝑑(𝑏 ∙ 𝐺)𝑎))
79	13, 1, 2, 4, 33, 39, 40, 41, 42, 78	mdetralt 22744	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → (𝐷‘(𝑏 ∙ 𝐺)) = (0_g‘𝑅))
80	32, 79	eqtrd 2796	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (0_g‘𝑅))
81	80	3expia 1137	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) → ((𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒)) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (0_g‘𝑅)))
82	81	ralrimivvva 3209	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝑁 ∀𝑑 ∈ 𝑁 ((𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒)) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (0_g‘𝑅)))
83		simp11 1220	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑅 ∈ CRing)
84	18	adantr 485	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝐴 ∈ Ring)
85		simprll 790	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑏 ∈ 𝐵)
86		simpl3 1210	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝐺 ∈ 𝐵)
87	84, 85, 86, 37	syl3anc 1396	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑏 ∙ 𝐺) ∈ 𝐵)
88	87	3adant3 1148	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ∙ 𝐺) ∈ 𝐵)
89		simprlr 791	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑐 ∈ 𝐵)
90	2, 22	ringcl 20331	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Ring ∧ 𝑐 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑐 ∙ 𝐺) ∈ 𝐵)
91	84, 89, 86, 90	syl3anc 1396	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑐 ∙ 𝐺) ∈ 𝐵)
92	91	3adant3 1148	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑐 ∙ 𝐺) ∈ 𝐵)
93		simprrl 792	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑑 ∈ 𝐵)
94	2, 22	ringcl 20331	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Ring ∧ 𝑑 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑑 ∙ 𝐺) ∈ 𝐵)
95	84, 93, 86, 94	syl3anc 1396	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑑 ∙ 𝐺) ∈ 𝐵)
96	95	3adant3 1148	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑑 ∙ 𝐺) ∈ 𝐵)
97		simp2rr 1260	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑒 ∈ 𝑁)
98		simp31 1226	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))))
99	98	oveq1d 7425	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) = (((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
100	12	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑅 ∈ Ring)
101		eqid 2761	. . . . . . . . . . . . 13 ⊢ (𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩) = (𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)
102		snfi 9039	. . . . . . . . . . . . . 14 ⊢ {𝑒} ∈ Fin
103	102	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → {𝑒} ∈ Fin)
104	10	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑁 ∈ Fin)
105	1, 3, 2	matbas2i 22558	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ∈ 𝐵 → 𝑐 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
106	89, 105	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑐 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
107		simprrr 793	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑒 ∈ 𝑁)
108	107	snssd 4751	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → {𝑒} ⊆ 𝑁)
109		xpss1 5680	. . . . . . . . . . . . . . 15 ⊢ ({𝑒} ⊆ 𝑁 → ({𝑒} × 𝑁) ⊆ (𝑁 × 𝑁))
110	108, 109	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ({𝑒} × 𝑁) ⊆ (𝑁 × 𝑁))
111		elmapssres 8863	. . . . . . . . . . . . . 14 ⊢ ((𝑐 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)) ∧ ({𝑒} × 𝑁) ⊆ (𝑁 × 𝑁)) → (𝑐 ↾ ({𝑒} × 𝑁)) ∈ ((Base‘𝑅) ↑_m ({𝑒} × 𝑁)))
112	106, 110, 111	syl2anc 595	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑐 ↾ ({𝑒} × 𝑁)) ∈ ((Base‘𝑅) ↑_m ({𝑒} × 𝑁)))
113	1, 3, 2	matbas2i 22558	. . . . . . . . . . . . . . 15 ⊢ (𝑑 ∈ 𝐵 → 𝑑 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
114	93, 113	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑑 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
115		elmapssres 8863	. . . . . . . . . . . . . 14 ⊢ ((𝑑 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)) ∧ ({𝑒} × 𝑁) ⊆ (𝑁 × 𝑁)) → (𝑑 ↾ ({𝑒} × 𝑁)) ∈ ((Base‘𝑅) ↑_m ({𝑒} × 𝑁)))
116	114, 110, 115	syl2anc 595	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑑 ↾ ({𝑒} × 𝑁)) ∈ ((Base‘𝑅) ↑_m ({𝑒} × 𝑁)))
117	65	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝐺 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
118	3, 100, 101, 103, 104, 104, 6, 112, 116, 117	mamudi 22539	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) = (((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) ∘_f (+_g‘𝑅)((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
119	118	3adant3 1148	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) = (((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) ∘_f (+_g‘𝑅)((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
120	99, 119	eqtrd 2796	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) = (((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) ∘_f (+_g‘𝑅)((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
121	55	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = ∙ )
122	121	oveqd 7427	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) = (𝑏 ∙ 𝐺))
123	122	reseq1d 5977	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁)))
124		simpl1 1208	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑅 ∈ CRing)
125	85, 62	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑏 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
126	52, 101, 3, 124, 104, 104, 104, 108, 125, 117	mamures 22533	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
127	123, 126	eqtr3d 2798	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
128	127	3adant3 1148	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
129	121	oveqd 7427	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑐(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) = (𝑐 ∙ 𝐺))
130	129	reseq1d 5977	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑐(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑐 ∙ 𝐺) ↾ ({𝑒} × 𝑁)))
131	52, 101, 3, 124, 104, 104, 104, 108, 106, 117	mamures 22533	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑐(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
132	130, 131	eqtr3d 2798	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑐 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
133	121	oveqd 7427	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) = (𝑑 ∙ 𝐺))
134	133	reseq1d 5977	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁)))
135	52, 101, 3, 124, 104, 104, 104, 108, 114, 117	mamures 22533	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
136	134, 135	eqtr3d 2798	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
137	132, 136	oveq12d 7428	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (((𝑐 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁))) = (((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) ∘_f (+_g‘𝑅)((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
138	137	3adant3 1148	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (((𝑐 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁))) = (((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) ∘_f (+_g‘𝑅)((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
139	120, 128, 138	3eqtr4d 2806	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = (((𝑐 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁))))
140		simp32 1227	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
141	140	oveq1d 7425	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺) = ((𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
142	122	reseq1d 5977	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
143		eqid 2761	. . . . . . . . . . . . 13 ⊢ (𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩) = (𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)
144		difssd 4090	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑁 ∖ {𝑒}) ⊆ 𝑁)
145	52, 143, 3, 124, 104, 104, 104, 144, 125, 117	mamures 22533	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
146	142, 145	eqtr3d 2798	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
147	146	3adant3 1148	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
148	129	reseq1d 5977	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑐(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑐 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
149	52, 143, 3, 124, 104, 104, 104, 144, 106, 117	mamures 22533	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑐(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
150	148, 149	eqtr3d 2798	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑐 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
151	150	3adant3 1148	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑐 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
152	141, 147, 151	3eqtr4d 2806	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑐 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
153		simp33 1228	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
154	153	oveq1d 7425	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
155	133	reseq1d 5977	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
156	52, 143, 3, 124, 104, 104, 104, 144, 114, 117	mamures 22533	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
157	155, 156	eqtr3d 2798	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
158	157	3adant3 1148	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
159	154, 147, 158	3eqtr4d 2806	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
160	13, 1, 2, 6, 83, 88, 92, 96, 97, 139, 152, 159	mdetrlin 22738	. . . . . . . 8 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝐷‘(𝑏 ∙ 𝐺)) = ((𝐷‘(𝑐 ∙ 𝐺))(+_g‘𝑅)(𝐷‘(𝑑 ∙ 𝐺))))
161	85, 31	syl 18	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝐷‘(𝑏 ∙ 𝐺)))
162	161	3adant3 1148	. . . . . . . 8 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝐷‘(𝑏 ∙ 𝐺)))
163		fvoveq1 7433	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → (𝐷‘(𝑎 ∙ 𝐺)) = (𝐷‘(𝑐 ∙ 𝐺)))
164		fvex 6894	. . . . . . . . . . . 12 ⊢ (𝐷‘(𝑐 ∙ 𝐺)) ∈ V
165	163, 29, 164	fvmpt 6989	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝐵 → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐) = (𝐷‘(𝑐 ∙ 𝐺)))
166	89, 165	syl 18	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐) = (𝐷‘(𝑐 ∙ 𝐺)))
167		fvoveq1 7433	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑑 → (𝐷‘(𝑎 ∙ 𝐺)) = (𝐷‘(𝑑 ∙ 𝐺)))
168		fvex 6894	. . . . . . . . . . . 12 ⊢ (𝐷‘(𝑑 ∙ 𝐺)) ∈ V
169	167, 29, 168	fvmpt 6989	. . . . . . . . . . 11 ⊢ (𝑑 ∈ 𝐵 → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑) = (𝐷‘(𝑑 ∙ 𝐺)))
170	93, 169	syl 18	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑) = (𝐷‘(𝑑 ∙ 𝐺)))
171	166, 170	oveq12d 7428	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐)(+_g‘𝑅)((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑)) = ((𝐷‘(𝑐 ∙ 𝐺))(+_g‘𝑅)(𝐷‘(𝑑 ∙ 𝐺))))
172	171	3adant3 1148	. . . . . . . 8 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐)(+_g‘𝑅)((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑)) = ((𝐷‘(𝑐 ∙ 𝐺))(+_g‘𝑅)(𝐷‘(𝑑 ∙ 𝐺))))
173	160, 162, 172	3eqtr4d 2806	. . . . . . 7 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐)(+_g‘𝑅)((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑)))
174	173	3expia 1137	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐)(+_g‘𝑅)((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑))))
175	174	anassrs 472	. . . . 5 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) → (((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐)(+_g‘𝑅)((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑))))
176	175	ralrimivva 3206	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → ∀𝑑 ∈ 𝐵 ∀𝑒 ∈ 𝑁 (((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐)(+_g‘𝑅)((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑))))
177	176	ralrimivva 3206	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑑 ∈ 𝐵 ∀𝑒 ∈ 𝑁 (((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐)(+_g‘𝑅)((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑))))
178		simp11 1220	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑅 ∈ CRing)
179	18	adantr 485	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝐴 ∈ Ring)
180		simprll 790	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑏 ∈ 𝐵)
181		simpl3 1210	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝐺 ∈ 𝐵)
182	179, 180, 181, 37	syl3anc 1396	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑏 ∙ 𝐺) ∈ 𝐵)
183	182	3adant3 1148	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ∙ 𝐺) ∈ 𝐵)
184		simp2lr 1258	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑐 ∈ (Base‘𝑅))
185		simprrl 792	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑑 ∈ 𝐵)
186	179, 185, 181, 94	syl3anc 1396	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑑 ∙ 𝐺) ∈ 𝐵)
187	186	3adant3 1148	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑑 ∙ 𝐺) ∈ 𝐵)
188		simp2rr 1260	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑒 ∈ 𝑁)
189		simp3l 1218	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))))
190	189	oveq1d 7425	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) = (((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
191	55	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = ∙ )
192	191	oveqd 7427	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) = (𝑏 ∙ 𝐺))
193	192	reseq1d 5977	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁)))
194		simpl1 1208	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑅 ∈ CRing)
195	10	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑁 ∈ Fin)
196		simprrr 793	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑒 ∈ 𝑁)
197	196	snssd 4751	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → {𝑒} ⊆ 𝑁)
198	180, 62	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑏 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
199	65	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝐺 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
200	52, 101, 3, 194, 195, 195, 195, 197, 198, 199	mamures 22533	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
201	193, 200	eqtr3d 2798	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
202	201	3adant3 1148	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
203	191	oveqd 7427	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) = (𝑑 ∙ 𝐺))
204	203	reseq1d 5977	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁)))
205	185, 113	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑑 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
206	52, 101, 3, 194, 195, 195, 195, 197, 205, 199	mamures 22533	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
207	204, 206	eqtr3d 2798	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
208	207	oveq2d 7426	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((({𝑒} × 𝑁) × {𝑐}) ∘_f · ((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁))) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
209	12	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑅 ∈ Ring)
210	102	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → {𝑒} ∈ Fin)
211		simprlr 791	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑐 ∈ (Base‘𝑅))
212	197, 109	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ({𝑒} × 𝑁) ⊆ (𝑁 × 𝑁))
213	205, 212, 115	syl2anc 595	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑑 ↾ ({𝑒} × 𝑁)) ∈ ((Base‘𝑅) ↑_m ({𝑒} × 𝑁)))
214	3, 209, 101, 210, 195, 195, 7, 211, 213, 199	mamuvs1 22541	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
215	208, 214	eqtr4d 2799	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((({𝑒} × 𝑁) × {𝑐}) ∘_f · ((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁))) = (((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
216	215	3adant3 1148	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((({𝑒} × 𝑁) × {𝑐}) ∘_f · ((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁))) = (((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
217	190, 202, 216	3eqtr4d 2806	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · ((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁))))
218		simp3r 1219	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
219	218	oveq1d 7425	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
220	192	reseq1d 5977	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
221		difssd 4090	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑁 ∖ {𝑒}) ⊆ 𝑁)
222	52, 143, 3, 194, 195, 195, 195, 221, 198, 199	mamures 22533	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
223	220, 222	eqtr3d 2798	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
224	223	3adant3 1148	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
225	203	reseq1d 5977	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
226	52, 143, 3, 194, 195, 195, 195, 221, 205, 199	mamures 22533	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
227	225, 226	eqtr3d 2798	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
228	227	3adant3 1148	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
229	219, 224, 228	3eqtr4d 2806	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
230	13, 1, 2, 3, 7, 178, 183, 184, 187, 188, 217, 229	mdetrsca 22739	. . . . . . . 8 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝐷‘(𝑏 ∙ 𝐺)) = (𝑐 · (𝐷‘(𝑑 ∙ 𝐺))))
231		simp2ll 1257	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑏 ∈ 𝐵)
232	231, 31	syl 18	. . . . . . . 8 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝐷‘(𝑏 ∙ 𝐺)))
233		simp2rl 1259	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑑 ∈ 𝐵)
234	169	oveq2d 7426	. . . . . . . . 9 ⊢ (𝑑 ∈ 𝐵 → (𝑐 · ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑)) = (𝑐 · (𝐷‘(𝑑 ∙ 𝐺))))
235	233, 234	syl 18	. . . . . . . 8 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑐 · ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑)) = (𝑐 · (𝐷‘(𝑑 ∙ 𝐺))))
236	230, 232, 235	3eqtr4d 2806	. . . . . . 7 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝑐 · ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑)))
237	236	3expia 1137	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝑐 · ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑))))
238	237	anassrs 472	. . . . 5 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) → (((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝑐 · ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑))))
239	238	ralrimivva 3206	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅))) → ∀𝑑 ∈ 𝐵 ∀𝑒 ∈ 𝑁 (((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝑐 · ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑))))
240	239	ralrimivva 3206	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ (Base‘𝑅)∀𝑑 ∈ 𝐵 ∀𝑒 ∈ 𝑁 (((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝑐 · ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑))))
241		simp2 1153	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐹 ∈ 𝐵)
242	1, 2, 3, 4, 5, 6, 7, 10, 12, 26, 82, 177, 240, 13, 51, 241	mdetuni0 22757	. 2 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝐹) = (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘(1_r‘𝐴)) · (𝐷‘𝐹)))
243		fvoveq1 7433	. . . 4 ⊢ (𝑎 = 𝐹 → (𝐷‘(𝑎 ∙ 𝐺)) = (𝐷‘(𝐹 ∙ 𝐺)))
244		fvex 6894	. . . 4 ⊢ (𝐷‘(𝐹 ∙ 𝐺)) ∈ V
245	243, 29, 244	fvmpt 6989	. . 3 ⊢ (𝐹 ∈ 𝐵 → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝐹) = (𝐷‘(𝐹 ∙ 𝐺)))
246	245	3ad2ant2 1150	. 2 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝐹) = (𝐷‘(𝐹 ∙ 𝐺)))
247		eqid 2761	. . . . . . 7 ⊢ (1_r‘𝐴) = (1_r‘𝐴)
248	2, 247	ringidcl 20347	. . . . . 6 ⊢ (𝐴 ∈ Ring → (1_r‘𝐴) ∈ 𝐵)
249		fvoveq1 7433	. . . . . . 7 ⊢ (𝑎 = (1_r‘𝐴) → (𝐷‘(𝑎 ∙ 𝐺)) = (𝐷‘((1_r‘𝐴) ∙ 𝐺)))
250		fvex 6894	. . . . . . 7 ⊢ (𝐷‘((1_r‘𝐴) ∙ 𝐺)) ∈ V
251	249, 29, 250	fvmpt 6989	. . . . . 6 ⊢ ((1_r‘𝐴) ∈ 𝐵 → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘(1_r‘𝐴)) = (𝐷‘((1_r‘𝐴) ∙ 𝐺)))
252	18, 248, 251	3syl 19	. . . . 5 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘(1_r‘𝐴)) = (𝐷‘((1_r‘𝐴) ∙ 𝐺)))
253		simp3 1154	. . . . . . 7 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐺 ∈ 𝐵)
254	2, 22, 247	ringlidm 20351	. . . . . . 7 ⊢ ((𝐴 ∈ Ring ∧ 𝐺 ∈ 𝐵) → ((1_r‘𝐴) ∙ 𝐺) = 𝐺)
255	18, 253, 254	syl2anc 595	. . . . . 6 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((1_r‘𝐴) ∙ 𝐺) = 𝐺)
256	255	fveq2d 6885	. . . . 5 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐷‘((1_r‘𝐴) ∙ 𝐺)) = (𝐷‘𝐺))
257	252, 256	eqtrd 2796	. . . 4 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘(1_r‘𝐴)) = (𝐷‘𝐺))
258	257	oveq1d 7425	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘(1_r‘𝐴)) · (𝐷‘𝐹)) = ((𝐷‘𝐺) · (𝐷‘𝐹)))
259	15, 253	ffvelcdmd 7080	. . . 4 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐷‘𝐺) ∈ (Base‘𝑅))
260	15, 241	ffvelcdmd 7080	. . . 4 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐷‘𝐹) ∈ (Base‘𝑅))
261	3, 7	crngcom 20332	. . . 4 ⊢ ((𝑅 ∈ CRing ∧ (𝐷‘𝐺) ∈ (Base‘𝑅) ∧ (𝐷‘𝐹) ∈ (Base‘𝑅)) → ((𝐷‘𝐺) · (𝐷‘𝐹)) = ((𝐷‘𝐹) · (𝐷‘𝐺)))
262	51, 259, 260, 261	syl3anc 1396	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝐷‘𝐺) · (𝐷‘𝐹)) = ((𝐷‘𝐹) · (𝐷‘𝐺)))
263	258, 262	eqtrd 2796	. 2 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘(1_r‘𝐴)) · (𝐷‘𝐹)) = ((𝐷‘𝐹) · (𝐷‘𝐺)))
264	242, 246, 263	3eqtr3d 2804	1 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐷‘(𝐹 ∙ 𝐺)) = ((𝐷‘𝐹) · (𝐷‘𝐺)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 ∧ w3a 1101 = wceq 1568 ∈ wcel 2141 ≠ wne 2956 ∀wral 3077 Vcvv 3453 ∖ cdif 3901 ⊆ wss 3904 {csn 4588 ⟨cotp 4596 ↦ cmpt 5191 × cxp 5659 ↾ cres 5663 ⟶wf 6532 ‘cfv 6536 (class class class)co 7410 ∘_f cof 7672 ↑_m cmap 8823 Fincfn 8942 Basecbs 17268 +_gcplusg 17309 ._rcmulr 17310 0_gc0g 17491 Σ_g cgsu 17492 1_rcur 20262 Ringcrg 20314 CRingccrg 20315 maMul cmmul 22526 Mat cmat 22543 maDet cmdat 22720

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1823 ax-4 1837 ax-5 1938 ax-6 1995 ax-7 2036 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11155 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 ax-pre-mulgt0 11176 ax-addf 11178 ax-mulf 11179

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-xor 1540 df-tru 1571 df-fal 1581 df-ex 1808 df-nf 1812 df-sb 2095 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4595 df-ot 4597 df-uni 4872 df-int 4912 df-iun 4957 df-iin 4958 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-se 5615 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-of 7674 df-om 7862 df-1st 7985 df-2nd 7986 df-supp 8156 df-tpos 8221 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8452 df-2o 8453 df-er 8693 df-map 8825 df-pm 8826 df-ixp 8895 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-fsupp 9321 df-sup 9401 df-oi 9471 df-card 9924 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-sub 11442 df-neg 11443 df-div 11871 df-nn 12233 df-2 12302 df-3 12303 df-4 12304 df-5 12305 df-6 12306 df-7 12307 df-8 12308 df-9 12309 df-n0 12504 df-xnn0 12577 df-z 12591 df-dec 12711 df-uz 12862 df-rp 13016 df-fz 13535 df-fzo 13682 df-seq 14037 df-exp 14097 df-hash 14366 df-word 14550 df-lsw 14599 df-concat 14607 df-s1 14633 df-substr 14678 df-pfx 14708 df-splice 14786 df-reverse 14795 df-s2 14884 df-struct 17206 df-sets 17223 df-slot 17241 df-ndx 17253 df-base 17269 df-ress 17290 df-plusg 17322 df-mulr 17323 df-starv 17324 df-sca 17325 df-vsca 17326 df-ip 17327 df-tset 17328 df-ple 17329 df-ds 17331 df-unif 17332 df-hom 17333 df-cco 17334 df-0g 17493 df-gsum 17494 df-prds 17499 df-pws 17501 df-mre 17637 df-mrc 17638 df-acs 17640 df-mgm 18697 df-sgrp 18776 df-mnd 18792 df-mhm 18840 df-submnd 18841 df-efmnd 18927 df-grp 19002 df-minusg 19003 df-sbg 19004 df-mulg 19133 df-subg 19188 df-ghm 19283 df-gim 19328 df-cntz 19386 df-oppg 19415 df-symg 19439 df-pmtr 19511 df-psgn 19560 df-evpm 19561 df-cmn 19851 df-abl 19852 df-mgp 20216 df-rng 20230 df-ur 20263 df-srg 20268 df-ring 20316 df-cring 20317 df-oppr 20418 df-dvdsr 20438 df-unit 20439 df-invr 20469 df-dvr 20482 df-rhm 20553 df-subrng 20630 df-subrg 20654 df-drng 20814 df-lmod 20962 df-lss 21032 df-sra 21273 df-rgmod 21274 df-cnfld 21502 df-zring 21576 df-zrh 21632 df-dsmm 21861 df-frlm 21876 df-mamu 22527 df-mat 22544 df-mdet 22721

This theorem is referenced by: matunit 22814 cramerimplem3 22821 matunitlindflem2 38212

W3C validator