Metamath Proof Explorer

Theorem evls1fldgencl

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

Ref Expression
Hypotheses evls1fldgencl.1 ⊢ 𝐵 = ( Base ‘ 𝐸 )
evls1fldgencl.2 ⊢ 𝑂 = ( 𝐸 evalSub1 𝐹 )
evls1fldgencl.3 ⊢ 𝑃 = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
evls1fldgencl.4 ⊢ 𝑈 = ( Base ‘ 𝑃 )
evls1fldgencl.5 ⊢ ( 𝜑 → 𝐸 ∈ Field )
evls1fldgencl.6 ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
evls1fldgencl.7 ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
evls1fldgencl.8 ⊢ ( 𝜑 → 𝐺 ∈ 𝑈 )
Assertion evls1fldgencl ( 𝜑 → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝐴 ) ∈ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )

Proof

Step Hyp Ref Expression
1 evls1fldgencl.1 ⊢ 𝐵 = ( Base ‘ 𝐸 )
2 evls1fldgencl.2 ⊢ 𝑂 = ( 𝐸 evalSub1 𝐹 )
3 evls1fldgencl.3 ⊢ 𝑃 = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
4 evls1fldgencl.4 ⊢ 𝑈 = ( Base ‘ 𝑃 )
5 evls1fldgencl.5 ⊢ ( 𝜑 → 𝐸 ∈ Field )
6 evls1fldgencl.6 ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
7 evls1fldgencl.7 ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
8 evls1fldgencl.8 ⊢ ( 𝜑 → 𝐺 ∈ 𝑈 )
9 eqid ⊢ ( 𝐸 ↾s 𝐹 ) = ( 𝐸 ↾s 𝐹 )
10 5 fldcrngd ⊢ ( 𝜑 → 𝐸 ∈ CRing )
11 sdrgsubrg ⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
12 6 11 syl ⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
13 eqid ⊢ ( .r ‘ 𝐸 ) = ( .r ‘ 𝐸 )
14 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝐸 ) ) = ( .g ‘ ( mulGrp ‘ 𝐸 ) )
15 eqid ⊢ ( coe1 ‘ 𝐺 ) = ( coe1 ‘ 𝐺 )
16 2 1 3 9 4 10 12 8 13 14 15 evls1fpws ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐺 ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝐸 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝑥 ) ) ) ) ) )
17 oveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝑥 ) = ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) )
18 17 oveq2d ⊢ ( 𝑥 = 𝐴 → ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝑥 ) ) = ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ) )
19 18 mpteq2dv ⊢ ( 𝑥 = 𝐴 → ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝑥 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ) ) )
20 19 oveq2d ⊢ ( 𝑥 = 𝐴 → ( 𝐸 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝑥 ) ) ) ) = ( 𝐸 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ) ) ) )
21 20 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝐸 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝑥 ) ) ) ) = ( 𝐸 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ) ) ) )
22 ovexd ⊢ ( 𝜑 → ( 𝐸 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ) ) ) ∈ V )
23 16 21 7 22 fvmptd ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝐴 ) = ( 𝐸 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ) ) ) )
24 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝐴 ) = ( 𝐸 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ) ) ) )
25 eqid ⊢ ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐸 )
26 10 crngringd ⊢ ( 𝜑 → 𝐸 ∈ Ring )
27 26 ringabld ⊢ ( 𝜑 → 𝐸 ∈ Abel )
28 27 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) → 𝐸 ∈ Abel )
29 nn0ex ⊢ ℕ0 ∈ V
30 29 a1i ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) → ℕ0 ∈ V )
31 simplr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) → 𝑎 ∈ ( SubDRing ‘ 𝐸 ) )
32 sdrgsubrg ⊢ ( 𝑎 ∈ ( SubDRing ‘ 𝐸 ) → 𝑎 ∈ ( SubRing ‘ 𝐸 ) )
33 subrgsubg ⊢ ( 𝑎 ∈ ( SubRing ‘ 𝐸 ) → 𝑎 ∈ ( SubGrp ‘ 𝐸 ) )
34 31 32 33 3syl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) → 𝑎 ∈ ( SubGrp ‘ 𝐸 ) )
35 32 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑎 ∈ ( SubRing ‘ 𝐸 ) )
36 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 )
37 36 unssad ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐹 ⊆ 𝑎 )
38 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐺 ∈ 𝑈 )
39 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
40 eqid ⊢ ( Base ‘ ( 𝐸 ↾s 𝐹 ) ) = ( Base ‘ ( 𝐸 ↾s 𝐹 ) )
41 15 4 3 40 coe1fvalcl ⊢ ( ( 𝐺 ∈ 𝑈 ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ∈ ( Base ‘ ( 𝐸 ↾s 𝐹 ) ) )
42 38 39 41 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ∈ ( Base ‘ ( 𝐸 ↾s 𝐹 ) ) )
43 1 sdrgss ⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) → 𝐹 ⊆ 𝐵 )
44 6 43 syl ⊢ ( 𝜑 → 𝐹 ⊆ 𝐵 )
45 9 1 ressbas2 ⊢ ( 𝐹 ⊆ 𝐵 → 𝐹 = ( Base ‘ ( 𝐸 ↾s 𝐹 ) ) )
46 44 45 syl ⊢ ( 𝜑 → 𝐹 = ( Base ‘ ( 𝐸 ↾s 𝐹 ) ) )
47 46 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐹 = ( Base ‘ ( 𝐸 ↾s 𝐹 ) ) )
48 42 47 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ∈ 𝐹 )
49 37 48 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ∈ 𝑎 )
50 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑎 ∈ ( SubDRing ‘ 𝐸 ) )
51 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ 𝐵 )
52 36 unssbd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) ∧ 𝑘 ∈ ℕ0 ) → { 𝐴 } ⊆ 𝑎 )
53 snssg ⊢ ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ 𝑎 ↔ { 𝐴 } ⊆ 𝑎 ) )
54 53 biimpar ⊢ ( ( 𝐴 ∈ 𝐵 ∧ { 𝐴 } ⊆ 𝑎 ) → 𝐴 ∈ 𝑎 )
55 51 52 54 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ 𝑎 )
56 eqid ⊢ ( mulGrp ‘ 𝐸 ) = ( mulGrp ‘ 𝐸 )
57 56 1 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝐸 ) )
58 56 13 mgpplusg ⊢ ( .r ‘ 𝐸 ) = ( +g ‘ ( mulGrp ‘ 𝐸 ) )
59 fvexd ⊢ ( 𝑎 ∈ ( SubDRing ‘ 𝐸 ) → ( mulGrp ‘ 𝐸 ) ∈ V )
60 1 sdrgss ⊢ ( 𝑎 ∈ ( SubDRing ‘ 𝐸 ) → 𝑎 ⊆ 𝐵 )
61 13 subrgmcl ⊢ ( ( 𝑎 ∈ ( SubRing ‘ 𝐸 ) ∧ 𝑥 ∈ 𝑎 ∧ 𝑦 ∈ 𝑎 ) → ( 𝑥 ( .r ‘ 𝐸 ) 𝑦 ) ∈ 𝑎 )
62 32 61 syl3an1 ⊢ ( ( 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ∧ 𝑥 ∈ 𝑎 ∧ 𝑦 ∈ 𝑎 ) → ( 𝑥 ( .r ‘ 𝐸 ) 𝑦 ) ∈ 𝑎 )
63 eqid ⊢ ( 0g ‘ ( mulGrp ‘ 𝐸 ) ) = ( 0g ‘ ( mulGrp ‘ 𝐸 ) )
64 eqid ⊢ ( 1r ‘ 𝐸 ) = ( 1r ‘ 𝐸 )
65 56 64 ringidval ⊢ ( 1r ‘ 𝐸 ) = ( 0g ‘ ( mulGrp ‘ 𝐸 ) )
66 65 eqcomi ⊢ ( 0g ‘ ( mulGrp ‘ 𝐸 ) ) = ( 1r ‘ 𝐸 )
67 66 subrg1cl ⊢ ( 𝑎 ∈ ( SubRing ‘ 𝐸 ) → ( 0g ‘ ( mulGrp ‘ 𝐸 ) ) ∈ 𝑎 )
68 32 67 syl ⊢ ( 𝑎 ∈ ( SubDRing ‘ 𝐸 ) → ( 0g ‘ ( mulGrp ‘ 𝐸 ) ) ∈ 𝑎 )
69 57 14 58 59 60 62 63 68 mulgnn0subcl ⊢ ( ( 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ∧ 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑎 ) → ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ∈ 𝑎 )
70 50 39 55 69 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ∈ 𝑎 )
71 13 subrgmcl ⊢ ( ( 𝑎 ∈ ( SubRing ‘ 𝐸 ) ∧ ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ∈ 𝑎 ∧ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ∈ 𝑎 ) → ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ) ∈ 𝑎 )
72 35 49 70 71 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ) ∈ 𝑎 )
73 72 fmpttd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ) ) : ℕ0 ⟶ 𝑎 )
74 30 mptexd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ) ) ∈ V )
75 73 ffund ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) → Fun ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ) ) )
76 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) → ( 0g ‘ 𝐸 ) ∈ V )
77 9 subrgring ⊢ ( 𝐹 ∈ ( SubRing ‘ 𝐸 ) → ( 𝐸 ↾s 𝐹 ) ∈ Ring )
78 12 77 syl ⊢ ( 𝜑 → ( 𝐸 ↾s 𝐹 ) ∈ Ring )
79 78 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) → ( 𝐸 ↾s 𝐹 ) ∈ Ring )
80 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) → 𝐺 ∈ 𝑈 )
81 eqid ⊢ ( 0g ‘ ( 𝐸 ↾s 𝐹 ) ) = ( 0g ‘ ( 𝐸 ↾s 𝐹 ) )
82 3 4 81 mptcoe1fsupp ⊢ ( ( ( 𝐸 ↾s 𝐹 ) ∈ Ring ∧ 𝐺 ∈ 𝑈 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ) finSupp ( 0g ‘ ( 𝐸 ↾s 𝐹 ) ) )
83 79 80 82 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ) finSupp ( 0g ‘ ( 𝐸 ↾s 𝐹 ) ) )
84 ringmnd ⊢ ( 𝐸 ∈ Ring → 𝐸 ∈ Mnd )
85 26 84 syl ⊢ ( 𝜑 → 𝐸 ∈ Mnd )
86 subrgsubg ⊢ ( 𝐹 ∈ ( SubRing ‘ 𝐸 ) → 𝐹 ∈ ( SubGrp ‘ 𝐸 ) )
87 subgsubm ⊢ ( 𝐹 ∈ ( SubGrp ‘ 𝐸 ) → 𝐹 ∈ ( SubMnd ‘ 𝐸 ) )
88 25 subm0cl ⊢ ( 𝐹 ∈ ( SubMnd ‘ 𝐸 ) → ( 0g ‘ 𝐸 ) ∈ 𝐹 )
89 12 86 87 88 4syl ⊢ ( 𝜑 → ( 0g ‘ 𝐸 ) ∈ 𝐹 )
90 9 1 25 ress0g ⊢ ( ( 𝐸 ∈ Mnd ∧ ( 0g ‘ 𝐸 ) ∈ 𝐹 ∧ 𝐹 ⊆ 𝐵 ) → ( 0g ‘ 𝐸 ) = ( 0g ‘ ( 𝐸 ↾s 𝐹 ) ) )
91 85 89 44 90 syl3anc ⊢ ( 𝜑 → ( 0g ‘ 𝐸 ) = ( 0g ‘ ( 𝐸 ↾s 𝐹 ) ) )
92 91 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) → ( 0g ‘ 𝐸 ) = ( 0g ‘ ( 𝐸 ↾s 𝐹 ) ) )
93 83 92 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ) finSupp ( 0g ‘ 𝐸 ) )
94 93 fsuppimpd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ) supp ( 0g ‘ 𝐸 ) ) ∈ Fin )
95 fveq2 ⊢ ( 𝑘 = 𝑖 → ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) = ( ( coe1 ‘ 𝐺 ) ‘ 𝑖 ) )
96 oveq1 ⊢ ( 𝑘 = 𝑖 → ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) )
97 95 96 oveq12d ⊢ ( 𝑘 = 𝑖 → ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ) = ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ) )
98 97 cbvmptv ⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ) ) = ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ) )
99 nfv ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 )
100 eqid ⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) )
101 99 42 100 fnmptd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ) Fn ℕ0 )
102 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) ∧ 𝑖 ∈ ℕ0 ) ∧ ( ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ) ‘ 𝑖 ) = ( 0g ‘ 𝐸 ) ) → 𝑖 ∈ ℕ0 )
103 fvexd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) ∧ 𝑖 ∈ ℕ0 ) ∧ ( ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ) ‘ 𝑖 ) = ( 0g ‘ 𝐸 ) ) → ( ( coe1 ‘ 𝐺 ) ‘ 𝑖 ) ∈ V )
104 100 95 102 103 fvmptd3 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) ∧ 𝑖 ∈ ℕ0 ) ∧ ( ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ) ‘ 𝑖 ) = ( 0g ‘ 𝐸 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ) ‘ 𝑖 ) = ( ( coe1 ‘ 𝐺 ) ‘ 𝑖 ) )
105 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) ∧ 𝑖 ∈ ℕ0 ) ∧ ( ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ) ‘ 𝑖 ) = ( 0g ‘ 𝐸 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ) ‘ 𝑖 ) = ( 0g ‘ 𝐸 ) )
106 104 105 eqtr3d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) ∧ 𝑖 ∈ ℕ0 ) ∧ ( ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ) ‘ 𝑖 ) = ( 0g ‘ 𝐸 ) ) → ( ( coe1 ‘ 𝐺 ) ‘ 𝑖 ) = ( 0g ‘ 𝐸 ) )
107 106 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) ∧ 𝑖 ∈ ℕ0 ) ∧ ( ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ) ‘ 𝑖 ) = ( 0g ‘ 𝐸 ) ) → ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ) = ( ( 0g ‘ 𝐸 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ) )
108 26 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) ∧ 𝑖 ∈ ℕ0 ) ∧ ( ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ) ‘ 𝑖 ) = ( 0g ‘ 𝐸 ) ) → 𝐸 ∈ Ring )
109 56 ringmgp ⊢ ( 𝐸 ∈ Ring → ( mulGrp ‘ 𝐸 ) ∈ Mnd )
110 26 109 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝐸 ) ∈ Mnd )
111 110 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) ∧ 𝑖 ∈ ℕ0 ) ∧ ( ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ) ‘ 𝑖 ) = ( 0g ‘ 𝐸 ) ) → ( mulGrp ‘ 𝐸 ) ∈ Mnd )
112 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) ∧ 𝑖 ∈ ℕ0 ) ∧ ( ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ) ‘ 𝑖 ) = ( 0g ‘ 𝐸 ) ) → 𝐴 ∈ 𝐵 )
113 57 14 111 102 112 mulgnn0cld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) ∧ 𝑖 ∈ ℕ0 ) ∧ ( ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ) ‘ 𝑖 ) = ( 0g ‘ 𝐸 ) ) → ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ∈ 𝐵 )
114 1 13 25 108 113 ringlzd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) ∧ 𝑖 ∈ ℕ0 ) ∧ ( ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ) ‘ 𝑖 ) = ( 0g ‘ 𝐸 ) ) → ( ( 0g ‘ 𝐸 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ) = ( 0g ‘ 𝐸 ) )
115 107 114 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) ∧ 𝑖 ∈ ℕ0 ) ∧ ( ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ) ‘ 𝑖 ) = ( 0g ‘ 𝐸 ) ) → ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ) = ( 0g ‘ 𝐸 ) )
116 115 3impa ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) ∧ 𝑖 ∈ ℕ0 ∧ ( ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ) ‘ 𝑖 ) = ( 0g ‘ 𝐸 ) ) → ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑖 ) ( .r ‘ 𝐸 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ) = ( 0g ‘ 𝐸 ) )
117 98 30 76 101 116 suppss3 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ) ) supp ( 0g ‘ 𝐸 ) ) ⊆ ( ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ) supp ( 0g ‘ 𝐸 ) ) )
118 suppssfifsupp ⊢ ( ( ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ) ) ∧ ( 0g ‘ 𝐸 ) ∈ V ) ∧ ( ( ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ) supp ( 0g ‘ 𝐸 ) ) ∈ Fin ∧ ( ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ) ) supp ( 0g ‘ 𝐸 ) ) ⊆ ( ( 𝑘 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ) supp ( 0g ‘ 𝐸 ) ) ) ) → ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ) ) finSupp ( 0g ‘ 𝐸 ) )
119 74 75 76 94 117 118 syl32anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ) ) finSupp ( 0g ‘ 𝐸 ) )
120 25 28 30 34 73 119 gsumsubgcl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) → ( 𝐸 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐺 ) ‘ 𝑘 ) ( .r ‘ 𝐸 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝐸 ) ) 𝐴 ) ) ) ) ∈ 𝑎 )
121 24 120 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) ∧ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 ) → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑎 )
122 121 ex ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ) → ( ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑎 ) )
123 122 ralrimiva ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ( ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑎 ) )
124 fvex ⊢ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝐴 ) ∈ V
125 124 elintrab ⊢ ( ( ( 𝑂 ‘ 𝐺 ) ‘ 𝐴 ) ∈ ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ∣ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 } ↔ ∀ 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ( ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝐴 ) ∈ 𝑎 ) )
126 123 125 sylibr ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝐴 ) ∈ ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ∣ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 } )
127 5 flddrngd ⊢ ( 𝜑 → 𝐸 ∈ DivRing )
128 7 snssd ⊢ ( 𝜑 → { 𝐴 } ⊆ 𝐵 )
129 44 128 unssd ⊢ ( 𝜑 → ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝐵 )
130 1 127 129 fldgenval ⊢ ( 𝜑 → ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) = ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐸 ) ∣ ( 𝐹 ∪ { 𝐴 } ) ⊆ 𝑎 } )
131 126 130 eleqtrrd ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝐴 ) ∈ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )