cply1mul

Description: The product of two constant polynomials is a constant polynomial. (Contributed by AV, 18-Nov-2019)

	Ref	Expression
Hypotheses	cply1mul.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
	cply1mul.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	cply1mul.0	⊢ 0 = ( 0_g ‘ 𝑅 )
	cply1mul.m	⊢ × = ( ._r ‘ 𝑃 )
Assertion	cply1mul	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( ∀ 𝑐 ∈ ℕ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 ∧ ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 ) → ∀ 𝑐 ∈ ℕ ( ( coe₁ ‘ ( 𝐹 × 𝐺 ) ) ‘ 𝑐 ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		cply1mul.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
2		cply1mul.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		cply1mul.0	⊢ 0 = ( 0_g ‘ 𝑅 )
4		cply1mul.m	⊢ × = ( ._r ‘ 𝑃 )
5		eqid	⊢ ( ._r ‘ 𝑅 ) = ( ._r ‘ 𝑅 )
6	1 4 5 2	coe1mul	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( coe₁ ‘ ( 𝐹 × 𝐺 ) ) = ( 𝑠 ∈ ℕ₀ ↦ ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑠 − 𝑘 ) ) ) ) ) ) )
7	6	3expb	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( coe₁ ‘ ( 𝐹 × 𝐺 ) ) = ( 𝑠 ∈ ℕ₀ ↦ ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑠 − 𝑘 ) ) ) ) ) ) )
8	7	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) ∧ ∀ 𝑐 ∈ ℕ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 ∧ ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 ) ) → ( coe₁ ‘ ( 𝐹 × 𝐺 ) ) = ( 𝑠 ∈ ℕ₀ ↦ ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑠 − 𝑘 ) ) ) ) ) ) )
9	8	adantr	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) ∧ ∀ 𝑐 ∈ ℕ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 ∧ ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 ) ) ∧ 𝑛 ∈ ℕ ) → ( coe₁ ‘ ( 𝐹 × 𝐺 ) ) = ( 𝑠 ∈ ℕ₀ ↦ ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑠 − 𝑘 ) ) ) ) ) ) )
10		oveq2	⊢ ( 𝑠 = 𝑛 → ( 0 ... 𝑠 ) = ( 0 ... 𝑛 ) )
11		fvoveq1	⊢ ( 𝑠 = 𝑛 → ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑠 − 𝑘 ) ) = ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) )
12	11	oveq2d	⊢ ( 𝑠 = 𝑛 → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑠 − 𝑘 ) ) ) = ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) )
13	10 12	mpteq12dv	⊢ ( 𝑠 = 𝑛 → ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑠 − 𝑘 ) ) ) ) = ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) ) )
14	13	oveq2d	⊢ ( 𝑠 = 𝑛 → ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑠 − 𝑘 ) ) ) ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) ) ) )
15	14	adantl	⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) ∧ ∀ 𝑐 ∈ ℕ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 ∧ ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑠 = 𝑛 ) → ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑠 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑠 − 𝑘 ) ) ) ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) ) ) )
16		nnnn0	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀ )
17	16	adantl	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) ∧ ∀ 𝑐 ∈ ℕ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 ∧ ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 ) ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ₀ )
18		ovexd	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) ∧ ∀ 𝑐 ∈ ℕ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 ∧ ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) ) ) ∈ V )
19	9 15 17 18	fvmptd	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) ∧ ∀ 𝑐 ∈ ℕ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 ∧ ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( coe₁ ‘ ( 𝐹 × 𝐺 ) ) ‘ 𝑛 ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) ) ) )
20		r19.26	⊢ ( ∀ 𝑐 ∈ ℕ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 ∧ ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 ) ↔ ( ∀ 𝑐 ∈ ℕ ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 ∧ ∀ 𝑐 ∈ ℕ ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 ) )
21		oveq2	⊢ ( 𝑘 = 0 → ( 𝑛 − 𝑘 ) = ( 𝑛 − 0 ) )
22		nncn	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
23	22	subid1d	⊢ ( 𝑛 ∈ ℕ → ( 𝑛 − 0 ) = 𝑛 )
24	23	adantr	⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝑛 − 0 ) = 𝑛 )
25	21 24	sylan9eqr	⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑘 = 0 ) → ( 𝑛 − 𝑘 ) = 𝑛 )
26		simpll	⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑘 = 0 ) → 𝑛 ∈ ℕ )
27	25 26	eqeltrd	⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑘 = 0 ) → ( 𝑛 − 𝑘 ) ∈ ℕ )
28		fveqeq2	⊢ ( 𝑐 = ( 𝑛 − 𝑘 ) → ( ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 ↔ ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) = 0 ) )
29	28	rspcv	⊢ ( ( 𝑛 − 𝑘 ) ∈ ℕ → ( ∀ 𝑐 ∈ ℕ ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 → ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) = 0 ) )
30	27 29	syl	⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑘 = 0 ) → ( ∀ 𝑐 ∈ ℕ ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 → ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) = 0 ) )
31		oveq2	⊢ ( ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) = 0 → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) 0 ) )
32		simpll	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) ∧ ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑘 = 0 ) ) → 𝑅 ∈ Ring )
33		simprl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → 𝐹 ∈ 𝐵 )
34		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... 𝑛 ) → 𝑘 ∈ ℕ₀ )
35	34	adantl	⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → 𝑘 ∈ ℕ₀ )
36	35	adantr	⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑘 = 0 ) → 𝑘 ∈ ℕ₀ )
37		eqid	⊢ ( coe₁ ‘ 𝐹 ) = ( coe₁ ‘ 𝐹 )
38		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
39	37 2 1 38	coe1fvalcl	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝑘 ∈ ℕ₀ ) → ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
40	33 36 39	syl2an	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) ∧ ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑘 = 0 ) ) → ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
41	38 5 3	ringrz	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) 0 ) = 0 )
42	32 40 41	syl2anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) ∧ ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑘 = 0 ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) 0 ) = 0 )
43	31 42	sylan9eqr	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) ∧ ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑘 = 0 ) ) ∧ ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) = 0 ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 )
44	43	ex	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) ∧ ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑘 = 0 ) ) → ( ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) = 0 → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 ) )
45	44	expcom	⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑘 = 0 ) → ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) = 0 → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 ) ) )
46	45	com23	⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑘 = 0 ) → ( ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) = 0 → ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 ) ) )
47	30 46	syldc	⊢ ( ∀ 𝑐 ∈ ℕ ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 → ( ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑘 = 0 ) → ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 ) ) )
48	47	expd	⊢ ( ∀ 𝑐 ∈ ℕ ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 → ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝑘 = 0 → ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 ) ) ) )
49	48	com24	⊢ ( ∀ 𝑐 ∈ ℕ ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 → ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( 𝑘 = 0 → ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 ) ) ) )
50	49	adantl	⊢ ( ( ∀ 𝑐 ∈ ℕ ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 ∧ ∀ 𝑐 ∈ ℕ ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 ) → ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( 𝑘 = 0 → ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 ) ) ) )
51	50	com13	⊢ ( 𝑘 = 0 → ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( ( ∀ 𝑐 ∈ ℕ ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 ∧ ∀ 𝑐 ∈ ℕ ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 ) → ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 ) ) ) )
52		neqne	⊢ ( ¬ 𝑘 = 0 → 𝑘 ≠ 0 )
53	52 34	anim12ci	⊢ ( ( ¬ 𝑘 = 0 ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝑘 ∈ ℕ₀ ∧ 𝑘 ≠ 0 ) )
54		elnnne0	⊢ ( 𝑘 ∈ ℕ ↔ ( 𝑘 ∈ ℕ₀ ∧ 𝑘 ≠ 0 ) )
55	53 54	sylibr	⊢ ( ( ¬ 𝑘 = 0 ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → 𝑘 ∈ ℕ )
56		fveqeq2	⊢ ( 𝑐 = 𝑘 → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 ↔ ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) = 0 ) )
57	56	rspcv	⊢ ( 𝑘 ∈ ℕ → ( ∀ 𝑐 ∈ ℕ ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 → ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) = 0 ) )
58	55 57	syl	⊢ ( ( ¬ 𝑘 = 0 ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ∀ 𝑐 ∈ ℕ ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 → ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) = 0 ) )
59		oveq1	⊢ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) = 0 → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = ( 0 ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) )
60		simpll	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → 𝑅 ∈ Ring )
61	2	eleq2i	⊢ ( 𝐺 ∈ 𝐵 ↔ 𝐺 ∈ ( Base ‘ 𝑃 ) )
62	61	bilani	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐺 ∈ ( Base ‘ 𝑃 ) )
63	62	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → 𝐺 ∈ ( Base ‘ 𝑃 ) )
64		fznn0sub	⊢ ( 𝑘 ∈ ( 0 ... 𝑛 ) → ( 𝑛 − 𝑘 ) ∈ ℕ₀ )
65		eqid	⊢ ( coe₁ ‘ 𝐺 ) = ( coe₁ ‘ 𝐺 )
66		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
67	65 66 1 38	coe1fvalcl	⊢ ( ( 𝐺 ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑛 − 𝑘 ) ∈ ℕ₀ ) → ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ∈ ( Base ‘ 𝑅 ) )
68	63 64 67	syl2an	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ∈ ( Base ‘ 𝑅 ) )
69	38 5 3	ringlz	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( 0 ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 )
70	60 68 69	syl2anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 0 ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 )
71	59 70	sylan9eqr	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) ∧ ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) = 0 ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 )
72	71	ex	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) = 0 → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 ) )
73	72	ex	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( 𝑘 ∈ ( 0 ... 𝑛 ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) = 0 → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 ) ) )
74	73	com23	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) = 0 → ( 𝑘 ∈ ( 0 ... 𝑛 ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 ) ) )
75	74	a1dd	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) = 0 → ( 𝑛 ∈ ℕ → ( 𝑘 ∈ ( 0 ... 𝑛 ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 ) ) ) )
76	75	com14	⊢ ( 𝑘 ∈ ( 0 ... 𝑛 ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) = 0 → ( 𝑛 ∈ ℕ → ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 ) ) ) )
77	76	adantl	⊢ ( ( ¬ 𝑘 = 0 ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) = 0 → ( 𝑛 ∈ ℕ → ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 ) ) ) )
78	58 77	syld	⊢ ( ( ¬ 𝑘 = 0 ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ∀ 𝑐 ∈ ℕ ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 → ( 𝑛 ∈ ℕ → ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 ) ) ) )
79	78	com24	⊢ ( ( ¬ 𝑘 = 0 ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( 𝑛 ∈ ℕ → ( ∀ 𝑐 ∈ ℕ ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 ) ) ) )
80	79	ex	⊢ ( ¬ 𝑘 = 0 → ( 𝑘 ∈ ( 0 ... 𝑛 ) → ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( 𝑛 ∈ ℕ → ( ∀ 𝑐 ∈ ℕ ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 ) ) ) ) )
81	80	com14	⊢ ( 𝑛 ∈ ℕ → ( 𝑘 ∈ ( 0 ... 𝑛 ) → ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( ¬ 𝑘 = 0 → ( ∀ 𝑐 ∈ ℕ ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 ) ) ) ) )
82	81	imp	⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( ¬ 𝑘 = 0 → ( ∀ 𝑐 ∈ ℕ ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 ) ) ) )
83	82	com14	⊢ ( ∀ 𝑐 ∈ ℕ ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 → ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( ¬ 𝑘 = 0 → ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 ) ) ) )
84	83	adantr	⊢ ( ( ∀ 𝑐 ∈ ℕ ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 ∧ ∀ 𝑐 ∈ ℕ ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 ) → ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( ¬ 𝑘 = 0 → ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 ) ) ) )
85	84	com13	⊢ ( ¬ 𝑘 = 0 → ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( ( ∀ 𝑐 ∈ ℕ ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 ∧ ∀ 𝑐 ∈ ℕ ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 ) → ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 ) ) ) )
86	51 85	pm2.61i	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( ( ∀ 𝑐 ∈ ℕ ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 ∧ ∀ 𝑐 ∈ ℕ ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 ) → ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 ) ) )
87	20 86	biimtrid	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( ∀ 𝑐 ∈ ℕ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 ∧ ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 ) → ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 ) ) )
88	87	imp	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) ∧ ∀ 𝑐 ∈ ℕ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 ∧ ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 ) ) → ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 ) )
89	88	impl	⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) ∧ ∀ 𝑐 ∈ ℕ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 ∧ ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) = 0 )
90	89	mpteq2dva	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) ∧ ∀ 𝑐 ∈ ℕ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 ∧ ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) ) = ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ 0 ) )
91	90	oveq2d	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) ∧ ∀ 𝑐 ∈ ℕ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 ∧ ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑘 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑛 − 𝑘 ) ) ) ) ) = ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ 0 ) ) )
92		ringmnd	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
93		ovexd	⊢ ( 𝑅 ∈ Ring → ( 0 ... 𝑛 ) ∈ V )
94	3	gsumz	⊢ ( ( 𝑅 ∈ Mnd ∧ ( 0 ... 𝑛 ) ∈ V ) → ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ 0 ) ) = 0 )
95	92 93 94	syl2anc	⊢ ( 𝑅 ∈ Ring → ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ 0 ) ) = 0 )
96	95	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ 0 ) ) = 0 )
97	96	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) ∧ ∀ 𝑐 ∈ ℕ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 ∧ ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 ) ) → ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ 0 ) ) = 0 )
98	97	adantr	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) ∧ ∀ 𝑐 ∈ ℕ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 ∧ ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑅 Σ_g ( 𝑘 ∈ ( 0 ... 𝑛 ) ↦ 0 ) ) = 0 )
99	19 91 98	3eqtrd	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) ∧ ∀ 𝑐 ∈ ℕ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 ∧ ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( coe₁ ‘ ( 𝐹 × 𝐺 ) ) ‘ 𝑛 ) = 0 )
100	99	ralrimiva	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) ∧ ∀ 𝑐 ∈ ℕ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 ∧ ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 ) ) → ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( 𝐹 × 𝐺 ) ) ‘ 𝑛 ) = 0 )
101		fveqeq2	⊢ ( 𝑐 = 𝑛 → ( ( ( coe₁ ‘ ( 𝐹 × 𝐺 ) ) ‘ 𝑐 ) = 0 ↔ ( ( coe₁ ‘ ( 𝐹 × 𝐺 ) ) ‘ 𝑛 ) = 0 ) )
102	101	cbvralvw	⊢ ( ∀ 𝑐 ∈ ℕ ( ( coe₁ ‘ ( 𝐹 × 𝐺 ) ) ‘ 𝑐 ) = 0 ↔ ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( 𝐹 × 𝐺 ) ) ‘ 𝑛 ) = 0 )
103	100 102	sylibr	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) ∧ ∀ 𝑐 ∈ ℕ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 ∧ ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 ) ) → ∀ 𝑐 ∈ ℕ ( ( coe₁ ‘ ( 𝐹 × 𝐺 ) ) ‘ 𝑐 ) = 0 )
104	103	ex	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) ) → ( ∀ 𝑐 ∈ ℕ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑐 ) = 0 ∧ ( ( coe₁ ‘ 𝐺 ) ‘ 𝑐 ) = 0 ) → ∀ 𝑐 ∈ ℕ ( ( coe₁ ‘ ( 𝐹 × 𝐺 ) ) ‘ 𝑐 ) = 0 ) )

Metamath Proof Explorer

Theorem cply1mul

Proof