Theorem cpmatmcllem

Description: Lemma for cpmatmcl . (Contributed by AV, 18-Nov-2019)

	Ref	Expression
Hypotheses	cpmatsrngpmat.s	⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
	cpmatsrngpmat.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	cpmatsrngpmat.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
Assertion	cpmatmcllem	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		cpmatsrngpmat.s	⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
2		cpmatsrngpmat.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		cpmatsrngpmat.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
4		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
5	1 2 3 4	cpmatelimp	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑥 ∈ 𝑆 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) )
6	1 2 3 4	cpmatelimp	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑦 ∈ 𝑆 → ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑙 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) )
7	6	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑦 ∈ 𝑆 → ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑙 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) )
8		ralcom	⊢ ( ∀ 𝑙 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ↔ ∀ 𝑗 ∈ 𝑁 ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) )
9		r19.26-2	⊢ ( ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ↔ ( ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
10		ralcom	⊢ ( ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ↔ ∀ 𝑐 ∈ ℕ ∀ 𝑙 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
11	9 10	bitr3i	⊢ ( ( ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ↔ ∀ 𝑐 ∈ ℕ ∀ 𝑙 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
12		nfv	⊢ Ⅎ 𝑐 ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) )
13		nfra1	⊢ Ⅎ 𝑐 ∀ 𝑐 ∈ ℕ ∀ 𝑙 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) )
14	12 13	nfan	⊢ Ⅎ 𝑐 ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ∀ 𝑐 ∈ ℕ ∀ 𝑙 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
15		simp-4r	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → 𝑅 ∈ Ring )
16		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
17		simplrl	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
18		simpr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → 𝑘 ∈ 𝑁 )
19		simplrl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
20	19	adantr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
21	3 16 4 17 18 20	matecld	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑖 𝑥 𝑘 ) ∈ ( Base ‘ 𝑃 ) )
22		simplrr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
23		simplrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
24	23	adantr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
25	3 16 4 18 22 24	matecld	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑘 𝑦 𝑗 ) ∈ ( Base ‘ 𝑃 ) )
26	15 21 25	jca32	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑅 ∈ Ring ∧ ( ( 𝑖 𝑥 𝑘 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑘 𝑦 𝑗 ) ∈ ( Base ‘ 𝑃 ) ) ) )
27	26	adantlr	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ∀ 𝑐 ∈ ℕ ∀ 𝑙 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑅 ∈ Ring ∧ ( ( 𝑖 𝑥 𝑘 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑘 𝑦 𝑗 ) ∈ ( Base ‘ 𝑃 ) ) ) )
28		oveq2	⊢ ( 𝑙 = 𝑘 → ( 𝑖 𝑥 𝑙 ) = ( 𝑖 𝑥 𝑘 ) )
29	28	fveq2d	⊢ ( 𝑙 = 𝑘 → ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) = ( coe1 ‘ ( 𝑖 𝑥 𝑘 ) ) )
30	29	fveq1d	⊢ ( 𝑙 = 𝑘 → ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( ( coe1 ‘ ( 𝑖 𝑥 𝑘 ) ) ‘ 𝑐 ) )
31	30	eqeq1d	⊢ ( 𝑙 = 𝑘 → ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ↔ ( ( coe1 ‘ ( 𝑖 𝑥 𝑘 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
32		fvoveq1	⊢ ( 𝑙 = 𝑘 → ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) = ( coe1 ‘ ( 𝑘 𝑦 𝑗 ) ) )
33	32	fveq1d	⊢ ( 𝑙 = 𝑘 → ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( ( coe1 ‘ ( 𝑘 𝑦 𝑗 ) ) ‘ 𝑐 ) )
34	33	eqeq1d	⊢ ( 𝑙 = 𝑘 → ( ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ↔ ( ( coe1 ‘ ( 𝑘 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
35	31 34	anbi12d	⊢ ( 𝑙 = 𝑘 → ( ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ↔ ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑘 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑘 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) )
36	35	rspcva	⊢ ( ( 𝑘 ∈ 𝑁 ∧ ∀ 𝑙 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) → ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑘 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑘 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
37	36	a1i	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑐 ∈ ℕ ) → ( ( 𝑘 ∈ 𝑁 ∧ ∀ 𝑙 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) → ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑘 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑘 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) )
38	37	exp4b	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑐 ∈ ℕ → ( 𝑘 ∈ 𝑁 → ( ∀ 𝑙 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) → ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑘 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑘 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) ) ) )
39	38	com23	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑘 ∈ 𝑁 → ( 𝑐 ∈ ℕ → ( ∀ 𝑙 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) → ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑘 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑘 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) ) ) )
40	39	imp31	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) ∧ 𝑐 ∈ ℕ ) → ( ∀ 𝑙 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) → ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑘 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑘 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) )
41	40	ralimdva	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → ( ∀ 𝑐 ∈ ℕ ∀ 𝑙 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) → ∀ 𝑐 ∈ ℕ ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑘 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑘 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) )
42	41	impancom	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ∀ 𝑐 ∈ ℕ ∀ 𝑙 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) → ( 𝑘 ∈ 𝑁 → ∀ 𝑐 ∈ ℕ ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑘 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑘 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) )
43	42	imp	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ∀ 𝑐 ∈ ℕ ∀ 𝑙 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) ∧ 𝑘 ∈ 𝑁 ) → ∀ 𝑐 ∈ ℕ ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑘 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑘 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
44		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
45		eqid	⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
46	2 16 44 45	cply1mul	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝑖 𝑥 𝑘 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑘 𝑦 𝑗 ) ∈ ( Base ‘ 𝑃 ) ) ) → ( ∀ 𝑐 ∈ ℕ ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑘 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑘 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) → ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
47	27 43 46	sylc	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ∀ 𝑐 ∈ ℕ ∀ 𝑙 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) ∧ 𝑘 ∈ 𝑁 ) → ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) )
48	47	r19.21bi	⊢ ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ∀ 𝑐 ∈ ℕ ∀ 𝑙 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) ∧ 𝑘 ∈ 𝑁 ) ∧ 𝑐 ∈ ℕ ) → ( ( coe1 ‘ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) )
49	48	an32s	⊢ ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ∀ 𝑐 ∈ ℕ ∀ 𝑙 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) ∧ 𝑐 ∈ ℕ ) ∧ 𝑘 ∈ 𝑁 ) → ( ( coe1 ‘ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) )
50	49	mpteq2dva	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ∀ 𝑐 ∈ ℕ ∀ 𝑙 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) ∧ 𝑐 ∈ ℕ ) → ( 𝑘 ∈ 𝑁 ↦ ( ( coe1 ‘ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ‘ 𝑐 ) ) = ( 𝑘 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) )
51	50	oveq2d	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ∀ 𝑐 ∈ ℕ ∀ 𝑙 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) ∧ 𝑐 ∈ ℕ ) → ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( coe1 ‘ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ‘ 𝑐 ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) ) )
52		ringmnd	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
53	52	anim2i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Mnd ) )
54	53	ancomd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑅 ∈ Mnd ∧ 𝑁 ∈ Fin ) )
55	44	gsumz	⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑁 ∈ Fin ) → ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑅 ) )
56	54 55	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑅 ) )
57	56	ad4antr	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ∀ 𝑐 ∈ ℕ ∀ 𝑙 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) ∧ 𝑐 ∈ ℕ ) → ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑅 ) )
58	51 57	eqtrd	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ∀ 𝑐 ∈ ℕ ∀ 𝑙 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) ∧ 𝑐 ∈ ℕ ) → ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( coe1 ‘ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ‘ 𝑐 ) ) ) = ( 0g ‘ 𝑅 ) )
59	58	ex	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ∀ 𝑐 ∈ ℕ ∀ 𝑙 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) → ( 𝑐 ∈ ℕ → ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( coe1 ‘ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ‘ 𝑐 ) ) ) = ( 0g ‘ 𝑅 ) ) )
60	14 59	ralrimi	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ∀ 𝑐 ∈ ℕ ∀ 𝑙 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) → ∀ 𝑐 ∈ ℕ ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( coe1 ‘ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ‘ 𝑐 ) ) ) = ( 0g ‘ 𝑅 ) )
61		simp-4r	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑐 ∈ ℕ ) → 𝑅 ∈ Ring )
62		nnnn0	⊢ ( 𝑐 ∈ ℕ → 𝑐 ∈ ℕ0 )
63	62	adantl	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑐 ∈ ℕ ) → 𝑐 ∈ ℕ0 )
64	2	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
65	64	ad4antlr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → 𝑃 ∈ Ring )
66	16 45	ringcl	⊢ ( ( 𝑃 ∈ Ring ∧ ( 𝑖 𝑥 𝑘 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑘 𝑦 𝑗 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ∈ ( Base ‘ 𝑃 ) )
67	65 21 25 66	syl3anc	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ∈ ( Base ‘ 𝑃 ) )
68	67	ralrimiva	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ∀ 𝑘 ∈ 𝑁 ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ∈ ( Base ‘ 𝑃 ) )
69	68	adantr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑐 ∈ ℕ ) → ∀ 𝑘 ∈ 𝑁 ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ∈ ( Base ‘ 𝑃 ) )
70		simp-4l	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑐 ∈ ℕ ) → 𝑁 ∈ Fin )
71	2 16 61 63 69 70	coe1fzgsumd	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑐 ∈ ℕ ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( coe1 ‘ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ‘ 𝑐 ) ) ) )
72	71	eqeq1d	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑐 ∈ ℕ ) → ( ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ↔ ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( coe1 ‘ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ‘ 𝑐 ) ) ) = ( 0g ‘ 𝑅 ) ) )
73	72	ralbidva	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ↔ ∀ 𝑐 ∈ ℕ ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( coe1 ‘ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ‘ 𝑐 ) ) ) = ( 0g ‘ 𝑅 ) ) )
74	73	adantr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ∀ 𝑐 ∈ ℕ ∀ 𝑙 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) → ( ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ↔ ∀ 𝑐 ∈ ℕ ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( coe1 ‘ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ‘ 𝑐 ) ) ) = ( 0g ‘ 𝑅 ) ) )
75	60 74	mpbird	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ∀ 𝑐 ∈ ℕ ∀ 𝑙 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) → ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) )
76	75	ex	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ∀ 𝑐 ∈ ℕ ∀ 𝑙 ∈ 𝑁 ( ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) → ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
77	11 76	syl5bi	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ( ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) → ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
78	77	expd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) → ( ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) → ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) )
79	78	expr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑖 ∈ 𝑁 ) → ( 𝑗 ∈ 𝑁 → ( ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) → ( ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) → ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) ) )
80	79	com23	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑖 ∈ 𝑁 ) → ( ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) → ( 𝑗 ∈ 𝑁 → ( ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) → ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) ) )
81	80	imp31	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑖 ∈ 𝑁 ) ∧ ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ∧ 𝑗 ∈ 𝑁 ) → ( ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) → ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
82	81	ralimdva	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑖 ∈ 𝑁 ) ∧ ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) → ( ∀ 𝑗 ∈ 𝑁 ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) → ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
83	8 82	syl5bi	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑖 ∈ 𝑁 ) ∧ ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) → ( ∀ 𝑙 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) → ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
84	83	ex	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑖 ∈ 𝑁 ) → ( ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) → ( ∀ 𝑙 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) → ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) )
85	84	com23	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑖 ∈ 𝑁 ) → ( ∀ 𝑙 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) → ( ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) → ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) )
86	85	impancom	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ∀ 𝑙 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑖 ∈ 𝑁 → ( ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) → ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) )
87	86	imp	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ∀ 𝑙 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ∧ 𝑖 ∈ 𝑁 ) → ( ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) → ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
88	87	ralimdva	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ∀ 𝑙 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) )
89	88	ex	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ∀ 𝑙 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) )
90	89	expr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐶 ) → ( ∀ 𝑙 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) ) )
91	90	impd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑙 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑙 𝑦 𝑗 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) )
92	7 91	syld	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑦 ∈ 𝑆 → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) )
93	92	com23	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) → ( 𝑦 ∈ 𝑆 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) )
94	93	ex	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑥 ∈ ( Base ‘ 𝐶 ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) → ( 𝑦 ∈ 𝑆 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) ) )
95	94	impd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑙 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑥 𝑙 ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑦 ∈ 𝑆 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) )
96	5 95	syld	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑥 ∈ 𝑆 → ( 𝑦 ∈ 𝑆 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) ) ) )
97	96	imp32	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑐 ∈ ℕ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑘 ) ( .r ‘ 𝑃 ) ( 𝑘 𝑦 𝑗 ) ) ) ) ) ‘ 𝑐 ) = ( 0g ‘ 𝑅 ) )