rngunsnply

Description: Adjoining one element to a ring results in a set of polynomial evaluations. (Contributed by Stefan O'Rear, 30-Nov-2014)

	Ref	Expression
Hypotheses	rngunsnply.b	$⊢ φ \to B \in SubRing (ℂ_{fld})$
	rngunsnply.x	$⊢ φ \to X \in ℂ$
	rngunsnply.s	$⊢ φ \to S = RingSpan (ℂ_{fld}) (B \cup \{X\})$
Assertion	rngunsnply	$⊢ φ \to (V \in S \leftrightarrow \exists p \in Poly (B) V = p (X))$

Proof

Step	Hyp	Ref	Expression
1		rngunsnply.b	$⊢ φ \to B \in SubRing (ℂ_{fld})$
2		rngunsnply.x	$⊢ φ \to X \in ℂ$
3		rngunsnply.s	$⊢ φ \to S = RingSpan (ℂ_{fld}) (B \cup \{X\})$
4	3	eleq2d	$⊢ φ \to (V \in S \leftrightarrow V \in RingSpan (ℂ_{fld}) (B \cup \{X\}))$
5		cnring	$⊢ ℂ_{fld} \in Ring$
6	5	a1i	$⊢ φ \to ℂ_{fld} \in Ring$
7		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
8	7	a1i	$⊢ φ \to ℂ = {Base}_{ℂ_{fld}}$
9	7	subrgss	$⊢ B \in SubRing (ℂ_{fld}) \to B \subseteq ℂ$
10	1 9	syl	$⊢ φ \to B \subseteq ℂ$
11	2	snssd	$⊢ φ \to \{X\} \subseteq ℂ$
12	10 11	unssd	$⊢ φ \to B \cup \{X\} \subseteq ℂ$
13		eqidd	$⊢ φ \to RingSpan (ℂ_{fld}) = RingSpan (ℂ_{fld})$
14		eqidd	$⊢ φ \to RingSpan (ℂ_{fld}) (B \cup \{X\}) = RingSpan (ℂ_{fld}) (B \cup \{X\})$
15		eqidd	$⊢ φ \to ℂ_{fld} ↾_{𝑠} \{a \| \exists p \in Poly (B) a = p (X)\} = ℂ_{fld} ↾_{𝑠} \{a \| \exists p \in Poly (B) a = p (X)\}$
16		cnfld0	$⊢ 0 = 0_{ℂ_{fld}}$
17	16	a1i	$⊢ φ \to 0 = 0_{ℂ_{fld}}$
18		cnfldadd	$⊢ + = +_{ℂ_{fld}}$
19	18	a1i	$⊢ φ \to + = +_{ℂ_{fld}}$
20		plyf	$⊢ p \in Poly (B) \to p : ℂ ⟶ ℂ$
21		ffvelrn	$⊢ (p : ℂ ⟶ ℂ \land X \in ℂ) \to p (X) \in ℂ$
22	20 2 21	syl2anr	$⊢ (φ \land p \in Poly (B)) \to p (X) \in ℂ$
23		eleq1	$⊢ a = p (X) \to (a \in ℂ \leftrightarrow p (X) \in ℂ)$
24	22 23	syl5ibrcom	$⊢ (φ \land p \in Poly (B)) \to (a = p (X) \to a \in ℂ)$
25	24	rexlimdva	$⊢ φ \to (\exists p \in Poly (B) a = p (X) \to a \in ℂ)$
26	25	ss2abdv	$⊢ φ \to \{a \| \exists p \in Poly (B) a = p (X)\} \subseteq \{a \| a \in ℂ\}$
27		abid2	$⊢ \{a \| a \in ℂ\} = ℂ$
28	27 7	eqtri	$⊢ \{a \| a \in ℂ\} = {Base}_{ℂ_{fld}}$
29	26 28	sseqtrdi	$⊢ φ \to \{a \| \exists p \in Poly (B) a = p (X)\} \subseteq {Base}_{ℂ_{fld}}$
30		abid2	$⊢ \{a \| a \in B\} = B$
31		plyconst	$⊢ (B \subseteq ℂ \land a \in B) \to ℂ \times \{a\} \in Poly (B)$
32	10 31	sylan	$⊢ (φ \land a \in B) \to ℂ \times \{a\} \in Poly (B)$
33	2	adantr	$⊢ (φ \land a \in B) \to X \in ℂ$
34		vex	$⊢ a \in V$
35	34	fvconst2	$⊢ X \in ℂ \to (ℂ \times \{a\}) (X) = a$
36	33 35	syl	$⊢ (φ \land a \in B) \to (ℂ \times \{a\}) (X) = a$
37	36	eqcomd	$⊢ (φ \land a \in B) \to a = (ℂ \times \{a\}) (X)$
38		fveq1	$⊢ p = ℂ \times \{a\} \to p (X) = (ℂ \times \{a\}) (X)$
39	38	rspceeqv	$⊢ (ℂ \times \{a\} \in Poly (B) \land a = (ℂ \times \{a\}) (X)) \to \exists p \in Poly (B) a = p (X)$
40	32 37 39	syl2anc	$⊢ (φ \land a \in B) \to \exists p \in Poly (B) a = p (X)$
41	40	ex	$⊢ φ \to (a \in B \to \exists p \in Poly (B) a = p (X))$
42	41	ss2abdv	$⊢ φ \to \{a \| a \in B\} \subseteq \{a \| \exists p \in Poly (B) a = p (X)\}$
43	30 42	eqsstrrid	$⊢ φ \to B \subseteq \{a \| \exists p \in Poly (B) a = p (X)\}$
44		subrgsubg	$⊢ B \in SubRing (ℂ_{fld}) \to B \in SubGrp (ℂ_{fld})$
45	1 44	syl	$⊢ φ \to B \in SubGrp (ℂ_{fld})$
46	16	subg0cl	$⊢ B \in SubGrp (ℂ_{fld}) \to 0 \in B$
47	45 46	syl	$⊢ φ \to 0 \in B$
48	43 47	sseldd	$⊢ φ \to 0 \in \{a \| \exists p \in Poly (B) a = p (X)\}$
49		biid	$⊢ φ \leftrightarrow φ$
50		vex	$⊢ b \in V$
51		eqeq1	$⊢ a = b \to (a = p (X) \leftrightarrow b = p (X))$
52	51	rexbidv	$⊢ a = b \to (\exists p \in Poly (B) a = p (X) \leftrightarrow \exists p \in Poly (B) b = p (X))$
53		fveq1	$⊢ p = e \to p (X) = e (X)$
54	53	eqeq2d	$⊢ p = e \to (b = p (X) \leftrightarrow b = e (X))$
55	54	cbvrexvw	$⊢ \exists p \in Poly (B) b = p (X) \leftrightarrow \exists e \in Poly (B) b = e (X)$
56	52 55	bitrdi	$⊢ a = b \to (\exists p \in Poly (B) a = p (X) \leftrightarrow \exists e \in Poly (B) b = e (X))$
57	50 56	elab	$⊢ b \in \{a \| \exists p \in Poly (B) a = p (X)\} \leftrightarrow \exists e \in Poly (B) b = e (X)$
58		vex	$⊢ c \in V$
59		eqeq1	$⊢ a = c \to (a = p (X) \leftrightarrow c = p (X))$
60	59	rexbidv	$⊢ a = c \to (\exists p \in Poly (B) a = p (X) \leftrightarrow \exists p \in Poly (B) c = p (X))$
61		fveq1	$⊢ p = d \to p (X) = d (X)$
62	61	eqeq2d	$⊢ p = d \to (c = p (X) \leftrightarrow c = d (X))$
63	62	cbvrexvw	$⊢ \exists p \in Poly (B) c = p (X) \leftrightarrow \exists d \in Poly (B) c = d (X)$
64	60 63	bitrdi	$⊢ a = c \to (\exists p \in Poly (B) a = p (X) \leftrightarrow \exists d \in Poly (B) c = d (X))$
65	58 64	elab	$⊢ c \in \{a \| \exists p \in Poly (B) a = p (X)\} \leftrightarrow \exists d \in Poly (B) c = d (X)$
66		simplr	$⊢ ((φ \land e \in Poly (B)) \land d \in Poly (B)) \to e \in Poly (B)$
67		simpr	$⊢ ((φ \land e \in Poly (B)) \land d \in Poly (B)) \to d \in Poly (B)$
68	18	subrgacl	$⊢ (B \in SubRing (ℂ_{fld}) \land a \in B \land b \in B) \to a + b \in B$
69	68	3expb	$⊢ (B \in SubRing (ℂ_{fld}) \land (a \in B \land b \in B)) \to a + b \in B$
70	1 69	sylan	$⊢ (φ \land (a \in B \land b \in B)) \to a + b \in B$
71	70	adantlr	$⊢ ((φ \land e \in Poly (B)) \land (a \in B \land b \in B)) \to a + b \in B$
72	71	adantlr	$⊢ (((φ \land e \in Poly (B)) \land d \in Poly (B)) \land (a \in B \land b \in B)) \to a + b \in B$
73	66 67 72	plyadd	$⊢ ((φ \land e \in Poly (B)) \land d \in Poly (B)) \to e +_{f} d \in Poly (B)$
74		plyf	$⊢ e \in Poly (B) \to e : ℂ ⟶ ℂ$
75	74	ffnd	$⊢ e \in Poly (B) \to e Fn ℂ$
76	75	ad2antlr	$⊢ ((φ \land e \in Poly (B)) \land d \in Poly (B)) \to e Fn ℂ$
77		plyf	$⊢ d \in Poly (B) \to d : ℂ ⟶ ℂ$
78	77	ffnd	$⊢ d \in Poly (B) \to d Fn ℂ$
79	78	adantl	$⊢ ((φ \land e \in Poly (B)) \land d \in Poly (B)) \to d Fn ℂ$
80		cnex	$⊢ ℂ \in V$
81	80	a1i	$⊢ ((φ \land e \in Poly (B)) \land d \in Poly (B)) \to ℂ \in V$
82	2	ad2antrr	$⊢ ((φ \land e \in Poly (B)) \land d \in Poly (B)) \to X \in ℂ$
83		fnfvof	$⊢ ((e Fn ℂ \land d Fn ℂ) \land (ℂ \in V \land X \in ℂ)) \to (e +_{f} d) (X) = e (X) + d (X)$
84	76 79 81 82 83	syl22anc	$⊢ ((φ \land e \in Poly (B)) \land d \in Poly (B)) \to (e +_{f} d) (X) = e (X) + d (X)$
85	84	eqcomd	$⊢ ((φ \land e \in Poly (B)) \land d \in Poly (B)) \to e (X) + d (X) = (e +_{f} d) (X)$
86		fveq1	$⊢ p = e +_{f} d \to p (X) = (e +_{f} d) (X)$
87	86	rspceeqv	$⊢ (e +_{f} d \in Poly (B) \land e (X) + d (X) = (e +_{f} d) (X)) \to \exists p \in Poly (B) e (X) + d (X) = p (X)$
88	73 85 87	syl2anc	$⊢ ((φ \land e \in Poly (B)) \land d \in Poly (B)) \to \exists p \in Poly (B) e (X) + d (X) = p (X)$
89		oveq2	$⊢ c = d (X) \to e (X) + c = e (X) + d (X)$
90	89	eqeq1d	$⊢ c = d (X) \to (e (X) + c = p (X) \leftrightarrow e (X) + d (X) = p (X))$
91	90	rexbidv	$⊢ c = d (X) \to (\exists p \in Poly (B) e (X) + c = p (X) \leftrightarrow \exists p \in Poly (B) e (X) + d (X) = p (X))$
92	88 91	syl5ibrcom	$⊢ ((φ \land e \in Poly (B)) \land d \in Poly (B)) \to (c = d (X) \to \exists p \in Poly (B) e (X) + c = p (X))$
93	92	rexlimdva	$⊢ (φ \land e \in Poly (B)) \to (\exists d \in Poly (B) c = d (X) \to \exists p \in Poly (B) e (X) + c = p (X))$
94		oveq1	$⊢ b = e (X) \to b + c = e (X) + c$
95	94	eqeq1d	$⊢ b = e (X) \to (b + c = p (X) \leftrightarrow e (X) + c = p (X))$
96	95	rexbidv	$⊢ b = e (X) \to (\exists p \in Poly (B) b + c = p (X) \leftrightarrow \exists p \in Poly (B) e (X) + c = p (X))$
97	96	imbi2d	$⊢ b = e (X) \to ((\exists d \in Poly (B) c = d (X) \to \exists p \in Poly (B) b + c = p (X)) \leftrightarrow (\exists d \in Poly (B) c = d (X) \to \exists p \in Poly (B) e (X) + c = p (X)))$
98	93 97	syl5ibrcom	$⊢ (φ \land e \in Poly (B)) \to (b = e (X) \to (\exists d \in Poly (B) c = d (X) \to \exists p \in Poly (B) b + c = p (X)))$
99	98	rexlimdva	$⊢ φ \to (\exists e \in Poly (B) b = e (X) \to (\exists d \in Poly (B) c = d (X) \to \exists p \in Poly (B) b + c = p (X)))$
100	99	3imp	$⊢ (φ \land \exists e \in Poly (B) b = e (X) \land \exists d \in Poly (B) c = d (X)) \to \exists p \in Poly (B) b + c = p (X)$
101	49 57 65 100	syl3anb	$⊢ (φ \land b \in \{a \| \exists p \in Poly (B) a = p (X)\} \land c \in \{a \| \exists p \in Poly (B) a = p (X)\}) \to \exists p \in Poly (B) b + c = p (X)$
102		ovex	$⊢ b + c \in V$
103		eqeq1	$⊢ a = b + c \to (a = p (X) \leftrightarrow b + c = p (X))$
104	103	rexbidv	$⊢ a = b + c \to (\exists p \in Poly (B) a = p (X) \leftrightarrow \exists p \in Poly (B) b + c = p (X))$
105	102 104	elab	$⊢ b + c \in \{a \| \exists p \in Poly (B) a = p (X)\} \leftrightarrow \exists p \in Poly (B) b + c = p (X)$
106	101 105	sylibr	$⊢ (φ \land b \in \{a \| \exists p \in Poly (B) a = p (X)\} \land c \in \{a \| \exists p \in Poly (B) a = p (X)\}) \to b + c \in \{a \| \exists p \in Poly (B) a = p (X)\}$
107		ax-1cn	$⊢ 1 \in ℂ$
108		cnfldneg	$⊢ 1 \in ℂ \to {inv}_{g} (ℂ_{fld}) (1) = - 1$
109	107 108	mp1i	$⊢ φ \to {inv}_{g} (ℂ_{fld}) (1) = - 1$
110		cnfld1	$⊢ 1 = 1_{ℂ_{fld}}$
111	110	subrg1cl	$⊢ B \in SubRing (ℂ_{fld}) \to 1 \in B$
112	1 111	syl	$⊢ φ \to 1 \in B$
113		eqid	$⊢ {inv}_{g} (ℂ_{fld}) = {inv}_{g} (ℂ_{fld})$
114	113	subginvcl	$⊢ (B \in SubGrp (ℂ_{fld}) \land 1 \in B) \to {inv}_{g} (ℂ_{fld}) (1) \in B$
115	45 112 114	syl2anc	$⊢ φ \to {inv}_{g} (ℂ_{fld}) (1) \in B$
116	109 115	eqeltrrd	$⊢ φ \to - 1 \in B$
117		plyconst	$⊢ (B \subseteq ℂ \land - 1 \in B) \to ℂ \times \{- 1\} \in Poly (B)$
118	10 116 117	syl2anc	$⊢ φ \to ℂ \times \{- 1\} \in Poly (B)$
119	118	adantr	$⊢ (φ \land e \in Poly (B)) \to ℂ \times \{- 1\} \in Poly (B)$
120		simpr	$⊢ (φ \land e \in Poly (B)) \to e \in Poly (B)$
121		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
122	121	subrgmcl	$⊢ (B \in SubRing (ℂ_{fld}) \land a \in B \land b \in B) \to a b \in B$
123	122	3expb	$⊢ (B \in SubRing (ℂ_{fld}) \land (a \in B \land b \in B)) \to a b \in B$
124	1 123	sylan	$⊢ (φ \land (a \in B \land b \in B)) \to a b \in B$
125	124	adantlr	$⊢ ((φ \land e \in Poly (B)) \land (a \in B \land b \in B)) \to a b \in B$
126	119 120 71 125	plymul	$⊢ (φ \land e \in Poly (B)) \to (ℂ \times \{- 1\}) \times_{f} e \in Poly (B)$
127		ffvelrn	$⊢ (e : ℂ ⟶ ℂ \land X \in ℂ) \to e (X) \in ℂ$
128	74 2 127	syl2anr	$⊢ (φ \land e \in Poly (B)) \to e (X) \in ℂ$
129		cnfldneg	$⊢ e (X) \in ℂ \to {inv}_{g} (ℂ_{fld}) (e (X)) = - e (X)$
130	128 129	syl	$⊢ (φ \land e \in Poly (B)) \to {inv}_{g} (ℂ_{fld}) (e (X)) = - e (X)$
131		negex	$⊢ - 1 \in V$
132		fnconstg	$⊢ - 1 \in V \to (ℂ \times \{- 1\}) Fn ℂ$
133	131 132	mp1i	$⊢ (φ \land e \in Poly (B)) \to (ℂ \times \{- 1\}) Fn ℂ$
134	75	adantl	$⊢ (φ \land e \in Poly (B)) \to e Fn ℂ$
135	80	a1i	$⊢ (φ \land e \in Poly (B)) \to ℂ \in V$
136	2	adantr	$⊢ (φ \land e \in Poly (B)) \to X \in ℂ$
137		fnfvof	$⊢ (((ℂ \times \{- 1\}) Fn ℂ \land e Fn ℂ) \land (ℂ \in V \land X \in ℂ)) \to ((ℂ \times \{- 1\}) \times_{f} e) (X) = (ℂ \times \{- 1\}) (X) e (X)$
138	133 134 135 136 137	syl22anc	$⊢ (φ \land e \in Poly (B)) \to ((ℂ \times \{- 1\}) \times_{f} e) (X) = (ℂ \times \{- 1\}) (X) e (X)$
139	131	fvconst2	$⊢ X \in ℂ \to (ℂ \times \{- 1\}) (X) = - 1$
140	136 139	syl	$⊢ (φ \land e \in Poly (B)) \to (ℂ \times \{- 1\}) (X) = - 1$
141	140	oveq1d	$⊢ (φ \land e \in Poly (B)) \to (ℂ \times \{- 1\}) (X) e (X) = -1 e (X)$
142	128	mulm1d	$⊢ (φ \land e \in Poly (B)) \to -1 e (X) = - e (X)$
143	138 141 142	3eqtrd	$⊢ (φ \land e \in Poly (B)) \to ((ℂ \times \{- 1\}) \times_{f} e) (X) = - e (X)$
144	130 143	eqtr4d	$⊢ (φ \land e \in Poly (B)) \to {inv}_{g} (ℂ_{fld}) (e (X)) = ((ℂ \times \{- 1\}) \times_{f} e) (X)$
145		fveq1	$⊢ p = (ℂ \times \{- 1\}) \times_{f} e \to p (X) = ((ℂ \times \{- 1\}) \times_{f} e) (X)$
146	145	rspceeqv	$⊢ ((ℂ \times \{- 1\}) \times_{f} e \in Poly (B) \land {inv}_{g} (ℂ_{fld}) (e (X)) = ((ℂ \times \{- 1\}) \times_{f} e) (X)) \to \exists p \in Poly (B) {inv}_{g} (ℂ_{fld}) (e (X)) = p (X)$
147	126 144 146	syl2anc	$⊢ (φ \land e \in Poly (B)) \to \exists p \in Poly (B) {inv}_{g} (ℂ_{fld}) (e (X)) = p (X)$
148		fveqeq2	$⊢ b = e (X) \to ({inv}_{g} (ℂ_{fld}) (b) = p (X) \leftrightarrow {inv}_{g} (ℂ_{fld}) (e (X)) = p (X))$
149	148	rexbidv	$⊢ b = e (X) \to (\exists p \in Poly (B) {inv}_{g} (ℂ_{fld}) (b) = p (X) \leftrightarrow \exists p \in Poly (B) {inv}_{g} (ℂ_{fld}) (e (X)) = p (X))$
150	147 149	syl5ibrcom	$⊢ (φ \land e \in Poly (B)) \to (b = e (X) \to \exists p \in Poly (B) {inv}_{g} (ℂ_{fld}) (b) = p (X))$
151	150	rexlimdva	$⊢ φ \to (\exists e \in Poly (B) b = e (X) \to \exists p \in Poly (B) {inv}_{g} (ℂ_{fld}) (b) = p (X))$
152	151	imp	$⊢ (φ \land \exists e \in Poly (B) b = e (X)) \to \exists p \in Poly (B) {inv}_{g} (ℂ_{fld}) (b) = p (X)$
153	57 152	sylan2b	$⊢ (φ \land b \in \{a \| \exists p \in Poly (B) a = p (X)\}) \to \exists p \in Poly (B) {inv}_{g} (ℂ_{fld}) (b) = p (X)$
154		fvex	$⊢ {inv}_{g} (ℂ_{fld}) (b) \in V$
155		eqeq1	$⊢ a = {inv}_{g} (ℂ_{fld}) (b) \to (a = p (X) \leftrightarrow {inv}_{g} (ℂ_{fld}) (b) = p (X))$
156	155	rexbidv	$⊢ a = {inv}_{g} (ℂ_{fld}) (b) \to (\exists p \in Poly (B) a = p (X) \leftrightarrow \exists p \in Poly (B) {inv}_{g} (ℂ_{fld}) (b) = p (X))$
157	154 156	elab	$⊢ {inv}_{g} (ℂ_{fld}) (b) \in \{a \| \exists p \in Poly (B) a = p (X)\} \leftrightarrow \exists p \in Poly (B) {inv}_{g} (ℂ_{fld}) (b) = p (X)$
158	153 157	sylibr	$⊢ (φ \land b \in \{a \| \exists p \in Poly (B) a = p (X)\}) \to {inv}_{g} (ℂ_{fld}) (b) \in \{a \| \exists p \in Poly (B) a = p (X)\}$
159	110	a1i	$⊢ φ \to 1 = 1_{ℂ_{fld}}$
160	121	a1i	$⊢ φ \to \times = \cdot_{ℂ_{fld}}$
161	43 112	sseldd	$⊢ φ \to 1 \in \{a \| \exists p \in Poly (B) a = p (X)\}$
162	125	adantlr	$⊢ (((φ \land e \in Poly (B)) \land d \in Poly (B)) \land (a \in B \land b \in B)) \to a b \in B$
163	66 67 72 162	plymul	$⊢ ((φ \land e \in Poly (B)) \land d \in Poly (B)) \to e \times_{f} d \in Poly (B)$
164		fnfvof	$⊢ ((e Fn ℂ \land d Fn ℂ) \land (ℂ \in V \land X \in ℂ)) \to (e \times_{f} d) (X) = e (X) d (X)$
165	76 79 81 82 164	syl22anc	$⊢ ((φ \land e \in Poly (B)) \land d \in Poly (B)) \to (e \times_{f} d) (X) = e (X) d (X)$
166	165	eqcomd	$⊢ ((φ \land e \in Poly (B)) \land d \in Poly (B)) \to e (X) d (X) = (e \times_{f} d) (X)$
167		fveq1	$⊢ p = e \times_{f} d \to p (X) = (e \times_{f} d) (X)$
168	167	rspceeqv	$⊢ (e \times_{f} d \in Poly (B) \land e (X) d (X) = (e \times_{f} d) (X)) \to \exists p \in Poly (B) e (X) d (X) = p (X)$
169	163 166 168	syl2anc	$⊢ ((φ \land e \in Poly (B)) \land d \in Poly (B)) \to \exists p \in Poly (B) e (X) d (X) = p (X)$
170		oveq2	$⊢ c = d (X) \to e (X) c = e (X) d (X)$
171	170	eqeq1d	$⊢ c = d (X) \to (e (X) c = p (X) \leftrightarrow e (X) d (X) = p (X))$
172	171	rexbidv	$⊢ c = d (X) \to (\exists p \in Poly (B) e (X) c = p (X) \leftrightarrow \exists p \in Poly (B) e (X) d (X) = p (X))$
173	169 172	syl5ibrcom	$⊢ ((φ \land e \in Poly (B)) \land d \in Poly (B)) \to (c = d (X) \to \exists p \in Poly (B) e (X) c = p (X))$
174	173	rexlimdva	$⊢ (φ \land e \in Poly (B)) \to (\exists d \in Poly (B) c = d (X) \to \exists p \in Poly (B) e (X) c = p (X))$
175		oveq1	$⊢ b = e (X) \to b c = e (X) c$
176	175	eqeq1d	$⊢ b = e (X) \to (b c = p (X) \leftrightarrow e (X) c = p (X))$
177	176	rexbidv	$⊢ b = e (X) \to (\exists p \in Poly (B) b c = p (X) \leftrightarrow \exists p \in Poly (B) e (X) c = p (X))$
178	177	imbi2d	$⊢ b = e (X) \to ((\exists d \in Poly (B) c = d (X) \to \exists p \in Poly (B) b c = p (X)) \leftrightarrow (\exists d \in Poly (B) c = d (X) \to \exists p \in Poly (B) e (X) c = p (X)))$
179	174 178	syl5ibrcom	$⊢ (φ \land e \in Poly (B)) \to (b = e (X) \to (\exists d \in Poly (B) c = d (X) \to \exists p \in Poly (B) b c = p (X)))$
180	179	rexlimdva	$⊢ φ \to (\exists e \in Poly (B) b = e (X) \to (\exists d \in Poly (B) c = d (X) \to \exists p \in Poly (B) b c = p (X)))$
181	180	3imp	$⊢ (φ \land \exists e \in Poly (B) b = e (X) \land \exists d \in Poly (B) c = d (X)) \to \exists p \in Poly (B) b c = p (X)$
182	49 57 65 181	syl3anb	$⊢ (φ \land b \in \{a \| \exists p \in Poly (B) a = p (X)\} \land c \in \{a \| \exists p \in Poly (B) a = p (X)\}) \to \exists p \in Poly (B) b c = p (X)$
183		ovex	$⊢ b c \in V$
184		eqeq1	$⊢ a = b c \to (a = p (X) \leftrightarrow b c = p (X))$
185	184	rexbidv	$⊢ a = b c \to (\exists p \in Poly (B) a = p (X) \leftrightarrow \exists p \in Poly (B) b c = p (X))$
186	183 185	elab	$⊢ b c \in \{a \| \exists p \in Poly (B) a = p (X)\} \leftrightarrow \exists p \in Poly (B) b c = p (X)$
187	182 186	sylibr	$⊢ (φ \land b \in \{a \| \exists p \in Poly (B) a = p (X)\} \land c \in \{a \| \exists p \in Poly (B) a = p (X)\}) \to b c \in \{a \| \exists p \in Poly (B) a = p (X)\}$
188	15 17 19 29 48 106 158 159 160 161 187 6	issubrngd2	$⊢ φ \to \{a \| \exists p \in Poly (B) a = p (X)\} \in SubRing (ℂ_{fld})$
189		plyid	$⊢ (B \subseteq ℂ \land 1 \in B) \to X^{p} \in Poly (B)$
190	10 112 189	syl2anc	$⊢ φ \to X^{p} \in Poly (B)$
191		df-idp	$⊢ X^{p} = {I ↾}_{ℂ}$
192	191	fveq1i	$⊢ X^{p} (X) = ({I ↾}_{ℂ}) (X)$
193		fvresi	$⊢ X \in ℂ \to ({I ↾}_{ℂ}) (X) = X$
194	2 193	syl	$⊢ φ \to ({I ↾}_{ℂ}) (X) = X$
195	192 194	eqtr2id	$⊢ φ \to X = X^{p} (X)$
196		fveq1	$⊢ p = X^{p} \to p (X) = X^{p} (X)$
197	196	rspceeqv	$⊢ (X^{p} \in Poly (B) \land X = X^{p} (X)) \to \exists p \in Poly (B) X = p (X)$
198	190 195 197	syl2anc	$⊢ φ \to \exists p \in Poly (B) X = p (X)$
199		eqeq1	$⊢ a = X \to (a = p (X) \leftrightarrow X = p (X))$
200	199	rexbidv	$⊢ a = X \to (\exists p \in Poly (B) a = p (X) \leftrightarrow \exists p \in Poly (B) X = p (X))$
201	2 198 200	elabd	$⊢ φ \to X \in \{a \| \exists p \in Poly (B) a = p (X)\}$
202	201	snssd	$⊢ φ \to \{X\} \subseteq \{a \| \exists p \in Poly (B) a = p (X)\}$
203	43 202	unssd	$⊢ φ \to B \cup \{X\} \subseteq \{a \| \exists p \in Poly (B) a = p (X)\}$
204	6 8 12 13 14 188 203	rgspnmin	$⊢ φ \to RingSpan (ℂ_{fld}) (B \cup \{X\}) \subseteq \{a \| \exists p \in Poly (B) a = p (X)\}$
205	204	sseld	$⊢ φ \to (V \in RingSpan (ℂ_{fld}) (B \cup \{X\}) \to V \in \{a \| \exists p \in Poly (B) a = p (X)\})$
206		fvex	$⊢ p (X) \in V$
207		eleq1	$⊢ V = p (X) \to (V \in V \leftrightarrow p (X) \in V)$
208	206 207	mpbiri	$⊢ V = p (X) \to V \in V$
209	208	rexlimivw	$⊢ \exists p \in Poly (B) V = p (X) \to V \in V$
210		eqeq1	$⊢ a = V \to (a = p (X) \leftrightarrow V = p (X))$
211	210	rexbidv	$⊢ a = V \to (\exists p \in Poly (B) a = p (X) \leftrightarrow \exists p \in Poly (B) V = p (X))$
212	209 211	elab3	$⊢ V \in \{a \| \exists p \in Poly (B) a = p (X)\} \leftrightarrow \exists p \in Poly (B) V = p (X)$
213	205 212	syl6ib	$⊢ φ \to (V \in RingSpan (ℂ_{fld}) (B \cup \{X\}) \to \exists p \in Poly (B) V = p (X))$
214	6 8 12 13 14	rgspncl	$⊢ φ \to RingSpan (ℂ_{fld}) (B \cup \{X\}) \in SubRing (ℂ_{fld})$
215	214	adantr	$⊢ (φ \land p \in Poly (B)) \to RingSpan (ℂ_{fld}) (B \cup \{X\}) \in SubRing (ℂ_{fld})$
216		simpr	$⊢ (φ \land p \in Poly (B)) \to p \in Poly (B)$
217	6 8 12 13 14	rgspnssid	$⊢ φ \to B \cup \{X\} \subseteq RingSpan (ℂ_{fld}) (B \cup \{X\})$
218	217	unssbd	$⊢ φ \to \{X\} \subseteq RingSpan (ℂ_{fld}) (B \cup \{X\})$
219		snidg	$⊢ X \in ℂ \to X \in \{X\}$
220	2 219	syl	$⊢ φ \to X \in \{X\}$
221	218 220	sseldd	$⊢ φ \to X \in RingSpan (ℂ_{fld}) (B \cup \{X\})$
222	221	adantr	$⊢ (φ \land p \in Poly (B)) \to X \in RingSpan (ℂ_{fld}) (B \cup \{X\})$
223	217	unssad	$⊢ φ \to B \subseteq RingSpan (ℂ_{fld}) (B \cup \{X\})$
224	223	adantr	$⊢ (φ \land p \in Poly (B)) \to B \subseteq RingSpan (ℂ_{fld}) (B \cup \{X\})$
225	215 216 222 224	cnsrplycl	$⊢ (φ \land p \in Poly (B)) \to p (X) \in RingSpan (ℂ_{fld}) (B \cup \{X\})$
226		eleq1	$⊢ V = p (X) \to (V \in RingSpan (ℂ_{fld}) (B \cup \{X\}) \leftrightarrow p (X) \in RingSpan (ℂ_{fld}) (B \cup \{X\}))$
227	225 226	syl5ibrcom	$⊢ (φ \land p \in Poly (B)) \to (V = p (X) \to V \in RingSpan (ℂ_{fld}) (B \cup \{X\}))$
228	227	rexlimdva	$⊢ φ \to (\exists p \in Poly (B) V = p (X) \to V \in RingSpan (ℂ_{fld}) (B \cup \{X\}))$
229	213 228	impbid	$⊢ φ \to (V \in RingSpan (ℂ_{fld}) (B \cup \{X\}) \leftrightarrow \exists p \in Poly (B) V = p (X))$
230	4 229	bitrd	$⊢ φ \to (V \in S \leftrightarrow \exists p \in Poly (B) V = p (X))$

Metamath Proof Explorer

Theorem rngunsnply

Proof