mdetuni0

	Ref	Expression
Hypotheses	mdetuni.a	$⊢ A = N Mat R$
	mdetuni.b	$⊢ B = {Base}_{A}$
	mdetuni.k	$⊢ K = {Base}_{R}$
	mdetuni.0g	$⊢ \underset{˙}{0} = 0_{R}$
	mdetuni.1r	$⊢ \underset{˙}{1} = 1_{R}$
	mdetuni.pg	$⊢ \underset{˙}{+} = +_{R}$
	mdetuni.tg	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	mdetuni.n	$⊢ φ \to N \in Fin$
	mdetuni.r	$⊢ φ \to R \in Ring$
	mdetuni.ff	$⊢ φ \to D : B ⟶ K$
	mdetuni.al	$⊢ φ \to \forall x \in B \forall y \in N \forall z \in N ((y \neq z \land \forall w \in N y x w = z x w) \to D (x) = \underset{˙}{0})$
	mdetuni.li	$⊢ φ \to \forall x \in B \forall y \in B \forall z \in B \forall w \in N (({x ↾}_{(\{w\} \times N)} = ({y ↾}_{(\{w\} \times N)}) {\underset{˙}{+}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {x ↾}_{((N ∖ \{w\}) \times N)} = {y ↾}_{((N ∖ \{w\}) \times N)} \land {x ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}) \to D (x) = D (y) \underset{˙}{+} D (z))$
	mdetuni.sc	$⊢ φ \to \forall x \in B \forall y \in K \forall z \in B \forall w \in N (({x ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{y\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {x ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}) \to D (x) = y \underset{˙}{\cdot} D (z))$
	mdetuni.e	$⊢ E = N maDet R$
	mdetuni.cr	$⊢ φ \to R \in CRing$
	mdetuni.f	$⊢ φ \to F \in B$
Assertion	mdetuni0	$⊢ φ \to D (F) = D (1_{A}) \underset{˙}{\cdot} E (F)$

Proof

Step	Hyp	Ref	Expression
1		mdetuni.a	$⊢ A = N Mat R$
2		mdetuni.b	$⊢ B = {Base}_{A}$
3		mdetuni.k	$⊢ K = {Base}_{R}$
4		mdetuni.0g	$⊢ \underset{˙}{0} = 0_{R}$
5		mdetuni.1r	$⊢ \underset{˙}{1} = 1_{R}$
6		mdetuni.pg	$⊢ \underset{˙}{+} = +_{R}$
7		mdetuni.tg	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
8		mdetuni.n	$⊢ φ \to N \in Fin$
9		mdetuni.r	$⊢ φ \to R \in Ring$
10		mdetuni.ff	$⊢ φ \to D : B ⟶ K$
11		mdetuni.al	$⊢ φ \to \forall x \in B \forall y \in N \forall z \in N ((y \neq z \land \forall w \in N y x w = z x w) \to D (x) = \underset{˙}{0})$
12		mdetuni.li	$⊢ φ \to \forall x \in B \forall y \in B \forall z \in B \forall w \in N (({x ↾}_{(\{w\} \times N)} = ({y ↾}_{(\{w\} \times N)}) {\underset{˙}{+}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {x ↾}_{((N ∖ \{w\}) \times N)} = {y ↾}_{((N ∖ \{w\}) \times N)} \land {x ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}) \to D (x) = D (y) \underset{˙}{+} D (z))$
13		mdetuni.sc	$⊢ φ \to \forall x \in B \forall y \in K \forall z \in B \forall w \in N (({x ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{y\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {x ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}) \to D (x) = y \underset{˙}{\cdot} D (z))$
14		mdetuni.e	$⊢ E = N maDet R$
15		mdetuni.cr	$⊢ φ \to R \in CRing$
16		mdetuni.f	$⊢ φ \to F \in B$
17		ringgrp	$⊢ R \in Ring \to R \in Grp$
18	9 17	syl	$⊢ φ \to R \in Grp$
19	18	adantr	$⊢ (φ \land a \in B) \to R \in Grp$
20	10	ffvelrnda	$⊢ (φ \land a \in B) \to D (a) \in K$
21	9	adantr	$⊢ (φ \land a \in B) \to R \in Ring$
22	8 9	jca	$⊢ φ \to (N \in Fin \land R \in Ring)$
23	1	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
24		eqid	$⊢ 1_{A} = 1_{A}$
25	2 24	ringidcl	$⊢ A \in Ring \to 1_{A} \in B$
26	22 23 25	3syl	$⊢ φ \to 1_{A} \in B$
27	10 26	ffvelrnd	$⊢ φ \to D (1_{A}) \in K$
28	27	adantr	$⊢ (φ \land a \in B) \to D (1_{A}) \in K$
29	14 1 2 3	mdetf	$⊢ R \in CRing \to E : B ⟶ K$
30	15 29	syl	$⊢ φ \to E : B ⟶ K$
31	30	ffvelrnda	$⊢ (φ \land a \in B) \to E (a) \in K$
32	3 7	ringcl	$⊢ (R \in Ring \land D (1_{A}) \in K \land E (a) \in K) \to D (1_{A}) \underset{˙}{\cdot} E (a) \in K$
33	21 28 31 32	syl3anc	$⊢ (φ \land a \in B) \to D (1_{A}) \underset{˙}{\cdot} E (a) \in K$
34		eqid	$⊢ -_{R} = -_{R}$
35	3 34	grpsubcl	$⊢ (R \in Grp \land D (a) \in K \land D (1_{A}) \underset{˙}{\cdot} E (a) \in K) \to D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a)) \in K$
36	19 20 33 35	syl3anc	$⊢ (φ \land a \in B) \to D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a)) \in K$
37	36	fmpttd	$⊢ φ \to (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) : B ⟶ K$
38		simpr1	$⊢ (φ \land (b \in B \land c \in N \land d \in N)) \to b \in B$
39		fveq2	$⊢ a = b \to D (a) = D (b)$
40		fveq2	$⊢ a = b \to E (a) = E (b)$
41	40	oveq2d	$⊢ a = b \to D (1_{A}) \underset{˙}{\cdot} E (a) = D (1_{A}) \underset{˙}{\cdot} E (b)$
42	39 41	oveq12d	$⊢ a = b \to D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a)) = D (b) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (b))$
43		eqid	$⊢ (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) = (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a)))$
44		ovex	$⊢ D (b) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (b)) \in V$
45	42 43 44	fvmpt	$⊢ b \in B \to (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (b) = D (b) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (b))$
46	38 45	syl	$⊢ (φ \land (b \in B \land c \in N \land d \in N)) \to (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (b) = D (b) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (b))$
47	46	3adant3	$⊢ (φ \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) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (b) = D (b) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (b))$
48		simp1	$⊢ (φ \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 φ$
49		simp21	$⊢ (φ \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$
50		simp3r	$⊢ (φ \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 e \in N c b e = d b e$
51		oveq2	$⊢ e = w \to c b e = c b w$
52		oveq2	$⊢ e = w \to d b e = d b w$
53	51 52	eqeq12d	$⊢ e = w \to (c b e = d b e \leftrightarrow c b w = d b w)$
54	53	cbvralvw	$⊢ \forall e \in N c b e = d b e \leftrightarrow \forall w \in N c b w = d b w$
55	50 54	sylib	$⊢ (φ \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 w \in N c b w = d b w$
56		simp22	$⊢ (φ \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$
57		simp23	$⊢ (φ \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$
58		simp3l	$⊢ (φ \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$
59	1 2 3 4 5 6 7 8 9 10 11 12 13	mdetunilem1	$⊢ ((φ \land b \in B \land \forall w \in N c b w = d b w) \land (c \in N \land d \in N \land c \neq d)) \to D (b) = \underset{˙}{0}$
60	48 49 55 56 57 58 59	syl33anc	$⊢ (φ \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{˙}{0}$
61	15	3ad2ant1	$⊢ (φ \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$
62	14 1 2 4 61 49 56 57 58 50	mdetralt	$⊢ (φ \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 E (b) = \underset{˙}{0}$
63	62	oveq2d	$⊢ (φ \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 (1_{A}) \underset{˙}{\cdot} E (b) = D (1_{A}) \underset{˙}{\cdot} \underset{˙}{0}$
64	60 63	oveq12d	$⊢ (φ \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) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (b)) = \underset{˙}{0} -_{R} (D (1_{A}) \underset{˙}{\cdot} \underset{˙}{0})$
65	3 7 4	ringrz	$⊢ (R \in Ring \land D (1_{A}) \in K) \to D (1_{A}) \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
66	9 27 65	syl2anc	$⊢ φ \to D (1_{A}) \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
67	66	oveq2d	$⊢ φ \to \underset{˙}{0} -_{R} (D (1_{A}) \underset{˙}{\cdot} \underset{˙}{0}) = \underset{˙}{0} -_{R} \underset{˙}{0}$
68	3 4	grpidcl	$⊢ R \in Grp \to \underset{˙}{0} \in K$
69	3 4 34	grpsubid	$⊢ (R \in Grp \land \underset{˙}{0} \in K) \to \underset{˙}{0} -_{R} \underset{˙}{0} = \underset{˙}{0}$
70	18 68 69	syl2anc2	$⊢ φ \to \underset{˙}{0} -_{R} \underset{˙}{0} = \underset{˙}{0}$
71	67 70	eqtrd	$⊢ φ \to \underset{˙}{0} -_{R} (D (1_{A}) \underset{˙}{\cdot} \underset{˙}{0}) = \underset{˙}{0}$
72	71	3ad2ant1	$⊢ (φ \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 \underset{˙}{0} -_{R} (D (1_{A}) \underset{˙}{\cdot} \underset{˙}{0}) = \underset{˙}{0}$
73	47 64 72	3eqtrd	$⊢ (φ \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) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (b) = \underset{˙}{0}$
74	73	3expia	$⊢ (φ \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) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (b) = \underset{˙}{0})$
75	74	ralrimivvva	$⊢ φ \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) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (b) = \underset{˙}{0})$
76		simp1	$⊢ (φ \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)}) {\underset{˙}{+}}_{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 φ$
77		simp2ll	$⊢ (φ \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)}) {\underset{˙}{+}}_{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 \in B$
78		simp2lr	$⊢ (φ \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)}) {\underset{˙}{+}}_{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 \in B$
79		simp2rl	$⊢ (φ \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)}) {\underset{˙}{+}}_{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 \in B$
80		simp2rr	$⊢ (φ \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)}) {\underset{˙}{+}}_{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$
81		simp31	$⊢ (φ \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)}) {\underset{˙}{+}}_{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)}) {\underset{˙}{+}}_{f} ({d ↾}_{(\{e\} \times N)})$
82		simp32	$⊢ (φ \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)}) {\underset{˙}{+}}_{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)}$
83		simp33	$⊢ (φ \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)}) {\underset{˙}{+}}_{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)}$
84	1 2 3 4 5 6 7 8 9 10 11 12 13	mdetunilem3	$⊢ ((φ \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)}) {\underset{˙}{+}}_{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) = D (c) \underset{˙}{+} D (d)$
85	76 77 78 79 80 81 82 83 84	syl332anc	$⊢ (φ \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)}) {\underset{˙}{+}}_{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) = D (c) \underset{˙}{+} D (d)$
86	15	3ad2ant1	$⊢ (φ \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)}) {\underset{˙}{+}}_{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$
87	14 1 2 6 86 77 78 79 80 81 82 83	mdetrlin	$⊢ (φ \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)}) {\underset{˙}{+}}_{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 (b) = E (c) \underset{˙}{+} E (d)$
88	87	oveq2d	$⊢ (φ \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)}) {\underset{˙}{+}}_{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 (1_{A}) \underset{˙}{\cdot} E (b) = D (1_{A}) \underset{˙}{\cdot} (E (c) \underset{˙}{+} E (d))$
89	85 88	oveq12d	$⊢ (φ \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)}) {\underset{˙}{+}}_{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) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (b)) = (D (c) \underset{˙}{+} D (d)) -_{R} (D (1_{A}) \underset{˙}{\cdot} (E (c) \underset{˙}{+} E (d)))$
90		simprll	$⊢ (φ \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to b \in B$
91	90 45	syl	$⊢ (φ \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (b) = D (b) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (b))$
92	91	3adant3	$⊢ (φ \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)}) {\underset{˙}{+}}_{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) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (b) = D (b) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (b))$
93		simprlr	$⊢ (φ \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to c \in B$
94		fveq2	$⊢ a = c \to D (a) = D (c)$
95		fveq2	$⊢ a = c \to E (a) = E (c)$
96	95	oveq2d	$⊢ a = c \to D (1_{A}) \underset{˙}{\cdot} E (a) = D (1_{A}) \underset{˙}{\cdot} E (c)$
97	94 96	oveq12d	$⊢ a = c \to D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a)) = D (c) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (c))$
98		ovex	$⊢ D (c) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (c)) \in V$
99	97 43 98	fvmpt	$⊢ c \in B \to (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (c) = D (c) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (c))$
100	93 99	syl	$⊢ (φ \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (c) = D (c) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (c))$
101		simprrl	$⊢ (φ \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to d \in B$
102		fveq2	$⊢ a = d \to D (a) = D (d)$
103		fveq2	$⊢ a = d \to E (a) = E (d)$
104	103	oveq2d	$⊢ a = d \to D (1_{A}) \underset{˙}{\cdot} E (a) = D (1_{A}) \underset{˙}{\cdot} E (d)$
105	102 104	oveq12d	$⊢ a = d \to D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a)) = D (d) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (d))$
106		ovex	$⊢ D (d) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (d)) \in V$
107	105 43 106	fvmpt	$⊢ d \in B \to (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (d) = D (d) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (d))$
108	101 107	syl	$⊢ (φ \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (d) = D (d) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (d))$
109	100 108	oveq12d	$⊢ (φ \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (c) \underset{˙}{+} (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (d) = (D (c) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (c))) \underset{˙}{+} (D (d) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (d)))$
110		ringabl	$⊢ R \in Ring \to R \in Abel$
111	9 110	syl	$⊢ φ \to R \in Abel$
112	111	adantr	$⊢ (φ \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to R \in Abel$
113	10	adantr	$⊢ (φ \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to D : B ⟶ K$
114	113 93	ffvelrnd	$⊢ (φ \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to D (c) \in K$
115	113 101	ffvelrnd	$⊢ (φ \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to D (d) \in K$
116	9	adantr	$⊢ (φ \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to R \in Ring$
117	27	adantr	$⊢ (φ \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to D (1_{A}) \in K$
118	30	adantr	$⊢ (φ \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to E : B ⟶ K$
119	118 93	ffvelrnd	$⊢ (φ \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to E (c) \in K$
120	3 7	ringcl	$⊢ (R \in Ring \land D (1_{A}) \in K \land E (c) \in K) \to D (1_{A}) \underset{˙}{\cdot} E (c) \in K$
121	116 117 119 120	syl3anc	$⊢ (φ \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to D (1_{A}) \underset{˙}{\cdot} E (c) \in K$
122	118 101	ffvelrnd	$⊢ (φ \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to E (d) \in K$
123	3 7	ringcl	$⊢ (R \in Ring \land D (1_{A}) \in K \land E (d) \in K) \to D (1_{A}) \underset{˙}{\cdot} E (d) \in K$
124	116 117 122 123	syl3anc	$⊢ (φ \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to D (1_{A}) \underset{˙}{\cdot} E (d) \in K$
125	3 6 34	ablsub4	$⊢ (R \in Abel \land (D (c) \in K \land D (d) \in K) \land (D (1_{A}) \underset{˙}{\cdot} E (c) \in K \land D (1_{A}) \underset{˙}{\cdot} E (d) \in K)) \to (D (c) \underset{˙}{+} D (d)) -_{R} ((D (1_{A}) \underset{˙}{\cdot} E (c)) \underset{˙}{+} (D (1_{A}) \underset{˙}{\cdot} E (d))) = (D (c) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (c))) \underset{˙}{+} (D (d) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (d)))$
126	112 114 115 121 124 125	syl122anc	$⊢ (φ \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to (D (c) \underset{˙}{+} D (d)) -_{R} ((D (1_{A}) \underset{˙}{\cdot} E (c)) \underset{˙}{+} (D (1_{A}) \underset{˙}{\cdot} E (d))) = (D (c) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (c))) \underset{˙}{+} (D (d) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (d)))$
127	3 6 7	ringdi	$⊢ (R \in Ring \land (D (1_{A}) \in K \land E (c) \in K \land E (d) \in K)) \to D (1_{A}) \underset{˙}{\cdot} (E (c) \underset{˙}{+} E (d)) = (D (1_{A}) \underset{˙}{\cdot} E (c)) \underset{˙}{+} (D (1_{A}) \underset{˙}{\cdot} E (d))$
128	116 117 119 122 127	syl13anc	$⊢ (φ \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to D (1_{A}) \underset{˙}{\cdot} (E (c) \underset{˙}{+} E (d)) = (D (1_{A}) \underset{˙}{\cdot} E (c)) \underset{˙}{+} (D (1_{A}) \underset{˙}{\cdot} E (d))$
129	128	eqcomd	$⊢ (φ \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to (D (1_{A}) \underset{˙}{\cdot} E (c)) \underset{˙}{+} (D (1_{A}) \underset{˙}{\cdot} E (d)) = D (1_{A}) \underset{˙}{\cdot} (E (c) \underset{˙}{+} E (d))$
130	129	oveq2d	$⊢ (φ \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to (D (c) \underset{˙}{+} D (d)) -_{R} ((D (1_{A}) \underset{˙}{\cdot} E (c)) \underset{˙}{+} (D (1_{A}) \underset{˙}{\cdot} E (d))) = (D (c) \underset{˙}{+} D (d)) -_{R} (D (1_{A}) \underset{˙}{\cdot} (E (c) \underset{˙}{+} E (d)))$
131	109 126 130	3eqtr2d	$⊢ (φ \land ((b \in B \land c \in B) \land (d \in B \land e \in N))) \to (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (c) \underset{˙}{+} (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (d) = (D (c) \underset{˙}{+} D (d)) -_{R} (D (1_{A}) \underset{˙}{\cdot} (E (c) \underset{˙}{+} E (d)))$
132	131	3adant3	$⊢ (φ \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)}) {\underset{˙}{+}}_{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) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (c) \underset{˙}{+} (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (d) = (D (c) \underset{˙}{+} D (d)) -_{R} (D (1_{A}) \underset{˙}{\cdot} (E (c) \underset{˙}{+} E (d)))$
133	89 92 132	3eqtr4d	$⊢ (φ \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)}) {\underset{˙}{+}}_{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) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (b) = (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (c) \underset{˙}{+} (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (d)$
134	133	3expia	$⊢ (φ \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)}) {\underset{˙}{+}}_{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) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (b) = (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (c) \underset{˙}{+} (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (d))$
135	134	anassrs	$⊢ ((φ \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)}) {\underset{˙}{+}}_{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) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (b) = (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (c) \underset{˙}{+} (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (d))$
136	135	ralrimivva	$⊢ (φ \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)}) {\underset{˙}{+}}_{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) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (b) = (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (c) \underset{˙}{+} (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (d))$
137	136	ralrimivva	$⊢ φ \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)}) {\underset{˙}{+}}_{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) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (b) = (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (c) \underset{˙}{+} (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (d))$
138		simp1	$⊢ (φ \land ((b \in B \land c \in K) \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 φ$
139		simp2ll	$⊢ (φ \land ((b \in B \land c \in K) \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$
140		simp2lr	$⊢ (φ \land ((b \in B \land c \in K) \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 K$
141		simp2rl	$⊢ (φ \land ((b \in B \land c \in K) \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$
142		simp2rr	$⊢ (φ \land ((b \in B \land c \in K) \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$
143		simp3l	$⊢ (φ \land ((b \in B \land c \in K) \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)})$
144		simp3r	$⊢ (φ \land ((b \in B \land c \in K) \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)}$
145	1 2 3 4 5 6 7 8 9 10 11 12 13	mdetunilem4	$⊢ (φ \land (b \in B \land c \in K \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) = c \underset{˙}{\cdot} D (d)$
146	138 139 140 141 142 143 144 145	syl133anc	$⊢ (φ \land ((b \in B \land c \in K) \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) = c \underset{˙}{\cdot} D (d)$
147	15	3ad2ant1	$⊢ (φ \land ((b \in B \land c \in K) \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$
148	14 1 2 3 7 147 139 140 141 142 143 144	mdetrsca	$⊢ (φ \land ((b \in B \land c \in K) \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 (b) = c \underset{˙}{\cdot} E (d)$
149	148	oveq2d	$⊢ (φ \land ((b \in B \land c \in K) \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 (1_{A}) \underset{˙}{\cdot} E (b) = D (1_{A}) \underset{˙}{\cdot} (c \underset{˙}{\cdot} E (d))$
150	146 149	oveq12d	$⊢ (φ \land ((b \in B \land c \in K) \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) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (b)) = (c \underset{˙}{\cdot} D (d)) -_{R} (D (1_{A}) \underset{˙}{\cdot} (c \underset{˙}{\cdot} E (d)))$
151		simprll	$⊢ (φ \land ((b \in B \land c \in K) \land (d \in B \land e \in N))) \to b \in B$
152	151 45	syl	$⊢ (φ \land ((b \in B \land c \in K) \land (d \in B \land e \in N))) \to (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (b) = D (b) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (b))$
153	152	3adant3	$⊢ (φ \land ((b \in B \land c \in K) \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) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (b) = D (b) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (b))$
154		simprrl	$⊢ (φ \land ((b \in B \land c \in K) \land (d \in B \land e \in N))) \to d \in B$
155	154 107	syl	$⊢ (φ \land ((b \in B \land c \in K) \land (d \in B \land e \in N))) \to (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (d) = D (d) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (d))$
156	155	oveq2d	$⊢ (φ \land ((b \in B \land c \in K) \land (d \in B \land e \in N))) \to c \underset{˙}{\cdot} (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (d) = c \underset{˙}{\cdot} (D (d) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (d)))$
157	9	adantr	$⊢ (φ \land ((b \in B \land c \in K) \land (d \in B \land e \in N))) \to R \in Ring$
158		simprlr	$⊢ (φ \land ((b \in B \land c \in K) \land (d \in B \land e \in N))) \to c \in K$
159	10	adantr	$⊢ (φ \land ((b \in B \land c \in K) \land (d \in B \land e \in N))) \to D : B ⟶ K$
160	159 154	ffvelrnd	$⊢ (φ \land ((b \in B \land c \in K) \land (d \in B \land e \in N))) \to D (d) \in K$
161	27	adantr	$⊢ (φ \land ((b \in B \land c \in K) \land (d \in B \land e \in N))) \to D (1_{A}) \in K$
162	30	adantr	$⊢ (φ \land ((b \in B \land c \in K) \land (d \in B \land e \in N))) \to E : B ⟶ K$
163	162 154	ffvelrnd	$⊢ (φ \land ((b \in B \land c \in K) \land (d \in B \land e \in N))) \to E (d) \in K$
164	157 161 163 123	syl3anc	$⊢ (φ \land ((b \in B \land c \in K) \land (d \in B \land e \in N))) \to D (1_{A}) \underset{˙}{\cdot} E (d) \in K$
165	3 7 34 157 158 160 164	ringsubdi	$⊢ (φ \land ((b \in B \land c \in K) \land (d \in B \land e \in N))) \to c \underset{˙}{\cdot} (D (d) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (d))) = (c \underset{˙}{\cdot} D (d)) -_{R} (c \underset{˙}{\cdot} (D (1_{A}) \underset{˙}{\cdot} E (d)))$
166		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
167	166	crngmgp	$⊢ R \in CRing \to {mulGrp}_{R} \in CMnd$
168	15 167	syl	$⊢ φ \to {mulGrp}_{R} \in CMnd$
169	168	adantr	$⊢ (φ \land ((b \in B \land c \in K) \land (d \in B \land e \in N))) \to {mulGrp}_{R} \in CMnd$
170	166 3	mgpbas	$⊢ K = {Base}_{{mulGrp}_{R}}$
171	166 7	mgpplusg	$⊢ \underset{˙}{\cdot} = +_{{mulGrp}_{R}}$
172	170 171	cmn12	$⊢ ({mulGrp}_{R} \in CMnd \land (c \in K \land D (1_{A}) \in K \land E (d) \in K)) \to c \underset{˙}{\cdot} (D (1_{A}) \underset{˙}{\cdot} E (d)) = D (1_{A}) \underset{˙}{\cdot} (c \underset{˙}{\cdot} E (d))$
173	169 158 161 163 172	syl13anc	$⊢ (φ \land ((b \in B \land c \in K) \land (d \in B \land e \in N))) \to c \underset{˙}{\cdot} (D (1_{A}) \underset{˙}{\cdot} E (d)) = D (1_{A}) \underset{˙}{\cdot} (c \underset{˙}{\cdot} E (d))$
174	173	oveq2d	$⊢ (φ \land ((b \in B \land c \in K) \land (d \in B \land e \in N))) \to (c \underset{˙}{\cdot} D (d)) -_{R} (c \underset{˙}{\cdot} (D (1_{A}) \underset{˙}{\cdot} E (d))) = (c \underset{˙}{\cdot} D (d)) -_{R} (D (1_{A}) \underset{˙}{\cdot} (c \underset{˙}{\cdot} E (d)))$
175	156 165 174	3eqtrd	$⊢ (φ \land ((b \in B \land c \in K) \land (d \in B \land e \in N))) \to c \underset{˙}{\cdot} (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (d) = (c \underset{˙}{\cdot} D (d)) -_{R} (D (1_{A}) \underset{˙}{\cdot} (c \underset{˙}{\cdot} E (d)))$
176	175	3adant3	$⊢ (φ \land ((b \in B \land c \in K) \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) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (d) = (c \underset{˙}{\cdot} D (d)) -_{R} (D (1_{A}) \underset{˙}{\cdot} (c \underset{˙}{\cdot} E (d)))$
177	150 153 176	3eqtr4d	$⊢ (φ \land ((b \in B \land c \in K) \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) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (b) = c \underset{˙}{\cdot} (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (d)$
178	177	3expia	$⊢ (φ \land ((b \in B \land c \in K) \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) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (b) = c \underset{˙}{\cdot} (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (d))$
179	178	anassrs	$⊢ ((φ \land (b \in B \land c \in K)) \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) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (b) = c \underset{˙}{\cdot} (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (d))$
180	179	ralrimivva	$⊢ (φ \land (b \in B \land c \in K)) \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) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (b) = c \underset{˙}{\cdot} (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (d))$
181	180	ralrimivva	$⊢ φ \to \forall b \in B \forall c \in K \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) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (b) = c \underset{˙}{\cdot} (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (d))$
182		eqidd	$⊢ φ \to (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) = (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a)))$
183		fveq2	$⊢ a = 1_{A} \to D (a) = D (1_{A})$
184		fveq2	$⊢ a = 1_{A} \to E (a) = E (1_{A})$
185	184	oveq2d	$⊢ a = 1_{A} \to D (1_{A}) \underset{˙}{\cdot} E (a) = D (1_{A}) \underset{˙}{\cdot} E (1_{A})$
186	183 185	oveq12d	$⊢ a = 1_{A} \to D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a)) = D (1_{A}) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (1_{A}))$
187	14 1 24 5	mdet1	$⊢ (R \in CRing \land N \in Fin) \to E (1_{A}) = \underset{˙}{1}$
188	15 8 187	syl2anc	$⊢ φ \to E (1_{A}) = \underset{˙}{1}$
189	188	oveq2d	$⊢ φ \to D (1_{A}) \underset{˙}{\cdot} E (1_{A}) = D (1_{A}) \underset{˙}{\cdot} \underset{˙}{1}$
190	3 7 5	ringridm	$⊢ (R \in Ring \land D (1_{A}) \in K) \to D (1_{A}) \underset{˙}{\cdot} \underset{˙}{1} = D (1_{A})$
191	9 27 190	syl2anc	$⊢ φ \to D (1_{A}) \underset{˙}{\cdot} \underset{˙}{1} = D (1_{A})$
192	189 191	eqtrd	$⊢ φ \to D (1_{A}) \underset{˙}{\cdot} E (1_{A}) = D (1_{A})$
193	192	oveq2d	$⊢ φ \to D (1_{A}) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (1_{A})) = D (1_{A}) -_{R} D (1_{A})$
194	3 4 34	grpsubid	$⊢ (R \in Grp \land D (1_{A}) \in K) \to D (1_{A}) -_{R} D (1_{A}) = \underset{˙}{0}$
195	18 27 194	syl2anc	$⊢ φ \to D (1_{A}) -_{R} D (1_{A}) = \underset{˙}{0}$
196	193 195	eqtrd	$⊢ φ \to D (1_{A}) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (1_{A})) = \underset{˙}{0}$
197	186 196	sylan9eqr	$⊢ (φ \land a = 1_{A}) \to D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a)) = \underset{˙}{0}$
198	4	fvexi	$⊢ \underset{˙}{0} \in V$
199	198	a1i	$⊢ φ \to \underset{˙}{0} \in V$
200	182 197 26 199	fvmptd	$⊢ φ \to (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (1_{A}) = \underset{˙}{0}$
201		eqid	$⊢ \{b \| \forall c \in B \forall d \in (N^{N}) (\forall e \in b c (e) = if (e \in d, \underset{˙}{1}, \underset{˙}{0}) \to (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (c) = \underset{˙}{0})\} = \{b \| \forall c \in B \forall d \in (N^{N}) (\forall e \in b c (e) = if (e \in d, \underset{˙}{1}, \underset{˙}{0}) \to (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (c) = \underset{˙}{0})\}$
202	1 2 3 4 5 6 7 8 9 37 75 137 181 200 201	mdetunilem9	$⊢ φ \to (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) = B \times \{\underset{˙}{0}\}$
203	202	fveq1d	$⊢ φ \to (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (F) = (B \times \{\underset{˙}{0}\}) (F)$
204		fveq2	$⊢ a = F \to D (a) = D (F)$
205		fveq2	$⊢ a = F \to E (a) = E (F)$
206	205	oveq2d	$⊢ a = F \to D (1_{A}) \underset{˙}{\cdot} E (a) = D (1_{A}) \underset{˙}{\cdot} E (F)$
207	204 206	oveq12d	$⊢ a = F \to D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a)) = D (F) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (F))$
208	207	adantl	$⊢ (φ \land a = F) \to D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a)) = D (F) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (F))$
209		ovexd	$⊢ φ \to D (F) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (F)) \in V$
210	182 208 16 209	fvmptd	$⊢ φ \to (a \in B ⟼ D (a) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (a))) (F) = D (F) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (F))$
211	198	fvconst2	$⊢ F \in B \to (B \times \{\underset{˙}{0}\}) (F) = \underset{˙}{0}$
212	16 211	syl	$⊢ φ \to (B \times \{\underset{˙}{0}\}) (F) = \underset{˙}{0}$
213	203 210 212	3eqtr3d	$⊢ φ \to D (F) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (F)) = \underset{˙}{0}$
214	10 16	ffvelrnd	$⊢ φ \to D (F) \in K$
215	30 16	ffvelrnd	$⊢ φ \to E (F) \in K$
216	3 7	ringcl	$⊢ (R \in Ring \land D (1_{A}) \in K \land E (F) \in K) \to D (1_{A}) \underset{˙}{\cdot} E (F) \in K$
217	9 27 215 216	syl3anc	$⊢ φ \to D (1_{A}) \underset{˙}{\cdot} E (F) \in K$
218	3 4 34	grpsubeq0	$⊢ (R \in Grp \land D (F) \in K \land D (1_{A}) \underset{˙}{\cdot} E (F) \in K) \to (D (F) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (F)) = \underset{˙}{0} \leftrightarrow D (F) = D (1_{A}) \underset{˙}{\cdot} E (F))$
219	18 214 217 218	syl3anc	$⊢ φ \to (D (F) -_{R} (D (1_{A}) \underset{˙}{\cdot} E (F)) = \underset{˙}{0} \leftrightarrow D (F) = D (1_{A}) \underset{˙}{\cdot} E (F))$
220	213 219	mpbid	$⊢ φ \to D (F) = D (1_{A}) \underset{˙}{\cdot} E (F)$

Metamath Proof Explorer

Theorem mdetuni0

Proof