evls1fldgencl

Description: Closure of the subring polynomial evaluation in the field extention. (Contributed by Thierry Arnoux, 2-Apr-2025)

	Ref	Expression
Hypotheses	evls1fldgencl.1	$⊢ B = {Base}_{E}$
	evls1fldgencl.2	$⊢ O = E {evalSub}_{1} F$
	evls1fldgencl.3	$⊢ P = {Poly}_{1} (E ↾_{𝑠} F)$
	evls1fldgencl.4	$⊢ U = {Base}_{P}$
	evls1fldgencl.5	$⊢ φ \to E \in Field$
	evls1fldgencl.6	$⊢ φ \to F \in SubDRing (E)$
	evls1fldgencl.7	$⊢ φ \to A \in B$
	evls1fldgencl.8	$⊢ φ \to G \in U$
Assertion	evls1fldgencl	$⊢ φ \to O (G) (A) \in (E fldGen (F \cup \{A\}))$

Proof

Step	Hyp	Ref	Expression
1		evls1fldgencl.1	$⊢ B = {Base}_{E}$
2		evls1fldgencl.2	$⊢ O = E {evalSub}_{1} F$
3		evls1fldgencl.3	$⊢ P = {Poly}_{1} (E ↾_{𝑠} F)$
4		evls1fldgencl.4	$⊢ U = {Base}_{P}$
5		evls1fldgencl.5	$⊢ φ \to E \in Field$
6		evls1fldgencl.6	$⊢ φ \to F \in SubDRing (E)$
7		evls1fldgencl.7	$⊢ φ \to A \in B$
8		evls1fldgencl.8	$⊢ φ \to G \in U$
9		eqid	$⊢ E ↾_{𝑠} F = E ↾_{𝑠} F$
10	5	fldcrngd	$⊢ φ \to E \in CRing$
11		sdrgsubrg	$⊢ F \in SubDRing (E) \to F \in SubRing (E)$
12	6 11	syl	$⊢ φ \to F \in SubRing (E)$
13		eqid	$⊢ \cdot_{E} = \cdot_{E}$
14		eqid	$⊢ \cdot_{{mulGrp}_{E}} = \cdot_{{mulGrp}_{E}}$
15		eqid	$⊢ {coe}_{1} (G) = {coe}_{1} (G)$
16	2 1 3 9 4 10 12 8 13 14 15	evls1fpws	$⊢ φ \to O (G) = (x \in B ⟼ \underset{k \in ℕ_{0}}{\sum_{E}} ({coe}_{1} (G) (k) \cdot_{E} (k \cdot_{{mulGrp}_{E}} x)))$
17		oveq2	$⊢ x = A \to k \cdot_{{mulGrp}_{E}} x = k \cdot_{{mulGrp}_{E}} A$
18	17	oveq2d	$⊢ x = A \to {coe}_{1} (G) (k) \cdot_{E} (k \cdot_{{mulGrp}_{E}} x) = {coe}_{1} (G) (k) \cdot_{E} (k \cdot_{{mulGrp}_{E}} A)$
19	18	mpteq2dv	$⊢ x = A \to (k \in ℕ_{0} ⟼ {coe}_{1} (G) (k) \cdot_{E} (k \cdot_{{mulGrp}_{E}} x)) = (k \in ℕ_{0} ⟼ {coe}_{1} (G) (k) \cdot_{E} (k \cdot_{{mulGrp}_{E}} A))$
20	19	oveq2d	$⊢ x = A \to \underset{k \in ℕ_{0}}{\sum_{E}} ({coe}_{1} (G) (k) \cdot_{E} (k \cdot_{{mulGrp}_{E}} x)) = \underset{k \in ℕ_{0}}{\sum_{E}} ({coe}_{1} (G) (k) \cdot_{E} (k \cdot_{{mulGrp}_{E}} A))$
21	20	adantl	$⊢ (φ \land x = A) \to \underset{k \in ℕ_{0}}{\sum_{E}} ({coe}_{1} (G) (k) \cdot_{E} (k \cdot_{{mulGrp}_{E}} x)) = \underset{k \in ℕ_{0}}{\sum_{E}} ({coe}_{1} (G) (k) \cdot_{E} (k \cdot_{{mulGrp}_{E}} A))$
22		ovexd	$⊢ φ \to \underset{k \in ℕ_{0}}{\sum_{E}} ({coe}_{1} (G) (k) \cdot_{E} (k \cdot_{{mulGrp}_{E}} A)) \in V$
23	16 21 7 22	fvmptd	$⊢ φ \to O (G) (A) = \underset{k \in ℕ_{0}}{\sum_{E}} ({coe}_{1} (G) (k) \cdot_{E} (k \cdot_{{mulGrp}_{E}} A))$
24	23	ad2antrr	$⊢ ((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \to O (G) (A) = \underset{k \in ℕ_{0}}{\sum_{E}} ({coe}_{1} (G) (k) \cdot_{E} (k \cdot_{{mulGrp}_{E}} A))$
25		eqid	$⊢ 0_{E} = 0_{E}$
26	10	crngringd	$⊢ φ \to E \in Ring$
27	26	ringabld	$⊢ φ \to E \in Abel$
28	27	ad2antrr	$⊢ ((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \to E \in Abel$
29		nn0ex	$⊢ ℕ_{0} \in V$
30	29	a1i	$⊢ ((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \to ℕ_{0} \in V$
31		simplr	$⊢ ((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \to a \in SubDRing (E)$
32		sdrgsubrg	$⊢ a \in SubDRing (E) \to a \in SubRing (E)$
33		subrgsubg	$⊢ a \in SubRing (E) \to a \in SubGrp (E)$
34	31 32 33	3syl	$⊢ ((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \to a \in SubGrp (E)$
35	32	ad3antlr	$⊢ (((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \land k \in ℕ_{0}) \to a \in SubRing (E)$
36		simplr	$⊢ (((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \land k \in ℕ_{0}) \to F \cup \{A\} \subseteq a$
37	36	unssad	$⊢ (((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \land k \in ℕ_{0}) \to F \subseteq a$
38	8	ad3antrrr	$⊢ (((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \land k \in ℕ_{0}) \to G \in U$
39		simpr	$⊢ (((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
40		eqid	$⊢ {Base}_{(E ↾_{𝑠} F)} = {Base}_{(E ↾_{𝑠} F)}$
41	15 4 3 40	coe1fvalcl	$⊢ (G \in U \land k \in ℕ_{0}) \to {coe}_{1} (G) (k) \in {Base}_{(E ↾_{𝑠} F)}$
42	38 39 41	syl2anc	$⊢ (((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \land k \in ℕ_{0}) \to {coe}_{1} (G) (k) \in {Base}_{(E ↾_{𝑠} F)}$
43	1	sdrgss	$⊢ F \in SubDRing (E) \to F \subseteq B$
44	6 43	syl	$⊢ φ \to F \subseteq B$
45	9 1	ressbas2	$⊢ F \subseteq B \to F = {Base}_{(E ↾_{𝑠} F)}$
46	44 45	syl	$⊢ φ \to F = {Base}_{(E ↾_{𝑠} F)}$
47	46	ad3antrrr	$⊢ (((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \land k \in ℕ_{0}) \to F = {Base}_{(E ↾_{𝑠} F)}$
48	42 47	eleqtrrd	$⊢ (((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \land k \in ℕ_{0}) \to {coe}_{1} (G) (k) \in F$
49	37 48	sseldd	$⊢ (((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \land k \in ℕ_{0}) \to {coe}_{1} (G) (k) \in a$
50		simpllr	$⊢ (((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \land k \in ℕ_{0}) \to a \in SubDRing (E)$
51	7	ad3antrrr	$⊢ (((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \land k \in ℕ_{0}) \to A \in B$
52	36	unssbd	$⊢ (((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \land k \in ℕ_{0}) \to \{A\} \subseteq a$
53		snssg	$⊢ A \in B \to (A \in a \leftrightarrow \{A\} \subseteq a)$
54	53	biimpar	$⊢ (A \in B \land \{A\} \subseteq a) \to A \in a$
55	51 52 54	syl2anc	$⊢ (((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \land k \in ℕ_{0}) \to A \in a$
56		eqid	$⊢ {mulGrp}_{E} = {mulGrp}_{E}$
57	56 1	mgpbas	$⊢ B = {Base}_{{mulGrp}_{E}}$
58	56 13	mgpplusg	$⊢ \cdot_{E} = +_{{mulGrp}_{E}}$
59		fvexd	$⊢ a \in SubDRing (E) \to {mulGrp}_{E} \in V$
60	1	sdrgss	$⊢ a \in SubDRing (E) \to a \subseteq B$
61	13	subrgmcl	$⊢ (a \in SubRing (E) \land x \in a \land y \in a) \to x \cdot_{E} y \in a$
62	32 61	syl3an1	$⊢ (a \in SubDRing (E) \land x \in a \land y \in a) \to x \cdot_{E} y \in a$
63		eqid	$⊢ 0_{{mulGrp}_{E}} = 0_{{mulGrp}_{E}}$
64		eqid	$⊢ 1_{E} = 1_{E}$
65	56 64	ringidval	$⊢ 1_{E} = 0_{{mulGrp}_{E}}$
66	65	eqcomi	$⊢ 0_{{mulGrp}_{E}} = 1_{E}$
67	66	subrg1cl	$⊢ a \in SubRing (E) \to 0_{{mulGrp}_{E}} \in a$
68	32 67	syl	$⊢ a \in SubDRing (E) \to 0_{{mulGrp}_{E}} \in a$
69	57 14 58 59 60 62 63 68	mulgnn0subcl	$⊢ (a \in SubDRing (E) \land k \in ℕ_{0} \land A \in a) \to k \cdot_{{mulGrp}_{E}} A \in a$
70	50 39 55 69	syl3anc	$⊢ (((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \land k \in ℕ_{0}) \to k \cdot_{{mulGrp}_{E}} A \in a$
71	13	subrgmcl	$⊢ (a \in SubRing (E) \land {coe}_{1} (G) (k) \in a \land k \cdot_{{mulGrp}_{E}} A \in a) \to {coe}_{1} (G) (k) \cdot_{E} (k \cdot_{{mulGrp}_{E}} A) \in a$
72	35 49 70 71	syl3anc	$⊢ (((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \land k \in ℕ_{0}) \to {coe}_{1} (G) (k) \cdot_{E} (k \cdot_{{mulGrp}_{E}} A) \in a$
73	72	fmpttd	$⊢ ((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \to (k \in ℕ_{0} ⟼ {coe}_{1} (G) (k) \cdot_{E} (k \cdot_{{mulGrp}_{E}} A)) : ℕ_{0} ⟶ a$
74	30	mptexd	$⊢ ((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \to (k \in ℕ_{0} ⟼ {coe}_{1} (G) (k) \cdot_{E} (k \cdot_{{mulGrp}_{E}} A)) \in V$
75	73	ffund	$⊢ ((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \to Fun (k \in ℕ_{0} ⟼ {coe}_{1} (G) (k) \cdot_{E} (k \cdot_{{mulGrp}_{E}} A))$
76		fvexd	$⊢ ((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \to 0_{E} \in V$
77	9	subrgring	$⊢ F \in SubRing (E) \to E ↾_{𝑠} F \in Ring$
78	12 77	syl	$⊢ φ \to E ↾_{𝑠} F \in Ring$
79	78	ad2antrr	$⊢ ((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \to E ↾_{𝑠} F \in Ring$
80	8	ad2antrr	$⊢ ((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \to G \in U$
81		eqid	$⊢ 0_{(E ↾_{𝑠} F)} = 0_{(E ↾_{𝑠} F)}$
82	3 4 81	mptcoe1fsupp	$⊢ (E ↾_{𝑠} F \in Ring \land G \in U) \to {finSupp}_{0_{(E ↾_{𝑠} F)}} ((k \in ℕ_{0} ⟼ {coe}_{1} (G) (k)))$
83	79 80 82	syl2anc	$⊢ ((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \to {finSupp}_{0_{(E ↾_{𝑠} F)}} ((k \in ℕ_{0} ⟼ {coe}_{1} (G) (k)))$
84		ringmnd	$⊢ E \in Ring \to E \in Mnd$
85	26 84	syl	$⊢ φ \to E \in Mnd$
86		subrgsubg	$⊢ F \in SubRing (E) \to F \in SubGrp (E)$
87		subgsubm	$⊢ F \in SubGrp (E) \to F \in SubMnd (E)$
88	25	subm0cl	$⊢ F \in SubMnd (E) \to 0_{E} \in F$
89	12 86 87 88	4syl	$⊢ φ \to 0_{E} \in F$
90	9 1 25	ress0g	$⊢ (E \in Mnd \land 0_{E} \in F \land F \subseteq B) \to 0_{E} = 0_{(E ↾_{𝑠} F)}$
91	85 89 44 90	syl3anc	$⊢ φ \to 0_{E} = 0_{(E ↾_{𝑠} F)}$
92	91	ad2antrr	$⊢ ((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \to 0_{E} = 0_{(E ↾_{𝑠} F)}$
93	83 92	breqtrrd	$⊢ ((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \to {finSupp}_{0_{E}} ((k \in ℕ_{0} ⟼ {coe}_{1} (G) (k)))$
94	93	fsuppimpd	$⊢ ((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \to (k \in ℕ_{0} ⟼ {coe}_{1} (G) (k)) supp 0_{E} \in Fin$
95		fveq2	$⊢ k = i \to {coe}_{1} (G) (k) = {coe}_{1} (G) (i)$
96		oveq1	$⊢ k = i \to k \cdot_{{mulGrp}_{E}} A = i \cdot_{{mulGrp}_{E}} A$
97	95 96	oveq12d	$⊢ k = i \to {coe}_{1} (G) (k) \cdot_{E} (k \cdot_{{mulGrp}_{E}} A) = {coe}_{1} (G) (i) \cdot_{E} (i \cdot_{{mulGrp}_{E}} A)$
98	97	cbvmptv	$⊢ (k \in ℕ_{0} ⟼ {coe}_{1} (G) (k) \cdot_{E} (k \cdot_{{mulGrp}_{E}} A)) = (i \in ℕ_{0} ⟼ {coe}_{1} (G) (i) \cdot_{E} (i \cdot_{{mulGrp}_{E}} A))$
99		nfv	$⊢ Ⅎ k ((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a)$
100		eqid	$⊢ (k \in ℕ_{0} ⟼ {coe}_{1} (G) (k)) = (k \in ℕ_{0} ⟼ {coe}_{1} (G) (k))$
101	99 42 100	fnmptd	$⊢ ((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \to (k \in ℕ_{0} ⟼ {coe}_{1} (G) (k)) Fn ℕ_{0}$
102		simplr	$⊢ ((((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \land i \in ℕ_{0}) \land (k \in ℕ_{0} ⟼ {coe}_{1} (G) (k)) (i) = 0_{E}) \to i \in ℕ_{0}$
103		fvexd	$⊢ ((((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \land i \in ℕ_{0}) \land (k \in ℕ_{0} ⟼ {coe}_{1} (G) (k)) (i) = 0_{E}) \to {coe}_{1} (G) (i) \in V$
104	100 95 102 103	fvmptd3	$⊢ ((((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \land i \in ℕ_{0}) \land (k \in ℕ_{0} ⟼ {coe}_{1} (G) (k)) (i) = 0_{E}) \to (k \in ℕ_{0} ⟼ {coe}_{1} (G) (k)) (i) = {coe}_{1} (G) (i)$
105		simpr	$⊢ ((((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \land i \in ℕ_{0}) \land (k \in ℕ_{0} ⟼ {coe}_{1} (G) (k)) (i) = 0_{E}) \to (k \in ℕ_{0} ⟼ {coe}_{1} (G) (k)) (i) = 0_{E}$
106	104 105	eqtr3d	$⊢ ((((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \land i \in ℕ_{0}) \land (k \in ℕ_{0} ⟼ {coe}_{1} (G) (k)) (i) = 0_{E}) \to {coe}_{1} (G) (i) = 0_{E}$
107	106	oveq1d	$⊢ ((((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \land i \in ℕ_{0}) \land (k \in ℕ_{0} ⟼ {coe}_{1} (G) (k)) (i) = 0_{E}) \to {coe}_{1} (G) (i) \cdot_{E} (i \cdot_{{mulGrp}_{E}} A) = 0_{E} \cdot_{E} (i \cdot_{{mulGrp}_{E}} A)$
108	26	ad4antr	$⊢ ((((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \land i \in ℕ_{0}) \land (k \in ℕ_{0} ⟼ {coe}_{1} (G) (k)) (i) = 0_{E}) \to E \in Ring$
109	56	ringmgp	$⊢ E \in Ring \to {mulGrp}_{E} \in Mnd$
110	26 109	syl	$⊢ φ \to {mulGrp}_{E} \in Mnd$
111	110	ad4antr	$⊢ ((((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \land i \in ℕ_{0}) \land (k \in ℕ_{0} ⟼ {coe}_{1} (G) (k)) (i) = 0_{E}) \to {mulGrp}_{E} \in Mnd$
112	7	ad4antr	$⊢ ((((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \land i \in ℕ_{0}) \land (k \in ℕ_{0} ⟼ {coe}_{1} (G) (k)) (i) = 0_{E}) \to A \in B$
113	57 14 111 102 112	mulgnn0cld	$⊢ ((((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \land i \in ℕ_{0}) \land (k \in ℕ_{0} ⟼ {coe}_{1} (G) (k)) (i) = 0_{E}) \to i \cdot_{{mulGrp}_{E}} A \in B$
114	1 13 25 108 113	ringlzd	$⊢ ((((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \land i \in ℕ_{0}) \land (k \in ℕ_{0} ⟼ {coe}_{1} (G) (k)) (i) = 0_{E}) \to 0_{E} \cdot_{E} (i \cdot_{{mulGrp}_{E}} A) = 0_{E}$
115	107 114	eqtrd	$⊢ ((((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \land i \in ℕ_{0}) \land (k \in ℕ_{0} ⟼ {coe}_{1} (G) (k)) (i) = 0_{E}) \to {coe}_{1} (G) (i) \cdot_{E} (i \cdot_{{mulGrp}_{E}} A) = 0_{E}$
116	115	3impa	$⊢ (((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \land i \in ℕ_{0} \land (k \in ℕ_{0} ⟼ {coe}_{1} (G) (k)) (i) = 0_{E}) \to {coe}_{1} (G) (i) \cdot_{E} (i \cdot_{{mulGrp}_{E}} A) = 0_{E}$
117	98 30 76 101 116	suppss3	$⊢ ((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \to (k \in ℕ_{0} ⟼ {coe}_{1} (G) (k) \cdot_{E} (k \cdot_{{mulGrp}_{E}} A)) supp 0_{E} \subseteq (k \in ℕ_{0} ⟼ {coe}_{1} (G) (k)) supp 0_{E}$
118		suppssfifsupp	$⊢ (((k \in ℕ_{0} ⟼ {coe}_{1} (G) (k) \cdot_{E} (k \cdot_{{mulGrp}_{E}} A)) \in V \land Fun (k \in ℕ_{0} ⟼ {coe}_{1} (G) (k) \cdot_{E} (k \cdot_{{mulGrp}_{E}} A)) \land 0_{E} \in V) \land ((k \in ℕ_{0} ⟼ {coe}_{1} (G) (k)) supp 0_{E} \in Fin \land (k \in ℕ_{0} ⟼ {coe}_{1} (G) (k) \cdot_{E} (k \cdot_{{mulGrp}_{E}} A)) supp 0_{E} \subseteq (k \in ℕ_{0} ⟼ {coe}_{1} (G) (k)) supp 0_{E})) \to {finSupp}_{0_{E}} ((k \in ℕ_{0} ⟼ {coe}_{1} (G) (k) \cdot_{E} (k \cdot_{{mulGrp}_{E}} A)))$
119	74 75 76 94 117 118	syl32anc	$⊢ ((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \to {finSupp}_{0_{E}} ((k \in ℕ_{0} ⟼ {coe}_{1} (G) (k) \cdot_{E} (k \cdot_{{mulGrp}_{E}} A)))$
120	25 28 30 34 73 119	gsumsubgcl	$⊢ ((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \to \underset{k \in ℕ_{0}}{\sum_{E}} ({coe}_{1} (G) (k) \cdot_{E} (k \cdot_{{mulGrp}_{E}} A)) \in a$
121	24 120	eqeltrd	$⊢ ((φ \land a \in SubDRing (E)) \land F \cup \{A\} \subseteq a) \to O (G) (A) \in a$
122	121	ex	$⊢ (φ \land a \in SubDRing (E)) \to (F \cup \{A\} \subseteq a \to O (G) (A) \in a)$
123	122	ralrimiva	$⊢ φ \to \forall a \in SubDRing (E) (F \cup \{A\} \subseteq a \to O (G) (A) \in a)$
124		fvex	$⊢ O (G) (A) \in V$
125	124	elintrab	$⊢ O (G) (A) \in ⋂ \{a \in SubDRing (E) \| F \cup \{A\} \subseteq a\} \leftrightarrow \forall a \in SubDRing (E) (F \cup \{A\} \subseteq a \to O (G) (A) \in a)$
126	123 125	sylibr	$⊢ φ \to O (G) (A) \in ⋂ \{a \in SubDRing (E) \| F \cup \{A\} \subseteq a\}$
127	5	flddrngd	$⊢ φ \to E \in DivRing$
128	7	snssd	$⊢ φ \to \{A\} \subseteq B$
129	44 128	unssd	$⊢ φ \to F \cup \{A\} \subseteq B$
130	1 127 129	fldgenval	$⊢ φ \to E fldGen (F \cup \{A\}) = ⋂ \{a \in SubDRing (E) \| F \cup \{A\} \subseteq a\}$
131	126 130	eleqtrrd	$⊢ φ \to O (G) (A) \in (E fldGen (F \cup \{A\}))$

Metamath Proof Explorer

Theorem evls1fldgencl

Proof