cply1coe0bi

Description: A polynomial is constant (i.e. a "lifted scalar") iff all but the first coefficient are zero. (Contributed by AV, 16-Nov-2019)

	Ref	Expression
Hypotheses	cply1coe0.k	$⊢ K = {Base}_{R}$
	cply1coe0.0	$⊢ \underset{˙}{0} = 0_{R}$
	cply1coe0.p	$⊢ P = {Poly}_{1} (R)$
	cply1coe0.b	$⊢ B = {Base}_{P}$
	cply1coe0.a	$⊢ A = algSc (P)$
Assertion	cply1coe0bi	$⊢ (R \in Ring \land M \in B) \to (\exists s \in K M = A (s) \leftrightarrow \forall n \in ℕ {coe}_{1} (M) (n) = \underset{˙}{0})$

Proof

Step	Hyp	Ref	Expression
1		cply1coe0.k	$⊢ K = {Base}_{R}$
2		cply1coe0.0	$⊢ \underset{˙}{0} = 0_{R}$
3		cply1coe0.p	$⊢ P = {Poly}_{1} (R)$
4		cply1coe0.b	$⊢ B = {Base}_{P}$
5		cply1coe0.a	$⊢ A = algSc (P)$
6	1 2 3 4 5	cply1coe0	$⊢ (R \in Ring \land s \in K) \to \forall n \in ℕ {coe}_{1} (A (s)) (n) = \underset{˙}{0}$
7	6	ad4ant13	$⊢ (((R \in Ring \land M \in B) \land s \in K) \land M = A (s)) \to \forall n \in ℕ {coe}_{1} (A (s)) (n) = \underset{˙}{0}$
8		fveq2	$⊢ M = A (s) \to {coe}_{1} (M) = {coe}_{1} (A (s))$
9	8	fveq1d	$⊢ M = A (s) \to {coe}_{1} (M) (n) = {coe}_{1} (A (s)) (n)$
10	9	eqeq1d	$⊢ M = A (s) \to ({coe}_{1} (M) (n) = \underset{˙}{0} \leftrightarrow {coe}_{1} (A (s)) (n) = \underset{˙}{0})$
11	10	ralbidv	$⊢ M = A (s) \to (\forall n \in ℕ {coe}_{1} (M) (n) = \underset{˙}{0} \leftrightarrow \forall n \in ℕ {coe}_{1} (A (s)) (n) = \underset{˙}{0})$
12	11	adantl	$⊢ (((R \in Ring \land M \in B) \land s \in K) \land M = A (s)) \to (\forall n \in ℕ {coe}_{1} (M) (n) = \underset{˙}{0} \leftrightarrow \forall n \in ℕ {coe}_{1} (A (s)) (n) = \underset{˙}{0})$
13	7 12	mpbird	$⊢ (((R \in Ring \land M \in B) \land s \in K) \land M = A (s)) \to \forall n \in ℕ {coe}_{1} (M) (n) = \underset{˙}{0}$
14	13	rexlimdva2	$⊢ (R \in Ring \land M \in B) \to (\exists s \in K M = A (s) \to \forall n \in ℕ {coe}_{1} (M) (n) = \underset{˙}{0})$
15		simpr	$⊢ (R \in Ring \land M \in B) \to M \in B$
16		0nn0	$⊢ 0 \in ℕ_{0}$
17		eqid	$⊢ {coe}_{1} (M) = {coe}_{1} (M)$
18	17 4 3 1	coe1fvalcl	$⊢ (M \in B \land 0 \in ℕ_{0}) \to {coe}_{1} (M) (0) \in K$
19	15 16 18	sylancl	$⊢ (R \in Ring \land M \in B) \to {coe}_{1} (M) (0) \in K$
20	19	adantr	$⊢ ((R \in Ring \land M \in B) \land \forall n \in ℕ {coe}_{1} (M) (n) = \underset{˙}{0}) \to {coe}_{1} (M) (0) \in K$
21		fveq2	$⊢ s = {coe}_{1} (M) (0) \to A (s) = A ({coe}_{1} (M) (0))$
22	21	eqeq2d	$⊢ s = {coe}_{1} (M) (0) \to (M = A (s) \leftrightarrow M = A ({coe}_{1} (M) (0)))$
23	22	adantl	$⊢ (((R \in Ring \land M \in B) \land \forall n \in ℕ {coe}_{1} (M) (n) = \underset{˙}{0}) \land s = {coe}_{1} (M) (0)) \to (M = A (s) \leftrightarrow M = A ({coe}_{1} (M) (0)))$
24		simpl	$⊢ (R \in Ring \land M \in B) \to R \in Ring$
25		eqid	$⊢ Scalar (P) = Scalar (P)$
26	3	ply1ring	$⊢ R \in Ring \to P \in Ring$
27	3	ply1lmod	$⊢ R \in Ring \to P \in LMod$
28		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
29	5 25 26 27 28 4	asclf	$⊢ R \in Ring \to A : {Base}_{Scalar (P)} ⟶ B$
30	29	adantr	$⊢ (R \in Ring \land M \in B) \to A : {Base}_{Scalar (P)} ⟶ B$
31		eqid	$⊢ {Base}_{R} = {Base}_{R}$
32	17 4 3 31	coe1fvalcl	$⊢ (M \in B \land 0 \in ℕ_{0}) \to {coe}_{1} (M) (0) \in {Base}_{R}$
33	15 16 32	sylancl	$⊢ (R \in Ring \land M \in B) \to {coe}_{1} (M) (0) \in {Base}_{R}$
34	3	ply1sca	$⊢ R \in Ring \to R = Scalar (P)$
35	34	eqcomd	$⊢ R \in Ring \to Scalar (P) = R$
36	35	fveq2d	$⊢ R \in Ring \to {Base}_{Scalar (P)} = {Base}_{R}$
37	36	adantr	$⊢ (R \in Ring \land M \in B) \to {Base}_{Scalar (P)} = {Base}_{R}$
38	33 37	eleqtrrd	$⊢ (R \in Ring \land M \in B) \to {coe}_{1} (M) (0) \in {Base}_{Scalar (P)}$
39	30 38	ffvelcdmd	$⊢ (R \in Ring \land M \in B) \to A ({coe}_{1} (M) (0)) \in B$
40	24 15 39	3jca	$⊢ (R \in Ring \land M \in B) \to (R \in Ring \land M \in B \land A ({coe}_{1} (M) (0)) \in B)$
41	40	adantr	$⊢ ((R \in Ring \land M \in B) \land \forall n \in ℕ {coe}_{1} (M) (n) = \underset{˙}{0}) \to (R \in Ring \land M \in B \land A ({coe}_{1} (M) (0)) \in B)$
42		simpr	$⊢ (((R \in Ring \land M \in B) \land n \in ℕ) \land {coe}_{1} (M) (n) = \underset{˙}{0}) \to {coe}_{1} (M) (n) = \underset{˙}{0}$
43	3 5 1 2	coe1scl	$⊢ (R \in Ring \land {coe}_{1} (M) (0) \in K) \to {coe}_{1} (A ({coe}_{1} (M) (0))) = (k \in ℕ_{0} ⟼ if (k = 0, {coe}_{1} (M) (0), \underset{˙}{0}))$
44	19 43	syldan	$⊢ (R \in Ring \land M \in B) \to {coe}_{1} (A ({coe}_{1} (M) (0))) = (k \in ℕ_{0} ⟼ if (k = 0, {coe}_{1} (M) (0), \underset{˙}{0}))$
45	44	adantr	$⊢ ((R \in Ring \land M \in B) \land n \in ℕ) \to {coe}_{1} (A ({coe}_{1} (M) (0))) = (k \in ℕ_{0} ⟼ if (k = 0, {coe}_{1} (M) (0), \underset{˙}{0}))$
46		nnne0	$⊢ n \in ℕ \to n \neq 0$
47	46	neneqd	$⊢ n \in ℕ \to \neg n = 0$
48	47	adantl	$⊢ ((R \in Ring \land M \in B) \land n \in ℕ) \to \neg n = 0$
49	48	adantr	$⊢ (((R \in Ring \land M \in B) \land n \in ℕ) \land k = n) \to \neg n = 0$
50		eqeq1	$⊢ k = n \to (k = 0 \leftrightarrow n = 0)$
51	50	notbid	$⊢ k = n \to (\neg k = 0 \leftrightarrow \neg n = 0)$
52	51	adantl	$⊢ (((R \in Ring \land M \in B) \land n \in ℕ) \land k = n) \to (\neg k = 0 \leftrightarrow \neg n = 0)$
53	49 52	mpbird	$⊢ (((R \in Ring \land M \in B) \land n \in ℕ) \land k = n) \to \neg k = 0$
54	53	iffalsed	$⊢ (((R \in Ring \land M \in B) \land n \in ℕ) \land k = n) \to if (k = 0, {coe}_{1} (M) (0), \underset{˙}{0}) = \underset{˙}{0}$
55		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
56	55	adantl	$⊢ ((R \in Ring \land M \in B) \land n \in ℕ) \to n \in ℕ_{0}$
57	2	fvexi	$⊢ \underset{˙}{0} \in V$
58	57	a1i	$⊢ ((R \in Ring \land M \in B) \land n \in ℕ) \to \underset{˙}{0} \in V$
59	45 54 56 58	fvmptd	$⊢ ((R \in Ring \land M \in B) \land n \in ℕ) \to {coe}_{1} (A ({coe}_{1} (M) (0))) (n) = \underset{˙}{0}$
60	59	eqcomd	$⊢ ((R \in Ring \land M \in B) \land n \in ℕ) \to \underset{˙}{0} = {coe}_{1} (A ({coe}_{1} (M) (0))) (n)$
61	60	adantr	$⊢ (((R \in Ring \land M \in B) \land n \in ℕ) \land {coe}_{1} (M) (n) = \underset{˙}{0}) \to \underset{˙}{0} = {coe}_{1} (A ({coe}_{1} (M) (0))) (n)$
62	42 61	eqtrd	$⊢ (((R \in Ring \land M \in B) \land n \in ℕ) \land {coe}_{1} (M) (n) = \underset{˙}{0}) \to {coe}_{1} (M) (n) = {coe}_{1} (A ({coe}_{1} (M) (0))) (n)$
63	62	ex	$⊢ ((R \in Ring \land M \in B) \land n \in ℕ) \to ({coe}_{1} (M) (n) = \underset{˙}{0} \to {coe}_{1} (M) (n) = {coe}_{1} (A ({coe}_{1} (M) (0))) (n))$
64	63	ralimdva	$⊢ (R \in Ring \land M \in B) \to (\forall n \in ℕ {coe}_{1} (M) (n) = \underset{˙}{0} \to \forall n \in ℕ {coe}_{1} (M) (n) = {coe}_{1} (A ({coe}_{1} (M) (0))) (n))$
65	64	imp	$⊢ ((R \in Ring \land M \in B) \land \forall n \in ℕ {coe}_{1} (M) (n) = \underset{˙}{0}) \to \forall n \in ℕ {coe}_{1} (M) (n) = {coe}_{1} (A ({coe}_{1} (M) (0))) (n)$
66	3 5 1	ply1sclid	$⊢ (R \in Ring \land {coe}_{1} (M) (0) \in K) \to {coe}_{1} (M) (0) = {coe}_{1} (A ({coe}_{1} (M) (0))) (0)$
67	19 66	syldan	$⊢ (R \in Ring \land M \in B) \to {coe}_{1} (M) (0) = {coe}_{1} (A ({coe}_{1} (M) (0))) (0)$
68	67	adantr	$⊢ ((R \in Ring \land M \in B) \land \forall n \in ℕ {coe}_{1} (M) (n) = \underset{˙}{0}) \to {coe}_{1} (M) (0) = {coe}_{1} (A ({coe}_{1} (M) (0))) (0)$
69		df-n0	$⊢ ℕ_{0} = ℕ \cup \{0\}$
70	69	raleqi	$⊢ \forall n \in ℕ_{0} {coe}_{1} (M) (n) = {coe}_{1} (A ({coe}_{1} (M) (0))) (n) \leftrightarrow \forall n \in (ℕ \cup \{0\}) {coe}_{1} (M) (n) = {coe}_{1} (A ({coe}_{1} (M) (0))) (n)$
71		c0ex	$⊢ 0 \in V$
72		fveq2	$⊢ n = 0 \to {coe}_{1} (M) (n) = {coe}_{1} (M) (0)$
73		fveq2	$⊢ n = 0 \to {coe}_{1} (A ({coe}_{1} (M) (0))) (n) = {coe}_{1} (A ({coe}_{1} (M) (0))) (0)$
74	72 73	eqeq12d	$⊢ n = 0 \to ({coe}_{1} (M) (n) = {coe}_{1} (A ({coe}_{1} (M) (0))) (n) \leftrightarrow {coe}_{1} (M) (0) = {coe}_{1} (A ({coe}_{1} (M) (0))) (0))$
75	74	ralunsn	$⊢ 0 \in V \to (\forall n \in (ℕ \cup \{0\}) {coe}_{1} (M) (n) = {coe}_{1} (A ({coe}_{1} (M) (0))) (n) \leftrightarrow (\forall n \in ℕ {coe}_{1} (M) (n) = {coe}_{1} (A ({coe}_{1} (M) (0))) (n) \land {coe}_{1} (M) (0) = {coe}_{1} (A ({coe}_{1} (M) (0))) (0)))$
76	71 75	mp1i	$⊢ ((R \in Ring \land M \in B) \land \forall n \in ℕ {coe}_{1} (M) (n) = \underset{˙}{0}) \to (\forall n \in (ℕ \cup \{0\}) {coe}_{1} (M) (n) = {coe}_{1} (A ({coe}_{1} (M) (0))) (n) \leftrightarrow (\forall n \in ℕ {coe}_{1} (M) (n) = {coe}_{1} (A ({coe}_{1} (M) (0))) (n) \land {coe}_{1} (M) (0) = {coe}_{1} (A ({coe}_{1} (M) (0))) (0)))$
77	70 76	bitrid	$⊢ ((R \in Ring \land M \in B) \land \forall n \in ℕ {coe}_{1} (M) (n) = \underset{˙}{0}) \to (\forall n \in ℕ_{0} {coe}_{1} (M) (n) = {coe}_{1} (A ({coe}_{1} (M) (0))) (n) \leftrightarrow (\forall n \in ℕ {coe}_{1} (M) (n) = {coe}_{1} (A ({coe}_{1} (M) (0))) (n) \land {coe}_{1} (M) (0) = {coe}_{1} (A ({coe}_{1} (M) (0))) (0)))$
78	65 68 77	mpbir2and	$⊢ ((R \in Ring \land M \in B) \land \forall n \in ℕ {coe}_{1} (M) (n) = \underset{˙}{0}) \to \forall n \in ℕ_{0} {coe}_{1} (M) (n) = {coe}_{1} (A ({coe}_{1} (M) (0))) (n)$
79		eqid	$⊢ {coe}_{1} (A ({coe}_{1} (M) (0))) = {coe}_{1} (A ({coe}_{1} (M) (0)))$
80	3 4 17 79	eqcoe1ply1eq	$⊢ (R \in Ring \land M \in B \land A ({coe}_{1} (M) (0)) \in B) \to (\forall n \in ℕ_{0} {coe}_{1} (M) (n) = {coe}_{1} (A ({coe}_{1} (M) (0))) (n) \to M = A ({coe}_{1} (M) (0)))$
81	41 78 80	sylc	$⊢ ((R \in Ring \land M \in B) \land \forall n \in ℕ {coe}_{1} (M) (n) = \underset{˙}{0}) \to M = A ({coe}_{1} (M) (0))$
82	20 23 81	rspcedvd	$⊢ ((R \in Ring \land M \in B) \land \forall n \in ℕ {coe}_{1} (M) (n) = \underset{˙}{0}) \to \exists s \in K M = A (s)$
83	82	ex	$⊢ (R \in Ring \land M \in B) \to (\forall n \in ℕ {coe}_{1} (M) (n) = \underset{˙}{0} \to \exists s \in K M = A (s))$
84	14 83	impbid	$⊢ (R \in Ring \land M \in B) \to (\exists s \in K M = A (s) \leftrightarrow \forall n \in ℕ {coe}_{1} (M) (n) = \underset{˙}{0})$

Metamath Proof Explorer

Theorem cply1coe0bi

Proof