Theorem rngunsnply1chr2lem2 34244

Description: Lemma for rngunsnply1chr2 . (Contributed by Thierry Arnoux, 8-Nov-2026.)

Hypotheses

Ref	Expression
rngunsnply1chr2.v	⊢ 𝑉 = (Base‘𝑅)
rngunsnply1chr2.p	⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))
rngunsnply1chr2.u	⊢ 𝑈 = (Base‘𝑃)
rngunsnply1chr2.q	⊢ 𝑄 = (𝑅 evalSub1 𝑆)
rngunsnply1chr2.r	⊢ (𝜑 → 𝑅 ∈ CRing)
rngunsnply1chr2.1	⊢ (𝜑 → 𝑅 ∈ NzRing)
rngunsnply1chr2.s	⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))
rngunsnply1chr2.x	⊢ (𝜑 → 𝑋 ∈ 𝑉)
rngunsnply1chr2.y	⊢ (𝜑 → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑋})))
rngunsnply1chr2.n	⊢ 𝑁 = (RingSpan‘𝑅)
rngunsnply1chr2.2	⊢ + = (+g‘𝑅)
rngunsnply1chr2.3	⊢ · = (.r‘𝑅)
rngunsnply1chr2.4	⊢ ↑ = (.g‘(mulGrp‘𝑅))
rngunsnply1chr2.a	⊢ (𝜑 → 𝐴 ∈ 𝑆)
rngunsnply1chr2.b	⊢ (𝜑 → 𝐵 ∈ 𝑆)
rngunsnply1chr2.5	⊢ (𝜑 → (2 ↑ 𝑋) = ((𝐴 · 𝑋) + 𝐵))
rngunsnply1chr2lem.d	⊢ 𝐷 = (deg1‘𝑅)
rngunsnply1chr2lem.e	⊢ 𝐸 = (rem1p‘(𝑅 ↾s 𝑆))
rngunsnply1chr2lem.g	⊢ 𝐺 = ((2(.g‘(mulGrp‘𝑃))(var1‘𝑅))(-g‘𝑃)((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵)))
rngunsnply1chr2lem.h	⊢ 𝐻 = (𝐹𝐸𝐺)
rngunsnply1chr2lem.f	⊢ (𝜑 → 𝐹 ∈ 𝑈)

Assertion

Ref	Expression
rngunsnply1chr2lem2	⊢ (𝜑 → 𝐺 ∈ (Unic1p‘(𝑅 ↾s 𝑆)))

Proof of Theorem rngunsnply1chr2lem2

Dummy variable 𝑖 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rngunsnply1chr2.s	. . 3 ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))
2		eqid 2763	. . . 4 ⊢ (𝑅 ↾s 𝑆) = (𝑅 ↾s 𝑆)
3	2	subrgring 20868	. . 3 ⊢ (𝑆 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝑆) ∈ Ring)
4	1, 3	syl 18	. 2 ⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ Ring)
5		rngunsnply1chr2lem.g	. . . . 5 ⊢ 𝐺 = ((2(.g‘(mulGrp‘𝑃))(var1‘𝑅))(-g‘𝑃)((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵)))
6		rngunsnply1chr2.u	. . . . . 6 ⊢ 𝑈 = (Base‘𝑃)
7		eqid 2763	. . . . . 6 ⊢ (-g‘𝑃) = (-g‘𝑃)
8		rngunsnply1chr2.p	. . . . . . . . 9 ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))
9	8	ply1ring 22609	. . . . . . . 8 ⊢ ((𝑅 ↾s 𝑆) ∈ Ring → 𝑃 ∈ Ring)
10	4, 9	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ Ring)
11	10	ringgrpd 20511	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ Grp)
12		eqid 2763	. . . . . . . 8 ⊢ (mulGrp‘𝑃) = (mulGrp‘𝑃)
13	12, 6	mgpbas 20407	. . . . . . 7 ⊢ 𝑈 = (Base‘(mulGrp‘𝑃))
14		eqid 2763	. . . . . . 7 ⊢ (.g‘(mulGrp‘𝑃)) = (.g‘(mulGrp‘𝑃))
15	12	ringmgp 20507	. . . . . . . 8 ⊢ (𝑃 ∈ Ring → (mulGrp‘𝑃) ∈ Mnd)
16	10, 15	syl 18	. . . . . . 7 ⊢ (𝜑 → (mulGrp‘𝑃) ∈ Mnd)
17		2nn0 12661	. . . . . . . 8 ⊢ 2 ∈ ℕ0
18	17	a1i 11	. . . . . . 7 ⊢ (𝜑 → 2 ∈ ℕ0)
19		eqid 2763	. . . . . . . 8 ⊢ (var1‘𝑅) = (var1‘𝑅)
20	19, 1, 2, 8, 6	subrgvr1cl 22625	. . . . . . 7 ⊢ (𝜑 → (var1‘𝑅) ∈ 𝑈)
21	13, 14, 16, 18, 20	mulgnn0cld 19346	. . . . . 6 ⊢ (𝜑 → (2(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ 𝑈)
22		eqid 2763	. . . . . . 7 ⊢ (+g‘𝑃) = (+g‘𝑃)
23		eqid 2763	. . . . . . . 8 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
24		eqid 2763	. . . . . . . 8 ⊢ ( ·𝑠 ‘𝑃) = ( ·𝑠 ‘𝑃)
25		eqid 2763	. . . . . . . 8 ⊢ (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
26	8	ply1lmod 22613	. . . . . . . . 9 ⊢ ((𝑅 ↾s 𝑆) ∈ Ring → 𝑃 ∈ LMod)
27	4, 26	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ LMod)
28		rngunsnply1chr2.a	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ 𝑆)
29	2	subrgbas 20875	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (SubRing‘𝑅) → 𝑆 = (Base‘(𝑅 ↾s 𝑆)))
30	1, 29	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 = (Base‘(𝑅 ↾s 𝑆)))
31		ovex 7482	. . . . . . . . . . . 12 ⊢ (𝑅 ↾s 𝑆) ∈ V
32	8	ply1sca 22614	. . . . . . . . . . . 12 ⊢ ((𝑅 ↾s 𝑆) ∈ V → (𝑅 ↾s 𝑆) = (Scalar‘𝑃))
33	31, 32	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝑅 ↾s 𝑆) = (Scalar‘𝑃)
34	33	fveq2i 6917	. . . . . . . . . 10 ⊢ (Base‘(𝑅 ↾s 𝑆)) = (Base‘(Scalar‘𝑃))
35	30, 34	eqtrdi 2814	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 = (Base‘(Scalar‘𝑃)))
36	28, 35	eleqtrd 2866	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ (Base‘(Scalar‘𝑃)))
37	6, 23, 24, 25, 27, 36, 20	lmodvscld 21196	. . . . . . 7 ⊢ (𝜑 → (𝐴( ·𝑠 ‘𝑃)(var1‘𝑅)) ∈ 𝑈)
38		eqid 2763	. . . . . . . 8 ⊢ (algSc‘𝑃) = (algSc‘𝑃)
39		rngunsnply1chr2.r	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ CRing)
40		rngunsnply1chr2.b	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ 𝑆)
41	8, 2, 38, 6, 39, 1, 40	ressasclcl 34199	. . . . . . 7 ⊢ (𝜑 → ((algSc‘𝑃)‘𝐵) ∈ 𝑈)
42	6, 22, 11, 37, 41	grpcld 19199	. . . . . 6 ⊢ (𝜑 → ((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵)) ∈ 𝑈)
43	6, 7, 11, 21, 42	grpsubcld 33691	. . . . 5 ⊢ (𝜑 → ((2(.g‘(mulGrp‘𝑃))(var1‘𝑅))(-g‘𝑃)((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵))) ∈ 𝑈)
44	5, 43	eqeltrid 2868	. . . 4 ⊢ (𝜑 → 𝐺 ∈ 𝑈)
45		eqid 2763	. . . . . . . 8 ⊢ (Poly1‘𝑅) = (Poly1‘𝑅)
46		eqid 2763	. . . . . . . 8 ⊢ (PwSer1‘(𝑅 ↾s 𝑆)) = (PwSer1‘(𝑅 ↾s 𝑆))
47		eqid 2763	. . . . . . . 8 ⊢ (Base‘(PwSer1‘(𝑅 ↾s 𝑆))) = (Base‘(PwSer1‘(𝑅 ↾s 𝑆)))
48		eqid 2763	. . . . . . . 8 ⊢ (Base‘(Poly1‘𝑅)) = (Base‘(Poly1‘𝑅))
49	45, 2, 8, 6, 1, 46, 47, 48	ressply1bas2 22589	. . . . . . 7 ⊢ (𝜑 → 𝑈 = ((Base‘(PwSer1‘(𝑅 ↾s 𝑆))) ∩ (Base‘(Poly1‘𝑅))))
50	44, 49	eleqtrd 2866	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ ((Base‘(PwSer1‘(𝑅 ↾s 𝑆))) ∩ (Base‘(Poly1‘𝑅))))
51	50	elin2d 4105	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ (Base‘(Poly1‘𝑅)))
52	39	crngringd 20515	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ Ring)
53		rngunsnply1chr2.v	. . . . . . . 8 ⊢ 𝑉 = (Base‘𝑅)
54		rngunsnply1chr2.q	. . . . . . . 8 ⊢ 𝑄 = (𝑅 evalSub1 𝑆)
55		rngunsnply1chr2.1	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ NzRing)
56		rngunsnply1chr2.x	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
57		rngunsnply1chr2.y	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑋})))
58		rngunsnply1chr2.n	. . . . . . . 8 ⊢ 𝑁 = (RingSpan‘𝑅)
59		rngunsnply1chr2.2	. . . . . . . 8 ⊢ + = (+g‘𝑅)
60		rngunsnply1chr2.3	. . . . . . . 8 ⊢ · = (.r‘𝑅)
61		rngunsnply1chr2.4	. . . . . . . 8 ⊢ ↑ = (.g‘(mulGrp‘𝑅))
62		rngunsnply1chr2.5	. . . . . . . 8 ⊢ (𝜑 → (2 ↑ 𝑋) = ((𝐴 · 𝑋) + 𝐵))
63		rngunsnply1chr2lem.d	. . . . . . . 8 ⊢ 𝐷 = (deg1‘𝑅)
64		rngunsnply1chr2lem.e	. . . . . . . 8 ⊢ 𝐸 = (rem1p‘(𝑅 ↾s 𝑆))
65		rngunsnply1chr2lem.h	. . . . . . . 8 ⊢ 𝐻 = (𝐹𝐸𝐺)
66		rngunsnply1chr2lem.f	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ 𝑈)
67	53, 8, 6, 54, 39, 55, 1, 56, 57, 58, 59, 60, 61, 28, 40, 62, 63, 64, 5, 65, 66	rngunsnply1chr2lem1 34243	. . . . . . 7 ⊢ (𝜑 → (𝐷‘𝐺) = 2)
68	67, 17	eqeltrdi 2872	. . . . . 6 ⊢ (𝜑 → (𝐷‘𝐺) ∈ ℕ0)
69		eqid 2763	. . . . . . . 8 ⊢ (0g‘(Poly1‘𝑅)) = (0g‘(Poly1‘𝑅))
70	63, 45, 69, 48	deg1nn0clb 26452	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ (Base‘(Poly1‘𝑅))) → (𝐺 ≠ (0g‘(Poly1‘𝑅)) ↔ (𝐷‘𝐺) ∈ ℕ0))
71	70	biimpar 483	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ (Base‘(Poly1‘𝑅))) ∧ (𝐷‘𝐺) ∈ ℕ0) → 𝐺 ≠ (0g‘(Poly1‘𝑅)))
72	52, 51, 68, 71	syl21anc 851	. . . . 5 ⊢ (𝜑 → 𝐺 ≠ (0g‘(Poly1‘𝑅)))
73	5	fveq2i 6917	. . . . . . . 8 ⊢ (coe1‘𝐺) = (coe1‘((2(.g‘(mulGrp‘𝑃))(var1‘𝑅))(-g‘𝑃)((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵))))
74	73	a1i 11	. . . . . . 7 ⊢ (𝜑 → (coe1‘𝐺) = (coe1‘((2(.g‘(mulGrp‘𝑃))(var1‘𝑅))(-g‘𝑃)((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵)))))
75	74, 67	fveq12d 6921	. . . . . 6 ⊢ (𝜑 → ((coe1‘𝐺)‘(𝐷‘𝐺)) = ((coe1‘((2(.g‘(mulGrp‘𝑃))(var1‘𝑅))(-g‘𝑃)((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵))))‘2))
76		eqid 2763	. . . . . . . 8 ⊢ (-g‘(𝑅 ↾s 𝑆)) = (-g‘(𝑅 ↾s 𝑆))
77	8, 6, 7, 76	coe1subfv 22629	. . . . . . 7 ⊢ ((((𝑅 ↾s 𝑆) ∈ Ring ∧ (2(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ 𝑈 ∧ ((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵)) ∈ 𝑈) ∧ 2 ∈ ℕ0) → ((coe1‘((2(.g‘(mulGrp‘𝑃))(var1‘𝑅))(-g‘𝑃)((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵))))‘2) = (((coe1‘(2(.g‘(mulGrp‘𝑃))(var1‘𝑅)))‘2)(-g‘(𝑅 ↾s 𝑆))((coe1‘((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵)))‘2)))
78	4, 21, 42, 18, 77	syl31anc 1401	. . . . . 6 ⊢ (𝜑 → ((coe1‘((2(.g‘(mulGrp‘𝑃))(var1‘𝑅))(-g‘𝑃)((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵))))‘2) = (((coe1‘(2(.g‘(mulGrp‘𝑃))(var1‘𝑅)))‘2)(-g‘(𝑅 ↾s 𝑆))((coe1‘((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵)))‘2)))
79	19, 1, 2	subrgvr1 22624	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (var1‘𝑅) = (var1‘(𝑅 ↾s 𝑆)))
80	79, 20	eqeltrrd 2865	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (var1‘(𝑅 ↾s 𝑆)) ∈ 𝑈)
81	13, 14, 16, 18, 80	mulgnn0cld 19346	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2(.g‘(mulGrp‘𝑃))(var1‘(𝑅 ↾s 𝑆))) ∈ 𝑈)
82		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (1r‘(Scalar‘𝑃)) = (1r‘(Scalar‘𝑃))
83	6, 23, 24, 82	lmodvs1 21207	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ LMod ∧ (2(.g‘(mulGrp‘𝑃))(var1‘(𝑅 ↾s 𝑆))) ∈ 𝑈) → ((1r‘(Scalar‘𝑃))( ·𝑠 ‘𝑃)(2(.g‘(mulGrp‘𝑃))(var1‘(𝑅 ↾s 𝑆)))) = (2(.g‘(mulGrp‘𝑃))(var1‘(𝑅 ↾s 𝑆))))
84	27, 81, 83	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1r‘(Scalar‘𝑃))( ·𝑠 ‘𝑃)(2(.g‘(mulGrp‘𝑃))(var1‘(𝑅 ↾s 𝑆)))) = (2(.g‘(mulGrp‘𝑃))(var1‘(𝑅 ↾s 𝑆))))
85		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ (1r‘𝑅) = (1r‘𝑅)
86	2, 85	subrg1 20876	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ∈ (SubRing‘𝑅) → (1r‘𝑅) = (1r‘(𝑅 ↾s 𝑆)))
87	1, 86	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1r‘𝑅) = (1r‘(𝑅 ↾s 𝑆)))
88	33	fveq2i 6917	. . . . . . . . . . . . . 14 ⊢ (1r‘(𝑅 ↾s 𝑆)) = (1r‘(Scalar‘𝑃))
89	87, 88	eqtrdi 2814	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1r‘𝑅) = (1r‘(Scalar‘𝑃)))
90	89	oveq1d 7464	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1r‘𝑅)( ·𝑠 ‘𝑃)(2(.g‘(mulGrp‘𝑃))(var1‘(𝑅 ↾s 𝑆)))) = ((1r‘(Scalar‘𝑃))( ·𝑠 ‘𝑃)(2(.g‘(mulGrp‘𝑃))(var1‘(𝑅 ↾s 𝑆)))))
91	79	oveq2d 7465	. . . . . . . . . . . 12 ⊢ (𝜑 → (2(.g‘(mulGrp‘𝑃))(var1‘𝑅)) = (2(.g‘(mulGrp‘𝑃))(var1‘(𝑅 ↾s 𝑆))))
92	84, 90, 91	3eqtr4d 2808	. . . . . . . . . . 11 ⊢ (𝜑 → ((1r‘𝑅)( ·𝑠 ‘𝑃)(2(.g‘(mulGrp‘𝑃))(var1‘(𝑅 ↾s 𝑆)))) = (2(.g‘(mulGrp‘𝑃))(var1‘𝑅)))
93	92	fveq2d 6918	. . . . . . . . . 10 ⊢ (𝜑 → (coe1‘((1r‘𝑅)( ·𝑠 ‘𝑃)(2(.g‘(mulGrp‘𝑃))(var1‘(𝑅 ↾s 𝑆))))) = (coe1‘(2(.g‘(mulGrp‘𝑃))(var1‘𝑅))))
94	93	fveq1d 6916	. . . . . . . . 9 ⊢ (𝜑 → ((coe1‘((1r‘𝑅)( ·𝑠 ‘𝑃)(2(.g‘(mulGrp‘𝑃))(var1‘(𝑅 ↾s 𝑆)))))‘2) = ((coe1‘(2(.g‘(mulGrp‘𝑃))(var1‘𝑅)))‘2))
95	85	subrg1cl 20874	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ (SubRing‘𝑅) → (1r‘𝑅) ∈ 𝑆)
96	1, 95	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (1r‘𝑅) ∈ 𝑆)
97	96, 30	eleqtrd 2866	. . . . . . . . . 10 ⊢ (𝜑 → (1r‘𝑅) ∈ (Base‘(𝑅 ↾s 𝑆)))
98		eqid 2763	. . . . . . . . . . 11 ⊢ (0g‘(𝑅 ↾s 𝑆)) = (0g‘(𝑅 ↾s 𝑆))
99		eqid 2763	. . . . . . . . . . 11 ⊢ (Base‘(𝑅 ↾s 𝑆)) = (Base‘(𝑅 ↾s 𝑆))
100		eqid 2763	. . . . . . . . . . 11 ⊢ (var1‘(𝑅 ↾s 𝑆)) = (var1‘(𝑅 ↾s 𝑆))
101	98, 99, 8, 100, 24, 12, 14	coe1tmfv1 22637	. . . . . . . . . 10 ⊢ (((𝑅 ↾s 𝑆) ∈ Ring ∧ (1r‘𝑅) ∈ (Base‘(𝑅 ↾s 𝑆)) ∧ 2 ∈ ℕ0) → ((coe1‘((1r‘𝑅)( ·𝑠 ‘𝑃)(2(.g‘(mulGrp‘𝑃))(var1‘(𝑅 ↾s 𝑆)))))‘2) = (1r‘𝑅))
102	4, 97, 18, 101	syl3anc 1399	. . . . . . . . 9 ⊢ (𝜑 → ((coe1‘((1r‘𝑅)( ·𝑠 ‘𝑃)(2(.g‘(mulGrp‘𝑃))(var1‘(𝑅 ↾s 𝑆)))))‘2) = (1r‘𝑅))
103	94, 102	eqtr3d 2800	. . . . . . . 8 ⊢ (𝜑 → ((coe1‘(2(.g‘(mulGrp‘𝑃))(var1‘𝑅)))‘2) = (1r‘𝑅))
104		eqid 2763	. . . . . . . . . . 11 ⊢ (+g‘(𝑅 ↾s 𝑆)) = (+g‘(𝑅 ↾s 𝑆))
105	8, 6, 22, 104	coe1addfv 22628	. . . . . . . . . 10 ⊢ ((((𝑅 ↾s 𝑆) ∈ Ring ∧ (𝐴( ·𝑠 ‘𝑃)(var1‘𝑅)) ∈ 𝑈 ∧ ((algSc‘𝑃)‘𝐵) ∈ 𝑈) ∧ 2 ∈ ℕ0) → ((coe1‘((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵)))‘2) = (((coe1‘(𝐴( ·𝑠 ‘𝑃)(var1‘𝑅)))‘2)(+g‘(𝑅 ↾s 𝑆))((coe1‘((algSc‘𝑃)‘𝐵))‘2)))
106	4, 37, 41, 18, 105	syl31anc 1401	. . . . . . . . 9 ⊢ (𝜑 → ((coe1‘((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵)))‘2) = (((coe1‘(𝐴( ·𝑠 ‘𝑃)(var1‘𝑅)))‘2)(+g‘(𝑅 ↾s 𝑆))((coe1‘((algSc‘𝑃)‘𝐵))‘2)))
107	52	ringgrpd 20511	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 ∈ Grp)
108	107	grpmndd 19198	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ∈ Mnd)
109		subrgsubg 20871	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ (SubRing‘𝑅) → 𝑆 ∈ (SubGrp‘𝑅))
110	1, 109	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝑅))
111		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (0g‘𝑅) = (0g‘𝑅)
112	111	subg0cl 19385	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ (SubGrp‘𝑅) → (0g‘𝑅) ∈ 𝑆)
113	110, 112	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (0g‘𝑅) ∈ 𝑆)
114	53	subrgss 20866	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ (SubRing‘𝑅) → 𝑆 ⊆ 𝑉)
115	1, 114	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ⊆ 𝑉)
116	2, 53, 111	ress0g 18995	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Mnd ∧ (0g‘𝑅) ∈ 𝑆 ∧ 𝑆 ⊆ 𝑉) → (0g‘𝑅) = (0g‘(𝑅 ↾s 𝑆)))
117	108, 113, 115, 116	syl3anc 1399	. . . . . . . . . . 11 ⊢ (𝜑 → (0g‘𝑅) = (0g‘(𝑅 ↾s 𝑆)))
118	28, 30	eleqtrd 2866	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ (Base‘(𝑅 ↾s 𝑆)))
119		1nn0 12660	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℕ0
120	119	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℕ0)
121		1ne2 12591	. . . . . . . . . . . . 13 ⊢ 1 ≠ 2
122	121	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ≠ 2)
123	98, 99, 8, 100, 24, 12, 14, 4, 118, 120, 18, 122	coe1tmfv2 22638	. . . . . . . . . . 11 ⊢ (𝜑 → ((coe1‘(𝐴( ·𝑠 ‘𝑃)(1(.g‘(mulGrp‘𝑃))(var1‘(𝑅 ↾s 𝑆)))))‘2) = (0g‘(𝑅 ↾s 𝑆)))
124	13, 14	mulg1 19332	. . . . . . . . . . . . . . . 16 ⊢ ((var1‘(𝑅 ↾s 𝑆)) ∈ 𝑈 → (1(.g‘(mulGrp‘𝑃))(var1‘(𝑅 ↾s 𝑆))) = (var1‘(𝑅 ↾s 𝑆)))
125	80, 124	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1(.g‘(mulGrp‘𝑃))(var1‘(𝑅 ↾s 𝑆))) = (var1‘(𝑅 ↾s 𝑆)))
126	125, 79	eqtr4d 2801	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1(.g‘(mulGrp‘𝑃))(var1‘(𝑅 ↾s 𝑆))) = (var1‘𝑅))
127	126	oveq2d 7465	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴( ·𝑠 ‘𝑃)(1(.g‘(mulGrp‘𝑃))(var1‘(𝑅 ↾s 𝑆)))) = (𝐴( ·𝑠 ‘𝑃)(var1‘𝑅)))
128	127	fveq2d 6918	. . . . . . . . . . . 12 ⊢ (𝜑 → (coe1‘(𝐴( ·𝑠 ‘𝑃)(1(.g‘(mulGrp‘𝑃))(var1‘(𝑅 ↾s 𝑆))))) = (coe1‘(𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))))
129	128	fveq1d 6916	. . . . . . . . . . 11 ⊢ (𝜑 → ((coe1‘(𝐴( ·𝑠 ‘𝑃)(1(.g‘(mulGrp‘𝑃))(var1‘(𝑅 ↾s 𝑆)))))‘2) = ((coe1‘(𝐴( ·𝑠 ‘𝑃)(var1‘𝑅)))‘2))
130	117, 123, 129	3eqtr2rd 2805	. . . . . . . . . 10 ⊢ (𝜑 → ((coe1‘(𝐴( ·𝑠 ‘𝑃)(var1‘𝑅)))‘2) = (0g‘𝑅))
131	40, 30	eleqtrd 2866	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ (Base‘(𝑅 ↾s 𝑆)))
132	8, 38, 99, 98	coe1scl 22650	. . . . . . . . . . . 12 ⊢ (((𝑅 ↾s 𝑆) ∈ Ring ∧ 𝐵 ∈ (Base‘(𝑅 ↾s 𝑆))) → (coe1‘((algSc‘𝑃)‘𝐵)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, 𝐵, (0g‘(𝑅 ↾s 𝑆)))))
133	4, 131, 132	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → (coe1‘((algSc‘𝑃)‘𝐵)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, 𝐵, (0g‘(𝑅 ↾s 𝑆)))))
134		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 = 2) → 𝑖 = 2)
135		2ne0 12487	. . . . . . . . . . . . . . . 16 ⊢ 2 ≠ 0
136	135	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 = 2) → 2 ≠ 0)
137	134, 136	eqnetrd 3026	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 = 2) → 𝑖 ≠ 0)
138	137	neneqd 2964	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 = 2) → ¬ 𝑖 = 0)
139	138	iffalsed 4496	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 = 2) → if(𝑖 = 0, 𝐵, (0g‘(𝑅 ↾s 𝑆))) = (0g‘(𝑅 ↾s 𝑆)))
140	117	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 = 2) → (0g‘𝑅) = (0g‘(𝑅 ↾s 𝑆)))
141	139, 140	eqtr4d 2801	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 = 2) → if(𝑖 = 0, 𝐵, (0g‘(𝑅 ↾s 𝑆))) = (0g‘𝑅))
142		fvexd 6929	. . . . . . . . . . 11 ⊢ (𝜑 → (0g‘𝑅) ∈ V)
143	133, 141, 18, 142	fvmptd 7030	. . . . . . . . . 10 ⊢ (𝜑 → ((coe1‘((algSc‘𝑃)‘𝐵))‘2) = (0g‘𝑅))
144	130, 143	oveq12d 7467	. . . . . . . . 9 ⊢ (𝜑 → (((coe1‘(𝐴( ·𝑠 ‘𝑃)(var1‘𝑅)))‘2)(+g‘(𝑅 ↾s 𝑆))((coe1‘((algSc‘𝑃)‘𝐵))‘2)) = ((0g‘𝑅)(+g‘(𝑅 ↾s 𝑆))(0g‘𝑅)))
145	2, 59	ressplusg 17503	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ (SubRing‘𝑅) → + = (+g‘(𝑅 ↾s 𝑆)))
146	1, 145	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → + = (+g‘(𝑅 ↾s 𝑆)))
147	146	oveqd 7466	. . . . . . . . . 10 ⊢ (𝜑 → ((0g‘𝑅) + (0g‘𝑅)) = ((0g‘𝑅)(+g‘(𝑅 ↾s 𝑆))(0g‘𝑅)))
148	53, 111, 107	grpidcld 33689	. . . . . . . . . . 11 ⊢ (𝜑 → (0g‘𝑅) ∈ 𝑉)
149	53, 59, 111, 107, 148	grplidd 19221	. . . . . . . . . 10 ⊢ (𝜑 → ((0g‘𝑅) + (0g‘𝑅)) = (0g‘𝑅))
150	147, 149	eqtr3d 2800	. . . . . . . . 9 ⊢ (𝜑 → ((0g‘𝑅)(+g‘(𝑅 ↾s 𝑆))(0g‘𝑅)) = (0g‘𝑅))
151	106, 144, 150	3eqtrd 2802	. . . . . . . 8 ⊢ (𝜑 → ((coe1‘((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵)))‘2) = (0g‘𝑅))
152	103, 151	oveq12d 7467	. . . . . . 7 ⊢ (𝜑 → (((coe1‘(2(.g‘(mulGrp‘𝑃))(var1‘𝑅)))‘2)(-g‘(𝑅 ↾s 𝑆))((coe1‘((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵)))‘2)) = ((1r‘𝑅)(-g‘(𝑅 ↾s 𝑆))(0g‘𝑅)))
153		eqid 2763	. . . . . . . . 9 ⊢ (-g‘𝑅) = (-g‘𝑅)
154	153, 2, 76	subgsub 19390	. . . . . . . 8 ⊢ ((𝑆 ∈ (SubGrp‘𝑅) ∧ (1r‘𝑅) ∈ 𝑆 ∧ (0g‘𝑅) ∈ 𝑆) → ((1r‘𝑅)(-g‘𝑅)(0g‘𝑅)) = ((1r‘𝑅)(-g‘(𝑅 ↾s 𝑆))(0g‘𝑅)))
155	110, 96, 113, 154	syl3anc 1399	. . . . . . 7 ⊢ (𝜑 → ((1r‘𝑅)(-g‘𝑅)(0g‘𝑅)) = ((1r‘𝑅)(-g‘(𝑅 ↾s 𝑆))(0g‘𝑅)))
156	53, 85, 52	ringidcld 20537	. . . . . . . 8 ⊢ (𝜑 → (1r‘𝑅) ∈ 𝑉)
157	53, 111, 153	grpsubid1 19276	. . . . . . . 8 ⊢ ((𝑅 ∈ Grp ∧ (1r‘𝑅) ∈ 𝑉) → ((1r‘𝑅)(-g‘𝑅)(0g‘𝑅)) = (1r‘𝑅))
158	107, 156, 157	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → ((1r‘𝑅)(-g‘𝑅)(0g‘𝑅)) = (1r‘𝑅))
159	152, 155, 158	3eqtr2d 2804	. . . . . 6 ⊢ (𝜑 → (((coe1‘(2(.g‘(mulGrp‘𝑃))(var1‘𝑅)))‘2)(-g‘(𝑅 ↾s 𝑆))((coe1‘((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵)))‘2)) = (1r‘𝑅))
160	75, 78, 159	3eqtrd 2802	. . . . 5 ⊢ (𝜑 → ((coe1‘𝐺)‘(𝐷‘𝐺)) = (1r‘𝑅))
161		eqid 2763	. . . . . 6 ⊢ (Monic1p‘𝑅) = (Monic1p‘𝑅)
162	45, 48, 69, 63, 161, 85	ismon1p 26505	. . . . 5 ⊢ (𝐺 ∈ (Monic1p‘𝑅) ↔ (𝐺 ∈ (Base‘(Poly1‘𝑅)) ∧ 𝐺 ≠ (0g‘(Poly1‘𝑅)) ∧ ((coe1‘𝐺)‘(𝐷‘𝐺)) = (1r‘𝑅)))
163	51, 72, 160, 162	syl3anbrc 1362	. . . 4 ⊢ (𝜑 → 𝐺 ∈ (Monic1p‘𝑅))
164	44, 163	elind 4100	. . 3 ⊢ (𝜑 → 𝐺 ∈ (𝑈 ∩ (Monic1p‘𝑅)))
165		eqid 2763	. . . 4 ⊢ (Monic1p‘(𝑅 ↾s 𝑆)) = (Monic1p‘(𝑅 ↾s 𝑆))
166	45, 2, 8, 6, 1, 161, 165	ressply1mon1p 34196	. . 3 ⊢ (𝜑 → (Monic1p‘(𝑅 ↾s 𝑆)) = (𝑈 ∩ (Monic1p‘𝑅)))
167	164, 166	eleqtrrd 2867	. 2 ⊢ (𝜑 → 𝐺 ∈ (Monic1p‘(𝑅 ↾s 𝑆)))
168		eqid 2763	. . 3 ⊢ (Unic1p‘(𝑅 ↾s 𝑆)) = (Unic1p‘(𝑅 ↾s 𝑆))
169	168, 165	mon1puc1p 26513	. 2 ⊢ (((𝑅 ↾s 𝑆) ∈ Ring ∧ 𝐺 ∈ (Monic1p‘(𝑅 ↾s 𝑆))) → 𝐺 ∈ (Unic1p‘(𝑅 ↾s 𝑆)))
170	4, 167, 169	syl2anc 596	1 ⊢ (𝜑 → 𝐺 ∈ (Unic1p‘(𝑅 ↾s 𝑆)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147   ≠ wne 2959  Vcvv 3454   ⊆ wss 3900   ∩ cin 4092   ∪ cun 4152  ifcif 4485  {csn 4588   ↦ cmpt 5190  ‘cfv 6564  (class class class)co 7449  0cc0 11237  1c1 11238  2c2 12435  ℕ₀cn0 12644  Basecbs 17428   ↾_s cress 17449  +_gcplusg 17469  ._rcmulr 17470  Scalarcsca 17472   ·_𝑠 cvsca 17473  0_gc0g 17651  Mndcmnd 18964  Grpcgrp 19185  -_gcsg 19187  ._gcmg 19318  SubGrpcsubg 19371  mulGrpcmgp 20402  1_rcur 20449  Ringcrg 20501  CRingccrg 20502  NzRingcnzr 20804  SubRingcsubrg 20863  RingSpancrgspn 20904  LModclmod 21177  algSccascl 22204  PwSer₁cps1 22537  var₁cv1 22538  Poly₁cpl1 22539  coe₁cco1 22540   evalSub₁ ces1 22675  deg₁cdg1 26416  Monic_1pcmn1 26488  Unic_1pcuc1p 26489  rem_1pcr1p 26491

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5236  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7781  ax-cnex 11293  ax-resscn 11294  ax-1cn 11295  ax-icn 11296  ax-addcl 11297  ax-addrcl 11298  ax-mulcl 11299  ax-mulrcl 11300  ax-mulcom 11301  ax-addass 11302  ax-mulass 11303  ax-distr 11304  ax-i2m1 11305  ax-1ne0 11306  ax-1rid 11307  ax-rnegex 11308  ax-rrecex 11309  ax-cnre 11310  ax-pre-lttri 11311  ax-pre-lttrn 11312  ax-pre-ltadd 11313  ax-pre-mulgt0 11314  ax-pre-sup 11315  ax-addf 11316

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-iin 4957  df-br 5107  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5551  df-eprel 5556  df-po 5564  df-so 5565  df-fr 5609  df-se 5610  df-we 5611  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-pred 6328  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6518  df-fun 6566  df-fn 6567  df-f 6568  df-f1 6569  df-fo 6570  df-f1o 6571  df-fv 6572  df-isom 6573  df-riota 7406  df-ov 7452  df-oprab 7453  df-mpo 7454  df-of 7723  df-ofr 7724  df-om 7910  df-1st 8033  df-2nd 8034  df-supp 8213  df-tpos 8279  df-frecs 8335  df-wrecs 8366  df-recs 8415  df-rdg 8454  df-1o 8512  df-2o 8513  df-er 8753  df-map 8885  df-pm 8886  df-ixp 8962  df-en 9010  df-dom 9011  df-sdom 9012  df-fin 9013  df-fsupp 9390  df-sup 9469  df-oi 9539  df-card 10055  df-pnf 11382  df-mnf 11383  df-xr 11384  df-ltxr 11385  df-le 11386  df-sub 11580  df-neg 11581  df-nn 12374  df-2 12443  df-3 12444  df-4 12445  df-5 12446  df-6 12447  df-7 12448  df-8 12449  df-9 12450  df-n0 12645  df-z 12732  df-dec 12853  df-uz 13004  df-fz 13678  df-fzo 13827  df-seq 14183  df-hash 14514  df-struct 17366  df-sets 17383  df-slot 17401  df-ndx 17413  df-base 17429  df-ress 17450  df-plusg 17482  df-mulr 17483  df-starv 17484  df-sca 17485  df-vsca 17486  df-ip 17487  df-tset 17488  df-ple 17489  df-ds 17491  df-unif 17492  df-hom 17493  df-cco 17494  df-0g 17653  df-gsum 17654  df-prds 17659  df-pws 17661  df-mre 17797  df-mrc 17798  df-acs 17800  df-mgm 18857  df-sgrp 18949  df-mnd 18965  df-mhm 19019  df-submnd 19020  df-grp 19188  df-minusg 19189  df-sbg 19190  df-mulg 19319  df-subg 19374  df-ghm 19469  df-cntz 19573  df-cmn 20038  df-abl 20039  df-mgp 20403  df-rng 20417  df-ur 20450  df-ring 20503  df-cring 20504  df-oppr 20609  df-dvdsr 20629  df-unit 20630  df-invr 20660  df-nzr 20805  df-subrng 20840  df-subrg 20864  df-rlreg 20988  df-lmod 21179  df-lss 21249  df-cnfld 21721  df-ascl 22207  df-psr 22261  df-mvr 22262  df-mpl 22263  df-opsr 22265  df-psr1 22542  df-vr1 22543  df-ply1 22544  df-coe1 22545  df-mdeg 26417  df-deg1 26418  df-mon1 26493  df-uc1p 26494

This theorem is used by:  rngunsnply1chr2lem3  34245  rngunsnply1chr2  34246