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 22968

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 2763	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
4		eqid 2763	. . 3 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
5		eqid 2763	. . 3 ⊢ (1_r‘𝑅) = (1_r‘𝑅)
6		eqid 2763	. . 3 ⊢ (+_g‘𝑅) = (+_g‘𝑅)
7		mdetmul.t1	. . 3 ⊢ · = (._r‘𝑅)
8	1, 2	matrcl 22757	. . . . 5 ⊢ (𝐹 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
9	8	simpld 500	. . . 4 ⊢ (𝐹 ∈ 𝐵 → 𝑁 ∈ Fin)
10	9	3ad2ant2 1152	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝑁 ∈ Fin)
11		crngring 20502	. . . 4 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
12	11	3ad2ant1 1151	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝑅 ∈ Ring)
13		mdetmul.d	. . . . . . . 8 ⊢ 𝐷 = (𝑁 maDet 𝑅)
14	13, 1, 2, 3	mdetf 22940	. . . . . . 7 ⊢ (𝑅 ∈ CRing → 𝐷:𝐵⟶(Base‘𝑅))
15	14	3ad2ant1 1151	. . . . . 6 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐷:𝐵⟶(Base‘𝑅))
16	15	adantr 486	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) → 𝐷:𝐵⟶(Base‘𝑅))
17	1	matring 22788	. . . . . . . 8 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring)
18	10, 12, 17	syl2anc 596	. . . . . . 7 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐴 ∈ Ring)
19	18	adantr 486	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) → 𝐴 ∈ Ring)
20		simpr 490	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) → 𝑎 ∈ 𝐵)
21		simpl3 1212	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) → 𝐺 ∈ 𝐵)
22		mdetmul.t2	. . . . . . 7 ⊢ ∙ = (._r‘𝐴)
23	2, 22	ringcl 20507	. . . . . 6 ⊢ ((𝐴 ∈ Ring ∧ 𝑎 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑎 ∙ 𝐺) ∈ 𝐵)
24	19, 20, 21, 23	syl3anc 1399	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) → (𝑎 ∙ 𝐺) ∈ 𝐵)
25	16, 24	ffvelcdmd 7109	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) → (𝐷‘(𝑎 ∙ 𝐺)) ∈ (Base‘𝑅))
26	25	fmpttd 7139	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺))):𝐵⟶(Base‘𝑅))
27		simp21 1225	. . . . . . 7 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑏 ∈ 𝐵)
28		fvoveq1 7466	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → (𝐷‘(𝑎 ∙ 𝐺)) = (𝐷‘(𝑏 ∙ 𝐺)))
29		eqid 2763	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺))) = (𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))
30		fvex 6921	. . . . . . . 8 ⊢ (𝐷‘(𝑏 ∙ 𝐺)) ∈ V
31	28, 29, 30	fvmpt 7016	. . . . . . 7 ⊢ (𝑏 ∈ 𝐵 → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝐷‘(𝑏 ∙ 𝐺)))
32	27, 31	syl 18	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝐷‘(𝑏 ∙ 𝐺)))
33		simp11 1222	. . . . . . 7 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑅 ∈ CRing)
34	18	adantr 486	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) → 𝐴 ∈ Ring)
35		simpr1 1213	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) → 𝑏 ∈ 𝐵)
36		simpl3 1212	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) → 𝐺 ∈ 𝐵)
37	2, 22	ringcl 20507	. . . . . . . . 9 ⊢ ((𝐴 ∈ Ring ∧ 𝑏 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑏 ∙ 𝐺) ∈ 𝐵)
38	34, 35, 36, 37	syl3anc 1399	. . . . . . . 8 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) → (𝑏 ∙ 𝐺) ∈ 𝐵)
39	38	3adant3 1150	. . . . . . 7 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → (𝑏 ∙ 𝐺) ∈ 𝐵)
40		simp22 1226	. . . . . . 7 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑐 ∈ 𝑁)
41		simp23 1227	. . . . . . 7 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑑 ∈ 𝑁)
42		simp3l 1220	. . . . . . 7 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → 𝑐 ≠ 𝑑)
43		simpl3r 1248	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) ∧ 𝑎 ∈ 𝑁) → ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))
44		eqid 2763	. . . . . . . . . . . 12 ⊢ 𝑁 = 𝑁
45		oveq1 7450	. . . . . . . . . . . . 13 ⊢ ((𝑐𝑏𝑒) = (𝑑𝑏𝑒) → ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)) = ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))
46	45	ralimi 3103	. . . . . . . . . . . 12 ⊢ (∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒) → ∀𝑒 ∈ 𝑁 ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)) = ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))
47		mpteq12 5196	. . . . . . . . . . . 12 ⊢ ((𝑁 = 𝑁 ∧ ∀𝑒 ∈ 𝑁 ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)) = ((𝑑𝑏𝑒) · (𝑒𝐺𝑎))) → (𝑒 ∈ 𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎))) = (𝑒 ∈ 𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎))))
48	44, 46, 47	sylancr 599	. . . . . . . . . . 11 ⊢ (∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒) → (𝑒 ∈ 𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎))) = (𝑒 ∈ 𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎))))
49	48	oveq2d 7459	. . . . . . . . . 10 ⊢ (∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒) → (𝑅 Σ_g (𝑒 ∈ 𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)))) = (𝑅 Σ_g (𝑒 ∈ 𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))))
50	43, 49	syl 18	. . . . . . . . 9 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) ∧ 𝑎 ∈ 𝑁) → (𝑅 Σ_g (𝑒 ∈ 𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)))) = (𝑅 Σ_g (𝑒 ∈ 𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))))
51		simp1 1154	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝑅 ∈ CRing)
52		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)
53	1, 52	matmulr 22783	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (._r‘𝐴))
54	53, 22	eqtr4di 2816	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = ∙ )
55	10, 51, 54	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = ∙ )
56	55	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = ∙ )
57	56	oveqd 7460	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) = (𝑏 ∙ 𝐺))
58	57	oveqd 7460	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑐(𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺)𝑎) = (𝑐(𝑏 ∙ 𝐺)𝑎))
59		simpll1 1231	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝑅 ∈ CRing)
60	10	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝑁 ∈ Fin)
61		simplr1 1234	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝑏 ∈ 𝐵)
62	1, 3, 2	matbas2i 22767	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ 𝐵 → 𝑏 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
63	61, 62	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝑏 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
64	1, 3, 2	matbas2i 22767	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ 𝐵 → 𝐺 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
65	64	3ad2ant3 1153	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐺 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
66	65	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝐺 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
67		simplr2 1235	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝑐 ∈ 𝑁)
68		simpr 490	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝑎 ∈ 𝑁)
69	52, 3, 7, 59, 60, 60, 60, 63, 66, 67, 68	mamufv 22739	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑐(𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺)𝑎) = (𝑅 Σ_g (𝑒 ∈ 𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)))))
70	58, 69	eqtr3d 2800	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑐(𝑏 ∙ 𝐺)𝑎) = (𝑅 Σ_g (𝑒 ∈ 𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)))))
71	70	3adantl3 1187	. . . . . . . . 9 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) ∧ 𝑎 ∈ 𝑁) → (𝑐(𝑏 ∙ 𝐺)𝑎) = (𝑅 Σ_g (𝑒 ∈ 𝑁 ↦ ((𝑐𝑏𝑒) · (𝑒𝐺𝑎)))))
72	57	oveqd 7460	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑑(𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺)𝑎) = (𝑑(𝑏 ∙ 𝐺)𝑎))
73		simplr3 1236	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → 𝑑 ∈ 𝑁)
74	52, 3, 7, 59, 60, 60, 60, 63, 66, 73, 68	mamufv 22739	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑑(𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺)𝑎) = (𝑅 Σ_g (𝑒 ∈ 𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))))
75	72, 74	eqtr3d 2800	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) ∧ 𝑎 ∈ 𝑁) → (𝑑(𝑏 ∙ 𝐺)𝑎) = (𝑅 Σ_g (𝑒 ∈ 𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))))
76	75	3adantl3 1187	. . . . . . . . 9 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) ∧ 𝑎 ∈ 𝑁) → (𝑑(𝑏 ∙ 𝐺)𝑎) = (𝑅 Σ_g (𝑒 ∈ 𝑁 ↦ ((𝑑𝑏𝑒) · (𝑒𝐺𝑎)))))
77	50, 71, 76	3eqtr4d 2808	. . . . . . . 8 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) ∧ 𝑎 ∈ 𝑁) → (𝑐(𝑏 ∙ 𝐺)𝑎) = (𝑑(𝑏 ∙ 𝐺)𝑎))
78	77	ralrimiva 3158	. . . . . . 7 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → ∀𝑎 ∈ 𝑁 (𝑐(𝑏 ∙ 𝐺)𝑎) = (𝑑(𝑏 ∙ 𝐺)𝑎))
79	13, 1, 2, 4, 33, 39, 40, 41, 42, 78	mdetralt 22953	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → (𝐷‘(𝑏 ∙ 𝐺)) = (0_g‘𝑅))
80	32, 79	eqtrd 2798	. . . . 5 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁) ∧ (𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (0_g‘𝑅))
81	80	3expia 1139	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝑁 ∧ 𝑑 ∈ 𝑁)) → ((𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒)) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (0_g‘𝑅)))
82	81	ralrimivvva 3212	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝑁 ∀𝑑 ∈ 𝑁 ((𝑐 ≠ 𝑑 ∧ ∀𝑒 ∈ 𝑁 (𝑐𝑏𝑒) = (𝑑𝑏𝑒)) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (0_g‘𝑅)))
83		simp11 1222	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑅 ∈ CRing)
84	18	adantr 486	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝐴 ∈ Ring)
85		simprll 791	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑏 ∈ 𝐵)
86		simpl3 1212	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝐺 ∈ 𝐵)
87	84, 85, 86, 37	syl3anc 1399	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑏 ∙ 𝐺) ∈ 𝐵)
88	87	3adant3 1150	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ∙ 𝐺) ∈ 𝐵)
89		simprlr 792	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑐 ∈ 𝐵)
90	2, 22	ringcl 20507	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Ring ∧ 𝑐 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑐 ∙ 𝐺) ∈ 𝐵)
91	84, 89, 86, 90	syl3anc 1399	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑐 ∙ 𝐺) ∈ 𝐵)
92	91	3adant3 1150	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑐 ∙ 𝐺) ∈ 𝐵)
93		simprrl 793	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑑 ∈ 𝐵)
94	2, 22	ringcl 20507	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Ring ∧ 𝑑 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑑 ∙ 𝐺) ∈ 𝐵)
95	84, 93, 86, 94	syl3anc 1399	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑑 ∙ 𝐺) ∈ 𝐵)
96	95	3adant3 1150	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑑 ∙ 𝐺) ∈ 𝐵)
97		simp2rr 1262	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑒 ∈ 𝑁)
98		simp31 1228	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))))
99	98	oveq1d 7458	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) = (((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
100	12	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑅 ∈ Ring)
101		eqid 2763	. . . . . . . . . . . . 13 ⊢ (𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩) = (𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)
102		snfi 9099	. . . . . . . . . . . . . 14 ⊢ {𝑒} ∈ Fin
103	102	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → {𝑒} ∈ Fin)
104	10	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑁 ∈ Fin)
105	1, 3, 2	matbas2i 22767	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ∈ 𝐵 → 𝑐 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
106	89, 105	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑐 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
107		simprrr 794	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑒 ∈ 𝑁)
108	107	snssd 4747	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → {𝑒} ⊆ 𝑁)
109		xpss1 5674	. . . . . . . . . . . . . . 15 ⊢ ({𝑒} ⊆ 𝑁 → ({𝑒} × 𝑁) ⊆ (𝑁 × 𝑁))
110	108, 109	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ({𝑒} × 𝑁) ⊆ (𝑁 × 𝑁))
111		elmapssres 8922	. . . . . . . . . . . . . 14 ⊢ ((𝑐 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)) ∧ ({𝑒} × 𝑁) ⊆ (𝑁 × 𝑁)) → (𝑐 ↾ ({𝑒} × 𝑁)) ∈ ((Base‘𝑅) ↑_m ({𝑒} × 𝑁)))
112	106, 110, 111	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑐 ↾ ({𝑒} × 𝑁)) ∈ ((Base‘𝑅) ↑_m ({𝑒} × 𝑁)))
113	1, 3, 2	matbas2i 22767	. . . . . . . . . . . . . . 15 ⊢ (𝑑 ∈ 𝐵 → 𝑑 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
114	93, 113	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑑 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
115		elmapssres 8922	. . . . . . . . . . . . . 14 ⊢ ((𝑑 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)) ∧ ({𝑒} × 𝑁) ⊆ (𝑁 × 𝑁)) → (𝑑 ↾ ({𝑒} × 𝑁)) ∈ ((Base‘𝑅) ↑_m ({𝑒} × 𝑁)))
116	114, 110, 115	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑑 ↾ ({𝑒} × 𝑁)) ∈ ((Base‘𝑅) ↑_m ({𝑒} × 𝑁)))
117	65	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝐺 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
118	3, 100, 101, 103, 104, 104, 6, 112, 116, 117	mamudi 22748	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) = (((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) ∘_f (+_g‘𝑅)((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
119	118	3adant3 1150	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) = (((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) ∘_f (+_g‘𝑅)((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
120	99, 119	eqtrd 2798	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) = (((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) ∘_f (+_g‘𝑅)((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
121	55	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = ∙ )
122	121	oveqd 7460	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) = (𝑏 ∙ 𝐺))
123	122	reseq1d 5980	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁)))
124		simpl1 1210	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑅 ∈ CRing)
125	85, 62	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑏 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
126	52, 101, 3, 124, 104, 104, 104, 108, 125, 117	mamures 22742	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
127	123, 126	eqtr3d 2800	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
128	127	3adant3 1150	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
129	121	oveqd 7460	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑐(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) = (𝑐 ∙ 𝐺))
130	129	reseq1d 5980	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑐(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑐 ∙ 𝐺) ↾ ({𝑒} × 𝑁)))
131	52, 101, 3, 124, 104, 104, 104, 108, 106, 117	mamures 22742	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑐(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
132	130, 131	eqtr3d 2800	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑐 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
133	121	oveqd 7460	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) = (𝑑 ∙ 𝐺))
134	133	reseq1d 5980	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁)))
135	52, 101, 3, 124, 104, 104, 104, 108, 114, 117	mamures 22742	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
136	134, 135	eqtr3d 2800	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
137	132, 136	oveq12d 7461	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (((𝑐 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁))) = (((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) ∘_f (+_g‘𝑅)((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
138	137	3adant3 1150	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (((𝑐 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁))) = (((𝑐 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) ∘_f (+_g‘𝑅)((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
139	120, 128, 138	3eqtr4d 2808	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = (((𝑐 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁))))
140		simp32 1229	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
141	140	oveq1d 7458	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺) = ((𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
142	122	reseq1d 5980	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
143		eqid 2763	. . . . . . . . . . . . 13 ⊢ (𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩) = (𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)
144		difssd 4076	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑁 ∖ {𝑒}) ⊆ 𝑁)
145	52, 143, 3, 124, 104, 104, 104, 144, 125, 117	mamures 22742	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
146	142, 145	eqtr3d 2800	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
147	146	3adant3 1150	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
148	129	reseq1d 5980	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑐(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑐 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
149	52, 143, 3, 124, 104, 104, 104, 144, 106, 117	mamures 22742	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑐(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
150	148, 149	eqtr3d 2800	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑐 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
151	150	3adant3 1150	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑐 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
152	141, 147, 151	3eqtr4d 2808	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑐 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
153		simp33 1230	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
154	153	oveq1d 7458	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
155	133	reseq1d 5980	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
156	52, 143, 3, 124, 104, 104, 104, 144, 114, 117	mamures 22742	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
157	155, 156	eqtr3d 2800	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
158	157	3adant3 1150	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
159	154, 147, 158	3eqtr4d 2808	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
160	13, 1, 2, 6, 83, 88, 92, 96, 97, 139, 152, 159	mdetrlin 22947	. . . . . . . 8 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝐷‘(𝑏 ∙ 𝐺)) = ((𝐷‘(𝑐 ∙ 𝐺))(+_g‘𝑅)(𝐷‘(𝑑 ∙ 𝐺))))
161	85, 31	syl 18	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝐷‘(𝑏 ∙ 𝐺)))
162	161	3adant3 1150	. . . . . . . 8 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝐷‘(𝑏 ∙ 𝐺)))
163		fvoveq1 7466	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → (𝐷‘(𝑎 ∙ 𝐺)) = (𝐷‘(𝑐 ∙ 𝐺)))
164		fvex 6921	. . . . . . . . . . . 12 ⊢ (𝐷‘(𝑐 ∙ 𝐺)) ∈ V
165	163, 29, 164	fvmpt 7016	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝐵 → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐) = (𝐷‘(𝑐 ∙ 𝐺)))
166	89, 165	syl 18	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐) = (𝐷‘(𝑐 ∙ 𝐺)))
167		fvoveq1 7466	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑑 → (𝐷‘(𝑎 ∙ 𝐺)) = (𝐷‘(𝑑 ∙ 𝐺)))
168		fvex 6921	. . . . . . . . . . . 12 ⊢ (𝐷‘(𝑑 ∙ 𝐺)) ∈ V
169	167, 29, 168	fvmpt 7016	. . . . . . . . . . 11 ⊢ (𝑑 ∈ 𝐵 → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑) = (𝐷‘(𝑑 ∙ 𝐺)))
170	93, 169	syl 18	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑) = (𝐷‘(𝑑 ∙ 𝐺)))
171	166, 170	oveq12d 7461	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐)(+_g‘𝑅)((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑)) = ((𝐷‘(𝑐 ∙ 𝐺))(+_g‘𝑅)(𝐷‘(𝑑 ∙ 𝐺))))
172	171	3adant3 1150	. . . . . . . 8 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐)(+_g‘𝑅)((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑)) = ((𝐷‘(𝑐 ∙ 𝐺))(+_g‘𝑅)(𝐷‘(𝑑 ∙ 𝐺))))
173	160, 162, 172	3eqtr4d 2808	. . . . . . 7 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐)(+_g‘𝑅)((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑)))
174	173	3expia 1139	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐)(+_g‘𝑅)((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑))))
175	174	anassrs 473	. . . . 5 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) → (((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐)(+_g‘𝑅)((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑))))
176	175	ralrimivva 3209	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → ∀𝑑 ∈ 𝐵 ∀𝑒 ∈ 𝑁 (((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐)(+_g‘𝑅)((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑))))
177	176	ralrimivva 3209	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑑 ∈ 𝐵 ∀𝑒 ∈ 𝑁 (((𝑏 ↾ ({𝑒} × 𝑁)) = ((𝑐 ↾ ({𝑒} × 𝑁)) ∘_f (+_g‘𝑅)(𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑐 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑐)(+_g‘𝑅)((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑))))
178		simp11 1222	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑅 ∈ CRing)
179	18	adantr 486	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝐴 ∈ Ring)
180		simprll 791	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑏 ∈ 𝐵)
181		simpl3 1212	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝐺 ∈ 𝐵)
182	179, 180, 181, 37	syl3anc 1399	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑏 ∙ 𝐺) ∈ 𝐵)
183	182	3adant3 1150	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ∙ 𝐺) ∈ 𝐵)
184		simp2lr 1260	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑐 ∈ (Base‘𝑅))
185		simprrl 793	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑑 ∈ 𝐵)
186	179, 185, 181, 94	syl3anc 1399	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑑 ∙ 𝐺) ∈ 𝐵)
187	186	3adant3 1150	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑑 ∙ 𝐺) ∈ 𝐵)
188		simp2rr 1262	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑒 ∈ 𝑁)
189		simp3l 1220	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))))
190	189	oveq1d 7458	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) = (((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
191	55	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = ∙ )
192	191	oveqd 7460	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) = (𝑏 ∙ 𝐺))
193	192	reseq1d 5980	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁)))
194		simpl1 1210	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑅 ∈ CRing)
195	10	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑁 ∈ Fin)
196		simprrr 794	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑒 ∈ 𝑁)
197	196	snssd 4747	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → {𝑒} ⊆ 𝑁)
198	180, 62	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑏 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
199	65	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝐺 ∈ ((Base‘𝑅) ↑_m (𝑁 × 𝑁)))
200	52, 101, 3, 194, 195, 195, 195, 197, 198, 199	mamures 22742	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
201	193, 200	eqtr3d 2800	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
202	201	3adant3 1150	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑏 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
203	191	oveqd 7460	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) = (𝑑 ∙ 𝐺))
204	203	reseq1d 5980	. . . . . . . . . . . . . 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 22742	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
207	204, 206	eqtr3d 2800	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
208	207	oveq2d 7459	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((({𝑒} × 𝑁) × {𝑐}) ∘_f · ((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁))) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
209	12	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑅 ∈ Ring)
210	102	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → {𝑒} ∈ Fin)
211		simprlr 792	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → 𝑐 ∈ (Base‘𝑅))
212	197, 109	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ({𝑒} × 𝑁) ⊆ (𝑁 × 𝑁))
213	205, 212, 115	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑑 ↾ ({𝑒} × 𝑁)) ∈ ((Base‘𝑅) ↑_m ({𝑒} × 𝑁)))
214	3, 209, 101, 210, 195, 195, 7, 211, 213, 199	mamuvs1 22750	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · ((𝑑 ↾ ({𝑒} × 𝑁))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺)))
215	208, 214	eqtr4d 2801	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((({𝑒} × 𝑁) × {𝑐}) ∘_f · ((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁))) = (((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
216	215	3adant3 1150	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((({𝑒} × 𝑁) × {𝑐}) ∘_f · ((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁))) = (((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁)))(𝑅 maMul ⟨{𝑒}, 𝑁, 𝑁⟩)𝐺))
217	190, 202, 216	3eqtr4d 2808	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · ((𝑑 ∙ 𝐺) ↾ ({𝑒} × 𝑁))))
218		simp3r 1221	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
219	218	oveq1d 7458	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
220	192	reseq1d 5980	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
221		difssd 4076	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (𝑁 ∖ {𝑒}) ⊆ 𝑁)
222	52, 143, 3, 194, 195, 195, 195, 221, 198, 199	mamures 22742	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
223	220, 222	eqtr3d 2800	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
224	223	3adant3 1150	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
225	203	reseq1d 5980	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
226	52, 143, 3, 194, 195, 195, 195, 221, 205, 199	mamures 22742	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
227	225, 226	eqtr3d 2800	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
228	227	3adant3 1150	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))(𝑅 maMul ⟨(𝑁 ∖ {𝑒}), 𝑁, 𝑁⟩)𝐺))
229	219, 224, 228	3eqtr4d 2808	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑏 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = ((𝑑 ∙ 𝐺) ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))
230	13, 1, 2, 3, 7, 178, 183, 184, 187, 188, 217, 229	mdetrsca 22948	. . . . . . . 8 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝐷‘(𝑏 ∙ 𝐺)) = (𝑐 · (𝐷‘(𝑑 ∙ 𝐺))))
231		simp2ll 1259	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑏 ∈ 𝐵)
232	231, 31	syl 18	. . . . . . . 8 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝐷‘(𝑏 ∙ 𝐺)))
233		simp2rl 1261	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → 𝑑 ∈ 𝐵)
234	169	oveq2d 7459	. . . . . . . . 9 ⊢ (𝑑 ∈ 𝐵 → (𝑐 · ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑)) = (𝑐 · (𝐷‘(𝑑 ∙ 𝐺))))
235	233, 234	syl 18	. . . . . . . 8 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → (𝑐 · ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑)) = (𝑐 · (𝐷‘(𝑑 ∙ 𝐺))))
236	230, 232, 235	3eqtr4d 2808	. . . . . . 7 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) ∧ ((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝑐 · ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑)))
237	236	3expia 1139	. . . . . 6 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ ((𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁))) → (((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝑐 · ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑))))
238	237	anassrs 473	. . . . 5 ⊢ ((((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝑁)) → (((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝑐 · ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑))))
239	238	ralrimivva 3209	. . . 4 ⊢ (((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ (Base‘𝑅))) → ∀𝑑 ∈ 𝐵 ∀𝑒 ∈ 𝑁 (((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝑐 · ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑))))
240	239	ralrimivva 3209	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ (Base‘𝑅)∀𝑑 ∈ 𝐵 ∀𝑒 ∈ 𝑁 (((𝑏 ↾ ({𝑒} × 𝑁)) = ((({𝑒} × 𝑁) × {𝑐}) ∘_f · (𝑑 ↾ ({𝑒} × 𝑁))) ∧ (𝑏 ↾ ((𝑁 ∖ {𝑒}) × 𝑁)) = (𝑑 ↾ ((𝑁 ∖ {𝑒}) × 𝑁))) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑏) = (𝑐 · ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝑑))))
241		simp2 1155	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐹 ∈ 𝐵)
242	1, 2, 3, 4, 5, 6, 7, 10, 12, 26, 82, 177, 240, 13, 51, 241	mdetuni0 22966	. 2 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝐹) = (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘(1_r‘𝐴)) · (𝐷‘𝐹)))
243		fvoveq1 7466	. . . 4 ⊢ (𝑎 = 𝐹 → (𝐷‘(𝑎 ∙ 𝐺)) = (𝐷‘(𝐹 ∙ 𝐺)))
244		fvex 6921	. . . 4 ⊢ (𝐷‘(𝐹 ∙ 𝐺)) ∈ V
245	243, 29, 244	fvmpt 7016	. . 3 ⊢ (𝐹 ∈ 𝐵 → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝐹) = (𝐷‘(𝐹 ∙ 𝐺)))
246	245	3ad2ant2 1152	. 2 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘𝐹) = (𝐷‘(𝐹 ∙ 𝐺)))
247		eqid 2763	. . . . . . 7 ⊢ (1_r‘𝐴) = (1_r‘𝐴)
248	2, 247	ringidcl 20524	. . . . . 6 ⊢ (𝐴 ∈ Ring → (1_r‘𝐴) ∈ 𝐵)
249		fvoveq1 7466	. . . . . . 7 ⊢ (𝑎 = (1_r‘𝐴) → (𝐷‘(𝑎 ∙ 𝐺)) = (𝐷‘((1_r‘𝐴) ∙ 𝐺)))
250		fvex 6921	. . . . . . 7 ⊢ (𝐷‘((1_r‘𝐴) ∙ 𝐺)) ∈ V
251	249, 29, 250	fvmpt 7016	. . . . . 6 ⊢ ((1_r‘𝐴) ∈ 𝐵 → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘(1_r‘𝐴)) = (𝐷‘((1_r‘𝐴) ∙ 𝐺)))
252	18, 248, 251	3syl 19	. . . . 5 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘(1_r‘𝐴)) = (𝐷‘((1_r‘𝐴) ∙ 𝐺)))
253		simp3 1156	. . . . . . 7 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → 𝐺 ∈ 𝐵)
254	2, 22, 247	ringlidm 20528	. . . . . . 7 ⊢ ((𝐴 ∈ Ring ∧ 𝐺 ∈ 𝐵) → ((1_r‘𝐴) ∙ 𝐺) = 𝐺)
255	18, 253, 254	syl2anc 596	. . . . . 6 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((1_r‘𝐴) ∙ 𝐺) = 𝐺)
256	255	fveq2d 6912	. . . . 5 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐷‘((1_r‘𝐴) ∙ 𝐺)) = (𝐷‘𝐺))
257	252, 256	eqtrd 2798	. . . 4 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘(1_r‘𝐴)) = (𝐷‘𝐺))
258	257	oveq1d 7458	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘(1_r‘𝐴)) · (𝐷‘𝐹)) = ((𝐷‘𝐺) · (𝐷‘𝐹)))
259	15, 253	ffvelcdmd 7109	. . . 4 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐷‘𝐺) ∈ (Base‘𝑅))
260	15, 241	ffvelcdmd 7109	. . . 4 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐷‘𝐹) ∈ (Base‘𝑅))
261	3, 7	crngcom 20508	. . . 4 ⊢ ((𝑅 ∈ CRing ∧ (𝐷‘𝐺) ∈ (Base‘𝑅) ∧ (𝐷‘𝐹) ∈ (Base‘𝑅)) → ((𝐷‘𝐺) · (𝐷‘𝐹)) = ((𝐷‘𝐹) · (𝐷‘𝐺)))
262	51, 259, 260, 261	syl3anc 1399	. . 3 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝐷‘𝐺) · (𝐷‘𝐹)) = ((𝐷‘𝐹) · (𝐷‘𝐺)))
263	258, 262	eqtrd 2798	. 2 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (((𝑎 ∈ 𝐵 ↦ (𝐷‘(𝑎 ∙ 𝐺)))‘(1_r‘𝐴)) · (𝐷‘𝐹)) = ((𝐷‘𝐹) · (𝐷‘𝐺)))
264	242, 246, 263	3eqtr3d 2806	1 ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐷‘(𝐹 ∙ 𝐺)) = ((𝐷‘𝐹) · (𝐷‘𝐺)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ∀wral 3080 Vcvv 3454 ⊆ wss 3900 ∖ cdif 4048 {csn 4588 ⟨cotp 4861 ↦ cmpt 5189 × cxp 5653 ↾ cres 5657 ⟶wf 6554 ‘cfv 6558 (class class class)co 7443 ∘_f cof 7715 ↑_m cmap 8875 Fincfn 9001 Basecbs 17416 +_gcplusg 17457 ._rcmulr 17458 0_gc0g 17639 Σ_g cgsu 17640 1_rcur 20437 Ringcrg 20489 CRingccrg 20490 maMul cmmul 22735 Mat cmat 22752 maDet cmdat 22929

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7775 ax-cnex 11283 ax-resscn 11284 ax-1cn 11285 ax-icn 11286 ax-addcl 11287 ax-addrcl 11288 ax-mulcl 11289 ax-mulrcl 11290 ax-mulcom 11291 ax-addass 11292 ax-mulass 11293 ax-distr 11294 ax-i2m1 11295 ax-1ne0 11296 ax-1rid 11297 ax-rnegex 11298 ax-rrecex 11299 ax-cnre 11300 ax-pre-lttri 11301 ax-pre-lttrn 11302 ax-pre-ltadd 11303 ax-pre-mulgt0 11304 ax-addf 11306 ax-mulf 11307

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-xor 1542 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-ot 4862 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6322 df-ord 6383 df-on 6384 df-lim 6385 df-suc 6386 df-iota 6512 df-fun 6560 df-fn 6561 df-f 6562 df-f1 6563 df-fo 6564 df-f1o 6565 df-fv 6566 df-isom 6567 df-riota 7400 df-ov 7446 df-oprab 7447 df-mpo 7448 df-of 7717 df-om 7902 df-1st 8025 df-2nd 8026 df-supp 8205 df-tpos 8271 df-frecs 8327 df-wrecs 8358 df-recs 8407 df-rdg 8446 df-1o 8504 df-2o 8505 df-er 8745 df-map 8877 df-pm 8878 df-ixp 8954 df-en 9002 df-dom 9003 df-sdom 9004 df-fin 9005 df-fsupp 9382 df-sup 9461 df-oi 9531 df-card 10047 df-pnf 11372 df-mnf 11373 df-xr 11374 df-ltxr 11375 df-le 11376 df-sub 11570 df-neg 11571 df-div 12001 df-nn 12363 df-2 12432 df-3 12433 df-4 12434 df-5 12435 df-6 12436 df-7 12437 df-8 12438 df-9 12439 df-n0 12634 df-xnn0 12707 df-z 12721 df-dec 12842 df-uz 12993 df-rp 13148 df-fz 13667 df-fzo 13816 df-seq 14172 df-exp 14232 df-hash 14502 df-word 14686 df-lsw 14735 df-concat 14743 df-s1 14770 df-substr 14817 df-pfx 14849 df-splice 14927 df-reverse 14936 df-s2 15027 df-struct 17354 df-sets 17371 df-slot 17389 df-ndx 17401 df-base 17417 df-ress 17438 df-plusg 17470 df-mulr 17471 df-starv 17472 df-sca 17473 df-vsca 17474 df-ip 17475 df-tset 17476 df-ple 17477 df-ds 17479 df-unif 17480 df-hom 17481 df-cco 17482 df-0g 17641 df-gsum 17642 df-prds 17647 df-pws 17649 df-mre 17785 df-mrc 17786 df-acs 17788 df-mgm 18845 df-sgrp 18937 df-mnd 18953 df-mhm 19007 df-submnd 19008 df-efmnd 19094 df-grp 19176 df-minusg 19177 df-sbg 19178 df-mulg 19307 df-subg 19362 df-ghm 19457 df-gim 19502 df-cntz 19561 df-oppg 19590 df-symg 19614 df-pmtr 19686 df-psgn 19735 df-evpm 19736 df-cmn 20026 df-abl 20027 df-mgp 20391 df-rng 20405 df-ur 20438 df-srg 20443 df-ring 20491 df-cring 20492 df-oppr 20597 df-dvdsr 20617 df-unit 20618 df-invr 20648 df-dvr 20661 df-rhm 20732 df-subrng 20828 df-subrg 20852 df-drng 21012 df-lmod 21167 df-lss 21237 df-sra 21478 df-rgmod 21479 df-cnfld 21709 df-zring 21783 df-zrh 21839 df-dsmm 22068 df-frlm 22083 df-mamu 22736 df-mat 22753 df-mdet 22930

This theorem is used by: matunit 23023 matunitlindflem2 23025 cramerimplem3 23033

W3C validator