Theorem mdetmul 22435

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 2724	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
4		eqid 2724	. . 3 ⊢ (0g‘𝑅) = (0g‘𝑅)
5		eqid 2724	. . 3 ⊢ (1r‘𝑅) = (1r‘𝑅)
6		eqid 2724	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
7		mdetmul.t1	. . 3 ⊢ · = (.r‘𝑅)
8	1, 2	matrcl 22222	. . . . 5 ⊢ (𝐹 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
9	8	simpld 494	. . . 4 ⊢ (𝐹 ∈ 𝐵 → 𝑁 ∈ Fin)
10	9	3ad2ant2 1131	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝑁 ∈ Fin)
11		crngring 20135	. . . 4 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
12	11	3ad2ant1 1130	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝑅 ∈ Ring)
13		mdetmul.d	. . . . . . . 8 ⊢ 𝐷 = (𝑁 maDet 𝑅)
14	13, 1, 2, 3	mdetf 22407	. . . . . . 7 ⊢ (𝑅 ∈ CRing → 𝐷:𝐵⟶(Base‘𝑅))
15	14	3ad2ant1 1130	. . . . . 6 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐷:𝐵⟶(Base‘𝑅))
16	15	adantr 480	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) → 𝐷:𝐵⟶(Base‘𝑅))
17	1	matring 22255	. . . . . . . 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 1190	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) → 𝐺 ∈ 𝐵)
22		mdetmul.t2	. . . . . . 7 ⊢ ∙ = (.r‘𝐴)
23	2, 22	ringcl 20140	. . . . . 6 ⊢ ((𝐴 ∈ Ring ∧ 𝑎 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑎 ∙ 𝐺) ∈ 𝐵)
24	19, 20, 21, 23	syl3anc 1368	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) → (𝑎 ∙ 𝐺) ∈ 𝐵)
25	16, 24	ffvelcdmd 7077	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) → (𝐷‘(𝑎 ∙ 𝐺)) ∈ (Base‘𝑅))
26	25	fmpttd 7106	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺))):𝐵⟶(Base‘𝑅))
27		simp21 1203	. . . . . . 7 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑏 ∈ 𝐵)
28		fvoveq1 7424	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → (𝐷‘(𝑎 ∙ 𝐺)) = (𝐷‘(𝑏 ∙ 𝐺)))
29		eqid 2724	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺))) = (𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))
30		fvex 6894	. . . . . . . 8 ⊢ (𝐷‘(𝑏 ∙ 𝐺)) ∈ V
31	28, 29, 30	fvmpt 6988	. . . . . . 7 ⊢ (𝑏 ∈ 𝐵 → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝐷‘(𝑏 ∙ 𝐺)))
32	27, 31	syl 17	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝐷‘(𝑏 ∙ 𝐺)))
33		simp11 1200	. . . . . . 7 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑅 ∈ CRing)
34	18	adantr 480	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) → 𝐴 ∈ Ring)
35		simpr1 1191	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) → 𝑏 ∈ 𝐵)
36		simpl3 1190	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) → 𝐺 ∈ 𝐵)
37	2, 22	ringcl 20140	. . . . . . . . 9 ⊢ ((𝐴 ∈ Ring ∧ 𝑏 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑏 ∙ 𝐺) ∈ 𝐵)
38	34, 35, 36, 37	syl3anc 1368	. . . . . . . 8 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) → (𝑏 ∙ 𝐺) ∈ 𝐵)
39	38	3adant3 1129	. . . . . . 7 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → (𝑏 ∙ 𝐺) ∈ 𝐵)
40		simp22 1204	. . . . . . 7 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑐 ∈ 𝑁)
41		simp23 1205	. . . . . . 7 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑑 ∈ 𝑁)
42		simp3l 1198	. . . . . . 7 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑐 ≠ 𝑑)
43		simpl3r 1226	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) ∧ 𝑎 ∈ 𝑁) → ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))
44		eqid 2724	. . . . . . . . . . . 12 ⊢ 𝑁 = 𝑁
45		oveq1 7408	. . . . . . . . . . . . 13 ⊢ ((𝑐𝑏𝑒) = (𝑑𝑏𝑒) → ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)) = ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))
46	45	ralimi 3075	. . . . . . . . . . . 12 ⊢ (∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒) → ∀𝑒 ∈ 𝑁 ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)) = ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))
47		mpteq12 5230	. . . . . . . . . . . 12 ⊢ ((𝑁 = 𝑁 ∧ ∀𝑒 ∈ 𝑁 ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)) = ((𝑑𝑏𝑒) · (𝑒𝐺𝑎))) → (𝑒 ∈ 𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎))) = (𝑒 ∈ 𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎))))
48	44, 46, 47	sylancr 586	. . . . . . . . . . 11 ⊢ (∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒) → (𝑒 ∈ 𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎))) = (𝑒 ∈ 𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎))))
49	48	oveq2d 7417	. . . . . . . . . 10 ⊢ (∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒) → (𝑅 Σg (𝑒 ∈ 𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)))) = (𝑅 Σg (𝑒 ∈ 𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))))
50	43, 49	syl 17	. . . . . . . . 9 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) ∧ 𝑎 ∈ 𝑁) → (𝑅 Σg (𝑒 ∈ 𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)))) = (𝑅 Σg (𝑒 ∈ 𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))))
51		simp1 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝑅 ∈ CRing)
52		eqid 2724	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)
53	1, 52	matmulr 22250	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (.r‘𝐴))
54	53, 22	eqtr4di 2782	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = ∙ )
55	10, 51, 54	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = ∙ )
56	55	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = ∙ )
57	56	oveqd 7418	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) = (𝑏 ∙ 𝐺))
58	57	oveqd 7418	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑐(𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺)𝑎) = (𝑐(𝑏 ∙ 𝐺)𝑎))
59		simpll1 1209	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝑅 ∈ CRing)
60	10	ad2antrr 723	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝑁 ∈ Fin)
61		simplr1 1212	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝑏 ∈ 𝐵)
62	1, 3, 2	matbas2i 22234	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ 𝐵 → 𝑏 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
63	61, 62	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝑏 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
64	1, 3, 2	matbas2i 22234	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ 𝐵 → 𝐺 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
65	64	3ad2ant3 1132	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐺 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
66	65	ad2antrr 723	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝐺 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
67		simplr2 1213	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝑐 ∈ 𝑁)
68		simpr 484	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝑎 ∈ 𝑁)
69	52, 3, 7, 59, 60, 60, 60, 63, 66, 67, 68	mamufv 22199	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑐(𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺)𝑎) = (𝑅 Σg (𝑒 ∈ 𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)))))
70	58, 69	eqtr3d 2766	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑐(𝑏 ∙ 𝐺)𝑎) = (𝑅 Σg (𝑒 ∈ 𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)))))
71	70	3adantl3 1165	. . . . . . . . 9 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) ∧ 𝑎 ∈ 𝑁) → (𝑐(𝑏 ∙ 𝐺)𝑎) = (𝑅 Σg (𝑒 ∈ 𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)))))
72	57	oveqd 7418	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑑(𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺)𝑎) = (𝑑(𝑏 ∙ 𝐺)𝑎))
73		simplr3 1214	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝑑 ∈ 𝑁)
74	52, 3, 7, 59, 60, 60, 60, 63, 66, 73, 68	mamufv 22199	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑑(𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺)𝑎) = (𝑅 Σg (𝑒 ∈ 𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))))
75	72, 74	eqtr3d 2766	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑑(𝑏 ∙ 𝐺)𝑎) = (𝑅 Σg (𝑒 ∈ 𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))))
76	75	3adantl3 1165	. . . . . . . . 9 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) ∧ 𝑎 ∈ 𝑁) → (𝑑(𝑏 ∙ 𝐺)𝑎) = (𝑅 Σg (𝑒 ∈ 𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))))
77	50, 71, 76	3eqtr4d 2774	. . . . . . . 8 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) ∧ 𝑎 ∈ 𝑁) → (𝑐(𝑏 ∙ 𝐺)𝑎) = (𝑑(𝑏 ∙ 𝐺)𝑎))
78	77	ralrimiva 3138	. . . . . . 7 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → ∀𝑎 ∈ 𝑁 (𝑐(𝑏 ∙ 𝐺)𝑎) = (𝑑(𝑏 ∙ 𝐺)𝑎))
79	13, 1, 2, 4, 33, 39, 40, 41, 42, 78	mdetralt 22420	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → (𝐷‘(𝑏 ∙ 𝐺)) = (0g‘𝑅))
80	32, 79	eqtrd 2764	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (0g‘𝑅))
81	80	3expia 1118	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) → ((𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒)) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (0g‘𝑅)))
82	81	ralrimivvva 3195	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝑁 ∀𝑑 ∈ 𝑁 ((𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒)) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (0g‘𝑅)))
83		simp11 1200	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑅 ∈ CRing)
84	18	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝐴 ∈ Ring)
85		simprll 776	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑏 ∈ 𝐵)
86		simpl3 1190	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝐺 ∈ 𝐵)
87	84, 85, 86, 37	syl3anc 1368	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑏 ∙ 𝐺) ∈ 𝐵)
88	87	3adant3 1129	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ∙ 𝐺) ∈ 𝐵)
89		simprlr 777	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑐 ∈ 𝐵)
90	2, 22	ringcl 20140	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Ring ∧ 𝑐 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑐 ∙ 𝐺) ∈ 𝐵)
91	84, 89, 86, 90	syl3anc 1368	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑐 ∙ 𝐺) ∈ 𝐵)
92	91	3adant3 1129	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑐 ∙ 𝐺) ∈ 𝐵)
93		simprrl 778	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑑 ∈ 𝐵)
94	2, 22	ringcl 20140	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Ring ∧ 𝑑 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑑 ∙ 𝐺) ∈ 𝐵)
95	84, 93, 86, 94	syl3anc 1368	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑑 ∙ 𝐺) ∈ 𝐵)
96	95	3adant3 1129	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑑 ∙ 𝐺) ∈ 𝐵)
97		simp2rr 1240	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑒 ∈ 𝑁)
98		simp31 1206	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))))
99	98	oveq1d 7416	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) = (((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
100	12	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑅 ∈ Ring)
101		eqid 2724	. . . . . . . . . . . . 13 ⊢ (𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩) = (𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)
102		snfi 9039	. . . . . . . . . . . . . 14 ⊢ {𝑒} ∈ Fin
103	102	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → {𝑒} ∈ Fin)
104	10	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑁 ∈ Fin)
105	1, 3, 2	matbas2i 22234	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ∈ 𝐵 → 𝑐 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
106	89, 105	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑐 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
107		simprrr 779	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑒 ∈ 𝑁)
108	107	snssd 4804	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → {𝑒} ⊆ 𝑁)
109		xpss1 5685	. . . . . . . . . . . . . . 15 ⊢ ({𝑒} ⊆ 𝑁 → ({𝑒} × 𝑁) ⊆ (𝑁 × 𝑁))
110	108, 109	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ({𝑒} × 𝑁) ⊆ (𝑁 × 𝑁))
111		elmapssres 8856	. . . . . . . . . . . . . 14 ⊢ ((𝑐 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) ∧ ({𝑒} × 𝑁) ⊆ (𝑁 × 𝑁)) → (𝑐 ↾ ({𝑒} × 𝑁)) ∈ ((Base‘𝑅) ↑m ({𝑒} × 𝑁)))
112	106, 110, 111	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑐 ↾ ({𝑒} × 𝑁)) ∈ ((Base‘𝑅) ↑m ({𝑒} × 𝑁)))
113	1, 3, 2	matbas2i 22234	. . . . . . . . . . . . . . 15 ⊢ (𝑑 ∈ 𝐵 → 𝑑 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
114	93, 113	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑑 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
115		elmapssres 8856	. . . . . . . . . . . . . 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 22213	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) = (((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) ∘f (+g‘𝑅)((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
119	118	3adant3 1129	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) = (((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) ∘f (+g‘𝑅)((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
120	99, 119	eqtrd 2764	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) = (((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) ∘f (+g‘𝑅)((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
121	55	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = ∙ )
122	121	oveqd 7418	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) = (𝑏 ∙ 𝐺))
123	122	reseq1d 5970	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁)))
124		simpl1 1188	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑅 ∈ CRing)
125	85, 62	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑏 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
126	52, 101, 3, 124, 104, 104, 104, 108, 125, 117	mamures 22202	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
127	123, 126	eqtr3d 2766	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
128	127	3adant3 1129	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
129	121	oveqd 7418	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑐(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) = (𝑐 ∙ 𝐺))
130	129	reseq1d 5970	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑐(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑐 ∙ 𝐺) ↾ ({𝑒} × 𝑁)))
131	52, 101, 3, 124, 104, 104, 104, 108, 106, 117	mamures 22202	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑐(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
132	130, 131	eqtr3d 2766	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑐 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
133	121	oveqd 7418	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) = (𝑑 ∙ 𝐺))
134	133	reseq1d 5970	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁)))
135	52, 101, 3, 124, 104, 104, 104, 108, 114, 117	mamures 22202	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
136	134, 135	eqtr3d 2766	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
137	132, 136	oveq12d 7419	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (((𝑐 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁))) = (((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) ∘f (+g‘𝑅)((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
138	137	3adant3 1129	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (((𝑐 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁))) = (((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) ∘f (+g‘𝑅)((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
139	120, 128, 138	3eqtr4d 2774	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = (((𝑐 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁))))
140		simp32 1207	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
141	140	oveq1d 7416	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺) = ((𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
142	122	reseq1d 5970	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
143		eqid 2724	. . . . . . . . . . . . 13 ⊢ (𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩) = (𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)
144		difssd 4124	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑁 ∖ {𝑒}) ⊆ 𝑁)
145	52, 143, 3, 124, 104, 104, 104, 144, 125, 117	mamures 22202	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
146	142, 145	eqtr3d 2766	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
147	146	3adant3 1129	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
148	129	reseq1d 5970	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑐(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑐 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
149	52, 143, 3, 124, 104, 104, 104, 144, 106, 117	mamures 22202	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑐(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
150	148, 149	eqtr3d 2766	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑐 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
151	150	3adant3 1129	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑐 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
152	141, 147, 151	3eqtr4d 2774	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑐 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
153		simp33 1208	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
154	153	oveq1d 7416	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
155	133	reseq1d 5970	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
156	52, 143, 3, 124, 104, 104, 104, 144, 114, 117	mamures 22202	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
157	155, 156	eqtr3d 2766	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
158	157	3adant3 1129	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
159	154, 147, 158	3eqtr4d 2774	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
160	13, 1, 2, 6, 83, 88, 92, 96, 97, 139, 152, 159	mdetrlin 22414	. . . . . . . 8 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝐷‘(𝑏 ∙ 𝐺)) = ((𝐷‘(𝑐 ∙ 𝐺))(+g‘𝑅)(𝐷‘(𝑑 ∙ 𝐺))))
161	85, 31	syl 17	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝐷‘(𝑏 ∙ 𝐺)))
162	161	3adant3 1129	. . . . . . . 8 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝐷‘(𝑏 ∙ 𝐺)))
163		fvoveq1 7424	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → (𝐷‘(𝑎 ∙ 𝐺)) = (𝐷‘(𝑐 ∙ 𝐺)))
164		fvex 6894	. . . . . . . . . . . 12 ⊢ (𝐷‘(𝑐 ∙ 𝐺)) ∈ V
165	163, 29, 164	fvmpt 6988	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝐵 → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐) = (𝐷‘(𝑐 ∙ 𝐺)))
166	89, 165	syl 17	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐) = (𝐷‘(𝑐 ∙ 𝐺)))
167		fvoveq1 7424	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑑 → (𝐷‘(𝑎 ∙ 𝐺)) = (𝐷‘(𝑑 ∙ 𝐺)))
168		fvex 6894	. . . . . . . . . . . 12 ⊢ (𝐷‘(𝑑 ∙ 𝐺)) ∈ V
169	167, 29, 168	fvmpt 6988	. . . . . . . . . . 11 ⊢ (𝑑 ∈ 𝐵 → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑) = (𝐷‘(𝑑 ∙ 𝐺)))
170	93, 169	syl 17	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑) = (𝐷‘(𝑑 ∙ 𝐺)))
171	166, 170	oveq12d 7419	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐)(+g‘𝑅)((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑)) = ((𝐷‘(𝑐 ∙ 𝐺))(+g‘𝑅)(𝐷‘(𝑑 ∙ 𝐺))))
172	171	3adant3 1129	. . . . . . . 8 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐)(+g‘𝑅)((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑)) = ((𝐷‘(𝑐 ∙ 𝐺))(+g‘𝑅)(𝐷‘(𝑑 ∙ 𝐺))))
173	160, 162, 172	3eqtr4d 2774	. . . . . . 7 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐)(+g‘𝑅)((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑)))
174	173	3expia 1118	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐)(+g‘𝑅)((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑))))
175	174	anassrs 467	. . . . 5 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) → (((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐)(+g‘𝑅)((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑))))
176	175	ralrimivva 3192	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → ∀𝑑 ∈ 𝐵 ∀𝑒 ∈ 𝑁 (((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐)(+g‘𝑅)((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑))))
177	176	ralrimivva 3192	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑑 ∈ 𝐵 ∀𝑒 ∈ 𝑁 (((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘f (+g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐)(+g‘𝑅)((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑))))
178		simp11 1200	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑅 ∈ CRing)
179	18	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝐴 ∈ Ring)
180		simprll 776	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑏 ∈ 𝐵)
181		simpl3 1190	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝐺 ∈ 𝐵)
182	179, 180, 181, 37	syl3anc 1368	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑏 ∙ 𝐺) ∈ 𝐵)
183	182	3adant3 1129	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ∙ 𝐺) ∈ 𝐵)
184		simp2lr 1238	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑐 ∈ (Base‘𝑅))
185		simprrl 778	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑑 ∈ 𝐵)
186	179, 185, 181, 94	syl3anc 1368	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑑 ∙ 𝐺) ∈ 𝐵)
187	186	3adant3 1129	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑑 ∙ 𝐺) ∈ 𝐵)
188		simp2rr 1240	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑒 ∈ 𝑁)
189		simp3l 1198	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))))
190	189	oveq1d 7416	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) = (((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
191	55	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = ∙ )
192	191	oveqd 7418	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) = (𝑏 ∙ 𝐺))
193	192	reseq1d 5970	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁)))
194		simpl1 1188	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑅 ∈ CRing)
195	10	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑁 ∈ Fin)
196		simprrr 779	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑒 ∈ 𝑁)
197	196	snssd 4804	. . . . . . . . . . . . 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 22202	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
201	193, 200	eqtr3d 2766	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
202	201	3adant3 1129	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
203	191	oveqd 7418	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) = (𝑑 ∙ 𝐺))
204	203	reseq1d 5970	. . . . . . . . . . . . . 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 22202	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
207	204, 206	eqtr3d 2766	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
208	207	oveq2d 7417	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((({𝑒} × 𝑁) × {𝑐}) ∘f · ((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁))) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
209	12	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑅 ∈ Ring)
210	102	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → {𝑒} ∈ Fin)
211		simprlr 777	. . . . . . . . . . . . 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 22215	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
215	208, 214	eqtr4d 2767	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((({𝑒} × 𝑁) × {𝑐}) ∘f · ((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁))) = (((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
216	215	3adant3 1129	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((({𝑒} × 𝑁) × {𝑐}) ∘f · ((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁))) = (((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
217	190, 202, 216	3eqtr4d 2774	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · ((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁))))
218		simp3r 1199	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
219	218	oveq1d 7416	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
220	192	reseq1d 5970	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
221		difssd 4124	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑁 ∖ {𝑒}) ⊆ 𝑁)
222	52, 143, 3, 194, 195, 195, 195, 221, 198, 199	mamures 22202	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
223	220, 222	eqtr3d 2766	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
224	223	3adant3 1129	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
225	203	reseq1d 5970	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
226	52, 143, 3, 194, 195, 195, 195, 221, 205, 199	mamures 22202	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
227	225, 226	eqtr3d 2766	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
228	227	3adant3 1129	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
229	219, 224, 228	3eqtr4d 2774	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
230	13, 1, 2, 3, 7, 178, 183, 184, 187, 188, 217, 229	mdetrsca 22415	. . . . . . . 8 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝐷‘(𝑏 ∙ 𝐺)) = (𝑐 · (𝐷‘(𝑑 ∙ 𝐺))))
231		simp2ll 1237	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑏 ∈ 𝐵)
232	231, 31	syl 17	. . . . . . . 8 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝐷‘(𝑏 ∙ 𝐺)))
233		simp2rl 1239	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑑 ∈ 𝐵)
234	169	oveq2d 7417	. . . . . . . . 9 ⊢ (𝑑 ∈ 𝐵 → (𝑐 · ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑)) = (𝑐 · (𝐷‘(𝑑 ∙ 𝐺))))
235	233, 234	syl 17	. . . . . . . 8 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑐 · ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑)) = (𝑐 · (𝐷‘(𝑑 ∙ 𝐺))))
236	230, 232, 235	3eqtr4d 2774	. . . . . . 7 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝑐 · ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑)))
237	236	3expia 1118	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝑐 · ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑))))
238	237	anassrs 467	. . . . 5 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) → (((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝑐 · ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑))))
239	238	ralrimivva 3192	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅))) → ∀𝑑 ∈ 𝐵 ∀𝑒 ∈ 𝑁 (((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝑐 · ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑))))
240	239	ralrimivva 3192	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ (Base‘𝑅)∀𝑑 ∈ 𝐵 ∀𝑒 ∈ 𝑁 (((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝑐 · ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑))))
241		simp2 1134	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐹 ∈ 𝐵)
242	1, 2, 3, 4, 5, 6, 7, 10, 12, 26, 82, 177, 240, 13, 51, 241	mdetuni0 22433	. 2 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝐹) = (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘(1r‘𝐴)) · (𝐷‘𝐹)))
243		fvoveq1 7424	. . . 4 ⊢ (𝑎 = 𝐹 → (𝐷‘(𝑎 ∙ 𝐺)) = (𝐷‘(𝐹 ∙ 𝐺)))
244		fvex 6894	. . . 4 ⊢ (𝐷‘(𝐹 ∙ 𝐺)) ∈ V
245	243, 29, 244	fvmpt 6988	. . 3 ⊢ (𝐹 ∈ 𝐵 → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝐹) = (𝐷‘(𝐹 ∙ 𝐺)))
246	245	3ad2ant2 1131	. 2 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝐹) = (𝐷‘(𝐹 ∙ 𝐺)))
247		eqid 2724	. . . . . . 7 ⊢ (1r‘𝐴) = (1r‘𝐴)
248	2, 247	ringidcl 20150	. . . . . 6 ⊢ (𝐴 ∈ Ring → (1r‘𝐴) ∈ 𝐵)
249		fvoveq1 7424	. . . . . . 7 ⊢ (𝑎 = (1r‘𝐴) → (𝐷‘(𝑎 ∙ 𝐺)) = (𝐷‘((1r‘𝐴) ∙ 𝐺)))
250		fvex 6894	. . . . . . 7 ⊢ (𝐷‘((1r‘𝐴) ∙ 𝐺)) ∈ V
251	249, 29, 250	fvmpt 6988	. . . . . 6 ⊢ ((1r‘𝐴) ∈ 𝐵 → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘(1r‘𝐴)) = (𝐷‘((1r‘𝐴) ∙ 𝐺)))
252	18, 248, 251	3syl 18	. . . . 5 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘(1r‘𝐴)) = (𝐷‘((1r‘𝐴) ∙ 𝐺)))
253		simp3 1135	. . . . . . 7 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐺 ∈ 𝐵)
254	2, 22, 247	ringlidm 20153	. . . . . . 7 ⊢ ((𝐴 ∈ Ring ∧ 𝐺 ∈ 𝐵) → ((1r‘𝐴) ∙ 𝐺) = 𝐺)
255	18, 253, 254	syl2anc 583	. . . . . 6 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((1r‘𝐴) ∙ 𝐺) = 𝐺)
256	255	fveq2d 6885	. . . . 5 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐷‘((1r‘𝐴) ∙ 𝐺)) = (𝐷‘𝐺))
257	252, 256	eqtrd 2764	. . . 4 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘(1r‘𝐴)) = (𝐷‘𝐺))
258	257	oveq1d 7416	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘(1r‘𝐴)) · (𝐷‘𝐹)) = ((𝐷‘𝐺) · (𝐷‘𝐹)))
259	15, 253	ffvelcdmd 7077	. . . 4 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐷‘𝐺) ∈ (Base‘𝑅))
260	15, 241	ffvelcdmd 7077	. . . 4 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐷‘𝐹) ∈ (Base‘𝑅))
261	3, 7	crngcom 20141	. . . 4 ⊢ ((𝑅 ∈ CRing ∧ (𝐷‘𝐺) ∈ (Base‘𝑅) ∧ (𝐷‘𝐹) ∈ (Base‘𝑅)) → ((𝐷‘𝐺) · (𝐷‘𝐹)) = ((𝐷‘𝐹) · (𝐷‘𝐺)))
262	51, 259, 260, 261	syl3anc 1368	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝐷‘𝐺) · (𝐷‘𝐹)) = ((𝐷‘𝐹) · (𝐷‘𝐺)))
263	258, 262	eqtrd 2764	. 2 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘(1r‘𝐴)) · (𝐷‘𝐹)) = ((𝐷‘𝐹) · (𝐷‘𝐺)))
264	242, 246, 263	3eqtr3d 2772	1 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐷‘(𝐹 ∙ 𝐺)) = ((𝐷‘𝐹) · (𝐷‘𝐺)))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   ≠ wne 2932  ∀wral 3053  Vcvv 3466   ∖ cdif 3937   ⊆ wss 3940  {csn 4620  ⟨cotp 4628   ↦ cmpt 5221   × cxp 5664   ↾ cres 5668  ⟶wf 6529  ‘cfv 6533  (class class class)co 7401   ∘_f cof 7661   ↑_m cmap 8815  Fincfn 8934  Basecbs 17140  +_gcplusg 17193  ._rcmulr 17194  0_gc0g 17381   Σ_g cgsu 17382  1_rcur 20071  Ringcrg 20123  CRingccrg 20124   maMul cmmul 22195   Mat cmat 22217   maDet cmdat 22396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-cnex 11161  ax-resscn 11162  ax-1cn 11163  ax-icn 11164  ax-addcl 11165  ax-addrcl 11166  ax-mulcl 11167  ax-mulrcl 11168  ax-mulcom 11169  ax-addass 11170  ax-mulass 11171  ax-distr 11172  ax-i2m1 11173  ax-1ne0 11174  ax-1rid 11175  ax-rnegex 11176  ax-rrecex 11177  ax-cnre 11178  ax-pre-lttri 11179  ax-pre-lttrn 11180  ax-pre-ltadd 11181  ax-pre-mulgt0 11182  ax-addf 11184  ax-mulf 11185

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-xor 1505  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-tp 4625  df-op 4627  df-ot 4629  df-uni 4900  df-int 4941  df-iun 4989  df-iin 4990  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-of 7663  df-om 7849  df-1st 7968  df-2nd 7969  df-supp 8141  df-tpos 8206  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-er 8698  df-map 8817  df-pm 8818  df-ixp 8887  df-en 8935  df-dom 8936  df-sdom 8937  df-fin 8938  df-fsupp 9357  df-sup 9432  df-oi 9500  df-card 9929  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-xnn0 12541  df-z 12555  df-dec 12674  df-uz 12819  df-rp 12971  df-fz 13481  df-fzo 13624  df-seq 13963  df-exp 14024  df-hash 14287  df-word 14461  df-lsw 14509  df-concat 14517  df-s1 14542  df-substr 14587  df-pfx 14617  df-splice 14696  df-reverse 14705  df-s2 14795  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-ress 17170  df-plusg 17206  df-mulr 17207  df-starv 17208  df-sca 17209  df-vsca 17210  df-ip 17211  df-tset 17212  df-ple 17213  df-ds 17215  df-unif 17216  df-hom 17217  df-cco 17218  df-0g 17383  df-gsum 17384  df-prds 17389  df-pws 17391  df-mre 17526  df-mrc 17527  df-acs 17529  df-mgm 18560  df-sgrp 18639  df-mnd 18655  df-mhm 18700  df-submnd 18701  df-efmnd 18781  df-grp 18853  df-minusg 18854  df-sbg 18855  df-mulg 18983  df-subg 19035  df-ghm 19124  df-gim 19169  df-cntz 19218  df-oppg 19247  df-symg 19272  df-pmtr 19347  df-psgn 19396  df-evpm 19397  df-cmn 19687  df-abl 19688  df-mgp 20025  df-rng 20043  df-ur 20072  df-srg 20077  df-ring 20125  df-cring 20126  df-oppr 20221  df-dvdsr 20244  df-unit 20245  df-invr 20275  df-dvr 20288  df-rhm 20359  df-subrng 20431  df-subrg 20456  df-drng 20574  df-lmod 20693  df-lss 20764  df-sra 21006  df-rgmod 21007  df-cnfld 21224  df-zring 21297  df-zrh 21353  df-dsmm 21587  df-frlm 21602  df-mamu 22196  df-mat 22218  df-mdet 22397

This theorem is referenced by:  matunit  22490  cramerimplem3  22497  matunitlindflem2  36941