dmatmul

Description: The product of two diagonal matrices. (Contributed by AV, 19-Aug-2019) (Revised by AV, 18-Dec-2019)

	Ref	Expression
Hypotheses	dmatid.a	$⊢ A = N Mat R$
	dmatid.b	$⊢ B = {Base}_{A}$
	dmatid.0	$⊢ \underset{˙}{0} = 0_{R}$
	dmatid.d	$⊢ D = N DMat R$
Assertion	dmatmul	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to X \cdot_{A} Y = (x \in N, y \in N ⟼ if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0}))$

Proof

Step	Hyp	Ref	Expression
1		dmatid.a	$⊢ A = N Mat R$
2		dmatid.b	$⊢ B = {Base}_{A}$
3		dmatid.0	$⊢ \underset{˙}{0} = 0_{R}$
4		dmatid.d	$⊢ D = N DMat R$
5		eqid	$⊢ R maMul ⟨N, N, N⟩ = R maMul ⟨N, N, N⟩$
6	1 5	matmulr	$⊢ (N \in Fin \land R \in Ring) \to R maMul ⟨N, N, N⟩ = \cdot_{A}$
7	6	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to R maMul ⟨N, N, N⟩ = \cdot_{A}$
8	7	eqcomd	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to \cdot_{A} = R maMul ⟨N, N, N⟩$
9	8	oveqd	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to X \cdot_{A} Y = X (R maMul ⟨N, N, N⟩) Y$
10		eqid	$⊢ {Base}_{R} = {Base}_{R}$
11		eqid	$⊢ \cdot_{R} = \cdot_{R}$
12		simplr	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to R \in Ring$
13		simpll	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to N \in Fin$
14	1 2 3 4	dmatmat	$⊢ (N \in Fin \land R \in Ring) \to (X \in D \to X \in B)$
15	14	imp	$⊢ ((N \in Fin \land R \in Ring) \land X \in D) \to X \in B$
16	1 10 2	matbas2i	$⊢ X \in B \to X \in ({Base}_{R}^{(N \times N)})$
17	15 16	syl	$⊢ ((N \in Fin \land R \in Ring) \land X \in D) \to X \in ({Base}_{R}^{(N \times N)})$
18	17	adantrr	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to X \in ({Base}_{R}^{(N \times N)})$
19	1 2 3 4	dmatmat	$⊢ (N \in Fin \land R \in Ring) \to (Y \in D \to Y \in B)$
20	19	imp	$⊢ ((N \in Fin \land R \in Ring) \land Y \in D) \to Y \in B$
21	1 10 2	matbas2i	$⊢ Y \in B \to Y \in ({Base}_{R}^{(N \times N)})$
22	20 21	syl	$⊢ ((N \in Fin \land R \in Ring) \land Y \in D) \to Y \in ({Base}_{R}^{(N \times N)})$
23	22	adantrl	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to Y \in ({Base}_{R}^{(N \times N)})$
24	5 10 11 12 13 13 13 18 23	mamuval	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to X (R maMul ⟨N, N, N⟩) Y = (x \in N, y \in N ⟼ \underset{k \in N}{\sum_{R}} ((x X k) \cdot_{R} (k Y y)))$
25		eqid	$⊢ +_{R} = +_{R}$
26		ringcmn	$⊢ R \in Ring \to R \in CMnd$
27	26	ad2antlr	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to R \in CMnd$
28	27	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to R \in CMnd$
29	28	adantl	$⊢ (x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \to R \in CMnd$
30	13	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to N \in Fin$
31	30	adantl	$⊢ (x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \to N \in Fin$
32		eqid	$⊢ (k \in N ⟼ (x X k) \cdot_{R} (k Y y)) = (k \in N ⟼ (x X k) \cdot_{R} (k Y y))$
33		ovexd	$⊢ ((x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N) \to (x X k) \cdot_{R} (k Y y) \in V$
34		fvexd	$⊢ (x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \to 0_{R} \in V$
35	32 31 33 34	fsuppmptdm	$⊢ (x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \to {finSupp}_{0_{R}} ((k \in N ⟼ (x X k) \cdot_{R} (k Y y)))$
36	12	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to R \in Ring$
37	36	ad2antlr	$⊢ ((x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N) \to R \in Ring$
38		simp2	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to x \in N$
39	38	ad2antlr	$⊢ ((x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N) \to x \in N$
40		simpr	$⊢ ((x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N) \to k \in N$
41		eqid	$⊢ {Base}_{A} = {Base}_{A}$
42	1 41 3 4	dmatmat	$⊢ (N \in Fin \land R \in Ring) \to (X \in D \to X \in {Base}_{A})$
43	42	imp	$⊢ ((N \in Fin \land R \in Ring) \land X \in D) \to X \in {Base}_{A}$
44	43	adantrr	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to X \in {Base}_{A}$
45	44	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to X \in {Base}_{A}$
46	45	ad2antlr	$⊢ ((x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N) \to X \in {Base}_{A}$
47	1 10	matecl	$⊢ (x \in N \land k \in N \land X \in {Base}_{A}) \to x X k \in {Base}_{R}$
48	39 40 46 47	syl3anc	$⊢ ((x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N) \to x X k \in {Base}_{R}$
49		simplr3	$⊢ ((x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N) \to y \in N$
50	1 41 3 4	dmatmat	$⊢ (N \in Fin \land R \in Ring) \to (Y \in D \to Y \in {Base}_{A})$
51	50	imp	$⊢ ((N \in Fin \land R \in Ring) \land Y \in D) \to Y \in {Base}_{A}$
52	51	adantrl	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to Y \in {Base}_{A}$
53	52	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to Y \in {Base}_{A}$
54	53	ad2antlr	$⊢ ((x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N) \to Y \in {Base}_{A}$
55	1 10	matecl	$⊢ (k \in N \land y \in N \land Y \in {Base}_{A}) \to k Y y \in {Base}_{R}$
56	40 49 54 55	syl3anc	$⊢ ((x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N) \to k Y y \in {Base}_{R}$
57	10 11	ringcl	$⊢ (R \in Ring \land x X k \in {Base}_{R} \land k Y y \in {Base}_{R}) \to (x X k) \cdot_{R} (k Y y) \in {Base}_{R}$
58	37 48 56 57	syl3anc	$⊢ ((x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N) \to (x X k) \cdot_{R} (k Y y) \in {Base}_{R}$
59	38	adantl	$⊢ (x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \to x \in N$
60		simp3	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to y \in N$
61	15	adantrr	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to X \in B$
62	61 2	eleqtrdi	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to X \in {Base}_{A}$
63	62	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to X \in {Base}_{A}$
64	1 10	matecl	$⊢ (x \in N \land y \in N \land X \in {Base}_{A}) \to x X y \in {Base}_{R}$
65	38 60 63 64	syl3anc	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to x X y \in {Base}_{R}$
66	50	a1d	$⊢ (N \in Fin \land R \in Ring) \to (X \in D \to (Y \in D \to Y \in {Base}_{A}))$
67	66	imp32	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to Y \in {Base}_{A}$
68	67	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to Y \in {Base}_{A}$
69	1 10	matecl	$⊢ (x \in N \land y \in N \land Y \in {Base}_{A}) \to x Y y \in {Base}_{R}$
70	38 60 68 69	syl3anc	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to x Y y \in {Base}_{R}$
71	10 11	ringcl	$⊢ (R \in Ring \land x X y \in {Base}_{R} \land x Y y \in {Base}_{R}) \to (x X y) \cdot_{R} (x Y y) \in {Base}_{R}$
72	36 65 70 71	syl3anc	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to (x X y) \cdot_{R} (x Y y) \in {Base}_{R}$
73	72	adantl	$⊢ (x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \to (x X y) \cdot_{R} (x Y y) \in {Base}_{R}$
74		eqtr	$⊢ (k = x \land x = y) \to k = y$
75	74	ancoms	$⊢ (x = y \land k = x) \to k = y$
76	75	oveq2d	$⊢ (x = y \land k = x) \to x X k = x X y$
77	76	adantlr	$⊢ ((x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k = x) \to x X k = x X y$
78		oveq1	$⊢ k = x \to k Y y = x Y y$
79	78	adantl	$⊢ ((x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k = x) \to k Y y = x Y y$
80	77 79	oveq12d	$⊢ ((x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k = x) \to (x X k) \cdot_{R} (k Y y) = (x X y) \cdot_{R} (x Y y)$
81	10 25 29 31 35 58 59 73 80	gsumdifsnd	$⊢ (x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \to \underset{k \in N}{\sum_{R}} ((x X k) \cdot_{R} (k Y y)) = (\underset{k \in N ∖ \{x\}}{\sum_{R}}, ((x X k) \cdot_{R} (k Y y))) +_{R} ((x X y) \cdot_{R} (x Y y))$
82		simprl	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to X \in D$
83	13 12 82	3jca	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to (N \in Fin \land R \in Ring \land X \in D)$
84	83	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to (N \in Fin \land R \in Ring \land X \in D)$
85	84	ad2antlr	$⊢ ((x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in (N ∖ \{x\})) \to (N \in Fin \land R \in Ring \land X \in D)$
86	38	ad2antlr	$⊢ ((x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in (N ∖ \{x\})) \to x \in N$
87		eldifi	$⊢ k \in (N ∖ \{x\}) \to k \in N$
88	87	adantl	$⊢ ((x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in (N ∖ \{x\})) \to k \in N$
89		eldifsni	$⊢ k \in (N ∖ \{x\}) \to k \neq x$
90	89	necomd	$⊢ k \in (N ∖ \{x\}) \to x \neq k$
91	90	adantl	$⊢ ((x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in (N ∖ \{x\})) \to x \neq k$
92	1 2 3 4	dmatelnd	$⊢ ((N \in Fin \land R \in Ring \land X \in D) \land (x \in N \land k \in N \land x \neq k)) \to x X k = \underset{˙}{0}$
93	85 86 88 91 92	syl13anc	$⊢ ((x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in (N ∖ \{x\})) \to x X k = \underset{˙}{0}$
94	93	oveq1d	$⊢ ((x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in (N ∖ \{x\})) \to (x X k) \cdot_{R} (k Y y) = \underset{˙}{0} \cdot_{R} (k Y y)$
95	36	ad2antlr	$⊢ ((x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in (N ∖ \{x\})) \to R \in Ring$
96		simplr3	$⊢ ((x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in (N ∖ \{x\})) \to y \in N$
97	53	ad2antlr	$⊢ ((x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in (N ∖ \{x\})) \to Y \in {Base}_{A}$
98	88 96 97 55	syl3anc	$⊢ ((x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in (N ∖ \{x\})) \to k Y y \in {Base}_{R}$
99	10 11 3	ringlz	$⊢ (R \in Ring \land k Y y \in {Base}_{R}) \to \underset{˙}{0} \cdot_{R} (k Y y) = \underset{˙}{0}$
100	95 98 99	syl2anc	$⊢ ((x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in (N ∖ \{x\})) \to \underset{˙}{0} \cdot_{R} (k Y y) = \underset{˙}{0}$
101	94 100	eqtrd	$⊢ ((x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in (N ∖ \{x\})) \to (x X k) \cdot_{R} (k Y y) = \underset{˙}{0}$
102	101	mpteq2dva	$⊢ (x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \to (k \in (N ∖ \{x\}) ⟼ (x X k) \cdot_{R} (k Y y)) = (k \in (N ∖ \{x\}) ⟼ \underset{˙}{0})$
103	102	oveq2d	$⊢ (x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \to \underset{k \in N ∖ \{x\}}{\sum_{R}} ((x X k) \cdot_{R} (k Y y)) = \underset{k \in N ∖ \{x\}}{\sum_{R}} \underset{˙}{0}$
104		diffi	$⊢ N \in Fin \to N ∖ \{x\} \in Fin$
105		ringmnd	$⊢ R \in Ring \to R \in Mnd$
106	104 105	anim12ci	$⊢ (N \in Fin \land R \in Ring) \to (R \in Mnd \land N ∖ \{x\} \in Fin)$
107	106	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to (R \in Mnd \land N ∖ \{x\} \in Fin)$
108	107	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to (R \in Mnd \land N ∖ \{x\} \in Fin)$
109	108	adantl	$⊢ (x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \to (R \in Mnd \land N ∖ \{x\} \in Fin)$
110	3	gsumz	$⊢ (R \in Mnd \land N ∖ \{x\} \in Fin) \to \underset{k \in N ∖ \{x\}}{\sum_{R}} \underset{˙}{0} = \underset{˙}{0}$
111	109 110	syl	$⊢ (x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \to \underset{k \in N ∖ \{x\}}{\sum_{R}} \underset{˙}{0} = \underset{˙}{0}$
112	103 111	eqtrd	$⊢ (x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \to \underset{k \in N ∖ \{x\}}{\sum_{R}} ((x X k) \cdot_{R} (k Y y)) = \underset{˙}{0}$
113	112	oveq1d	$⊢ (x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \to (\underset{k \in N ∖ \{x\}}{\sum_{R}}, ((x X k) \cdot_{R} (k Y y))) +_{R} ((x X y) \cdot_{R} (x Y y)) = \underset{˙}{0} +_{R} ((x X y) \cdot_{R} (x Y y))$
114	105	ad2antlr	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to R \in Mnd$
115	114	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to R \in Mnd$
116	38 60 53 69	syl3anc	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to x Y y \in {Base}_{R}$
117	36 65 116 71	syl3anc	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to (x X y) \cdot_{R} (x Y y) \in {Base}_{R}$
118	115 117	jca	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to (R \in Mnd \land (x X y) \cdot_{R} (x Y y) \in {Base}_{R})$
119	118	adantl	$⊢ (x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \to (R \in Mnd \land (x X y) \cdot_{R} (x Y y) \in {Base}_{R})$
120	10 25 3	mndlid	$⊢ (R \in Mnd \land (x X y) \cdot_{R} (x Y y) \in {Base}_{R}) \to \underset{˙}{0} +_{R} ((x X y) \cdot_{R} (x Y y)) = (x X y) \cdot_{R} (x Y y)$
121	119 120	syl	$⊢ (x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \to \underset{˙}{0} +_{R} ((x X y) \cdot_{R} (x Y y)) = (x X y) \cdot_{R} (x Y y)$
122	81 113 121	3eqtrd	$⊢ (x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \to \underset{k \in N}{\sum_{R}} ((x X k) \cdot_{R} (k Y y)) = (x X y) \cdot_{R} (x Y y)$
123		iftrue	$⊢ x = y \to if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0}) = (x X y) \cdot_{R} (x Y y)$
124	123	adantr	$⊢ (x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \to if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0}) = (x X y) \cdot_{R} (x Y y)$
125	122 124	eqtr4d	$⊢ (x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \to \underset{k \in N}{\sum_{R}} ((x X k) \cdot_{R} (k Y y)) = if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0})$
126		simprr	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to Y \in D$
127	13 12 126	3jca	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to (N \in Fin \land R \in Ring \land Y \in D)$
128	127	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to (N \in Fin \land R \in Ring \land Y \in D)$
129	128	ad2antlr	$⊢ ((\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N) \to (N \in Fin \land R \in Ring \land Y \in D)$
130	129	adantl	$⊢ (x = k \land ((\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N)) \to (N \in Fin \land R \in Ring \land Y \in D)$
131		simprr	$⊢ (x = k \land ((\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N)) \to k \in N$
132		simplr3	$⊢ ((\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N) \to y \in N$
133	132	adantl	$⊢ (x = k \land ((\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N)) \to y \in N$
134		df-ne	$⊢ x \neq y \leftrightarrow \neg x = y$
135		neeq1	$⊢ x = k \to (x \neq y \leftrightarrow k \neq y)$
136	135	biimpcd	$⊢ x \neq y \to (x = k \to k \neq y)$
137	134 136	sylbir	$⊢ \neg x = y \to (x = k \to k \neq y)$
138	137	adantr	$⊢ (\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \to (x = k \to k \neq y)$
139	138	adantr	$⊢ ((\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N) \to (x = k \to k \neq y)$
140	139	impcom	$⊢ (x = k \land ((\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N)) \to k \neq y$
141	1 2 3 4	dmatelnd	$⊢ ((N \in Fin \land R \in Ring \land Y \in D) \land (k \in N \land y \in N \land k \neq y)) \to k Y y = \underset{˙}{0}$
142	130 131 133 140 141	syl13anc	$⊢ (x = k \land ((\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N)) \to k Y y = \underset{˙}{0}$
143	142	oveq2d	$⊢ (x = k \land ((\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N)) \to (x X k) \cdot_{R} (k Y y) = (x X k) \cdot_{R} \underset{˙}{0}$
144	36	ad2antlr	$⊢ ((\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N) \to R \in Ring$
145	38	ad2antlr	$⊢ ((\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N) \to x \in N$
146		simpr	$⊢ ((\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N) \to k \in N$
147	63	ad2antlr	$⊢ ((\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N) \to X \in {Base}_{A}$
148	145 146 147 47	syl3anc	$⊢ ((\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N) \to x X k \in {Base}_{R}$
149	10 11 3	ringrz	$⊢ (R \in Ring \land x X k \in {Base}_{R}) \to (x X k) \cdot_{R} \underset{˙}{0} = \underset{˙}{0}$
150	144 148 149	syl2anc	$⊢ ((\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N) \to (x X k) \cdot_{R} \underset{˙}{0} = \underset{˙}{0}$
151	150	adantl	$⊢ (x = k \land ((\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N)) \to (x X k) \cdot_{R} \underset{˙}{0} = \underset{˙}{0}$
152	143 151	eqtrd	$⊢ (x = k \land ((\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N)) \to (x X k) \cdot_{R} (k Y y) = \underset{˙}{0}$
153	84	ad2antlr	$⊢ ((\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N) \to (N \in Fin \land R \in Ring \land X \in D)$
154	153	adantl	$⊢ (\neg x = k \land ((\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N)) \to (N \in Fin \land R \in Ring \land X \in D)$
155	145	adantl	$⊢ (\neg x = k \land ((\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N)) \to x \in N$
156		simprr	$⊢ (\neg x = k \land ((\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N)) \to k \in N$
157		neqne	$⊢ \neg x = k \to x \neq k$
158	157	adantr	$⊢ (\neg x = k \land ((\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N)) \to x \neq k$
159	154 155 156 158 92	syl13anc	$⊢ (\neg x = k \land ((\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N)) \to x X k = \underset{˙}{0}$
160	159	oveq1d	$⊢ (\neg x = k \land ((\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N)) \to (x X k) \cdot_{R} (k Y y) = \underset{˙}{0} \cdot_{R} (k Y y)$
161	68	ad2antlr	$⊢ ((\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N) \to Y \in {Base}_{A}$
162	146 132 161 55	syl3anc	$⊢ ((\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N) \to k Y y \in {Base}_{R}$
163	144 162 99	syl2anc	$⊢ ((\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N) \to \underset{˙}{0} \cdot_{R} (k Y y) = \underset{˙}{0}$
164	163	adantl	$⊢ (\neg x = k \land ((\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N)) \to \underset{˙}{0} \cdot_{R} (k Y y) = \underset{˙}{0}$
165	160 164	eqtrd	$⊢ (\neg x = k \land ((\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N)) \to (x X k) \cdot_{R} (k Y y) = \underset{˙}{0}$
166	152 165	pm2.61ian	$⊢ ((\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \land k \in N) \to (x X k) \cdot_{R} (k Y y) = \underset{˙}{0}$
167	166	mpteq2dva	$⊢ (\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \to (k \in N ⟼ (x X k) \cdot_{R} (k Y y)) = (k \in N ⟼ \underset{˙}{0})$
168	167	oveq2d	$⊢ (\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \to \underset{k \in N}{\sum_{R}} ((x X k) \cdot_{R} (k Y y)) = \underset{k \in N}{\sum_{R}} \underset{˙}{0}$
169	105	anim2i	$⊢ (N \in Fin \land R \in Ring) \to (N \in Fin \land R \in Mnd)$
170	169	ancomd	$⊢ (N \in Fin \land R \in Ring) \to (R \in Mnd \land N \in Fin)$
171	3	gsumz	$⊢ (R \in Mnd \land N \in Fin) \to \underset{k \in N}{\sum_{R}} \underset{˙}{0} = \underset{˙}{0}$
172	170 171	syl	$⊢ (N \in Fin \land R \in Ring) \to \underset{k \in N}{\sum_{R}} \underset{˙}{0} = \underset{˙}{0}$
173	172	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to \underset{k \in N}{\sum_{R}} \underset{˙}{0} = \underset{˙}{0}$
174	173	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to \underset{k \in N}{\sum_{R}} \underset{˙}{0} = \underset{˙}{0}$
175	174	adantl	$⊢ (\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \to \underset{k \in N}{\sum_{R}} \underset{˙}{0} = \underset{˙}{0}$
176		iffalse	$⊢ \neg x = y \to if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0}) = \underset{˙}{0}$
177	176	eqcomd	$⊢ \neg x = y \to \underset{˙}{0} = if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0})$
178	177	adantr	$⊢ (\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \to \underset{˙}{0} = if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0})$
179	168 175 178	3eqtrd	$⊢ (\neg x = y \land (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N)) \to \underset{k \in N}{\sum_{R}} ((x X k) \cdot_{R} (k Y y)) = if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0})$
180	125 179	pm2.61ian	$⊢ (((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \land x \in N \land y \in N) \to \underset{k \in N}{\sum_{R}} ((x X k) \cdot_{R} (k Y y)) = if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0})$
181	180	mpoeq3dva	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to (x \in N, y \in N ⟼ \underset{k \in N}{\sum_{R}} ((x X k) \cdot_{R} (k Y y))) = (x \in N, y \in N ⟼ if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0}))$
182	9 24 181	3eqtrd	$⊢ ((N \in Fin \land R \in Ring) \land (X \in D \land Y \in D)) \to X \cdot_{A} Y = (x \in N, y \in N ⟼ if (x = y, (x X y) \cdot_{R} (x Y y), \underset{˙}{0}))$

Metamath Proof Explorer

Theorem dmatmul

Proof