linply2cfv

Description: The evaluation of a linear polynomial over a subset of the complex numbers with explicit coefficients at a complex number. (Contributed by AV, 31-Oct-2026)

	Ref	Expression
Hypotheses	linplyfv.p	$⊢ P = (z \in ℂ ⟼ \sum_{k = 0}^{1} C (k) z^{k})$
	linplyfv2.c	$⊢ C = (x \in ℕ_{0} ⟼ if (x = 0, A, B))$
Assertion	linply2cfv	$⊢ (S \subseteq ℂ \land (A \in S \land B \in S) \land X \in ℂ) \to P (X) = A + B X$

Proof

Step	Hyp	Ref	Expression
1		linplyfv.p	$⊢ P = (z \in ℂ ⟼ \sum_{k = 0}^{1} C (k) z^{k})$
2		linplyfv2.c	$⊢ C = (x \in ℕ_{0} ⟼ if (x = 0, A, B))$
3		cnex	$⊢ ℂ \in V$
4	3	ssex	$⊢ S \subseteq ℂ \to S \in V$
5	4	3ad2ant1	$⊢ (S \subseteq ℂ \land (A \in S \land B \in S) \land X \in ℂ) \to S \in V$
6		nn0ex	$⊢ ℕ_{0} \in V$
7	6	a1i	$⊢ (S \subseteq ℂ \land (A \in S \land B \in S) \land X \in ℂ) \to ℕ_{0} \in V$
8		ifcl	$⊢ (A \in S \land B \in S) \to if (x = 0, A, B) \in S$
9	8	3ad2ant2	$⊢ (S \subseteq ℂ \land (A \in S \land B \in S) \land X \in ℂ) \to if (x = 0, A, B) \in S$
10	9	adantr	$⊢ ((S \subseteq ℂ \land (A \in S \land B \in S) \land X \in ℂ) \land x \in ℕ_{0}) \to if (x = 0, A, B) \in S$
11	10 2	fmptd	$⊢ (S \subseteq ℂ \land (A \in S \land B \in S) \land X \in ℂ) \to C : ℕ_{0} ⟶ S$
12	5 7 11	elmapdd	$⊢ (S \subseteq ℂ \land (A \in S \land B \in S) \land X \in ℂ) \to C \in (S^{ℕ_{0}})$
13	1	linplyfv	$⊢ (S \subseteq ℂ \land C \in (S^{ℕ_{0}}) \land X \in ℂ) \to P (X) = C (0) + C (1) X$
14	12 13	syld3an2	$⊢ (S \subseteq ℂ \land (A \in S \land B \in S) \land X \in ℂ) \to P (X) = C (0) + C (1) X$
15	2	a1i	$⊢ (S \subseteq ℂ \land (A \in S \land B \in S)) \to C = (x \in ℕ_{0} ⟼ if (x = 0, A, B))$
16		iftrue	$⊢ x = 0 \to if (x = 0, A, B) = A$
17	16	adantl	$⊢ ((S \subseteq ℂ \land (A \in S \land B \in S)) \land x = 0) \to if (x = 0, A, B) = A$
18		0nn0	$⊢ 0 \in ℕ_{0}$
19	18	a1i	$⊢ (S \subseteq ℂ \land (A \in S \land B \in S)) \to 0 \in ℕ_{0}$
20		simprl	$⊢ (S \subseteq ℂ \land (A \in S \land B \in S)) \to A \in S$
21	15 17 19 20	fvmptd	$⊢ (S \subseteq ℂ \land (A \in S \land B \in S)) \to C (0) = A$
22		ax-1ne0	$⊢ 1 \neq 0$
23	22	neii	$⊢ \neg 1 = 0$
24		eqeq1	$⊢ x = 1 \to (x = 0 \leftrightarrow 1 = 0)$
25	23 24	mtbiri	$⊢ x = 1 \to \neg x = 0$
26	25	adantl	$⊢ ((S \subseteq ℂ \land (A \in S \land B \in S)) \land x = 1) \to \neg x = 0$
27	26	iffalsed	$⊢ ((S \subseteq ℂ \land (A \in S \land B \in S)) \land x = 1) \to if (x = 0, A, B) = B$
28		1nn0	$⊢ 1 \in ℕ_{0}$
29	28	a1i	$⊢ (S \subseteq ℂ \land (A \in S \land B \in S)) \to 1 \in ℕ_{0}$
30		simprr	$⊢ (S \subseteq ℂ \land (A \in S \land B \in S)) \to B \in S$
31	15 27 29 30	fvmptd	$⊢ (S \subseteq ℂ \land (A \in S \land B \in S)) \to C (1) = B$
32	31	oveq1d	$⊢ (S \subseteq ℂ \land (A \in S \land B \in S)) \to C (1) X = B X$
33	21 32	oveq12d	$⊢ (S \subseteq ℂ \land (A \in S \land B \in S)) \to C (0) + C (1) X = A + B X$
34	33	3adant3	$⊢ (S \subseteq ℂ \land (A \in S \land B \in S) \land X \in ℂ) \to C (0) + C (1) X = A + B X$
35	14 34	eqtrd	$⊢ (S \subseteq ℂ \land (A \in S \land B \in S) \land X \in ℂ) \to P (X) = A + B X$

Metamath Proof Explorer

Theorem linply2cfv

Proof