opsrle

Description: An alternative expression for the set of polynomials, as the smallest subalgebra of the set of power series that contains all the variable generators. (Contributed by Mario Carneiro, 8-Feb-2015) (Revised by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	opsrle.s	$⊢ S = I mPwSer R$
	opsrle.o	$⊢ O = (I ordPwSer R) (T)$
	opsrle.b	$⊢ B = {Base}_{S}$
	opsrle.q	$⊢ \underset{˙}{<} = <_{R}$
	opsrle.c	$⊢ C = T <_{bag} I$
	opsrle.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
	opsrle.l	$⊢ \underset{˙}{\leq} = \leq_{O}$
	opsrle.t	$⊢ φ \to T \subseteq I \times I$
Assertion	opsrle	$⊢ φ \to \underset{˙}{\leq} = \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y))\}$

Proof

Step	Hyp	Ref	Expression
1		opsrle.s	$⊢ S = I mPwSer R$
2		opsrle.o	$⊢ O = (I ordPwSer R) (T)$
3		opsrle.b	$⊢ B = {Base}_{S}$
4		opsrle.q	$⊢ \underset{˙}{<} = <_{R}$
5		opsrle.c	$⊢ C = T <_{bag} I$
6		opsrle.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
7		opsrle.l	$⊢ \underset{˙}{\leq} = \leq_{O}$
8		opsrle.t	$⊢ φ \to T \subseteq I \times I$
9		eqid	$⊢ \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y))\} = \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y))\}$
10		simprl	$⊢ (φ \land (I \in V \land R \in V)) \to I \in V$
11		simprr	$⊢ (φ \land (I \in V \land R \in V)) \to R \in V$
12	8	adantr	$⊢ (φ \land (I \in V \land R \in V)) \to T \subseteq I \times I$
13	1 2 3 4 5 6 9 10 11 12	opsrval	$⊢ (φ \land (I \in V \land R \in V)) \to O = S sSet ⟨\leq_{ndx}, \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y))\}⟩$
14	13	fveq2d	$⊢ (φ \land (I \in V \land R \in V)) \to \leq_{O} = \leq_{(S sSet ⟨\leq_{ndx}, \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y))\}⟩)}$
15	1	ovexi	$⊢ S \in V$
16	3	fvexi	$⊢ B \in V$
17	16 16	xpex	$⊢ B \times B \in V$
18		vex	$⊢ x \in V$
19		vex	$⊢ y \in V$
20	18 19	prss	$⊢ (x \in B \land y \in B) \leftrightarrow \{x, y\} \subseteq B$
21	20	anbi1i	$⊢ ((x \in B \land y \in B) \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y)) \leftrightarrow (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y))$
22	21	opabbii	$⊢ \{⟨x, y⟩ \| ((x \in B \land y \in B) \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y))\} = \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y))\}$
23		opabssxp	$⊢ \{⟨x, y⟩ \| ((x \in B \land y \in B) \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y))\} \subseteq B \times B$
24	22 23	eqsstrri	$⊢ \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y))\} \subseteq B \times B$
25	17 24	ssexi	$⊢ \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y))\} \in V$
26		pleid	$⊢ le = Slot \leq_{ndx}$
27	26	setsid	$⊢ (S \in V \land \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y))\} \in V) \to \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y))\} = \leq_{(S sSet ⟨\leq_{ndx}, \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y))\}⟩)}$
28	15 25 27	mp2an	$⊢ \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y))\} = \leq_{(S sSet ⟨\leq_{ndx}, \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y))\}⟩)}$
29	14 7 28	3eqtr4g	$⊢ (φ \land (I \in V \land R \in V)) \to \underset{˙}{\leq} = \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y))\}$
30		reldmopsr	$⊢ Rel dom ordPwSer$
31	30	ovprc	$⊢ \neg (I \in V \land R \in V) \to I ordPwSer R = \emptyset$
32	31	adantl	$⊢ (φ \land \neg (I \in V \land R \in V)) \to I ordPwSer R = \emptyset$
33	32	fveq1d	$⊢ (φ \land \neg (I \in V \land R \in V)) \to (I ordPwSer R) (T) = \emptyset (T)$
34	2 33	syl5eq	$⊢ (φ \land \neg (I \in V \land R \in V)) \to O = \emptyset (T)$
35		0fv	$⊢ \emptyset (T) = \emptyset$
36	34 35	eqtrdi	$⊢ (φ \land \neg (I \in V \land R \in V)) \to O = \emptyset$
37	36	fveq2d	$⊢ (φ \land \neg (I \in V \land R \in V)) \to \leq_{O} = \leq_{\emptyset}$
38	26	str0	$⊢ \emptyset = \leq_{\emptyset}$
39	37 7 38	3eqtr4g	$⊢ (φ \land \neg (I \in V \land R \in V)) \to \underset{˙}{\leq} = \emptyset$
40		reldmpsr	$⊢ Rel dom mPwSer$
41	40	ovprc	$⊢ \neg (I \in V \land R \in V) \to I mPwSer R = \emptyset$
42	41	adantl	$⊢ (φ \land \neg (I \in V \land R \in V)) \to I mPwSer R = \emptyset$
43	1 42	syl5eq	$⊢ (φ \land \neg (I \in V \land R \in V)) \to S = \emptyset$
44	43	fveq2d	$⊢ (φ \land \neg (I \in V \land R \in V)) \to {Base}_{S} = {Base}_{\emptyset}$
45		base0	$⊢ \emptyset = {Base}_{\emptyset}$
46	44 3 45	3eqtr4g	$⊢ (φ \land \neg (I \in V \land R \in V)) \to B = \emptyset$
47	46	xpeq2d	$⊢ (φ \land \neg (I \in V \land R \in V)) \to B \times B = B \times \emptyset$
48		xp0	$⊢ B \times \emptyset = \emptyset$
49	47 48	eqtrdi	$⊢ (φ \land \neg (I \in V \land R \in V)) \to B \times B = \emptyset$
50		sseq0	$⊢ (\{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y))\} \subseteq B \times B \land B \times B = \emptyset) \to \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y))\} = \emptyset$
51	24 49 50	sylancr	$⊢ (φ \land \neg (I \in V \land R \in V)) \to \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y))\} = \emptyset$
52	39 51	eqtr4d	$⊢ (φ \land \neg (I \in V \land R \in V)) \to \underset{˙}{\leq} = \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y))\}$
53	29 52	pm2.61dan	$⊢ φ \to \underset{˙}{\leq} = \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land (\exists z \in D (x (z) \underset{˙}{<} y (z) \land \forall w \in D (w C z \to x (w) = y (w))) \lor x = y))\}$

Metamath Proof Explorer

Theorem opsrle

Proof