mdetmul

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

	Ref	Expression
Hypotheses	mdetmul.a	$⊢ A = N Mat R$
	mdetmul.b	$⊢ B = {Base}_{A}$
	mdetmul.d	$⊢ D = N maDet R$
	mdetmul.t1	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	mdetmul.t2	$⊢ \underset{˙}{∙} = \cdot_{A}$
Assertion	mdetmul	$⊢ (R \in CRing \land F \in B \land G \in B) \to D (F \underset{˙}{∙} G) = D (F) \underset{˙}{\cdot} D (G)$

Proof

Step	Hyp	Ref	Expression
1		mdetmul.a	$⊢ A = N Mat R$
2		mdetmul.b	$⊢ B = {Base}_{A}$
3		mdetmul.d	$⊢ D = N maDet R$
4		mdetmul.t1	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		mdetmul.t2	$⊢ \underset{˙}{∙} = \cdot_{A}$
6		eqid	$⊢ {Base}_{R} = {Base}_{R}$
7		eqid	$⊢ 0_{R} = 0_{R}$
8		eqid	$⊢ 1_{R} = 1_{R}$
9		eqid	$⊢ +_{R} = +_{R}$
10	1 2	matrcl	$⊢ F \in B \to (N \in Fin \land R \in V)$
11	10	simpld	$⊢ F \in B \to N \in Fin$
12	11	3ad2ant2	$⊢ (R \in CRing \land F \in B \land G \in B) \to N \in Fin$
13		crngring	$⊢ R \in CRing \to R \in Ring$
14	13	3ad2ant1	$⊢ (R \in CRing \land F \in B \land G \in B) \to R \in Ring$
15	3 1 2 6	mdetf	$⊢ R \in CRing \to D : B ⟶ {Base}_{R}$
16	15	3ad2ant1	$⊢ (R \in CRing \land F \in B \land G \in B) \to D : B ⟶ {Base}_{R}$
17	16	adantr	$⊢ ((R \in CRing \land F \in B \land G \in B) \land a \in B) \to D : B ⟶ {Base}_{R}$
18	1	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
19	12 14 18	syl2anc	$⊢ (R \in CRing \land F \in B \land G \in B) \to A \in Ring$
20	19	adantr	$⊢ ((R \in CRing \land F \in B \land G \in B) \land a \in B) \to A \in Ring$
21		simpr	$⊢ ((R \in CRing \land F \in B \land G \in B) \land a \in B) \to a \in B$
22		simpl3	$⊢ ((R \in CRing \land F \in B \land G \in B) \land a \in B) \to G \in B$
23	2 5	ringcl	$⊢ (A \in Ring \land a \in B \land G \in B) \to a \underset{˙}{∙} G \in B$
24	20 21 22 23	syl3anc	$⊢ ((R \in CRing \land F \in B \land G \in B) \land a \in B) \to a \underset{˙}{∙} G \in B$
25	17 24	ffvelrnd	$⊢ ((R \in CRing \land F \in B \land G \in B) \land a \in B) \to D (a \underset{˙}{∙} G) \in {Base}_{R}$
26	25	fmpttd	$⊢ (R \in CRing \land F \in B \land G \in B) \to (a \in B ⟼ D (a \underset{˙}{∙} G)) : B ⟶ {Base}_{R}$
27		simp21	$⊢ ((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N) \land (c \neq d \land \forall e \in N c b e = d b e)) \to b \in B$
28		fvoveq1	$⊢ a = b \to D (a \underset{˙}{∙} G) = D (b \underset{˙}{∙} G)$
29		eqid	$⊢ (a \in B ⟼ D (a \underset{˙}{∙} G)) = (a \in B ⟼ D (a \underset{˙}{∙} G))$
30		fvex	$⊢ D (b \underset{˙}{∙} G) \in V$
31	28 29 30	fvmpt	$⊢ b \in B \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (b) = D (b \underset{˙}{∙} G)$
32	27 31	syl	$⊢ ((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N) \land (c \neq d \land \forall e \in N c b e = d b e)) \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (b) = D (b \underset{˙}{∙} G)$
33		simp11	$⊢ ((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N) \land (c \neq d \land \forall e \in N c b e = d b e)) \to R \in CRing$
34	19	adantr	$⊢ ((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N)) \to A \in Ring$
35		simpr1	$⊢ ((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N)) \to b \in B$
36		simpl3	$⊢ ((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N)) \to G \in B$
37	2 5	ringcl	$⊢ (A \in Ring \land b \in B \land G \in B) \to b \underset{˙}{∙} G \in B$
38	34 35 36 37	syl3anc	$⊢ ((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N)) \to b \underset{˙}{∙} G \in B$
39	38	3adant3	$⊢ ((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N) \land (c \neq d \land \forall e \in N c b e = d b e)) \to b \underset{˙}{∙} G \in B$
40		simp22	$⊢ ((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N) \land (c \neq d \land \forall e \in N c b e = d b e)) \to c \in N$
41		simp23	$⊢ ((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N) \land (c \neq d \land \forall e \in N c b e = d b e)) \to d \in N$
42		simp3l	$⊢ ((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N) \land (c \neq d \land \forall e \in N c b e = d b e)) \to c \neq d$
43		simpl3r	$⊢ (((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N) \land (c \neq d \land \forall e \in N c b e = d b e)) \land a \in N) \to \forall e \in N c b e = d b e$
44		eqid	$⊢ N = N$
45		oveq1	$⊢ c b e = d b e \to (c b e) \underset{˙}{\cdot} (e G a) = (d b e) \underset{˙}{\cdot} (e G a)$
46	45	ralimi	$⊢ \forall e \in N c b e = d b e \to \forall e \in N (c b e) \underset{˙}{\cdot} (e G a) = (d b e) \underset{˙}{\cdot} (e G a)$
47		mpteq12	$⊢ (N = N \land \forall e \in N (c b e) \underset{˙}{\cdot} (e G a) = (d b e) \underset{˙}{\cdot} (e G a)) \to (e \in N ⟼ (c b e) \underset{˙}{\cdot} (e G a)) = (e \in N ⟼ (d b e) \underset{˙}{\cdot} (e G a))$
48	44 46 47	sylancr	$⊢ \forall e \in N c b e = d b e \to (e \in N ⟼ (c b e) \underset{˙}{\cdot} (e G a)) = (e \in N ⟼ (d b e) \underset{˙}{\cdot} (e G a))$
49	48	oveq2d	$⊢ \forall e \in N c b e = d b e \to \underset{e \in N}{\sum_{R}} ((c b e) \underset{˙}{\cdot} (e G a)) = \underset{e \in N}{\sum_{R}} ((d b e) \underset{˙}{\cdot} (e G a))$
50	43 49	syl	$⊢ (((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N) \land (c \neq d \land \forall e \in N c b e = d b e)) \land a \in N) \to \underset{e \in N}{\sum_{R}} ((c b e) \underset{˙}{\cdot} (e G a)) = \underset{e \in N}{\sum_{R}} ((d b e) \underset{˙}{\cdot} (e G a))$
51		simp1	$⊢ (R \in CRing \land F \in B \land G \in B) \to R \in CRing$
52		eqid	$⊢ R maMul ⟨N, N, N⟩ = R maMul ⟨N, N, N⟩$
53	1 52	matmulr	$⊢ (N \in Fin \land R \in CRing) \to R maMul ⟨N, N, N⟩ = \cdot_{A}$
54	53 5	eqtr4di	$⊢ (N \in Fin \land R \in CRing) \to R maMul ⟨N, N, N⟩ = \underset{˙}{∙}$
55	12 51 54	syl2anc	$⊢ (R \in CRing \land F \in B \land G \in B) \to R maMul ⟨N, N, N⟩ = \underset{˙}{∙}$
56	55	ad2antrr	$⊢ (((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N)) \land a \in N) \to R maMul ⟨N, N, N⟩ = \underset{˙}{∙}$
57	56	oveqd	$⊢ (((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N)) \land a \in N) \to b (R maMul ⟨N, N, N⟩) G = b \underset{˙}{∙} G$
58	57	oveqd	$⊢ (((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N)) \land a \in N) \to c (b (R maMul ⟨N, N, N⟩) G) a = c (b \underset{˙}{∙} G) a$
59		simpll1	$⊢ (((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N)) \land a \in N) \to R \in CRing$
60	12	ad2antrr	$⊢ (((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N)) \land a \in N) \to N \in Fin$
61		simplr1	$⊢ (((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N)) \land a \in N) \to b \in B$
62	1 6 2	matbas2i	$⊢ b \in B \to b \in ({Base}_{R}^{(N \times N)})$
63	61 62	syl	$⊢ (((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N)) \land a \in N) \to b \in ({Base}_{R}^{(N \times N)})$
64	1 6 2	matbas2i	$⊢ G \in B \to G \in ({Base}_{R}^{(N \times N)})$
65	64	3ad2ant3	$⊢ (R \in CRing \land F \in B \land G \in B) \to G \in ({Base}_{R}^{(N \times N)})$
66	65	ad2antrr	$⊢ (((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N)) \land a \in N) \to G \in ({Base}_{R}^{(N \times N)})$
67		simplr2	$⊢ (((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N)) \land a \in N) \to c \in N$
68		simpr	$⊢ (((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N)) \land a \in N) \to a \in N$
69	52 6 4 59 60 60 60 63 66 67 68	mamufv	$⊢ (((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N)) \land a \in N) \to c (b (R maMul ⟨N, N, N⟩) G) a = \underset{e \in N}{\sum_{R}} ((c b e) \underset{˙}{\cdot} (e G a))$
70	58 69	eqtr3d	$⊢ (((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N)) \land a \in N) \to c (b \underset{˙}{∙} G) a = \underset{e \in N}{\sum_{R}} ((c b e) \underset{˙}{\cdot} (e G a))$
71	70	3adantl3	$⊢ (((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N) \land (c \neq d \land \forall e \in N c b e = d b e)) \land a \in N) \to c (b \underset{˙}{∙} G) a = \underset{e \in N}{\sum_{R}} ((c b e) \underset{˙}{\cdot} (e G a))$
72	57	oveqd	$⊢ (((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N)) \land a \in N) \to d (b (R maMul ⟨N, N, N⟩) G) a = d (b \underset{˙}{∙} G) a$
73		simplr3	$⊢ (((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N)) \land a \in N) \to d \in N$
74	52 6 4 59 60 60 60 63 66 73 68	mamufv	$⊢ (((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N)) \land a \in N) \to d (b (R maMul ⟨N, N, N⟩) G) a = \underset{e \in N}{\sum_{R}} ((d b e) \underset{˙}{\cdot} (e G a))$
75	72 74	eqtr3d	$⊢ (((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N)) \land a \in N) \to d (b \underset{˙}{∙} G) a = \underset{e \in N}{\sum_{R}} ((d b e) \underset{˙}{\cdot} (e G a))$
76	75	3adantl3	$⊢ (((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N) \land (c \neq d \land \forall e \in N c b e = d b e)) \land a \in N) \to d (b \underset{˙}{∙} G) a = \underset{e \in N}{\sum_{R}} ((d b e) \underset{˙}{\cdot} (e G a))$
77	50 71 76	3eqtr4d	$⊢ (((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N) \land (c \neq d \land \forall e \in N c b e = d b e)) \land a \in N) \to c (b \underset{˙}{∙} G) a = d (b \underset{˙}{∙} G) a$
78	77	ralrimiva	$⊢ ((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N) \land (c \neq d \land \forall e \in N c b e = d b e)) \to \forall a \in N c (b \underset{˙}{∙} G) a = d (b \underset{˙}{∙} G) a$
79	3 1 2 7 33 39 40 41 42 78	mdetralt	$⊢ ((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N) \land (c \neq d \land \forall e \in N c b e = d b e)) \to D (b \underset{˙}{∙} G) = 0_{R}$
80	32 79	eqtrd	$⊢ ((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N) \land (c \neq d \land \forall e \in N c b e = d b e)) \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (b) = 0_{R}$
81	80	3expia	$⊢ ((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in N \land d \in N)) \to ((c \neq d \land \forall e \in N c b e = d b e) \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (b) = 0_{R})$
82	81	ralrimivvva	$⊢ (R \in CRing \land F \in B \land G \in B) \to \forall b \in B \forall c \in N \forall d \in N ((c \neq d \land \forall e \in N c b e = d b e) \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (b) = 0_{R})$
83		simp11	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {c ↾}_{((N ∖ \{e\}) \times N)} \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to R \in CRing$
84	19	adantr	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to A \in Ring$
85		simprll	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to b \in B$
86		simpl3	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to G \in B$
87	84 85 86 37	syl3anc	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to b \underset{˙}{∙} G \in B$
88	87	3adant3	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {c ↾}_{((N ∖ \{e\}) \times N)} \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to b \underset{˙}{∙} G \in B$
89		simprlr	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to c \in B$
90	2 5	ringcl	$⊢ (A \in Ring \land c \in B \land G \in B) \to c \underset{˙}{∙} G \in B$
91	84 89 86 90	syl3anc	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to c \underset{˙}{∙} G \in B$
92	91	3adant3	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {c ↾}_{((N ∖ \{e\}) \times N)} \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to c \underset{˙}{∙} G \in B$
93		simprrl	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to d \in B$
94	2 5	ringcl	$⊢ (A \in Ring \land d \in B \land G \in B) \to d \underset{˙}{∙} G \in B$
95	84 93 86 94	syl3anc	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to d \underset{˙}{∙} G \in B$
96	95	3adant3	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {c ↾}_{((N ∖ \{e\}) \times N)} \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to d \underset{˙}{∙} G \in B$
97		simp2rr	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {c ↾}_{((N ∖ \{e\}) \times N)} \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to e \in N$
98		simp31	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {c ↾}_{((N ∖ \{e\}) \times N)} \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to {b ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)})$
99	98	oveq1d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {c ↾}_{((N ∖ \{e\}) \times N)} \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to ({b ↾}_{(\{e\} \times N)}) (R maMul ⟨\{e\}, N, N⟩) G = (({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)})) (R maMul ⟨\{e\}, N, N⟩) G$
100	14	adantr	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to R \in Ring$
101		eqid	$⊢ R maMul ⟨\{e\}, N, N⟩ = R maMul ⟨\{e\}, N, N⟩$
102		snfi	$⊢ \{e\} \in Fin$
103	102	a1i	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to \{e\} \in Fin$
104	12	adantr	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to N \in Fin$
105	1 6 2	matbas2i	$⊢ c \in B \to c \in ({Base}_{R}^{(N \times N)})$
106	89 105	syl	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to c \in ({Base}_{R}^{(N \times N)})$
107		simprrr	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to e \in N$
108	107	snssd	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to \{e\} \subseteq N$
109		xpss1	$⊢ \{e\} \subseteq N \to \{e\} \times N \subseteq N \times N$
110	108 109	syl	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to \{e\} \times N \subseteq N \times N$
111		elmapssres	$⊢ (c \in ({Base}_{R}^{(N \times N)}) \land \{e\} \times N \subseteq N \times N) \to {c ↾}_{(\{e\} \times N)} \in ({Base}_{R}^{(\{e\} \times N)})$
112	106 110 111	syl2anc	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to {c ↾}_{(\{e\} \times N)} \in ({Base}_{R}^{(\{e\} \times N)})$
113	1 6 2	matbas2i	$⊢ d \in B \to d \in ({Base}_{R}^{(N \times N)})$
114	93 113	syl	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to d \in ({Base}_{R}^{(N \times N)})$
115		elmapssres	$⊢ (d \in ({Base}_{R}^{(N \times N)}) \land \{e\} \times N \subseteq N \times N) \to {d ↾}_{(\{e\} \times N)} \in ({Base}_{R}^{(\{e\} \times N)})$
116	114 110 115	syl2anc	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to {d ↾}_{(\{e\} \times N)} \in ({Base}_{R}^{(\{e\} \times N)})$
117	65	adantr	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to G \in ({Base}_{R}^{(N \times N)})$
118	6 100 101 103 104 104 9 112 116 117	mamudi	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to (({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)})) (R maMul ⟨\{e\}, N, N⟩) G = (({c ↾}_{(\{e\} \times N)}) (R maMul ⟨\{e\}, N, N⟩) G) {+_{R}}_{f} (({d ↾}_{(\{e\} \times N)}) (R maMul ⟨\{e\}, N, N⟩) G)$
119	118	3adant3	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {c ↾}_{((N ∖ \{e\}) \times N)} \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to (({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)})) (R maMul ⟨\{e\}, N, N⟩) G = (({c ↾}_{(\{e\} \times N)}) (R maMul ⟨\{e\}, N, N⟩) G) {+_{R}}_{f} (({d ↾}_{(\{e\} \times N)}) (R maMul ⟨\{e\}, N, N⟩) G)$
120	99 119	eqtrd	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {c ↾}_{((N ∖ \{e\}) \times N)} \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to ({b ↾}_{(\{e\} \times N)}) (R maMul ⟨\{e\}, N, N⟩) G = (({c ↾}_{(\{e\} \times N)}) (R maMul ⟨\{e\}, N, N⟩) G) {+_{R}}_{f} (({d ↾}_{(\{e\} \times N)}) (R maMul ⟨\{e\}, N, N⟩) G)$
121	55	adantr	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to R maMul ⟨N, N, N⟩ = \underset{˙}{∙}$
122	121	oveqd	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to b (R maMul ⟨N, N, N⟩) G = b \underset{˙}{∙} G$
123	122	reseq1d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to {(b (R maMul ⟨N, N, N⟩) G) ↾}_{(\{e\} \times N)} = {(b \underset{˙}{∙} G) ↾}_{(\{e\} \times N)}$
124		simpl1	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to R \in CRing$
125	85 62	syl	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to b \in ({Base}_{R}^{(N \times N)})$
126	52 101 6 124 104 104 104 108 125 117	mamures	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to {(b (R maMul ⟨N, N, N⟩) G) ↾}_{(\{e\} \times N)} = ({b ↾}_{(\{e\} \times N)}) (R maMul ⟨\{e\}, N, N⟩) G$
127	123 126	eqtr3d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to {(b \underset{˙}{∙} G) ↾}_{(\{e\} \times N)} = ({b ↾}_{(\{e\} \times N)}) (R maMul ⟨\{e\}, N, N⟩) G$
128	127	3adant3	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {c ↾}_{((N ∖ \{e\}) \times N)} \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to {(b \underset{˙}{∙} G) ↾}_{(\{e\} \times N)} = ({b ↾}_{(\{e\} \times N)}) (R maMul ⟨\{e\}, N, N⟩) G$
129	121	oveqd	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to c (R maMul ⟨N, N, N⟩) G = c \underset{˙}{∙} G$
130	129	reseq1d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to {(c (R maMul ⟨N, N, N⟩) G) ↾}_{(\{e\} \times N)} = {(c \underset{˙}{∙} G) ↾}_{(\{e\} \times N)}$
131	52 101 6 124 104 104 104 108 106 117	mamures	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to {(c (R maMul ⟨N, N, N⟩) G) ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) (R maMul ⟨\{e\}, N, N⟩) G$
132	130 131	eqtr3d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to {(c \underset{˙}{∙} G) ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) (R maMul ⟨\{e\}, N, N⟩) G$
133	121	oveqd	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to d (R maMul ⟨N, N, N⟩) G = d \underset{˙}{∙} G$
134	133	reseq1d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to {(d (R maMul ⟨N, N, N⟩) G) ↾}_{(\{e\} \times N)} = {(d \underset{˙}{∙} G) ↾}_{(\{e\} \times N)}$
135	52 101 6 124 104 104 104 108 114 117	mamures	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to {(d (R maMul ⟨N, N, N⟩) G) ↾}_{(\{e\} \times N)} = ({d ↾}_{(\{e\} \times N)}) (R maMul ⟨\{e\}, N, N⟩) G$
136	134 135	eqtr3d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to {(d \underset{˙}{∙} G) ↾}_{(\{e\} \times N)} = ({d ↾}_{(\{e\} \times N)}) (R maMul ⟨\{e\}, N, N⟩) G$
137	132 136	oveq12d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to ({(c \underset{˙}{∙} G) ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({(d \underset{˙}{∙} G) ↾}_{(\{e\} \times N)}) = (({c ↾}_{(\{e\} \times N)}) (R maMul ⟨\{e\}, N, N⟩) G) {+_{R}}_{f} (({d ↾}_{(\{e\} \times N)}) (R maMul ⟨\{e\}, N, N⟩) G)$
138	137	3adant3	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {c ↾}_{((N ∖ \{e\}) \times N)} \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to ({(c \underset{˙}{∙} G) ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({(d \underset{˙}{∙} G) ↾}_{(\{e\} \times N)}) = (({c ↾}_{(\{e\} \times N)}) (R maMul ⟨\{e\}, N, N⟩) G) {+_{R}}_{f} (({d ↾}_{(\{e\} \times N)}) (R maMul ⟨\{e\}, N, N⟩) G)$
139	120 128 138	3eqtr4d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {c ↾}_{((N ∖ \{e\}) \times N)} \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to {(b \underset{˙}{∙} G) ↾}_{(\{e\} \times N)} = ({(c \underset{˙}{∙} G) ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({(d \underset{˙}{∙} G) ↾}_{(\{e\} \times N)})$
140		simp32	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {c ↾}_{((N ∖ \{e\}) \times N)} \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to {b ↾}_{((N ∖ \{e\}) \times N)} = {c ↾}_{((N ∖ \{e\}) \times N)}$
141	140	oveq1d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {c ↾}_{((N ∖ \{e\}) \times N)} \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to ({b ↾}_{((N ∖ \{e\}) \times N)}) (R maMul ⟨N ∖ \{e\}, N, N⟩) G = ({c ↾}_{((N ∖ \{e\}) \times N)}) (R maMul ⟨N ∖ \{e\}, N, N⟩) G$
142	122	reseq1d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to {(b (R maMul ⟨N, N, N⟩) G) ↾}_{((N ∖ \{e\}) \times N)} = {(b \underset{˙}{∙} G) ↾}_{((N ∖ \{e\}) \times N)}$
143		eqid	$⊢ R maMul ⟨N ∖ \{e\}, N, N⟩ = R maMul ⟨N ∖ \{e\}, N, N⟩$
144		difssd	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to N ∖ \{e\} \subseteq N$
145	52 143 6 124 104 104 104 144 125 117	mamures	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to {(b (R maMul ⟨N, N, N⟩) G) ↾}_{((N ∖ \{e\}) \times N)} = ({b ↾}_{((N ∖ \{e\}) \times N)}) (R maMul ⟨N ∖ \{e\}, N, N⟩) G$
146	142 145	eqtr3d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to {(b \underset{˙}{∙} G) ↾}_{((N ∖ \{e\}) \times N)} = ({b ↾}_{((N ∖ \{e\}) \times N)}) (R maMul ⟨N ∖ \{e\}, N, N⟩) G$
147	146	3adant3	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {c ↾}_{((N ∖ \{e\}) \times N)} \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to {(b \underset{˙}{∙} G) ↾}_{((N ∖ \{e\}) \times N)} = ({b ↾}_{((N ∖ \{e\}) \times N)}) (R maMul ⟨N ∖ \{e\}, N, N⟩) G$
148	129	reseq1d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to {(c (R maMul ⟨N, N, N⟩) G) ↾}_{((N ∖ \{e\}) \times N)} = {(c \underset{˙}{∙} G) ↾}_{((N ∖ \{e\}) \times N)}$
149	52 143 6 124 104 104 104 144 106 117	mamures	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to {(c (R maMul ⟨N, N, N⟩) G) ↾}_{((N ∖ \{e\}) \times N)} = ({c ↾}_{((N ∖ \{e\}) \times N)}) (R maMul ⟨N ∖ \{e\}, N, N⟩) G$
150	148 149	eqtr3d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to {(c \underset{˙}{∙} G) ↾}_{((N ∖ \{e\}) \times N)} = ({c ↾}_{((N ∖ \{e\}) \times N)}) (R maMul ⟨N ∖ \{e\}, N, N⟩) G$
151	150	3adant3	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {c ↾}_{((N ∖ \{e\}) \times N)} \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to {(c \underset{˙}{∙} G) ↾}_{((N ∖ \{e\}) \times N)} = ({c ↾}_{((N ∖ \{e\}) \times N)}) (R maMul ⟨N ∖ \{e\}, N, N⟩) G$
152	141 147 151	3eqtr4d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {c ↾}_{((N ∖ \{e\}) \times N)} \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to {(b \underset{˙}{∙} G) ↾}_{((N ∖ \{e\}) \times N)} = {(c \underset{˙}{∙} G) ↾}_{((N ∖ \{e\}) \times N)}$
153		simp33	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {c ↾}_{((N ∖ \{e\}) \times N)} \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)}$
154	153	oveq1d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {c ↾}_{((N ∖ \{e\}) \times N)} \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to ({b ↾}_{((N ∖ \{e\}) \times N)}) (R maMul ⟨N ∖ \{e\}, N, N⟩) G = ({d ↾}_{((N ∖ \{e\}) \times N)}) (R maMul ⟨N ∖ \{e\}, N, N⟩) G$
155	133	reseq1d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to {(d (R maMul ⟨N, N, N⟩) G) ↾}_{((N ∖ \{e\}) \times N)} = {(d \underset{˙}{∙} G) ↾}_{((N ∖ \{e\}) \times N)}$
156	52 143 6 124 104 104 104 144 114 117	mamures	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to {(d (R maMul ⟨N, N, N⟩) G) ↾}_{((N ∖ \{e\}) \times N)} = ({d ↾}_{((N ∖ \{e\}) \times N)}) (R maMul ⟨N ∖ \{e\}, N, N⟩) G$
157	155 156	eqtr3d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to {(d \underset{˙}{∙} G) ↾}_{((N ∖ \{e\}) \times N)} = ({d ↾}_{((N ∖ \{e\}) \times N)}) (R maMul ⟨N ∖ \{e\}, N, N⟩) G$
158	157	3adant3	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {c ↾}_{((N ∖ \{e\}) \times N)} \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to {(d \underset{˙}{∙} G) ↾}_{((N ∖ \{e\}) \times N)} = ({d ↾}_{((N ∖ \{e\}) \times N)}) (R maMul ⟨N ∖ \{e\}, N, N⟩) G$
159	154 147 158	3eqtr4d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {c ↾}_{((N ∖ \{e\}) \times N)} \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to {(b \underset{˙}{∙} G) ↾}_{((N ∖ \{e\}) \times N)} = {(d \underset{˙}{∙} G) ↾}_{((N ∖ \{e\}) \times N)}$
160	3 1 2 9 83 88 92 96 97 139 152 159	mdetrlin	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {c ↾}_{((N ∖ \{e\}) \times N)} \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to D (b \underset{˙}{∙} G) = D (c \underset{˙}{∙} G) +_{R} D (d \underset{˙}{∙} G)$
161	85 31	syl	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (b) = D (b \underset{˙}{∙} G)$
162	161	3adant3	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {c ↾}_{((N ∖ \{e\}) \times N)} \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (b) = D (b \underset{˙}{∙} G)$
163		fvoveq1	$⊢ a = c \to D (a \underset{˙}{∙} G) = D (c \underset{˙}{∙} G)$
164		fvex	$⊢ D (c \underset{˙}{∙} G) \in V$
165	163 29 164	fvmpt	$⊢ c \in B \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (c) = D (c \underset{˙}{∙} G)$
166	89 165	syl	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (c) = D (c \underset{˙}{∙} G)$
167		fvoveq1	$⊢ a = d \to D (a \underset{˙}{∙} G) = D (d \underset{˙}{∙} G)$
168		fvex	$⊢ D (d \underset{˙}{∙} G) \in V$
169	167 29 168	fvmpt	$⊢ d \in B \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (d) = D (d \underset{˙}{∙} G)$
170	93 169	syl	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (d) = D (d \underset{˙}{∙} G)$
171	166 170	oveq12d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (c) +_{R} (a \in B ⟼ D (a \underset{˙}{∙} G)) (d) = D (c \underset{˙}{∙} G) +_{R} D (d \underset{˙}{∙} G)$
172	171	3adant3	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {c ↾}_{((N ∖ \{e\}) \times N)} \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (c) +_{R} (a \in B ⟼ D (a \underset{˙}{∙} G)) (d) = D (c \underset{˙}{∙} G) +_{R} D (d \underset{˙}{∙} G)$
173	160 162 172	3eqtr4d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {c ↾}_{((N ∖ \{e\}) \times N)} \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (b) = (a \in B ⟼ D (a \underset{˙}{∙} G)) (c) +_{R} (a \in B ⟼ D (a \underset{˙}{∙} G)) (d)$
174	173	3expia	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to (({b ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {c ↾}_{((N ∖ \{e\}) \times N)} \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)}) \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (b) = (a \in B ⟼ D (a \underset{˙}{∙} G)) (c) +_{R} (a \in B ⟼ D (a \underset{˙}{∙} G)) (d))$
175	174	anassrs	$⊢ (((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in B)) \land (d \in B \land e \in N)) \to (({b ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {c ↾}_{((N ∖ \{e\}) \times N)} \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)}) \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (b) = (a \in B ⟼ D (a \underset{˙}{∙} G)) (c) +_{R} (a \in B ⟼ D (a \underset{˙}{∙} G)) (d))$
176	175	ralrimivva	$⊢ ((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in B)) \to \forall d \in B \forall e \in N (({b ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {c ↾}_{((N ∖ \{e\}) \times N)} \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)}) \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (b) = (a \in B ⟼ D (a \underset{˙}{∙} G)) (c) +_{R} (a \in B ⟼ D (a \underset{˙}{∙} G)) (d))$
177	176	ralrimivva	$⊢ (R \in CRing \land F \in B \land G \in B) \to \forall b \in B \forall c \in B \forall d \in B \forall e \in N (({b ↾}_{(\{e\} \times N)} = ({c ↾}_{(\{e\} \times N)}) {+_{R}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {c ↾}_{((N ∖ \{e\}) \times N)} \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)}) \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (b) = (a \in B ⟼ D (a \underset{˙}{∙} G)) (c) +_{R} (a \in B ⟼ D (a \underset{˙}{∙} G)) (d))$
178		simp11	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to R \in CRing$
179	19	adantr	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to A \in Ring$
180		simprll	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to b \in B$
181		simpl3	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to G \in B$
182	179 180 181 37	syl3anc	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to b \underset{˙}{∙} G \in B$
183	182	3adant3	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to b \underset{˙}{∙} G \in B$
184		simp2lr	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to c \in {Base}_{R}$
185		simprrl	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to d \in B$
186	179 185 181 94	syl3anc	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to d \underset{˙}{∙} G \in B$
187	186	3adant3	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to d \underset{˙}{∙} G \in B$
188		simp2rr	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to e \in N$
189		simp3l	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to {b ↾}_{(\{e\} \times N)} = ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({d ↾}_{(\{e\} \times N)})$
190	189	oveq1d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to ({b ↾}_{(\{e\} \times N)}) (R maMul ⟨\{e\}, N, N⟩) G = (((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({d ↾}_{(\{e\} \times N)})) (R maMul ⟨\{e\}, N, N⟩) G$
191	55	adantr	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to R maMul ⟨N, N, N⟩ = \underset{˙}{∙}$
192	191	oveqd	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to b (R maMul ⟨N, N, N⟩) G = b \underset{˙}{∙} G$
193	192	reseq1d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to {(b (R maMul ⟨N, N, N⟩) G) ↾}_{(\{e\} \times N)} = {(b \underset{˙}{∙} G) ↾}_{(\{e\} \times N)}$
194		simpl1	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to R \in CRing$
195	12	adantr	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to N \in Fin$
196		simprrr	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to e \in N$
197	196	snssd	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to \{e\} \subseteq N$
198	180 62	syl	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to b \in ({Base}_{R}^{(N \times N)})$
199	65	adantr	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to G \in ({Base}_{R}^{(N \times N)})$
200	52 101 6 194 195 195 195 197 198 199	mamures	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to {(b (R maMul ⟨N, N, N⟩) G) ↾}_{(\{e\} \times N)} = ({b ↾}_{(\{e\} \times N)}) (R maMul ⟨\{e\}, N, N⟩) G$
201	193 200	eqtr3d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to {(b \underset{˙}{∙} G) ↾}_{(\{e\} \times N)} = ({b ↾}_{(\{e\} \times N)}) (R maMul ⟨\{e\}, N, N⟩) G$
202	201	3adant3	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to {(b \underset{˙}{∙} G) ↾}_{(\{e\} \times N)} = ({b ↾}_{(\{e\} \times N)}) (R maMul ⟨\{e\}, N, N⟩) G$
203	191	oveqd	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to d (R maMul ⟨N, N, N⟩) G = d \underset{˙}{∙} G$
204	203	reseq1d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to {(d (R maMul ⟨N, N, N⟩) G) ↾}_{(\{e\} \times N)} = {(d \underset{˙}{∙} G) ↾}_{(\{e\} \times N)}$
205	185 113	syl	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to d \in ({Base}_{R}^{(N \times N)})$
206	52 101 6 194 195 195 195 197 205 199	mamures	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to {(d (R maMul ⟨N, N, N⟩) G) ↾}_{(\{e\} \times N)} = ({d ↾}_{(\{e\} \times N)}) (R maMul ⟨\{e\}, N, N⟩) G$
207	204 206	eqtr3d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to {(d \underset{˙}{∙} G) ↾}_{(\{e\} \times N)} = ({d ↾}_{(\{e\} \times N)}) (R maMul ⟨\{e\}, N, N⟩) G$
208	207	oveq2d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({(d \underset{˙}{∙} G) ↾}_{(\{e\} \times N)}) = ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} (({d ↾}_{(\{e\} \times N)}) (R maMul ⟨\{e\}, N, N⟩) G)$
209	14	adantr	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to R \in Ring$
210	102	a1i	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to \{e\} \in Fin$
211		simprlr	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to c \in {Base}_{R}$
212	197 109	syl	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to \{e\} \times N \subseteq N \times N$
213	205 212 115	syl2anc	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to {d ↾}_{(\{e\} \times N)} \in ({Base}_{R}^{(\{e\} \times N)})$
214	6 209 101 210 195 195 4 211 213 199	mamuvs1	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to (((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({d ↾}_{(\{e\} \times N)})) (R maMul ⟨\{e\}, N, N⟩) G = ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} (({d ↾}_{(\{e\} \times N)}) (R maMul ⟨\{e\}, N, N⟩) G)$
215	208 214	eqtr4d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({(d \underset{˙}{∙} G) ↾}_{(\{e\} \times N)}) = (((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({d ↾}_{(\{e\} \times N)})) (R maMul ⟨\{e\}, N, N⟩) G$
216	215	3adant3	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({(d \underset{˙}{∙} G) ↾}_{(\{e\} \times N)}) = (((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({d ↾}_{(\{e\} \times N)})) (R maMul ⟨\{e\}, N, N⟩) G$
217	190 202 216	3eqtr4d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to {(b \underset{˙}{∙} G) ↾}_{(\{e\} \times N)} = ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({(d \underset{˙}{∙} G) ↾}_{(\{e\} \times N)})$
218		simp3r	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)}$
219	218	oveq1d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to ({b ↾}_{((N ∖ \{e\}) \times N)}) (R maMul ⟨N ∖ \{e\}, N, N⟩) G = ({d ↾}_{((N ∖ \{e\}) \times N)}) (R maMul ⟨N ∖ \{e\}, N, N⟩) G$
220	192	reseq1d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to {(b (R maMul ⟨N, N, N⟩) G) ↾}_{((N ∖ \{e\}) \times N)} = {(b \underset{˙}{∙} G) ↾}_{((N ∖ \{e\}) \times N)}$
221		difssd	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to N ∖ \{e\} \subseteq N$
222	52 143 6 194 195 195 195 221 198 199	mamures	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to {(b (R maMul ⟨N, N, N⟩) G) ↾}_{((N ∖ \{e\}) \times N)} = ({b ↾}_{((N ∖ \{e\}) \times N)}) (R maMul ⟨N ∖ \{e\}, N, N⟩) G$
223	220 222	eqtr3d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to {(b \underset{˙}{∙} G) ↾}_{((N ∖ \{e\}) \times N)} = ({b ↾}_{((N ∖ \{e\}) \times N)}) (R maMul ⟨N ∖ \{e\}, N, N⟩) G$
224	223	3adant3	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to {(b \underset{˙}{∙} G) ↾}_{((N ∖ \{e\}) \times N)} = ({b ↾}_{((N ∖ \{e\}) \times N)}) (R maMul ⟨N ∖ \{e\}, N, N⟩) G$
225	203	reseq1d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to {(d (R maMul ⟨N, N, N⟩) G) ↾}_{((N ∖ \{e\}) \times N)} = {(d \underset{˙}{∙} G) ↾}_{((N ∖ \{e\}) \times N)}$
226	52 143 6 194 195 195 195 221 205 199	mamures	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to {(d (R maMul ⟨N, N, N⟩) G) ↾}_{((N ∖ \{e\}) \times N)} = ({d ↾}_{((N ∖ \{e\}) \times N)}) (R maMul ⟨N ∖ \{e\}, N, N⟩) G$
227	225 226	eqtr3d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to {(d \underset{˙}{∙} G) ↾}_{((N ∖ \{e\}) \times N)} = ({d ↾}_{((N ∖ \{e\}) \times N)}) (R maMul ⟨N ∖ \{e\}, N, N⟩) G$
228	227	3adant3	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to {(d \underset{˙}{∙} G) ↾}_{((N ∖ \{e\}) \times N)} = ({d ↾}_{((N ∖ \{e\}) \times N)}) (R maMul ⟨N ∖ \{e\}, N, N⟩) G$
229	219 224 228	3eqtr4d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to {(b \underset{˙}{∙} G) ↾}_{((N ∖ \{e\}) \times N)} = {(d \underset{˙}{∙} G) ↾}_{((N ∖ \{e\}) \times N)}$
230	3 1 2 6 4 178 183 184 187 188 217 229	mdetrsca	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to D (b \underset{˙}{∙} G) = c \underset{˙}{\cdot} D (d \underset{˙}{∙} G)$
231		simp2ll	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to b \in B$
232	231 31	syl	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (b) = D (b \underset{˙}{∙} G)$
233		simp2rl	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to d \in B$
234	169	oveq2d	$⊢ d \in B \to c \underset{˙}{\cdot} (a \in B ⟼ D (a \underset{˙}{∙} G)) (d) = c \underset{˙}{\cdot} D (d \underset{˙}{∙} G)$
235	233 234	syl	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to c \underset{˙}{\cdot} (a \in B ⟼ D (a \underset{˙}{∙} G)) (d) = c \underset{˙}{\cdot} D (d \underset{˙}{∙} G)$
236	230 232 235	3eqtr4d	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N)) \land ({b ↾}_{(\{e\} \times N)} = ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)})) \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (b) = c \underset{˙}{\cdot} (a \in B ⟼ D (a \underset{˙}{∙} G)) (d)$
237	236	3expia	$⊢ ((R \in CRing \land F \in B \land G \in B) \land ((b \in B \land c \in {Base}_{R}) \land (d \in B \land e \in N))) \to (({b ↾}_{(\{e\} \times N)} = ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)}) \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (b) = c \underset{˙}{\cdot} (a \in B ⟼ D (a \underset{˙}{∙} G)) (d))$
238	237	anassrs	$⊢ (((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in {Base}_{R})) \land (d \in B \land e \in N)) \to (({b ↾}_{(\{e\} \times N)} = ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)}) \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (b) = c \underset{˙}{\cdot} (a \in B ⟼ D (a \underset{˙}{∙} G)) (d))$
239	238	ralrimivva	$⊢ ((R \in CRing \land F \in B \land G \in B) \land (b \in B \land c \in {Base}_{R})) \to \forall d \in B \forall e \in N (({b ↾}_{(\{e\} \times N)} = ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)}) \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (b) = c \underset{˙}{\cdot} (a \in B ⟼ D (a \underset{˙}{∙} G)) (d))$
240	239	ralrimivva	$⊢ (R \in CRing \land F \in B \land G \in B) \to \forall b \in B \forall c \in {Base}_{R} \forall d \in B \forall e \in N (({b ↾}_{(\{e\} \times N)} = ((\{e\} \times N) \times \{c\}) {\underset{˙}{\cdot}}_{f} ({d ↾}_{(\{e\} \times N)}) \land {b ↾}_{((N ∖ \{e\}) \times N)} = {d ↾}_{((N ∖ \{e\}) \times N)}) \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (b) = c \underset{˙}{\cdot} (a \in B ⟼ D (a \underset{˙}{∙} G)) (d))$
241		simp2	$⊢ (R \in CRing \land F \in B \land G \in B) \to F \in B$
242	1 2 6 7 8 9 4 12 14 26 82 177 240 3 51 241	mdetuni0	$⊢ (R \in CRing \land F \in B \land G \in B) \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (F) = (a \in B ⟼ D (a \underset{˙}{∙} G)) (1_{A}) \underset{˙}{\cdot} D (F)$
243		fvoveq1	$⊢ a = F \to D (a \underset{˙}{∙} G) = D (F \underset{˙}{∙} G)$
244		fvex	$⊢ D (F \underset{˙}{∙} G) \in V$
245	243 29 244	fvmpt	$⊢ F \in B \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (F) = D (F \underset{˙}{∙} G)$
246	245	3ad2ant2	$⊢ (R \in CRing \land F \in B \land G \in B) \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (F) = D (F \underset{˙}{∙} G)$
247		eqid	$⊢ 1_{A} = 1_{A}$
248	2 247	ringidcl	$⊢ A \in Ring \to 1_{A} \in B$
249		fvoveq1	$⊢ a = 1_{A} \to D (a \underset{˙}{∙} G) = D (1_{A} \underset{˙}{∙} G)$
250		fvex	$⊢ D (1_{A} \underset{˙}{∙} G) \in V$
251	249 29 250	fvmpt	$⊢ 1_{A} \in B \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (1_{A}) = D (1_{A} \underset{˙}{∙} G)$
252	19 248 251	3syl	$⊢ (R \in CRing \land F \in B \land G \in B) \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (1_{A}) = D (1_{A} \underset{˙}{∙} G)$
253		simp3	$⊢ (R \in CRing \land F \in B \land G \in B) \to G \in B$
254	2 5 247	ringlidm	$⊢ (A \in Ring \land G \in B) \to 1_{A} \underset{˙}{∙} G = G$
255	19 253 254	syl2anc	$⊢ (R \in CRing \land F \in B \land G \in B) \to 1_{A} \underset{˙}{∙} G = G$
256	255	fveq2d	$⊢ (R \in CRing \land F \in B \land G \in B) \to D (1_{A} \underset{˙}{∙} G) = D (G)$
257	252 256	eqtrd	$⊢ (R \in CRing \land F \in B \land G \in B) \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (1_{A}) = D (G)$
258	257	oveq1d	$⊢ (R \in CRing \land F \in B \land G \in B) \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (1_{A}) \underset{˙}{\cdot} D (F) = D (G) \underset{˙}{\cdot} D (F)$
259	16 253	ffvelrnd	$⊢ (R \in CRing \land F \in B \land G \in B) \to D (G) \in {Base}_{R}$
260	16 241	ffvelrnd	$⊢ (R \in CRing \land F \in B \land G \in B) \to D (F) \in {Base}_{R}$
261	6 4	crngcom	$⊢ (R \in CRing \land D (G) \in {Base}_{R} \land D (F) \in {Base}_{R}) \to D (G) \underset{˙}{\cdot} D (F) = D (F) \underset{˙}{\cdot} D (G)$
262	51 259 260 261	syl3anc	$⊢ (R \in CRing \land F \in B \land G \in B) \to D (G) \underset{˙}{\cdot} D (F) = D (F) \underset{˙}{\cdot} D (G)$
263	258 262	eqtrd	$⊢ (R \in CRing \land F \in B \land G \in B) \to (a \in B ⟼ D (a \underset{˙}{∙} G)) (1_{A}) \underset{˙}{\cdot} D (F) = D (F) \underset{˙}{\cdot} D (G)$
264	242 246 263	3eqtr3d	$⊢ (R \in CRing \land F \in B \land G \in B) \to D (F \underset{˙}{∙} G) = D (F) \underset{˙}{\cdot} D (G)$

Metamath Proof Explorer

Theorem mdetmul

Proof