Theorem rngunsnply1chr2lem3 34245

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
rngunsnply1chr2lem3	⊢ (𝜑 → ((𝐷‘𝐻) ≤ 1 ∧ ((𝑄‘𝐻)‘𝑋) = ((𝑄‘𝐹)‘𝑋)))

Proof of Theorem rngunsnply1chr2lem3

Step	Hyp	Ref	Expression
1		rngunsnply1chr2lem.h	. . . . 5 ⊢ 𝐻 = (𝐹𝐸𝐺)
2	1	fveq2i 6917	. . . 4 ⊢ (𝐷‘𝐻) = (𝐷‘(𝐹𝐸𝐺))
3		eqid 2763	. . . . 5 ⊢ (𝑅 ↾s 𝑆) = (𝑅 ↾s 𝑆)
4		rngunsnply1chr2lem.d	. . . . 5 ⊢ 𝐷 = (deg1‘𝑅)
5		rngunsnply1chr2.p	. . . . 5 ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆))
6		rngunsnply1chr2.u	. . . . 5 ⊢ 𝑈 = (Base‘𝑃)
7		rngunsnply1chr2.s	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))
8	3	subrgring 20868	. . . . . . 7 ⊢ (𝑆 ∈ (SubRing‘𝑅) → (𝑅 ↾s 𝑆) ∈ Ring)
9	7, 8	syl 18	. . . . . 6 ⊢ (𝜑 → (𝑅 ↾s 𝑆) ∈ Ring)
10		rngunsnply1chr2lem.f	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ 𝑈)
11		rngunsnply1chr2.v	. . . . . . 7 ⊢ 𝑉 = (Base‘𝑅)
12		rngunsnply1chr2.q	. . . . . . 7 ⊢ 𝑄 = (𝑅 evalSub1 𝑆)
13		rngunsnply1chr2.r	. . . . . . 7 ⊢ (𝜑 → 𝑅 ∈ CRing)
14		rngunsnply1chr2.1	. . . . . . 7 ⊢ (𝜑 → 𝑅 ∈ NzRing)
15		rngunsnply1chr2.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
16		rngunsnply1chr2.y	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑋})))
17		rngunsnply1chr2.n	. . . . . . 7 ⊢ 𝑁 = (RingSpan‘𝑅)
18		rngunsnply1chr2.2	. . . . . . 7 ⊢ + = (+g‘𝑅)
19		rngunsnply1chr2.3	. . . . . . 7 ⊢ · = (.r‘𝑅)
20		rngunsnply1chr2.4	. . . . . . 7 ⊢ ↑ = (.g‘(mulGrp‘𝑅))
21		rngunsnply1chr2.a	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ 𝑆)
22		rngunsnply1chr2.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ 𝑆)
23		rngunsnply1chr2.5	. . . . . . 7 ⊢ (𝜑 → (2 ↑ 𝑋) = ((𝐴 · 𝑋) + 𝐵))
24		rngunsnply1chr2lem.e	. . . . . . 7 ⊢ 𝐸 = (rem1p‘(𝑅 ↾s 𝑆))
25		rngunsnply1chr2lem.g	. . . . . . 7 ⊢ 𝐺 = ((2(.g‘(mulGrp‘𝑃))(var1‘𝑅))(-g‘𝑃)((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵)))
26	11, 5, 6, 12, 13, 14, 7, 15, 16, 17, 18, 19, 20, 21, 22, 23, 4, 24, 25, 1, 10	rngunsnply1chr2lem2 34244	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ (Unic1p‘(𝑅 ↾s 𝑆)))
27		eqid 2763	. . . . . . 7 ⊢ (Unic1p‘(𝑅 ↾s 𝑆)) = (Unic1p‘(𝑅 ↾s 𝑆))
28	24, 5, 6, 27	r1pcl 26521	. . . . . 6 ⊢ (((𝑅 ↾s 𝑆) ∈ Ring ∧ 𝐹 ∈ 𝑈 ∧ 𝐺 ∈ (Unic1p‘(𝑅 ↾s 𝑆))) → (𝐹𝐸𝐺) ∈ 𝑈)
29	9, 10, 26, 28	syl3anc 1399	. . . . 5 ⊢ (𝜑 → (𝐹𝐸𝐺) ∈ 𝑈)
30	3, 4, 5, 6, 29, 7	ressdeg1 34194	. . . 4 ⊢ (𝜑 → (𝐷‘(𝐹𝐸𝐺)) = ((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)))
31	2, 30	eqtrid 2810	. . 3 ⊢ (𝜑 → (𝐷‘𝐻) = ((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)))
32		simpr 490	. . . . 5 ⊢ ((𝜑 ∧ ((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) ∈ ℕ0) → ((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) ∈ ℕ0)
33		1nn0 12660	. . . . . 6 ⊢ 1 ∈ ℕ0
34	33	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ ((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) ∈ ℕ0) → 1 ∈ ℕ0)
35		eqid 2763	. . . . . . . . 9 ⊢ (deg1‘(𝑅 ↾s 𝑆)) = (deg1‘(𝑅 ↾s 𝑆))
36	24, 5, 6, 27, 35	r1pdeglt 26522	. . . . . . . 8 ⊢ (((𝑅 ↾s 𝑆) ∈ Ring ∧ 𝐹 ∈ 𝑈 ∧ 𝐺 ∈ (Unic1p‘(𝑅 ↾s 𝑆))) → ((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) < ((deg1‘(𝑅 ↾s 𝑆))‘𝐺))
37	9, 10, 26, 36	syl3anc 1399	. . . . . . 7 ⊢ (𝜑 → ((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) < ((deg1‘(𝑅 ↾s 𝑆))‘𝐺))
38	37	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ ((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) ∈ ℕ0) → ((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) < ((deg1‘(𝑅 ↾s 𝑆))‘𝐺))
39		1p1e2 12504	. . . . . . . 8 ⊢ (1 + 1) = 2
40	5, 6, 27	uc1pcl 26506	. . . . . . . . . . 11 ⊢ (𝐺 ∈ (Unic1p‘(𝑅 ↾s 𝑆)) → 𝐺 ∈ 𝑈)
41	26, 40	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ 𝑈)
42	3, 4, 5, 6, 41, 7	ressdeg1 34194	. . . . . . . . 9 ⊢ (𝜑 → (𝐷‘𝐺) = ((deg1‘(𝑅 ↾s 𝑆))‘𝐺))
43	11, 5, 6, 12, 13, 14, 7, 15, 16, 17, 18, 19, 20, 21, 22, 23, 4, 24, 25, 1, 10	rngunsnply1chr2lem1 34243	. . . . . . . . 9 ⊢ (𝜑 → (𝐷‘𝐺) = 2)
44	42, 43	eqtr3d 2800	. . . . . . . 8 ⊢ (𝜑 → ((deg1‘(𝑅 ↾s 𝑆))‘𝐺) = 2)
45	39, 44	eqtr4id 2817	. . . . . . 7 ⊢ (𝜑 → (1 + 1) = ((deg1‘(𝑅 ↾s 𝑆))‘𝐺))
46	45	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ ((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) ∈ ℕ0) → (1 + 1) = ((deg1‘(𝑅 ↾s 𝑆))‘𝐺))
47	38, 46	breqtrrd 5137	. . . . 5 ⊢ ((𝜑 ∧ ((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) ∈ ℕ0) → ((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) < (1 + 1))
48		nn0leltp1 12796	. . . . . 6 ⊢ ((((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) ∈ ℕ0 ∧ 1 ∈ ℕ0) → (((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) ≤ 1 ↔ ((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) < (1 + 1)))
49	48	biimpar 483	. . . . 5 ⊢ (((((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) ∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ ((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) < (1 + 1)) → ((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) ≤ 1)
50	32, 34, 47, 49	syl21anc 851	. . . 4 ⊢ ((𝜑 ∧ ((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) ∈ ℕ0) → ((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) ≤ 1)
51		simpr 490	. . . . 5 ⊢ ((𝜑 ∧ ((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) = -∞) → ((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) = -∞)
52		1xr 11405	. . . . . 6 ⊢ 1 ∈ ℝ*
53		mnfle 13302	. . . . . 6 ⊢ (1 ∈ ℝ* → -∞ ≤ 1)
54	52, 53	ax-mp 5	. . . . 5 ⊢ -∞ ≤ 1
55	51, 54	eqbrtrdi 5148	. . . 4 ⊢ ((𝜑 ∧ ((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) = -∞) → ((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) ≤ 1)
56	35, 5, 6	deg1cl 26445	. . . . . 6 ⊢ ((𝐹𝐸𝐺) ∈ 𝑈 → ((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) ∈ (ℕ0 ∪ {-∞}))
57	29, 56	syl 18	. . . . 5 ⊢ (𝜑 → ((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) ∈ (ℕ0 ∪ {-∞}))
58		fvex 6927	. . . . . 6 ⊢ ((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) ∈ V
59		elunsn 4644	. . . . . 6 ⊢ (((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) ∈ V → (((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) ∈ (ℕ0 ∪ {-∞}) ↔ (((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) ∈ ℕ0 ∨ ((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) = -∞)))
60	58, 59	ax-mp 5	. . . . 5 ⊢ (((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) ∈ (ℕ0 ∪ {-∞}) ↔ (((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) ∈ ℕ0 ∨ ((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) = -∞))
61	57, 60	sylib 221	. . . 4 ⊢ (𝜑 → (((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) ∈ ℕ0 ∨ ((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) = -∞))
62	50, 55, 61	mpjaodan 973	. . 3 ⊢ (𝜑 → ((deg1‘(𝑅 ↾s 𝑆))‘(𝐹𝐸𝐺)) ≤ 1)
63	31, 62	eqbrtrd 5131	. 2 ⊢ (𝜑 → (𝐷‘𝐻) ≤ 1)
64		eqid 2763	. . . . 5 ⊢ (+g‘𝑃) = (+g‘𝑃)
65		eqid 2763	. . . . . 6 ⊢ (.r‘𝑃) = (.r‘𝑃)
66	5	ply1ring 22609	. . . . . . 7 ⊢ ((𝑅 ↾s 𝑆) ∈ Ring → 𝑃 ∈ Ring)
67	9, 66	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ Ring)
68		eqid 2763	. . . . . . . 8 ⊢ (quot1p‘(𝑅 ↾s 𝑆)) = (quot1p‘(𝑅 ↾s 𝑆))
69	68, 5, 6, 27	q1pcl 26519	. . . . . . 7 ⊢ (((𝑅 ↾s 𝑆) ∈ Ring ∧ 𝐹 ∈ 𝑈 ∧ 𝐺 ∈ (Unic1p‘(𝑅 ↾s 𝑆))) → (𝐹(quot1p‘(𝑅 ↾s 𝑆))𝐺) ∈ 𝑈)
70	9, 10, 26, 69	syl3anc 1399	. . . . . 6 ⊢ (𝜑 → (𝐹(quot1p‘(𝑅 ↾s 𝑆))𝐺) ∈ 𝑈)
71	6, 65, 67, 70, 41	ringcld 20526	. . . . 5 ⊢ (𝜑 → ((𝐹(quot1p‘(𝑅 ↾s 𝑆))𝐺)(.r‘𝑃)𝐺) ∈ 𝑈)
72	12, 11, 5, 3, 6, 64, 18, 13, 7, 71, 29, 15	evls1addd 22733	. . . 4 ⊢ (𝜑 → ((𝑄‘(((𝐹(quot1p‘(𝑅 ↾s 𝑆))𝐺)(.r‘𝑃)𝐺)(+g‘𝑃)(𝐹𝐸𝐺)))‘𝑋) = (((𝑄‘((𝐹(quot1p‘(𝑅 ↾s 𝑆))𝐺)(.r‘𝑃)𝐺))‘𝑋) + ((𝑄‘(𝐹𝐸𝐺))‘𝑋)))
73	12, 11, 5, 3, 6, 65, 19, 13, 7, 70, 41, 15	evls1muld 22734	. . . . . 6 ⊢ (𝜑 → ((𝑄‘((𝐹(quot1p‘(𝑅 ↾s 𝑆))𝐺)(.r‘𝑃)𝐺))‘𝑋) = (((𝑄‘(𝐹(quot1p‘(𝑅 ↾s 𝑆))𝐺))‘𝑋) · ((𝑄‘𝐺)‘𝑋)))
74	25	fveq2i 6917	. . . . . . . . . 10 ⊢ (𝑄‘𝐺) = (𝑄‘((2(.g‘(mulGrp‘𝑃))(var1‘𝑅))(-g‘𝑃)((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵))))
75	74	fveq1i 6915	. . . . . . . . 9 ⊢ ((𝑄‘𝐺)‘𝑋) = ((𝑄‘((2(.g‘(mulGrp‘𝑃))(var1‘𝑅))(-g‘𝑃)((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵))))‘𝑋)
76	75	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘𝐺)‘𝑋) = ((𝑄‘((2(.g‘(mulGrp‘𝑃))(var1‘𝑅))(-g‘𝑃)((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵))))‘𝑋))
77		eqid 2763	. . . . . . . . 9 ⊢ (-g‘𝑃) = (-g‘𝑃)
78		eqid 2763	. . . . . . . . 9 ⊢ (-g‘𝑅) = (-g‘𝑅)
79		eqid 2763	. . . . . . . . . . 11 ⊢ (mulGrp‘𝑃) = (mulGrp‘𝑃)
80	79, 6	mgpbas 20407	. . . . . . . . . 10 ⊢ 𝑈 = (Base‘(mulGrp‘𝑃))
81		eqid 2763	. . . . . . . . . 10 ⊢ (.g‘(mulGrp‘𝑃)) = (.g‘(mulGrp‘𝑃))
82	79	ringmgp 20507	. . . . . . . . . . 11 ⊢ (𝑃 ∈ Ring → (mulGrp‘𝑃) ∈ Mnd)
83	67, 82	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (mulGrp‘𝑃) ∈ Mnd)
84		2nn0 12661	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ0
85	84	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 2 ∈ ℕ0)
86		eqid 2763	. . . . . . . . . . 11 ⊢ (var1‘𝑅) = (var1‘𝑅)
87	86, 7, 3, 5, 6	subrgvr1cl 22625	. . . . . . . . . 10 ⊢ (𝜑 → (var1‘𝑅) ∈ 𝑈)
88	80, 81, 83, 85, 87	mulgnn0cld 19346	. . . . . . . . 9 ⊢ (𝜑 → (2(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ 𝑈)
89	67	ringgrpd 20511	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ Grp)
90		eqid 2763	. . . . . . . . . . 11 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
91		eqid 2763	. . . . . . . . . . 11 ⊢ ( ·𝑠 ‘𝑃) = ( ·𝑠 ‘𝑃)
92		eqid 2763	. . . . . . . . . . 11 ⊢ (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
93	5	ply1lmod 22613	. . . . . . . . . . . 12 ⊢ ((𝑅 ↾s 𝑆) ∈ Ring → 𝑃 ∈ LMod)
94	9, 93	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ LMod)
95	3	subrgbas 20875	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ (SubRing‘𝑅) → 𝑆 = (Base‘(𝑅 ↾s 𝑆)))
96	7, 95	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 = (Base‘(𝑅 ↾s 𝑆)))
97		ovex 7482	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ↾s 𝑆) ∈ V
98	5	ply1sca 22614	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ↾s 𝑆) ∈ V → (𝑅 ↾s 𝑆) = (Scalar‘𝑃))
99	97, 98	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (𝑅 ↾s 𝑆) = (Scalar‘𝑃)
100	99	fveq2i 6917	. . . . . . . . . . . . 13 ⊢ (Base‘(𝑅 ↾s 𝑆)) = (Base‘(Scalar‘𝑃))
101	96, 100	eqtrdi 2814	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 = (Base‘(Scalar‘𝑃)))
102	21, 101	eleqtrd 2866	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ (Base‘(Scalar‘𝑃)))
103	6, 90, 91, 92, 94, 102, 87	lmodvscld 21196	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴( ·𝑠 ‘𝑃)(var1‘𝑅)) ∈ 𝑈)
104		eqid 2763	. . . . . . . . . . 11 ⊢ (algSc‘𝑃) = (algSc‘𝑃)
105	5, 3, 104, 6, 13, 7, 22	ressasclcl 34199	. . . . . . . . . 10 ⊢ (𝜑 → ((algSc‘𝑃)‘𝐵) ∈ 𝑈)
106	6, 64, 89, 103, 105	grpcld 19199	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵)) ∈ 𝑈)
107	12, 11, 5, 3, 6, 77, 78, 13, 7, 88, 106, 15	evls1subd 34200	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘((2(.g‘(mulGrp‘𝑃))(var1‘𝑅))(-g‘𝑃)((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵))))‘𝑋) = (((𝑄‘(2(.g‘(mulGrp‘𝑃))(var1‘𝑅)))‘𝑋)(-g‘𝑅)((𝑄‘((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵)))‘𝑋)))
108	12, 11, 5, 3, 6, 13, 7, 81, 20, 85, 87, 15	evls1expd 22729	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑄‘(2(.g‘(mulGrp‘𝑃))(var1‘𝑅)))‘𝑋) = (2 ↑ ((𝑄‘(var1‘𝑅))‘𝑋)))
109	86, 7, 3	subrgvr1 22624	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (var1‘𝑅) = (var1‘(𝑅 ↾s 𝑆)))
110	109	fveq2d 6918	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑄‘(var1‘𝑅)) = (𝑄‘(var1‘(𝑅 ↾s 𝑆))))
111	110	fveq1d 6916	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑄‘(var1‘𝑅))‘𝑋) = ((𝑄‘(var1‘(𝑅 ↾s 𝑆)))‘𝑋))
112		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ (var1‘(𝑅 ↾s 𝑆)) = (var1‘(𝑅 ↾s 𝑆))
113	12, 112, 3, 11, 13, 7	evls1var 22700	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑄‘(var1‘(𝑅 ↾s 𝑆))) = ( I ↾ 𝑉))
114	113	fveq1d 6916	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑄‘(var1‘(𝑅 ↾s 𝑆)))‘𝑋) = (( I ↾ 𝑉)‘𝑋))
115		fvresi 7207	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ 𝑉 → (( I ↾ 𝑉)‘𝑋) = 𝑋)
116	15, 115	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (( I ↾ 𝑉)‘𝑋) = 𝑋)
117	111, 114, 116	3eqtrd 2802	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑄‘(var1‘𝑅))‘𝑋) = 𝑋)
118	117	oveq2d 7465	. . . . . . . . . . 11 ⊢ (𝜑 → (2 ↑ ((𝑄‘(var1‘𝑅))‘𝑋)) = (2 ↑ 𝑋))
119	108, 118	eqtrd 2798	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑄‘(2(.g‘(mulGrp‘𝑃))(var1‘𝑅)))‘𝑋) = (2 ↑ 𝑋))
120	12, 11, 5, 3, 6, 64, 18, 13, 7, 103, 105, 15	evls1addd 22733	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑄‘((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵)))‘𝑋) = (((𝑄‘(𝐴( ·𝑠 ‘𝑃)(var1‘𝑅)))‘𝑋) + ((𝑄‘((algSc‘𝑃)‘𝐵))‘𝑋)))
121	12, 11, 5, 3, 6, 91, 19, 13, 7, 21, 87, 15	evls1vsca 22735	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑄‘(𝐴( ·𝑠 ‘𝑃)(var1‘𝑅)))‘𝑋) = (𝐴 · ((𝑄‘(var1‘𝑅))‘𝑋)))
122	117	oveq2d 7465	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 · ((𝑄‘(var1‘𝑅))‘𝑋)) = (𝐴 · 𝑋))
123	121, 122	eqtrd 2798	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑄‘(𝐴( ·𝑠 ‘𝑃)(var1‘𝑅)))‘𝑋) = (𝐴 · 𝑋))
124	12, 5, 3, 11, 104, 13, 7, 22, 15	evls1scafv 22728	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑄‘((algSc‘𝑃)‘𝐵))‘𝑋) = 𝐵)
125	123, 124	oveq12d 7467	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑄‘(𝐴( ·𝑠 ‘𝑃)(var1‘𝑅)))‘𝑋) + ((𝑄‘((algSc‘𝑃)‘𝐵))‘𝑋)) = ((𝐴 · 𝑋) + 𝐵))
126	120, 125	eqtrd 2798	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑄‘((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵)))‘𝑋) = ((𝐴 · 𝑋) + 𝐵))
127	119, 126	oveq12d 7467	. . . . . . . . 9 ⊢ (𝜑 → (((𝑄‘(2(.g‘(mulGrp‘𝑃))(var1‘𝑅)))‘𝑋)(-g‘𝑅)((𝑄‘((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵)))‘𝑋)) = ((2 ↑ 𝑋)(-g‘𝑅)((𝐴 · 𝑋) + 𝐵)))
128	13	crnggrpd 20516	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ Grp)
129		eqid 2763	. . . . . . . . . . . 12 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
130	129, 11	mgpbas 20407	. . . . . . . . . . 11 ⊢ 𝑉 = (Base‘(mulGrp‘𝑅))
131	13	crngringd 20515	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 ∈ Ring)
132	129	ringmgp 20507	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ Ring → (mulGrp‘𝑅) ∈ Mnd)
133	131, 132	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (mulGrp‘𝑅) ∈ Mnd)
134	130, 20, 133, 85, 15	mulgnn0cld 19346	. . . . . . . . . 10 ⊢ (𝜑 → (2 ↑ 𝑋) ∈ 𝑉)
135	23, 134	eqeltrrd 2865	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 · 𝑋) + 𝐵) ∈ 𝑉)
136		eqid 2763	. . . . . . . . . . . 12 ⊢ (0g‘𝑅) = (0g‘𝑅)
137	11, 136, 78	grpsubeq0 19277	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Grp ∧ (2 ↑ 𝑋) ∈ 𝑉 ∧ ((𝐴 · 𝑋) + 𝐵) ∈ 𝑉) → (((2 ↑ 𝑋)(-g‘𝑅)((𝐴 · 𝑋) + 𝐵)) = (0g‘𝑅) ↔ (2 ↑ 𝑋) = ((𝐴 · 𝑋) + 𝐵)))
138	137	biimpar 483	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Grp ∧ (2 ↑ 𝑋) ∈ 𝑉 ∧ ((𝐴 · 𝑋) + 𝐵) ∈ 𝑉) ∧ (2 ↑ 𝑋) = ((𝐴 · 𝑋) + 𝐵)) → ((2 ↑ 𝑋)(-g‘𝑅)((𝐴 · 𝑋) + 𝐵)) = (0g‘𝑅))
139	128, 134, 135, 23, 138	syl31anc 1401	. . . . . . . . 9 ⊢ (𝜑 → ((2 ↑ 𝑋)(-g‘𝑅)((𝐴 · 𝑋) + 𝐵)) = (0g‘𝑅))
140	127, 139	eqtrd 2798	. . . . . . . 8 ⊢ (𝜑 → (((𝑄‘(2(.g‘(mulGrp‘𝑃))(var1‘𝑅)))‘𝑋)(-g‘𝑅)((𝑄‘((𝐴( ·𝑠 ‘𝑃)(var1‘𝑅))(+g‘𝑃)((algSc‘𝑃)‘𝐵)))‘𝑋)) = (0g‘𝑅))
141	76, 107, 140	3eqtrd 2802	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘𝐺)‘𝑋) = (0g‘𝑅))
142	141	oveq2d 7465	. . . . . 6 ⊢ (𝜑 → (((𝑄‘(𝐹(quot1p‘(𝑅 ↾s 𝑆))𝐺))‘𝑋) · ((𝑄‘𝐺)‘𝑋)) = (((𝑄‘(𝐹(quot1p‘(𝑅 ↾s 𝑆))𝐺))‘𝑋) · (0g‘𝑅)))
143	12, 5, 11, 6, 13, 7, 15, 70	evls1fvcl 22737	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘(𝐹(quot1p‘(𝑅 ↾s 𝑆))𝐺))‘𝑋) ∈ 𝑉)
144	11, 19, 136, 131, 143	ringrzd 20569	. . . . . 6 ⊢ (𝜑 → (((𝑄‘(𝐹(quot1p‘(𝑅 ↾s 𝑆))𝐺))‘𝑋) · (0g‘𝑅)) = (0g‘𝑅))
145	73, 142, 144	3eqtrd 2802	. . . . 5 ⊢ (𝜑 → ((𝑄‘((𝐹(quot1p‘(𝑅 ↾s 𝑆))𝐺)(.r‘𝑃)𝐺))‘𝑋) = (0g‘𝑅))
146	145	oveq1d 7464	. . . 4 ⊢ (𝜑 → (((𝑄‘((𝐹(quot1p‘(𝑅 ↾s 𝑆))𝐺)(.r‘𝑃)𝐺))‘𝑋) + ((𝑄‘(𝐹𝐸𝐺))‘𝑋)) = ((0g‘𝑅) + ((𝑄‘(𝐹𝐸𝐺))‘𝑋)))
147	12, 5, 11, 6, 13, 7, 15, 29	evls1fvcl 22737	. . . . 5 ⊢ (𝜑 → ((𝑄‘(𝐹𝐸𝐺))‘𝑋) ∈ 𝑉)
148	11, 18, 136, 128, 147	grplidd 19221	. . . 4 ⊢ (𝜑 → ((0g‘𝑅) + ((𝑄‘(𝐹𝐸𝐺))‘𝑋)) = ((𝑄‘(𝐹𝐸𝐺))‘𝑋))
149	72, 146, 148	3eqtrd 2802	. . 3 ⊢ (𝜑 → ((𝑄‘(((𝐹(quot1p‘(𝑅 ↾s 𝑆))𝐺)(.r‘𝑃)𝐺)(+g‘𝑃)(𝐹𝐸𝐺)))‘𝑋) = ((𝑄‘(𝐹𝐸𝐺))‘𝑋))
150	5, 6, 27, 68, 24, 65, 64	r1pid 26523	. . . . . 6 ⊢ (((𝑅 ↾s 𝑆) ∈ Ring ∧ 𝐹 ∈ 𝑈 ∧ 𝐺 ∈ (Unic1p‘(𝑅 ↾s 𝑆))) → 𝐹 = (((𝐹(quot1p‘(𝑅 ↾s 𝑆))𝐺)(.r‘𝑃)𝐺)(+g‘𝑃)(𝐹𝐸𝐺)))
151	9, 10, 26, 150	syl3anc 1399	. . . . 5 ⊢ (𝜑 → 𝐹 = (((𝐹(quot1p‘(𝑅 ↾s 𝑆))𝐺)(.r‘𝑃)𝐺)(+g‘𝑃)(𝐹𝐸𝐺)))
152	151	fveq2d 6918	. . . 4 ⊢ (𝜑 → (𝑄‘𝐹) = (𝑄‘(((𝐹(quot1p‘(𝑅 ↾s 𝑆))𝐺)(.r‘𝑃)𝐺)(+g‘𝑃)(𝐹𝐸𝐺))))
153	152	fveq1d 6916	. . 3 ⊢ (𝜑 → ((𝑄‘𝐹)‘𝑋) = ((𝑄‘(((𝐹(quot1p‘(𝑅 ↾s 𝑆))𝐺)(.r‘𝑃)𝐺)(+g‘𝑃)(𝐹𝐸𝐺)))‘𝑋))
154	1	fveq2i 6917	. . . . 5 ⊢ (𝑄‘𝐻) = (𝑄‘(𝐹𝐸𝐺))
155	154	fveq1i 6915	. . . 4 ⊢ ((𝑄‘𝐻)‘𝑋) = ((𝑄‘(𝐹𝐸𝐺))‘𝑋)
156	155	a1i 11	. . 3 ⊢ (𝜑 → ((𝑄‘𝐻)‘𝑋) = ((𝑄‘(𝐹𝐸𝐺))‘𝑋))
157	149, 153, 156	3eqtr4rd 2809	. 2 ⊢ (𝜑 → ((𝑄‘𝐻)‘𝑋) = ((𝑄‘𝐹)‘𝑋))
158	63, 157	jca 521	1 ⊢ (𝜑 → ((𝐷‘𝐻) ≤ 1 ∧ ((𝑄‘𝐻)‘𝑋) = ((𝑄‘𝐹)‘𝑋)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  Vcvv 3454   ∪ cun 4152  {csn 4588   class class class wbr 5106   I cid 5550   ↾ cres 5658  ‘cfv 6564  (class class class)co 7449  1c1 11238   + caddc 11240  -∞cmnf 11378  ℝ^*cxr 11379   < clt 11380   ≤ cle 11381  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  mulGrpcmgp 20402  Ringcrg 20501  CRingccrg 20502  NzRingcnzr 20804  SubRingcsubrg 20863  RingSpancrgspn 20904  LModclmod 21177  algSccascl 22204  var₁cv1 22538  Poly₁cpl1 22539   evalSub₁ ces1 22675  deg₁cdg1 26416  Unic_1pcuc1p 26489  quot_1pcq1p 26490  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-srg 20455  df-ring 20503  df-cring 20504  df-oppr 20609  df-dvdsr 20629  df-unit 20630  df-invr 20660  df-rhm 20744  df-nzr 20805  df-subrng 20840  df-subrg 20864  df-rlreg 20988  df-lmod 21179  df-lss 21249  df-lsp 21289  df-cnfld 21721  df-assa 22205  df-asp 22206  df-ascl 22207  df-psr 22261  df-mvr 22262  df-mpl 22263  df-opsr 22265  df-evls 22427  df-evl 22428  df-psr1 22542  df-vr1 22543  df-ply1 22544  df-coe1 22545  df-evls1 22677  df-evl1 22678  df-mdeg 26417  df-deg1 26418  df-mon1 26493  df-uc1p 26494  df-q1p 26495  df-r1p 26496

This theorem is used by:  rngunsnply1chr2  34246