ply1mulgsumlem1

	Ref	Expression
Hypotheses	ply1mulgsum.p	$⊢ P = {Poly}_{1} (R)$
	ply1mulgsum.b	$⊢ B = {Base}_{P}$
	ply1mulgsum.a	$⊢ A = {coe}_{1} (K)$
	ply1mulgsum.c	$⊢ C = {coe}_{1} (L)$
	ply1mulgsum.x	$⊢ X = {var}_{1} (R)$
	ply1mulgsum.pm	$⊢ \underset{˙}{\times} = \cdot_{P}$
	ply1mulgsum.sm	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	ply1mulgsum.rm	$⊢ \underset{˙}{*} = \cdot_{R}$
	ply1mulgsum.m	$⊢ M = {mulGrp}_{P}$
	ply1mulgsum.e	$⊢ \underset{˙}{\times} = \cdot_{M}$
Assertion	ply1mulgsumlem1	$⊢ (R \in Ring \land K \in B \land L \in B) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to (A (n) = 0_{R} \land C (n) = 0_{R}))$

Proof

Step	Hyp	Ref	Expression
1		ply1mulgsum.p	$⊢ P = {Poly}_{1} (R)$
2		ply1mulgsum.b	$⊢ B = {Base}_{P}$
3		ply1mulgsum.a	$⊢ A = {coe}_{1} (K)$
4		ply1mulgsum.c	$⊢ C = {coe}_{1} (L)$
5		ply1mulgsum.x	$⊢ X = {var}_{1} (R)$
6		ply1mulgsum.pm	$⊢ \underset{˙}{\times} = \cdot_{P}$
7		ply1mulgsum.sm	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
8		ply1mulgsum.rm	$⊢ \underset{˙}{*} = \cdot_{R}$
9		ply1mulgsum.m	$⊢ M = {mulGrp}_{P}$
10		ply1mulgsum.e	$⊢ \underset{˙}{\times} = \cdot_{M}$
11		eqid	$⊢ 0_{R} = 0_{R}$
12	3 2 1 11	coe1ae0	$⊢ K \in B \to \exists b \in ℕ_{0} \forall n \in ℕ_{0} (b < n \to A (n) = 0_{R})$
13	12	3ad2ant2	$⊢ (R \in Ring \land K \in B \land L \in B) \to \exists b \in ℕ_{0} \forall n \in ℕ_{0} (b < n \to A (n) = 0_{R})$
14	4 2 1 11	coe1ae0	$⊢ L \in B \to \exists a \in ℕ_{0} \forall n \in ℕ_{0} (a < n \to C (n) = 0_{R})$
15	14	3ad2ant3	$⊢ (R \in Ring \land K \in B \land L \in B) \to \exists a \in ℕ_{0} \forall n \in ℕ_{0} (a < n \to C (n) = 0_{R})$
16		nn0addcl	$⊢ (a \in ℕ_{0} \land b \in ℕ_{0}) \to a + b \in ℕ_{0}$
17	16	adantr	$⊢ ((a \in ℕ_{0} \land b \in ℕ_{0}) \land (R \in Ring \land K \in B \land L \in B)) \to a + b \in ℕ_{0}$
18	17	adantr	$⊢ (((a \in ℕ_{0} \land b \in ℕ_{0}) \land (R \in Ring \land K \in B \land L \in B)) \land (\forall n \in ℕ_{0} (a < n \to C (n) = 0_{R}) \land \forall n \in ℕ_{0} (b < n \to A (n) = 0_{R}))) \to a + b \in ℕ_{0}$
19		breq1	$⊢ s = a + b \to (s < n \leftrightarrow a + b < n)$
20	19	imbi1d	$⊢ s = a + b \to ((s < n \to (A (n) = 0_{R} \land C (n) = 0_{R})) \leftrightarrow (a + b < n \to (A (n) = 0_{R} \land C (n) = 0_{R})))$
21	20	ralbidv	$⊢ s = a + b \to (\forall n \in ℕ_{0} (s < n \to (A (n) = 0_{R} \land C (n) = 0_{R})) \leftrightarrow \forall n \in ℕ_{0} (a + b < n \to (A (n) = 0_{R} \land C (n) = 0_{R})))$
22	21	adantl	$⊢ ((((a \in ℕ_{0} \land b \in ℕ_{0}) \land (R \in Ring \land K \in B \land L \in B)) \land (\forall n \in ℕ_{0} (a < n \to C (n) = 0_{R}) \land \forall n \in ℕ_{0} (b < n \to A (n) = 0_{R}))) \land s = a + b) \to (\forall n \in ℕ_{0} (s < n \to (A (n) = 0_{R} \land C (n) = 0_{R})) \leftrightarrow \forall n \in ℕ_{0} (a + b < n \to (A (n) = 0_{R} \land C (n) = 0_{R})))$
23		r19.26	$⊢ \forall n \in ℕ_{0} ((a < n \to C (n) = 0_{R}) \land (b < n \to A (n) = 0_{R})) \leftrightarrow (\forall n \in ℕ_{0} (a < n \to C (n) = 0_{R}) \land \forall n \in ℕ_{0} (b < n \to A (n) = 0_{R}))$
24		nn0cn	$⊢ a \in ℕ_{0} \to a \in ℂ$
25	24	adantl	$⊢ (b \in ℕ_{0} \land a \in ℕ_{0}) \to a \in ℂ$
26		nn0cn	$⊢ b \in ℕ_{0} \to b \in ℂ$
27	26	adantr	$⊢ (b \in ℕ_{0} \land a \in ℕ_{0}) \to b \in ℂ$
28	25 27	addcomd	$⊢ (b \in ℕ_{0} \land a \in ℕ_{0}) \to a + b = b + a$
29	28	3adant3	$⊢ (b \in ℕ_{0} \land a \in ℕ_{0} \land n \in ℕ_{0}) \to a + b = b + a$
30	29	breq1d	$⊢ (b \in ℕ_{0} \land a \in ℕ_{0} \land n \in ℕ_{0}) \to (a + b < n \leftrightarrow b + a < n)$
31		nn0sumltlt	$⊢ (b \in ℕ_{0} \land a \in ℕ_{0} \land n \in ℕ_{0}) \to (b + a < n \to a < n)$
32	30 31	sylbid	$⊢ (b \in ℕ_{0} \land a \in ℕ_{0} \land n \in ℕ_{0}) \to (a + b < n \to a < n)$
33	32	3expia	$⊢ (b \in ℕ_{0} \land a \in ℕ_{0}) \to (n \in ℕ_{0} \to (a + b < n \to a < n))$
34	33	ancoms	$⊢ (a \in ℕ_{0} \land b \in ℕ_{0}) \to (n \in ℕ_{0} \to (a + b < n \to a < n))$
35	34	adantr	$⊢ ((a \in ℕ_{0} \land b \in ℕ_{0}) \land (R \in Ring \land K \in B \land L \in B)) \to (n \in ℕ_{0} \to (a + b < n \to a < n))$
36	35	imp	$⊢ (((a \in ℕ_{0} \land b \in ℕ_{0}) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \to (a + b < n \to a < n)$
37	36	imim1d	$⊢ (((a \in ℕ_{0} \land b \in ℕ_{0}) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \to ((a < n \to C (n) = 0_{R}) \to (a + b < n \to C (n) = 0_{R}))$
38	37	com23	$⊢ (((a \in ℕ_{0} \land b \in ℕ_{0}) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \to (a + b < n \to ((a < n \to C (n) = 0_{R}) \to C (n) = 0_{R}))$
39	38	imp	$⊢ ((((a \in ℕ_{0} \land b \in ℕ_{0}) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land a + b < n) \to ((a < n \to C (n) = 0_{R}) \to C (n) = 0_{R})$
40		nn0sumltlt	$⊢ (a \in ℕ_{0} \land b \in ℕ_{0} \land n \in ℕ_{0}) \to (a + b < n \to b < n)$
41	40	3expia	$⊢ (a \in ℕ_{0} \land b \in ℕ_{0}) \to (n \in ℕ_{0} \to (a + b < n \to b < n))$
42	41	adantr	$⊢ ((a \in ℕ_{0} \land b \in ℕ_{0}) \land (R \in Ring \land K \in B \land L \in B)) \to (n \in ℕ_{0} \to (a + b < n \to b < n))$
43	42	imp	$⊢ (((a \in ℕ_{0} \land b \in ℕ_{0}) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \to (a + b < n \to b < n)$
44	43	imim1d	$⊢ (((a \in ℕ_{0} \land b \in ℕ_{0}) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \to ((b < n \to A (n) = 0_{R}) \to (a + b < n \to A (n) = 0_{R}))$
45	44	com23	$⊢ (((a \in ℕ_{0} \land b \in ℕ_{0}) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \to (a + b < n \to ((b < n \to A (n) = 0_{R}) \to A (n) = 0_{R}))$
46	45	imp	$⊢ ((((a \in ℕ_{0} \land b \in ℕ_{0}) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land a + b < n) \to ((b < n \to A (n) = 0_{R}) \to A (n) = 0_{R})$
47	39 46	anim12d	$⊢ ((((a \in ℕ_{0} \land b \in ℕ_{0}) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land a + b < n) \to (((a < n \to C (n) = 0_{R}) \land (b < n \to A (n) = 0_{R})) \to (C (n) = 0_{R} \land A (n) = 0_{R}))$
48	47	imp	$⊢ (((((a \in ℕ_{0} \land b \in ℕ_{0}) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land a + b < n) \land ((a < n \to C (n) = 0_{R}) \land (b < n \to A (n) = 0_{R}))) \to (C (n) = 0_{R} \land A (n) = 0_{R})$
49	48	ancomd	$⊢ (((((a \in ℕ_{0} \land b \in ℕ_{0}) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \land a + b < n) \land ((a < n \to C (n) = 0_{R}) \land (b < n \to A (n) = 0_{R}))) \to (A (n) = 0_{R} \land C (n) = 0_{R})$
50	49	exp31	$⊢ (((a \in ℕ_{0} \land b \in ℕ_{0}) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \to (a + b < n \to (((a < n \to C (n) = 0_{R}) \land (b < n \to A (n) = 0_{R})) \to (A (n) = 0_{R} \land C (n) = 0_{R})))$
51	50	com23	$⊢ (((a \in ℕ_{0} \land b \in ℕ_{0}) \land (R \in Ring \land K \in B \land L \in B)) \land n \in ℕ_{0}) \to (((a < n \to C (n) = 0_{R}) \land (b < n \to A (n) = 0_{R})) \to (a + b < n \to (A (n) = 0_{R} \land C (n) = 0_{R})))$
52	51	ralimdva	$⊢ ((a \in ℕ_{0} \land b \in ℕ_{0}) \land (R \in Ring \land K \in B \land L \in B)) \to (\forall n \in ℕ_{0} ((a < n \to C (n) = 0_{R}) \land (b < n \to A (n) = 0_{R})) \to \forall n \in ℕ_{0} (a + b < n \to (A (n) = 0_{R} \land C (n) = 0_{R})))$
53	23 52	biimtrrid	$⊢ ((a \in ℕ_{0} \land b \in ℕ_{0}) \land (R \in Ring \land K \in B \land L \in B)) \to ((\forall n \in ℕ_{0} (a < n \to C (n) = 0_{R}) \land \forall n \in ℕ_{0} (b < n \to A (n) = 0_{R})) \to \forall n \in ℕ_{0} (a + b < n \to (A (n) = 0_{R} \land C (n) = 0_{R})))$
54	53	imp	$⊢ (((a \in ℕ_{0} \land b \in ℕ_{0}) \land (R \in Ring \land K \in B \land L \in B)) \land (\forall n \in ℕ_{0} (a < n \to C (n) = 0_{R}) \land \forall n \in ℕ_{0} (b < n \to A (n) = 0_{R}))) \to \forall n \in ℕ_{0} (a + b < n \to (A (n) = 0_{R} \land C (n) = 0_{R}))$
55	18 22 54	rspcedvd	$⊢ (((a \in ℕ_{0} \land b \in ℕ_{0}) \land (R \in Ring \land K \in B \land L \in B)) \land (\forall n \in ℕ_{0} (a < n \to C (n) = 0_{R}) \land \forall n \in ℕ_{0} (b < n \to A (n) = 0_{R}))) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to (A (n) = 0_{R} \land C (n) = 0_{R}))$
56	55	exp31	$⊢ (a \in ℕ_{0} \land b \in ℕ_{0}) \to ((R \in Ring \land K \in B \land L \in B) \to ((\forall n \in ℕ_{0} (a < n \to C (n) = 0_{R}) \land \forall n \in ℕ_{0} (b < n \to A (n) = 0_{R})) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to (A (n) = 0_{R} \land C (n) = 0_{R}))))$
57	56	com23	$⊢ (a \in ℕ_{0} \land b \in ℕ_{0}) \to ((\forall n \in ℕ_{0} (a < n \to C (n) = 0_{R}) \land \forall n \in ℕ_{0} (b < n \to A (n) = 0_{R})) \to ((R \in Ring \land K \in B \land L \in B) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to (A (n) = 0_{R} \land C (n) = 0_{R}))))$
58	57	expd	$⊢ (a \in ℕ_{0} \land b \in ℕ_{0}) \to (\forall n \in ℕ_{0} (a < n \to C (n) = 0_{R}) \to (\forall n \in ℕ_{0} (b < n \to A (n) = 0_{R}) \to ((R \in Ring \land K \in B \land L \in B) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to (A (n) = 0_{R} \land C (n) = 0_{R})))))$
59	58	com34	$⊢ (a \in ℕ_{0} \land b \in ℕ_{0}) \to (\forall n \in ℕ_{0} (a < n \to C (n) = 0_{R}) \to ((R \in Ring \land K \in B \land L \in B) \to (\forall n \in ℕ_{0} (b < n \to A (n) = 0_{R}) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to (A (n) = 0_{R} \land C (n) = 0_{R})))))$
60	59	impancom	$⊢ (a \in ℕ_{0} \land \forall n \in ℕ_{0} (a < n \to C (n) = 0_{R})) \to (b \in ℕ_{0} \to ((R \in Ring \land K \in B \land L \in B) \to (\forall n \in ℕ_{0} (b < n \to A (n) = 0_{R}) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to (A (n) = 0_{R} \land C (n) = 0_{R})))))$
61	60	com14	$⊢ \forall n \in ℕ_{0} (b < n \to A (n) = 0_{R}) \to (b \in ℕ_{0} \to ((R \in Ring \land K \in B \land L \in B) \to ((a \in ℕ_{0} \land \forall n \in ℕ_{0} (a < n \to C (n) = 0_{R})) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to (A (n) = 0_{R} \land C (n) = 0_{R})))))$
62	61	impcom	$⊢ (b \in ℕ_{0} \land \forall n \in ℕ_{0} (b < n \to A (n) = 0_{R})) \to ((R \in Ring \land K \in B \land L \in B) \to ((a \in ℕ_{0} \land \forall n \in ℕ_{0} (a < n \to C (n) = 0_{R})) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to (A (n) = 0_{R} \land C (n) = 0_{R}))))$
63	62	rexlimiva	$⊢ \exists b \in ℕ_{0} \forall n \in ℕ_{0} (b < n \to A (n) = 0_{R}) \to ((R \in Ring \land K \in B \land L \in B) \to ((a \in ℕ_{0} \land \forall n \in ℕ_{0} (a < n \to C (n) = 0_{R})) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to (A (n) = 0_{R} \land C (n) = 0_{R}))))$
64	63	com13	$⊢ (a \in ℕ_{0} \land \forall n \in ℕ_{0} (a < n \to C (n) = 0_{R})) \to ((R \in Ring \land K \in B \land L \in B) \to (\exists b \in ℕ_{0} \forall n \in ℕ_{0} (b < n \to A (n) = 0_{R}) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to (A (n) = 0_{R} \land C (n) = 0_{R}))))$
65	64	rexlimiva	$⊢ \exists a \in ℕ_{0} \forall n \in ℕ_{0} (a < n \to C (n) = 0_{R}) \to ((R \in Ring \land K \in B \land L \in B) \to (\exists b \in ℕ_{0} \forall n \in ℕ_{0} (b < n \to A (n) = 0_{R}) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to (A (n) = 0_{R} \land C (n) = 0_{R}))))$
66	15 65	mpcom	$⊢ (R \in Ring \land K \in B \land L \in B) \to (\exists b \in ℕ_{0} \forall n \in ℕ_{0} (b < n \to A (n) = 0_{R}) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to (A (n) = 0_{R} \land C (n) = 0_{R})))$
67	13 66	mpd	$⊢ (R \in Ring \land K \in B \land L \in B) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to (A (n) = 0_{R} \land C (n) = 0_{R}))$

Metamath Proof Explorer

Theorem ply1mulgsumlem1

Proof