cpmatmcllem

	Ref	Expression
Hypotheses	cpmatsrngpmat.s	$⊢ S = N ConstPolyMat R$
	cpmatsrngpmat.p	$⊢ P = {Poly}_{1} (R)$
	cpmatsrngpmat.c	$⊢ C = N Mat P$
Assertion	cpmatmcllem	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to \forall i \in N \forall j \in N \forall c \in ℕ {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R}$

Proof

Step	Hyp	Ref	Expression
1		cpmatsrngpmat.s	$⊢ S = N ConstPolyMat R$
2		cpmatsrngpmat.p	$⊢ P = {Poly}_{1} (R)$
3		cpmatsrngpmat.c	$⊢ C = N Mat P$
4		eqid	$⊢ {Base}_{C} = {Base}_{C}$
5	1 2 3 4	cpmatelimp	$⊢ (N \in Fin \land R \in Ring) \to (x \in S \to (x \in {Base}_{C} \land \forall i \in N \forall l \in N \forall c \in ℕ {coe}_{1} (i x l) (c) = 0_{R}))$
6	1 2 3 4	cpmatelimp	$⊢ (N \in Fin \land R \in Ring) \to (y \in S \to (y \in {Base}_{C} \land \forall l \in N \forall j \in N \forall c \in ℕ {coe}_{1} (l y j) (c) = 0_{R}))$
7	6	adantr	$⊢ ((N \in Fin \land R \in Ring) \land x \in {Base}_{C}) \to (y \in S \to (y \in {Base}_{C} \land \forall l \in N \forall j \in N \forall c \in ℕ {coe}_{1} (l y j) (c) = 0_{R}))$
8		ralcom	$⊢ \forall l \in N \forall j \in N \forall c \in ℕ {coe}_{1} (l y j) (c) = 0_{R} \leftrightarrow \forall j \in N \forall l \in N \forall c \in ℕ {coe}_{1} (l y j) (c) = 0_{R}$
9		r19.26-2	$⊢ \forall l \in N \forall c \in ℕ ({coe}_{1} (i x l) (c) = 0_{R} \land {coe}_{1} (l y j) (c) = 0_{R}) \leftrightarrow (\forall l \in N \forall c \in ℕ {coe}_{1} (i x l) (c) = 0_{R} \land \forall l \in N \forall c \in ℕ {coe}_{1} (l y j) (c) = 0_{R})$
10		ralcom	$⊢ \forall l \in N \forall c \in ℕ ({coe}_{1} (i x l) (c) = 0_{R} \land {coe}_{1} (l y j) (c) = 0_{R}) \leftrightarrow \forall c \in ℕ \forall l \in N ({coe}_{1} (i x l) (c) = 0_{R} \land {coe}_{1} (l y j) (c) = 0_{R})$
11	9 10	bitr3i	$⊢ (\forall l \in N \forall c \in ℕ {coe}_{1} (i x l) (c) = 0_{R} \land \forall l \in N \forall c \in ℕ {coe}_{1} (l y j) (c) = 0_{R}) \leftrightarrow \forall c \in ℕ \forall l \in N ({coe}_{1} (i x l) (c) = 0_{R} \land {coe}_{1} (l y j) (c) = 0_{R})$
12		nfv	$⊢ Ⅎ c (((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N))$
13		nfra1	$⊢ Ⅎ c \forall c \in ℕ \forall l \in N ({coe}_{1} (i x l) (c) = 0_{R} \land {coe}_{1} (l y j) (c) = 0_{R})$
14	12 13	nfan	$⊢ Ⅎ c ((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land \forall c \in ℕ \forall l \in N ({coe}_{1} (i x l) (c) = 0_{R} \land {coe}_{1} (l y j) (c) = 0_{R}))$
15		simp-4r	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land k \in N) \to R \in Ring$
16		eqid	$⊢ {Base}_{P} = {Base}_{P}$
17		simplrl	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land k \in N) \to i \in N$
18		simpr	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land k \in N) \to k \in N$
19		simplrl	$⊢ (((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \to x \in {Base}_{C}$
20	19	adantr	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land k \in N) \to x \in {Base}_{C}$
21	3 16 4 17 18 20	matecld	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land k \in N) \to i x k \in {Base}_{P}$
22		simplrr	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land k \in N) \to j \in N$
23		simplrr	$⊢ (((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \to y \in {Base}_{C}$
24	23	adantr	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land k \in N) \to y \in {Base}_{C}$
25	3 16 4 18 22 24	matecld	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land k \in N) \to k y j \in {Base}_{P}$
26	15 21 25	jca32	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land k \in N) \to (R \in Ring \land (i x k \in {Base}_{P} \land k y j \in {Base}_{P}))$
27	26	adantlr	$⊢ (((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land \forall c \in ℕ \forall l \in N ({coe}_{1} (i x l) (c) = 0_{R} \land {coe}_{1} (l y j) (c) = 0_{R})) \land k \in N) \to (R \in Ring \land (i x k \in {Base}_{P} \land k y j \in {Base}_{P}))$
28		oveq2	$⊢ l = k \to i x l = i x k$
29	28	fveq2d	$⊢ l = k \to {coe}_{1} (i x l) = {coe}_{1} (i x k)$
30	29	fveq1d	$⊢ l = k \to {coe}_{1} (i x l) (c) = {coe}_{1} (i x k) (c)$
31	30	eqeq1d	$⊢ l = k \to ({coe}_{1} (i x l) (c) = 0_{R} \leftrightarrow {coe}_{1} (i x k) (c) = 0_{R})$
32		fvoveq1	$⊢ l = k \to {coe}_{1} (l y j) = {coe}_{1} (k y j)$
33	32	fveq1d	$⊢ l = k \to {coe}_{1} (l y j) (c) = {coe}_{1} (k y j) (c)$
34	33	eqeq1d	$⊢ l = k \to ({coe}_{1} (l y j) (c) = 0_{R} \leftrightarrow {coe}_{1} (k y j) (c) = 0_{R})$
35	31 34	anbi12d	$⊢ l = k \to (({coe}_{1} (i x l) (c) = 0_{R} \land {coe}_{1} (l y j) (c) = 0_{R}) \leftrightarrow ({coe}_{1} (i x k) (c) = 0_{R} \land {coe}_{1} (k y j) (c) = 0_{R}))$
36	35	rspcva	$⊢ (k \in N \land \forall l \in N ({coe}_{1} (i x l) (c) = 0_{R} \land {coe}_{1} (l y j) (c) = 0_{R})) \to ({coe}_{1} (i x k) (c) = 0_{R} \land {coe}_{1} (k y j) (c) = 0_{R})$
37	36	a1i	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land c \in ℕ) \to ((k \in N \land \forall l \in N ({coe}_{1} (i x l) (c) = 0_{R} \land {coe}_{1} (l y j) (c) = 0_{R})) \to ({coe}_{1} (i x k) (c) = 0_{R} \land {coe}_{1} (k y j) (c) = 0_{R}))$
38	37	exp4b	$⊢ (((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \to (c \in ℕ \to (k \in N \to (\forall l \in N ({coe}_{1} (i x l) (c) = 0_{R} \land {coe}_{1} (l y j) (c) = 0_{R}) \to ({coe}_{1} (i x k) (c) = 0_{R} \land {coe}_{1} (k y j) (c) = 0_{R}))))$
39	38	com23	$⊢ (((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \to (k \in N \to (c \in ℕ \to (\forall l \in N ({coe}_{1} (i x l) (c) = 0_{R} \land {coe}_{1} (l y j) (c) = 0_{R}) \to ({coe}_{1} (i x k) (c) = 0_{R} \land {coe}_{1} (k y j) (c) = 0_{R}))))$
40	39	imp31	$⊢ (((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land k \in N) \land c \in ℕ) \to (\forall l \in N ({coe}_{1} (i x l) (c) = 0_{R} \land {coe}_{1} (l y j) (c) = 0_{R}) \to ({coe}_{1} (i x k) (c) = 0_{R} \land {coe}_{1} (k y j) (c) = 0_{R}))$
41	40	ralimdva	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land k \in N) \to (\forall c \in ℕ \forall l \in N ({coe}_{1} (i x l) (c) = 0_{R} \land {coe}_{1} (l y j) (c) = 0_{R}) \to \forall c \in ℕ ({coe}_{1} (i x k) (c) = 0_{R} \land {coe}_{1} (k y j) (c) = 0_{R}))$
42	41	impancom	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land \forall c \in ℕ \forall l \in N ({coe}_{1} (i x l) (c) = 0_{R} \land {coe}_{1} (l y j) (c) = 0_{R})) \to (k \in N \to \forall c \in ℕ ({coe}_{1} (i x k) (c) = 0_{R} \land {coe}_{1} (k y j) (c) = 0_{R}))$
43	42	imp	$⊢ (((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land \forall c \in ℕ \forall l \in N ({coe}_{1} (i x l) (c) = 0_{R} \land {coe}_{1} (l y j) (c) = 0_{R})) \land k \in N) \to \forall c \in ℕ ({coe}_{1} (i x k) (c) = 0_{R} \land {coe}_{1} (k y j) (c) = 0_{R})$
44		eqid	$⊢ 0_{R} = 0_{R}$
45		eqid	$⊢ \cdot_{P} = \cdot_{P}$
46	2 16 44 45	cply1mul	$⊢ (R \in Ring \land (i x k \in {Base}_{P} \land k y j \in {Base}_{P})) \to (\forall c \in ℕ ({coe}_{1} (i x k) (c) = 0_{R} \land {coe}_{1} (k y j) (c) = 0_{R}) \to \forall c \in ℕ {coe}_{1} ((i x k) \cdot_{P} (k y j)) (c) = 0_{R})$
47	27 43 46	sylc	$⊢ (((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land \forall c \in ℕ \forall l \in N ({coe}_{1} (i x l) (c) = 0_{R} \land {coe}_{1} (l y j) (c) = 0_{R})) \land k \in N) \to \forall c \in ℕ {coe}_{1} ((i x k) \cdot_{P} (k y j)) (c) = 0_{R}$
48	47	r19.21bi	$⊢ ((((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land \forall c \in ℕ \forall l \in N ({coe}_{1} (i x l) (c) = 0_{R} \land {coe}_{1} (l y j) (c) = 0_{R})) \land k \in N) \land c \in ℕ) \to {coe}_{1} ((i x k) \cdot_{P} (k y j)) (c) = 0_{R}$
49	48	an32s	$⊢ ((((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land \forall c \in ℕ \forall l \in N ({coe}_{1} (i x l) (c) = 0_{R} \land {coe}_{1} (l y j) (c) = 0_{R})) \land c \in ℕ) \land k \in N) \to {coe}_{1} ((i x k) \cdot_{P} (k y j)) (c) = 0_{R}$
50	49	mpteq2dva	$⊢ (((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land \forall c \in ℕ \forall l \in N ({coe}_{1} (i x l) (c) = 0_{R} \land {coe}_{1} (l y j) (c) = 0_{R})) \land c \in ℕ) \to (k \in N ⟼ {coe}_{1} ((i x k) \cdot_{P} (k y j)) (c)) = (k \in N ⟼ 0_{R})$
51	50	oveq2d	$⊢ (((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land \forall c \in ℕ \forall l \in N ({coe}_{1} (i x l) (c) = 0_{R} \land {coe}_{1} (l y j) (c) = 0_{R})) \land c \in ℕ) \to \underset{k \in N}{\sum_{R}} {coe}_{1} ((i x k) \cdot_{P} (k y j)) (c) = \underset{k \in N}{\sum_{R}} 0_{R}$
52		ringmnd	$⊢ R \in Ring \to R \in Mnd$
53	52	anim2i	$⊢ (N \in Fin \land R \in Ring) \to (N \in Fin \land R \in Mnd)$
54	53	ancomd	$⊢ (N \in Fin \land R \in Ring) \to (R \in Mnd \land N \in Fin)$
55	44	gsumz	$⊢ (R \in Mnd \land N \in Fin) \to \underset{k \in N}{\sum_{R}} 0_{R} = 0_{R}$
56	54 55	syl	$⊢ (N \in Fin \land R \in Ring) \to \underset{k \in N}{\sum_{R}} 0_{R} = 0_{R}$
57	56	ad4antr	$⊢ (((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land \forall c \in ℕ \forall l \in N ({coe}_{1} (i x l) (c) = 0_{R} \land {coe}_{1} (l y j) (c) = 0_{R})) \land c \in ℕ) \to \underset{k \in N}{\sum_{R}} 0_{R} = 0_{R}$
58	51 57	eqtrd	$⊢ (((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land \forall c \in ℕ \forall l \in N ({coe}_{1} (i x l) (c) = 0_{R} \land {coe}_{1} (l y j) (c) = 0_{R})) \land c \in ℕ) \to \underset{k \in N}{\sum_{R}} {coe}_{1} ((i x k) \cdot_{P} (k y j)) (c) = 0_{R}$
59	58	ex	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land \forall c \in ℕ \forall l \in N ({coe}_{1} (i x l) (c) = 0_{R} \land {coe}_{1} (l y j) (c) = 0_{R})) \to (c \in ℕ \to \underset{k \in N}{\sum_{R}} {coe}_{1} ((i x k) \cdot_{P} (k y j)) (c) = 0_{R})$
60	14 59	ralrimi	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land \forall c \in ℕ \forall l \in N ({coe}_{1} (i x l) (c) = 0_{R} \land {coe}_{1} (l y j) (c) = 0_{R})) \to \forall c \in ℕ \underset{k \in N}{\sum_{R}} {coe}_{1} ((i x k) \cdot_{P} (k y j)) (c) = 0_{R}$
61		simp-4r	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land c \in ℕ) \to R \in Ring$
62		nnnn0	$⊢ c \in ℕ \to c \in ℕ_{0}$
63	62	adantl	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land c \in ℕ) \to c \in ℕ_{0}$
64	2	ply1ring	$⊢ R \in Ring \to P \in Ring$
65	64	ad4antlr	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land k \in N) \to P \in Ring$
66	16 45	ringcl	$⊢ (P \in Ring \land i x k \in {Base}_{P} \land k y j \in {Base}_{P}) \to (i x k) \cdot_{P} (k y j) \in {Base}_{P}$
67	65 21 25 66	syl3anc	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land k \in N) \to (i x k) \cdot_{P} (k y j) \in {Base}_{P}$
68	67	ralrimiva	$⊢ (((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \to \forall k \in N (i x k) \cdot_{P} (k y j) \in {Base}_{P}$
69	68	adantr	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land c \in ℕ) \to \forall k \in N (i x k) \cdot_{P} (k y j) \in {Base}_{P}$
70		simp-4l	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land c \in ℕ) \to N \in Fin$
71	2 16 61 63 69 70	coe1fzgsumd	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land c \in ℕ) \to {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = \underset{k \in N}{\sum_{R}} {coe}_{1} ((i x k) \cdot_{P} (k y j)) (c)$
72	71	eqeq1d	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land c \in ℕ) \to ({coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R} \leftrightarrow \underset{k \in N}{\sum_{R}} {coe}_{1} ((i x k) \cdot_{P} (k y j)) (c) = 0_{R})$
73	72	ralbidva	$⊢ (((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \to (\forall c \in ℕ {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R} \leftrightarrow \forall c \in ℕ \underset{k \in N}{\sum_{R}} {coe}_{1} ((i x k) \cdot_{P} (k y j)) (c) = 0_{R})$
74	73	adantr	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land \forall c \in ℕ \forall l \in N ({coe}_{1} (i x l) (c) = 0_{R} \land {coe}_{1} (l y j) (c) = 0_{R})) \to (\forall c \in ℕ {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R} \leftrightarrow \forall c \in ℕ \underset{k \in N}{\sum_{R}} {coe}_{1} ((i x k) \cdot_{P} (k y j)) (c) = 0_{R})$
75	60 74	mpbird	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \land \forall c \in ℕ \forall l \in N ({coe}_{1} (i x l) (c) = 0_{R} \land {coe}_{1} (l y j) (c) = 0_{R})) \to \forall c \in ℕ {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R}$
76	75	ex	$⊢ (((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \to (\forall c \in ℕ \forall l \in N ({coe}_{1} (i x l) (c) = 0_{R} \land {coe}_{1} (l y j) (c) = 0_{R}) \to \forall c \in ℕ {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R})$
77	11 76	biimtrid	$⊢ (((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \to ((\forall l \in N \forall c \in ℕ {coe}_{1} (i x l) (c) = 0_{R} \land \forall l \in N \forall c \in ℕ {coe}_{1} (l y j) (c) = 0_{R}) \to \forall c \in ℕ {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R})$
78	77	expd	$⊢ (((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land (i \in N \land j \in N)) \to (\forall l \in N \forall c \in ℕ {coe}_{1} (i x l) (c) = 0_{R} \to (\forall l \in N \forall c \in ℕ {coe}_{1} (l y j) (c) = 0_{R} \to \forall c \in ℕ {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R}))$
79	78	expr	$⊢ (((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land i \in N) \to (j \in N \to (\forall l \in N \forall c \in ℕ {coe}_{1} (i x l) (c) = 0_{R} \to (\forall l \in N \forall c \in ℕ {coe}_{1} (l y j) (c) = 0_{R} \to \forall c \in ℕ {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R})))$
80	79	com23	$⊢ (((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land i \in N) \to (\forall l \in N \forall c \in ℕ {coe}_{1} (i x l) (c) = 0_{R} \to (j \in N \to (\forall l \in N \forall c \in ℕ {coe}_{1} (l y j) (c) = 0_{R} \to \forall c \in ℕ {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R})))$
81	80	imp31	$⊢ (((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land i \in N) \land \forall l \in N \forall c \in ℕ {coe}_{1} (i x l) (c) = 0_{R}) \land j \in N) \to (\forall l \in N \forall c \in ℕ {coe}_{1} (l y j) (c) = 0_{R} \to \forall c \in ℕ {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R})$
82	81	ralimdva	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land i \in N) \land \forall l \in N \forall c \in ℕ {coe}_{1} (i x l) (c) = 0_{R}) \to (\forall j \in N \forall l \in N \forall c \in ℕ {coe}_{1} (l y j) (c) = 0_{R} \to \forall j \in N \forall c \in ℕ {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R})$
83	8 82	biimtrid	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land i \in N) \land \forall l \in N \forall c \in ℕ {coe}_{1} (i x l) (c) = 0_{R}) \to (\forall l \in N \forall j \in N \forall c \in ℕ {coe}_{1} (l y j) (c) = 0_{R} \to \forall j \in N \forall c \in ℕ {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R})$
84	83	ex	$⊢ (((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land i \in N) \to (\forall l \in N \forall c \in ℕ {coe}_{1} (i x l) (c) = 0_{R} \to (\forall l \in N \forall j \in N \forall c \in ℕ {coe}_{1} (l y j) (c) = 0_{R} \to \forall j \in N \forall c \in ℕ {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R}))$
85	84	com23	$⊢ (((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land i \in N) \to (\forall l \in N \forall j \in N \forall c \in ℕ {coe}_{1} (l y j) (c) = 0_{R} \to (\forall l \in N \forall c \in ℕ {coe}_{1} (i x l) (c) = 0_{R} \to \forall j \in N \forall c \in ℕ {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R}))$
86	85	impancom	$⊢ (((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land \forall l \in N \forall j \in N \forall c \in ℕ {coe}_{1} (l y j) (c) = 0_{R}) \to (i \in N \to (\forall l \in N \forall c \in ℕ {coe}_{1} (i x l) (c) = 0_{R} \to \forall j \in N \forall c \in ℕ {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R}))$
87	86	imp	$⊢ ((((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land \forall l \in N \forall j \in N \forall c \in ℕ {coe}_{1} (l y j) (c) = 0_{R}) \land i \in N) \to (\forall l \in N \forall c \in ℕ {coe}_{1} (i x l) (c) = 0_{R} \to \forall j \in N \forall c \in ℕ {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R})$
88	87	ralimdva	$⊢ (((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land \forall l \in N \forall j \in N \forall c \in ℕ {coe}_{1} (l y j) (c) = 0_{R}) \to (\forall i \in N \forall l \in N \forall c \in ℕ {coe}_{1} (i x l) (c) = 0_{R} \to \forall i \in N \forall j \in N \forall c \in ℕ {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R})$
89	88	ex	$⊢ ((N \in Fin \land R \in Ring) \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (\forall l \in N \forall j \in N \forall c \in ℕ {coe}_{1} (l y j) (c) = 0_{R} \to (\forall i \in N \forall l \in N \forall c \in ℕ {coe}_{1} (i x l) (c) = 0_{R} \to \forall i \in N \forall j \in N \forall c \in ℕ {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R}))$
90	89	expr	$⊢ ((N \in Fin \land R \in Ring) \land x \in {Base}_{C}) \to (y \in {Base}_{C} \to (\forall l \in N \forall j \in N \forall c \in ℕ {coe}_{1} (l y j) (c) = 0_{R} \to (\forall i \in N \forall l \in N \forall c \in ℕ {coe}_{1} (i x l) (c) = 0_{R} \to \forall i \in N \forall j \in N \forall c \in ℕ {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R})))$
91	90	impd	$⊢ ((N \in Fin \land R \in Ring) \land x \in {Base}_{C}) \to ((y \in {Base}_{C} \land \forall l \in N \forall j \in N \forall c \in ℕ {coe}_{1} (l y j) (c) = 0_{R}) \to (\forall i \in N \forall l \in N \forall c \in ℕ {coe}_{1} (i x l) (c) = 0_{R} \to \forall i \in N \forall j \in N \forall c \in ℕ {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R}))$
92	7 91	syld	$⊢ ((N \in Fin \land R \in Ring) \land x \in {Base}_{C}) \to (y \in S \to (\forall i \in N \forall l \in N \forall c \in ℕ {coe}_{1} (i x l) (c) = 0_{R} \to \forall i \in N \forall j \in N \forall c \in ℕ {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R}))$
93	92	com23	$⊢ ((N \in Fin \land R \in Ring) \land x \in {Base}_{C}) \to (\forall i \in N \forall l \in N \forall c \in ℕ {coe}_{1} (i x l) (c) = 0_{R} \to (y \in S \to \forall i \in N \forall j \in N \forall c \in ℕ {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R}))$
94	93	ex	$⊢ (N \in Fin \land R \in Ring) \to (x \in {Base}_{C} \to (\forall i \in N \forall l \in N \forall c \in ℕ {coe}_{1} (i x l) (c) = 0_{R} \to (y \in S \to \forall i \in N \forall j \in N \forall c \in ℕ {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R})))$
95	94	impd	$⊢ (N \in Fin \land R \in Ring) \to ((x \in {Base}_{C} \land \forall i \in N \forall l \in N \forall c \in ℕ {coe}_{1} (i x l) (c) = 0_{R}) \to (y \in S \to \forall i \in N \forall j \in N \forall c \in ℕ {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R}))$
96	5 95	syld	$⊢ (N \in Fin \land R \in Ring) \to (x \in S \to (y \in S \to \forall i \in N \forall j \in N \forall c \in ℕ {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R}))$
97	96	imp32	$⊢ ((N \in Fin \land R \in Ring) \land (x \in S \land y \in S)) \to \forall i \in N \forall j \in N \forall c \in ℕ {coe}_{1} (\underset{k \in N}{\sum_{P}} ((i x k) \cdot_{P} (k y j))) (c) = 0_{R}$

Metamath Proof Explorer

Theorem cpmatmcllem

Proof