madugsum

Description: The determinant of a matrix with a row L consisting of the same element X is the sum of the elements of the L -th column of the adjunct of the matrix multiplied with X . (Contributed by Stefan O'Rear, 16-Jul-2018)

	Ref	Expression
Hypotheses	maduf.a	$⊢ A = N Mat R$
	maduf.j	$⊢ J = N maAdju R$
	maduf.b	$⊢ B = {Base}_{A}$
	madugsum.d	$⊢ D = N maDet R$
	madugsum.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	madugsum.k	$⊢ K = {Base}_{R}$
	madugsum.m	$⊢ φ \to M \in B$
	madugsum.r	$⊢ φ \to R \in CRing$
	madugsum.x	$⊢ (φ \land i \in N) \to X \in K$
	madugsum.l	$⊢ φ \to L \in N$
Assertion	madugsum	$⊢ φ \to \underset{i \in N}{\sum_{R}} (X \underset{˙}{\cdot} (i J (M) L)) = D ((j \in N, i \in N ⟼ if (j = L, X, j M i)))$

Proof

Step	Hyp	Ref	Expression
1		maduf.a	$⊢ A = N Mat R$
2		maduf.j	$⊢ J = N maAdju R$
3		maduf.b	$⊢ B = {Base}_{A}$
4		madugsum.d	$⊢ D = N maDet R$
5		madugsum.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
6		madugsum.k	$⊢ K = {Base}_{R}$
7		madugsum.m	$⊢ φ \to M \in B$
8		madugsum.r	$⊢ φ \to R \in CRing$
9		madugsum.x	$⊢ (φ \land i \in N) \to X \in K$
10		madugsum.l	$⊢ φ \to L \in N$
11		mpteq1	$⊢ c = \emptyset \to (b \in c ⟼ ⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = (b \in \emptyset ⟼ ⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L))$
12	11	oveq2d	$⊢ c = \emptyset \to \underset{b \in c}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = \underset{b \in \emptyset}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L))$
13		eleq2	$⊢ c = \emptyset \to (b \in c \leftrightarrow b \in \emptyset)$
14	13	ifbid	$⊢ c = \emptyset \to if (b \in c, ⦋ b / i ⦌ X, 0_{R}) = if (b \in \emptyset, ⦋ b / i ⦌ X, 0_{R})$
15	14	ifeq1d	$⊢ c = \emptyset \to if (a = L, if (b \in c, ⦋ b / i ⦌ X, 0_{R}), a M b) = if (a = L, if (b \in \emptyset, ⦋ b / i ⦌ X, 0_{R}), a M b)$
16	15	mpoeq3dv	$⊢ c = \emptyset \to (a \in N, b \in N ⟼ if (a = L, if (b \in c, ⦋ b / i ⦌ X, 0_{R}), a M b)) = (a \in N, b \in N ⟼ if (a = L, if (b \in \emptyset, ⦋ b / i ⦌ X, 0_{R}), a M b))$
17	16	fveq2d	$⊢ c = \emptyset \to D ((a \in N, b \in N ⟼ if (a = L, if (b \in c, ⦋ b / i ⦌ X, 0_{R}), a M b))) = D ((a \in N, b \in N ⟼ if (a = L, if (b \in \emptyset, ⦋ b / i ⦌ X, 0_{R}), a M b)))$
18	12 17	eqeq12d	$⊢ c = \emptyset \to (\underset{b \in c}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = D ((a \in N, b \in N ⟼ if (a = L, if (b \in c, ⦋ b / i ⦌ X, 0_{R}), a M b))) \leftrightarrow \underset{b \in \emptyset}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = D ((a \in N, b \in N ⟼ if (a = L, if (b \in \emptyset, ⦋ b / i ⦌ X, 0_{R}), a M b))))$
19		mpteq1	$⊢ c = d \to (b \in c ⟼ ⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = (b \in d ⟼ ⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L))$
20	19	oveq2d	$⊢ c = d \to \underset{b \in c}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = \underset{b \in d}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L))$
21		eleq2	$⊢ c = d \to (b \in c \leftrightarrow b \in d)$
22	21	ifbid	$⊢ c = d \to if (b \in c, ⦋ b / i ⦌ X, 0_{R}) = if (b \in d, ⦋ b / i ⦌ X, 0_{R})$
23	22	ifeq1d	$⊢ c = d \to if (a = L, if (b \in c, ⦋ b / i ⦌ X, 0_{R}), a M b) = if (a = L, if (b \in d, ⦋ b / i ⦌ X, 0_{R}), a M b)$
24	23	mpoeq3dv	$⊢ c = d \to (a \in N, b \in N ⟼ if (a = L, if (b \in c, ⦋ b / i ⦌ X, 0_{R}), a M b)) = (a \in N, b \in N ⟼ if (a = L, if (b \in d, ⦋ b / i ⦌ X, 0_{R}), a M b))$
25	24	fveq2d	$⊢ c = d \to D ((a \in N, b \in N ⟼ if (a = L, if (b \in c, ⦋ b / i ⦌ X, 0_{R}), a M b))) = D ((a \in N, b \in N ⟼ if (a = L, if (b \in d, ⦋ b / i ⦌ X, 0_{R}), a M b)))$
26	20 25	eqeq12d	$⊢ c = d \to (\underset{b \in c}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = D ((a \in N, b \in N ⟼ if (a = L, if (b \in c, ⦋ b / i ⦌ X, 0_{R}), a M b))) \leftrightarrow \underset{b \in d}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = D ((a \in N, b \in N ⟼ if (a = L, if (b \in d, ⦋ b / i ⦌ X, 0_{R}), a M b))))$
27		mpteq1	$⊢ c = d \cup \{e\} \to (b \in c ⟼ ⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = (b \in (d \cup \{e\}) ⟼ ⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L))$
28	27	oveq2d	$⊢ c = d \cup \{e\} \to \underset{b \in c}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = \underset{b \in d \cup \{e\}}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L))$
29		eleq2	$⊢ c = d \cup \{e\} \to (b \in c \leftrightarrow b \in (d \cup \{e\}))$
30	29	ifbid	$⊢ c = d \cup \{e\} \to if (b \in c, ⦋ b / i ⦌ X, 0_{R}) = if (b \in (d \cup \{e\}), ⦋ b / i ⦌ X, 0_{R})$
31	30	ifeq1d	$⊢ c = d \cup \{e\} \to if (a = L, if (b \in c, ⦋ b / i ⦌ X, 0_{R}), a M b) = if (a = L, if (b \in (d \cup \{e\}), ⦋ b / i ⦌ X, 0_{R}), a M b)$
32	31	mpoeq3dv	$⊢ c = d \cup \{e\} \to (a \in N, b \in N ⟼ if (a = L, if (b \in c, ⦋ b / i ⦌ X, 0_{R}), a M b)) = (a \in N, b \in N ⟼ if (a = L, if (b \in (d \cup \{e\}), ⦋ b / i ⦌ X, 0_{R}), a M b))$
33	32	fveq2d	$⊢ c = d \cup \{e\} \to D ((a \in N, b \in N ⟼ if (a = L, if (b \in c, ⦋ b / i ⦌ X, 0_{R}), a M b))) = D ((a \in N, b \in N ⟼ if (a = L, if (b \in (d \cup \{e\}), ⦋ b / i ⦌ X, 0_{R}), a M b)))$
34	28 33	eqeq12d	$⊢ c = d \cup \{e\} \to (\underset{b \in c}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = D ((a \in N, b \in N ⟼ if (a = L, if (b \in c, ⦋ b / i ⦌ X, 0_{R}), a M b))) \leftrightarrow \underset{b \in d \cup \{e\}}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = D ((a \in N, b \in N ⟼ if (a = L, if (b \in (d \cup \{e\}), ⦋ b / i ⦌ X, 0_{R}), a M b))))$
35		mpteq1	$⊢ c = N \to (b \in c ⟼ ⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = (b \in N ⟼ ⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L))$
36	35	oveq2d	$⊢ c = N \to \underset{b \in c}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = \underset{b \in N}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L))$
37		eleq2	$⊢ c = N \to (b \in c \leftrightarrow b \in N)$
38	37	ifbid	$⊢ c = N \to if (b \in c, ⦋ b / i ⦌ X, 0_{R}) = if (b \in N, ⦋ b / i ⦌ X, 0_{R})$
39	38	ifeq1d	$⊢ c = N \to if (a = L, if (b \in c, ⦋ b / i ⦌ X, 0_{R}), a M b) = if (a = L, if (b \in N, ⦋ b / i ⦌ X, 0_{R}), a M b)$
40	39	mpoeq3dv	$⊢ c = N \to (a \in N, b \in N ⟼ if (a = L, if (b \in c, ⦋ b / i ⦌ X, 0_{R}), a M b)) = (a \in N, b \in N ⟼ if (a = L, if (b \in N, ⦋ b / i ⦌ X, 0_{R}), a M b))$
41	40	fveq2d	$⊢ c = N \to D ((a \in N, b \in N ⟼ if (a = L, if (b \in c, ⦋ b / i ⦌ X, 0_{R}), a M b))) = D ((a \in N, b \in N ⟼ if (a = L, if (b \in N, ⦋ b / i ⦌ X, 0_{R}), a M b)))$
42	36 41	eqeq12d	$⊢ c = N \to (\underset{b \in c}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = D ((a \in N, b \in N ⟼ if (a = L, if (b \in c, ⦋ b / i ⦌ X, 0_{R}), a M b))) \leftrightarrow \underset{b \in N}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = D ((a \in N, b \in N ⟼ if (a = L, if (b \in N, ⦋ b / i ⦌ X, 0_{R}), a M b))))$
43		mpt0	$⊢ (b \in \emptyset ⟼ ⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = \emptyset$
44	43	oveq2i	$⊢ \underset{b \in \emptyset}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = \sum_{R} \emptyset$
45		eqid	$⊢ 0_{R} = 0_{R}$
46	45	gsum0	$⊢ \sum_{R} \emptyset = 0_{R}$
47	44 46	eqtri	$⊢ \underset{b \in \emptyset}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = 0_{R}$
48		noel	$⊢ \neg b \in \emptyset$
49		iffalse	$⊢ \neg b \in \emptyset \to if (b \in \emptyset, ⦋ b / i ⦌ X, 0_{R}) = 0_{R}$
50	48 49	mp1i	$⊢ (a \in N \land b \in N) \to if (b \in \emptyset, ⦋ b / i ⦌ X, 0_{R}) = 0_{R}$
51	50	ifeq1d	$⊢ (a \in N \land b \in N) \to if (a = L, if (b \in \emptyset, ⦋ b / i ⦌ X, 0_{R}), a M b) = if (a = L, 0_{R}, a M b)$
52	51	mpoeq3ia	$⊢ (a \in N, b \in N ⟼ if (a = L, if (b \in \emptyset, ⦋ b / i ⦌ X, 0_{R}), a M b)) = (a \in N, b \in N ⟼ if (a = L, 0_{R}, a M b))$
53	52	fveq2i	$⊢ D ((a \in N, b \in N ⟼ if (a = L, if (b \in \emptyset, ⦋ b / i ⦌ X, 0_{R}), a M b))) = D ((a \in N, b \in N ⟼ if (a = L, 0_{R}, a M b)))$
54	1 3	matrcl	$⊢ M \in B \to (N \in Fin \land R \in V)$
55	7 54	syl	$⊢ φ \to (N \in Fin \land R \in V)$
56	55	simpld	$⊢ φ \to N \in Fin$
57	1 6 3	matbas2i	$⊢ M \in B \to M \in (K^{(N \times N)})$
58		elmapi	$⊢ M \in (K^{(N \times N)}) \to M : N \times N ⟶ K$
59	7 57 58	3syl	$⊢ φ \to M : N \times N ⟶ K$
60	59	fovcdmda	$⊢ (φ \land (a \in N \land b \in N)) \to a M b \in K$
61	60	3impb	$⊢ (φ \land a \in N \land b \in N) \to a M b \in K$
62	4 6 45 8 56 61 10	mdetr0	$⊢ φ \to D ((a \in N, b \in N ⟼ if (a = L, 0_{R}, a M b))) = 0_{R}$
63	53 62	eqtrid	$⊢ φ \to D ((a \in N, b \in N ⟼ if (a = L, if (b \in \emptyset, ⦋ b / i ⦌ X, 0_{R}), a M b))) = 0_{R}$
64	47 63	eqtr4id	$⊢ φ \to \underset{b \in \emptyset}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = D ((a \in N, b \in N ⟼ if (a = L, if (b \in \emptyset, ⦋ b / i ⦌ X, 0_{R}), a M b)))$
65		eqid	$⊢ +_{R} = +_{R}$
66	8	adantr	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to R \in CRing$
67		crngring	$⊢ R \in CRing \to R \in Ring$
68	66 67	syl	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to R \in Ring$
69		ringcmn	$⊢ R \in Ring \to R \in CMnd$
70	68 69	syl	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to R \in CMnd$
71	56	adantr	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to N \in Fin$
72		simprl	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to d \subseteq N$
73	71 72	ssfid	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to d \in Fin$
74	68	adantr	$⊢ ((φ \land (d \subseteq N \land e \in (N ∖ d))) \land b \in d) \to R \in Ring$
75	72	sselda	$⊢ ((φ \land (d \subseteq N \land e \in (N ∖ d))) \land b \in d) \to b \in N$
76	9	ralrimiva	$⊢ φ \to \forall i \in N X \in K$
77	76	ad2antrr	$⊢ ((φ \land (d \subseteq N \land e \in (N ∖ d))) \land b \in d) \to \forall i \in N X \in K$
78		rspcsbela	$⊢ (b \in N \land \forall i \in N X \in K) \to ⦋ b / i ⦌ X \in K$
79	75 77 78	syl2anc	$⊢ ((φ \land (d \subseteq N \land e \in (N ∖ d))) \land b \in d) \to ⦋ b / i ⦌ X \in K$
80	1 2 3	maduf	$⊢ R \in CRing \to J : B ⟶ B$
81	8 80	syl	$⊢ φ \to J : B ⟶ B$
82	81 7	ffvelcdmd	$⊢ φ \to J (M) \in B$
83	1 6 3	matbas2i	$⊢ J (M) \in B \to J (M) \in (K^{(N \times N)})$
84		elmapi	$⊢ J (M) \in (K^{(N \times N)}) \to J (M) : N \times N ⟶ K$
85	82 83 84	3syl	$⊢ φ \to J (M) : N \times N ⟶ K$
86	85	ad2antrr	$⊢ ((φ \land (d \subseteq N \land e \in (N ∖ d))) \land b \in d) \to J (M) : N \times N ⟶ K$
87	10	ad2antrr	$⊢ ((φ \land (d \subseteq N \land e \in (N ∖ d))) \land b \in d) \to L \in N$
88	86 75 87	fovcdmd	$⊢ ((φ \land (d \subseteq N \land e \in (N ∖ d))) \land b \in d) \to b J (M) L \in K$
89	6 5	ringcl	$⊢ (R \in Ring \land ⦋ b / i ⦌ X \in K \land b J (M) L \in K) \to ⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L) \in K$
90	74 79 88 89	syl3anc	$⊢ ((φ \land (d \subseteq N \land e \in (N ∖ d))) \land b \in d) \to ⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L) \in K$
91		vex	$⊢ e \in V$
92	91	a1i	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to e \in V$
93		eldifn	$⊢ e \in (N ∖ d) \to \neg e \in d$
94	93	ad2antll	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to \neg e \in d$
95		eldifi	$⊢ e \in (N ∖ d) \to e \in N$
96	95	ad2antll	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to e \in N$
97	76	adantr	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to \forall i \in N X \in K$
98		rspcsbela	$⊢ (e \in N \land \forall i \in N X \in K) \to ⦋ e / i ⦌ X \in K$
99	96 97 98	syl2anc	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to ⦋ e / i ⦌ X \in K$
100	85	adantr	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to J (M) : N \times N ⟶ K$
101	10	adantr	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to L \in N$
102	100 96 101	fovcdmd	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to e J (M) L \in K$
103	6 5	ringcl	$⊢ (R \in Ring \land ⦋ e / i ⦌ X \in K \land e J (M) L \in K) \to ⦋ e / i ⦌ X \underset{˙}{\cdot} (e J (M) L) \in K$
104	68 99 102 103	syl3anc	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to ⦋ e / i ⦌ X \underset{˙}{\cdot} (e J (M) L) \in K$
105		csbeq1	$⊢ b = e \to ⦋ b / i ⦌ X = ⦋ e / i ⦌ X$
106		oveq1	$⊢ b = e \to b J (M) L = e J (M) L$
107	105 106	oveq12d	$⊢ b = e \to ⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L) = ⦋ e / i ⦌ X \underset{˙}{\cdot} (e J (M) L)$
108	6 65 70 73 90 92 94 104 107	gsumunsn	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to \underset{b \in d \cup \{e\}}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = (\underset{b \in d}{\sum_{R}}, (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L))) +_{R} (⦋ e / i ⦌ X \underset{˙}{\cdot} (e J (M) L))$
109	108	adantr	$⊢ ((φ \land (d \subseteq N \land e \in (N ∖ d))) \land \underset{b \in d}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = D ((a \in N, b \in N ⟼ if (a = L, if (b \in d, ⦋ b / i ⦌ X, 0_{R}), a M b)))) \to \underset{b \in d \cup \{e\}}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = (\underset{b \in d}{\sum_{R}}, (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L))) +_{R} (⦋ e / i ⦌ X \underset{˙}{\cdot} (e J (M) L))$
110		oveq1	$⊢ \underset{b \in d}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = D ((a \in N, b \in N ⟼ if (a = L, if (b \in d, ⦋ b / i ⦌ X, 0_{R}), a M b))) \to (\underset{b \in d}{\sum_{R}}, (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L))) +_{R} (⦋ e / i ⦌ X \underset{˙}{\cdot} (e J (M) L)) = D ((a \in N, b \in N ⟼ if (a = L, if (b \in d, ⦋ b / i ⦌ X, 0_{R}), a M b))) +_{R} (⦋ e / i ⦌ X \underset{˙}{\cdot} (e J (M) L))$
111	110	adantl	$⊢ ((φ \land (d \subseteq N \land e \in (N ∖ d))) \land \underset{b \in d}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = D ((a \in N, b \in N ⟼ if (a = L, if (b \in d, ⦋ b / i ⦌ X, 0_{R}), a M b)))) \to (\underset{b \in d}{\sum_{R}}, (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L))) +_{R} (⦋ e / i ⦌ X \underset{˙}{\cdot} (e J (M) L)) = D ((a \in N, b \in N ⟼ if (a = L, if (b \in d, ⦋ b / i ⦌ X, 0_{R}), a M b))) +_{R} (⦋ e / i ⦌ X \underset{˙}{\cdot} (e J (M) L))$
112		elun	$⊢ b \in (d \cup \{e\}) \leftrightarrow (b \in d \lor b \in \{e\})$
113		velsn	$⊢ b \in \{e\} \leftrightarrow b = e$
114	113	orbi2i	$⊢ (b \in d \lor b \in \{e\}) \leftrightarrow (b \in d \lor b = e)$
115	112 114	bitri	$⊢ b \in (d \cup \{e\}) \leftrightarrow (b \in d \lor b = e)$
116		ifbi	$⊢ (b \in (d \cup \{e\}) \leftrightarrow (b \in d \lor b = e)) \to if (b \in (d \cup \{e\}), ⦋ b / i ⦌ X, 0_{R}) = if ((b \in d \lor b = e), ⦋ b / i ⦌ X, 0_{R})$
117	115 116	ax-mp	$⊢ if (b \in (d \cup \{e\}), ⦋ b / i ⦌ X, 0_{R}) = if ((b \in d \lor b = e), ⦋ b / i ⦌ X, 0_{R})$
118		ringmnd	$⊢ R \in Ring \to R \in Mnd$
119	68 118	syl	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to R \in Mnd$
120	119	3ad2ant1	$⊢ ((φ \land (d \subseteq N \land e \in (N ∖ d))) \land a \in N \land b \in N) \to R \in Mnd$
121		simp3	$⊢ ((φ \land (d \subseteq N \land e \in (N ∖ d))) \land a \in N \land b \in N) \to b \in N$
122	97	3ad2ant1	$⊢ ((φ \land (d \subseteq N \land e \in (N ∖ d))) \land a \in N \land b \in N) \to \forall i \in N X \in K$
123	121 122 78	syl2anc	$⊢ ((φ \land (d \subseteq N \land e \in (N ∖ d))) \land a \in N \land b \in N) \to ⦋ b / i ⦌ X \in K$
124		elequ1	$⊢ b = e \to (b \in d \leftrightarrow e \in d)$
125	124	biimpac	$⊢ (b \in d \land b = e) \to e \in d$
126	94 125	nsyl	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to \neg (b \in d \land b = e)$
127	126	3ad2ant1	$⊢ ((φ \land (d \subseteq N \land e \in (N ∖ d))) \land a \in N \land b \in N) \to \neg (b \in d \land b = e)$
128	6 45 65	mndifsplit	$⊢ (R \in Mnd \land ⦋ b / i ⦌ X \in K \land \neg (b \in d \land b = e)) \to if ((b \in d \lor b = e), ⦋ b / i ⦌ X, 0_{R}) = if (b \in d, ⦋ b / i ⦌ X, 0_{R}) +_{R} if (b = e, ⦋ b / i ⦌ X, 0_{R})$
129	120 123 127 128	syl3anc	$⊢ ((φ \land (d \subseteq N \land e \in (N ∖ d))) \land a \in N \land b \in N) \to if ((b \in d \lor b = e), ⦋ b / i ⦌ X, 0_{R}) = if (b \in d, ⦋ b / i ⦌ X, 0_{R}) +_{R} if (b = e, ⦋ b / i ⦌ X, 0_{R})$
130	117 129	eqtrid	$⊢ ((φ \land (d \subseteq N \land e \in (N ∖ d))) \land a \in N \land b \in N) \to if (b \in (d \cup \{e\}), ⦋ b / i ⦌ X, 0_{R}) = if (b \in d, ⦋ b / i ⦌ X, 0_{R}) +_{R} if (b = e, ⦋ b / i ⦌ X, 0_{R})$
131	105	adantl	$⊢ ((φ \land (d \subseteq N \land e \in (N ∖ d))) \land b = e) \to ⦋ b / i ⦌ X = ⦋ e / i ⦌ X$
132	131	ifeq1da	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to if (b = e, ⦋ b / i ⦌ X, 0_{R}) = if (b = e, ⦋ e / i ⦌ X, 0_{R})$
133		ovif2	$⊢ ⦋ e / i ⦌ X \underset{˙}{\cdot} if (b = e, 1_{R}, 0_{R}) = if (b = e, ⦋ e / i ⦌ X \underset{˙}{\cdot} 1_{R}, ⦋ e / i ⦌ X \underset{˙}{\cdot} 0_{R})$
134		eqid	$⊢ 1_{R} = 1_{R}$
135	6 5 134	ringridm	$⊢ (R \in Ring \land ⦋ e / i ⦌ X \in K) \to ⦋ e / i ⦌ X \underset{˙}{\cdot} 1_{R} = ⦋ e / i ⦌ X$
136	68 99 135	syl2anc	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to ⦋ e / i ⦌ X \underset{˙}{\cdot} 1_{R} = ⦋ e / i ⦌ X$
137	6 5 45	ringrz	$⊢ (R \in Ring \land ⦋ e / i ⦌ X \in K) \to ⦋ e / i ⦌ X \underset{˙}{\cdot} 0_{R} = 0_{R}$
138	68 99 137	syl2anc	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to ⦋ e / i ⦌ X \underset{˙}{\cdot} 0_{R} = 0_{R}$
139	136 138	ifeq12d	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to if (b = e, ⦋ e / i ⦌ X \underset{˙}{\cdot} 1_{R}, ⦋ e / i ⦌ X \underset{˙}{\cdot} 0_{R}) = if (b = e, ⦋ e / i ⦌ X, 0_{R})$
140	133 139	eqtrid	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to ⦋ e / i ⦌ X \underset{˙}{\cdot} if (b = e, 1_{R}, 0_{R}) = if (b = e, ⦋ e / i ⦌ X, 0_{R})$
141	132 140	eqtr4d	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to if (b = e, ⦋ b / i ⦌ X, 0_{R}) = ⦋ e / i ⦌ X \underset{˙}{\cdot} if (b = e, 1_{R}, 0_{R})$
142	141	oveq2d	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to if (b \in d, ⦋ b / i ⦌ X, 0_{R}) +_{R} if (b = e, ⦋ b / i ⦌ X, 0_{R}) = if (b \in d, ⦋ b / i ⦌ X, 0_{R}) +_{R} (⦋ e / i ⦌ X \underset{˙}{\cdot} if (b = e, 1_{R}, 0_{R}))$
143	142	3ad2ant1	$⊢ ((φ \land (d \subseteq N \land e \in (N ∖ d))) \land a \in N \land b \in N) \to if (b \in d, ⦋ b / i ⦌ X, 0_{R}) +_{R} if (b = e, ⦋ b / i ⦌ X, 0_{R}) = if (b \in d, ⦋ b / i ⦌ X, 0_{R}) +_{R} (⦋ e / i ⦌ X \underset{˙}{\cdot} if (b = e, 1_{R}, 0_{R}))$
144	130 143	eqtrd	$⊢ ((φ \land (d \subseteq N \land e \in (N ∖ d))) \land a \in N \land b \in N) \to if (b \in (d \cup \{e\}), ⦋ b / i ⦌ X, 0_{R}) = if (b \in d, ⦋ b / i ⦌ X, 0_{R}) +_{R} (⦋ e / i ⦌ X \underset{˙}{\cdot} if (b = e, 1_{R}, 0_{R}))$
145	144	ifeq1d	$⊢ ((φ \land (d \subseteq N \land e \in (N ∖ d))) \land a \in N \land b \in N) \to if (a = L, if (b \in (d \cup \{e\}), ⦋ b / i ⦌ X, 0_{R}), a M b) = if (a = L, if (b \in d, ⦋ b / i ⦌ X, 0_{R}) +_{R} (⦋ e / i ⦌ X \underset{˙}{\cdot} if (b = e, 1_{R}, 0_{R})), a M b)$
146	145	mpoeq3dva	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to (a \in N, b \in N ⟼ if (a = L, if (b \in (d \cup \{e\}), ⦋ b / i ⦌ X, 0_{R}), a M b)) = (a \in N, b \in N ⟼ if (a = L, if (b \in d, ⦋ b / i ⦌ X, 0_{R}) +_{R} (⦋ e / i ⦌ X \underset{˙}{\cdot} if (b = e, 1_{R}, 0_{R})), a M b))$
147	146	fveq2d	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to D ((a \in N, b \in N ⟼ if (a = L, if (b \in (d \cup \{e\}), ⦋ b / i ⦌ X, 0_{R}), a M b))) = D ((a \in N, b \in N ⟼ if (a = L, if (b \in d, ⦋ b / i ⦌ X, 0_{R}) +_{R} (⦋ e / i ⦌ X \underset{˙}{\cdot} if (b = e, 1_{R}, 0_{R})), a M b)))$
148	6 45	ring0cl	$⊢ R \in Ring \to 0_{R} \in K$
149	68 148	syl	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to 0_{R} \in K$
150	149	3ad2ant1	$⊢ ((φ \land (d \subseteq N \land e \in (N ∖ d))) \land a \in N \land b \in N) \to 0_{R} \in K$
151	123 150	ifcld	$⊢ ((φ \land (d \subseteq N \land e \in (N ∖ d))) \land a \in N \land b \in N) \to if (b \in d, ⦋ b / i ⦌ X, 0_{R}) \in K$
152	6 134	ringidcl	$⊢ R \in Ring \to 1_{R} \in K$
153	68 152	syl	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to 1_{R} \in K$
154	153 149	ifcld	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to if (b = e, 1_{R}, 0_{R}) \in K$
155	6 5	ringcl	$⊢ (R \in Ring \land ⦋ e / i ⦌ X \in K \land if (b = e, 1_{R}, 0_{R}) \in K) \to ⦋ e / i ⦌ X \underset{˙}{\cdot} if (b = e, 1_{R}, 0_{R}) \in K$
156	68 99 154 155	syl3anc	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to ⦋ e / i ⦌ X \underset{˙}{\cdot} if (b = e, 1_{R}, 0_{R}) \in K$
157	156	3ad2ant1	$⊢ ((φ \land (d \subseteq N \land e \in (N ∖ d))) \land a \in N \land b \in N) \to ⦋ e / i ⦌ X \underset{˙}{\cdot} if (b = e, 1_{R}, 0_{R}) \in K$
158	59	adantr	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to M : N \times N ⟶ K$
159	158	fovcdmda	$⊢ ((φ \land (d \subseteq N \land e \in (N ∖ d))) \land (a \in N \land b \in N)) \to a M b \in K$
160	159	3impb	$⊢ ((φ \land (d \subseteq N \land e \in (N ∖ d))) \land a \in N \land b \in N) \to a M b \in K$
161	4 6 65 66 71 151 157 160 101	mdetrlin2	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to D ((a \in N, b \in N ⟼ if (a = L, if (b \in d, ⦋ b / i ⦌ X, 0_{R}) +_{R} (⦋ e / i ⦌ X \underset{˙}{\cdot} if (b = e, 1_{R}, 0_{R})), a M b))) = D ((a \in N, b \in N ⟼ if (a = L, if (b \in d, ⦋ b / i ⦌ X, 0_{R}), a M b))) +_{R} D ((a \in N, b \in N ⟼ if (a = L, ⦋ e / i ⦌ X \underset{˙}{\cdot} if (b = e, 1_{R}, 0_{R}), a M b)))$
162	154	3ad2ant1	$⊢ ((φ \land (d \subseteq N \land e \in (N ∖ d))) \land a \in N \land b \in N) \to if (b = e, 1_{R}, 0_{R}) \in K$
163	4 6 5 66 71 162 160 99 101	mdetrsca2	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to D ((a \in N, b \in N ⟼ if (a = L, ⦋ e / i ⦌ X \underset{˙}{\cdot} if (b = e, 1_{R}, 0_{R}), a M b))) = ⦋ e / i ⦌ X \underset{˙}{\cdot} D ((a \in N, b \in N ⟼ if (a = L, if (b = e, 1_{R}, 0_{R}), a M b)))$
164	7	adantr	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to M \in B$
165	1 4 2 3 134 45	maducoeval	$⊢ (M \in B \land e \in N \land L \in N) \to e J (M) L = D ((a \in N, b \in N ⟼ if (a = L, if (b = e, 1_{R}, 0_{R}), a M b)))$
166	164 96 101 165	syl3anc	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to e J (M) L = D ((a \in N, b \in N ⟼ if (a = L, if (b = e, 1_{R}, 0_{R}), a M b)))$
167	166	oveq2d	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to ⦋ e / i ⦌ X \underset{˙}{\cdot} (e J (M) L) = ⦋ e / i ⦌ X \underset{˙}{\cdot} D ((a \in N, b \in N ⟼ if (a = L, if (b = e, 1_{R}, 0_{R}), a M b)))$
168	163 167	eqtr4d	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to D ((a \in N, b \in N ⟼ if (a = L, ⦋ e / i ⦌ X \underset{˙}{\cdot} if (b = e, 1_{R}, 0_{R}), a M b))) = ⦋ e / i ⦌ X \underset{˙}{\cdot} (e J (M) L)$
169	168	oveq2d	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to D ((a \in N, b \in N ⟼ if (a = L, if (b \in d, ⦋ b / i ⦌ X, 0_{R}), a M b))) +_{R} D ((a \in N, b \in N ⟼ if (a = L, ⦋ e / i ⦌ X \underset{˙}{\cdot} if (b = e, 1_{R}, 0_{R}), a M b))) = D ((a \in N, b \in N ⟼ if (a = L, if (b \in d, ⦋ b / i ⦌ X, 0_{R}), a M b))) +_{R} (⦋ e / i ⦌ X \underset{˙}{\cdot} (e J (M) L))$
170	147 161 169	3eqtrrd	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to D ((a \in N, b \in N ⟼ if (a = L, if (b \in d, ⦋ b / i ⦌ X, 0_{R}), a M b))) +_{R} (⦋ e / i ⦌ X \underset{˙}{\cdot} (e J (M) L)) = D ((a \in N, b \in N ⟼ if (a = L, if (b \in (d \cup \{e\}), ⦋ b / i ⦌ X, 0_{R}), a M b)))$
171	170	adantr	$⊢ ((φ \land (d \subseteq N \land e \in (N ∖ d))) \land \underset{b \in d}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = D ((a \in N, b \in N ⟼ if (a = L, if (b \in d, ⦋ b / i ⦌ X, 0_{R}), a M b)))) \to D ((a \in N, b \in N ⟼ if (a = L, if (b \in d, ⦋ b / i ⦌ X, 0_{R}), a M b))) +_{R} (⦋ e / i ⦌ X \underset{˙}{\cdot} (e J (M) L)) = D ((a \in N, b \in N ⟼ if (a = L, if (b \in (d \cup \{e\}), ⦋ b / i ⦌ X, 0_{R}), a M b)))$
172	109 111 171	3eqtrd	$⊢ ((φ \land (d \subseteq N \land e \in (N ∖ d))) \land \underset{b \in d}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = D ((a \in N, b \in N ⟼ if (a = L, if (b \in d, ⦋ b / i ⦌ X, 0_{R}), a M b)))) \to \underset{b \in d \cup \{e\}}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = D ((a \in N, b \in N ⟼ if (a = L, if (b \in (d \cup \{e\}), ⦋ b / i ⦌ X, 0_{R}), a M b)))$
173	172	ex	$⊢ (φ \land (d \subseteq N \land e \in (N ∖ d))) \to (\underset{b \in d}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = D ((a \in N, b \in N ⟼ if (a = L, if (b \in d, ⦋ b / i ⦌ X, 0_{R}), a M b))) \to \underset{b \in d \cup \{e\}}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = D ((a \in N, b \in N ⟼ if (a = L, if (b \in (d \cup \{e\}), ⦋ b / i ⦌ X, 0_{R}), a M b))))$
174	18 26 34 42 64 173 56	findcard2d	$⊢ φ \to \underset{b \in N}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)) = D ((a \in N, b \in N ⟼ if (a = L, if (b \in N, ⦋ b / i ⦌ X, 0_{R}), a M b)))$
175		nfcv	$⊢ \underline{Ⅎ} b (X \underset{˙}{\cdot} (i J (M) L))$
176		nfcsb1v	$⊢ \underline{Ⅎ} i ⦋ b / i ⦌ X$
177		nfcv	$⊢ \underline{Ⅎ} i \underset{˙}{\cdot}$
178		nfcv	$⊢ \underline{Ⅎ} i (b J (M) L)$
179	176 177 178	nfov	$⊢ \underline{Ⅎ} i (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L))$
180		csbeq1a	$⊢ i = b \to X = ⦋ b / i ⦌ X$
181		oveq1	$⊢ i = b \to i J (M) L = b J (M) L$
182	180 181	oveq12d	$⊢ i = b \to X \underset{˙}{\cdot} (i J (M) L) = ⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L)$
183	175 179 182	cbvmpt	$⊢ (i \in N ⟼ X \underset{˙}{\cdot} (i J (M) L)) = (b \in N ⟼ ⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L))$
184	183	oveq2i	$⊢ \underset{i \in N}{\sum_{R}} (X \underset{˙}{\cdot} (i J (M) L)) = \underset{b \in N}{\sum_{R}} (⦋ b / i ⦌ X \underset{˙}{\cdot} (b J (M) L))$
185		nfcv	$⊢ \underline{Ⅎ} a if (j = L, X, j M i)$
186		nfcv	$⊢ \underline{Ⅎ} b if (j = L, X, j M i)$
187		nfcv	$⊢ \underline{Ⅎ} j if (a = L, ⦋ b / i ⦌ X, a M b)$
188		nfv	$⊢ Ⅎ i a = L$
189		nfcv	$⊢ \underline{Ⅎ} i (a M b)$
190	188 176 189	nfif	$⊢ \underline{Ⅎ} i if (a = L, ⦋ b / i ⦌ X, a M b)$
191		eqeq1	$⊢ j = a \to (j = L \leftrightarrow a = L)$
192	191	adantr	$⊢ (j = a \land i = b) \to (j = L \leftrightarrow a = L)$
193	180	adantl	$⊢ (j = a \land i = b) \to X = ⦋ b / i ⦌ X$
194		oveq12	$⊢ (j = a \land i = b) \to j M i = a M b$
195	192 193 194	ifbieq12d	$⊢ (j = a \land i = b) \to if (j = L, X, j M i) = if (a = L, ⦋ b / i ⦌ X, a M b)$
196	185 186 187 190 195	cbvmpo	$⊢ (j \in N, i \in N ⟼ if (j = L, X, j M i)) = (a \in N, b \in N ⟼ if (a = L, ⦋ b / i ⦌ X, a M b))$
197		iftrue	$⊢ b \in N \to if (b \in N, ⦋ b / i ⦌ X, 0_{R}) = ⦋ b / i ⦌ X$
198	197	eqcomd	$⊢ b \in N \to ⦋ b / i ⦌ X = if (b \in N, ⦋ b / i ⦌ X, 0_{R})$
199	198	adantl	$⊢ (a \in N \land b \in N) \to ⦋ b / i ⦌ X = if (b \in N, ⦋ b / i ⦌ X, 0_{R})$
200	199	ifeq1d	$⊢ (a \in N \land b \in N) \to if (a = L, ⦋ b / i ⦌ X, a M b) = if (a = L, if (b \in N, ⦋ b / i ⦌ X, 0_{R}), a M b)$
201	200	mpoeq3ia	$⊢ (a \in N, b \in N ⟼ if (a = L, ⦋ b / i ⦌ X, a M b)) = (a \in N, b \in N ⟼ if (a = L, if (b \in N, ⦋ b / i ⦌ X, 0_{R}), a M b))$
202	196 201	eqtri	$⊢ (j \in N, i \in N ⟼ if (j = L, X, j M i)) = (a \in N, b \in N ⟼ if (a = L, if (b \in N, ⦋ b / i ⦌ X, 0_{R}), a M b))$
203	202	fveq2i	$⊢ D ((j \in N, i \in N ⟼ if (j = L, X, j M i))) = D ((a \in N, b \in N ⟼ if (a = L, if (b \in N, ⦋ b / i ⦌ X, 0_{R}), a M b)))$
204	174 184 203	3eqtr4g	$⊢ φ \to \underset{i \in N}{\sum_{R}} (X \underset{˙}{\cdot} (i J (M) L)) = D ((j \in N, i \in N ⟼ if (j = L, X, j M i)))$

Metamath Proof Explorer

Theorem madugsum

Proof