rngunsnply1chr2lem3

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

	Ref	Expression
Hypotheses	rngunsnply1chr2.v	$⊢ V = {Base}_{R}$
	rngunsnply1chr2.p	$⊢ P = {Poly}_{1} (R ↾_{𝑠} S)$
	rngunsnply1chr2.u	$⊢ U = {Base}_{P}$
	rngunsnply1chr2.q	$⊢ Q = R {evalSub}_{1} S$
	rngunsnply1chr2.r	$⊢ φ \to R \in CRing$
	rngunsnply1chr2.1	$⊢ φ \to R \in NzRing$
	rngunsnply1chr2.s	$⊢ φ \to S \in SubRing (R)$
	rngunsnply1chr2.x	$⊢ φ \to X \in V$
	rngunsnply1chr2.y	$⊢ φ \to Y \in N (S \cup \{X\})$
	rngunsnply1chr2.n	$⊢ N = RingSpan (R)$
	rngunsnply1chr2.2	$⊢ \underset{˙}{+} = +_{R}$
	rngunsnply1chr2.3	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	rngunsnply1chr2.4	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{R}}$
	rngunsnply1chr2.a	$⊢ φ \to A \in S$
	rngunsnply1chr2.b	$⊢ φ \to B \in S$
	rngunsnply1chr2.5	$⊢ φ \to 2 \underset{˙}{\times} X = (A \underset{˙}{\cdot} X) \underset{˙}{+} B$
	rngunsnply1chr2lem.d	$⊢ D = \deg_{1} (R)$
	rngunsnply1chr2lem.e	$⊢ E = {rem}_{1p} (R ↾_{𝑠} S)$
	rngunsnply1chr2lem.g	$⊢ G = (2 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) -_{P} ((A \cdot_{P} {var}_{1} (R)) +_{P} algSc (P) (B))$
	rngunsnply1chr2lem.h	$⊢ H = F E G$
	rngunsnply1chr2lem.f	$⊢ φ \to F \in U$
Assertion	rngunsnply1chr2lem3	$⊢ φ \to (D (H) \leq 1 \land Q (H) (X) = Q (F) (X))$

Proof

Step	Hyp	Ref	Expression
1		rngunsnply1chr2.v	$⊢ V = {Base}_{R}$
2		rngunsnply1chr2.p	$⊢ P = {Poly}_{1} (R ↾_{𝑠} S)$
3		rngunsnply1chr2.u	$⊢ U = {Base}_{P}$
4		rngunsnply1chr2.q	$⊢ Q = R {evalSub}_{1} S$
5		rngunsnply1chr2.r	$⊢ φ \to R \in CRing$
6		rngunsnply1chr2.1	$⊢ φ \to R \in NzRing$
7		rngunsnply1chr2.s	$⊢ φ \to S \in SubRing (R)$
8		rngunsnply1chr2.x	$⊢ φ \to X \in V$
9		rngunsnply1chr2.y	$⊢ φ \to Y \in N (S \cup \{X\})$
10		rngunsnply1chr2.n	$⊢ N = RingSpan (R)$
11		rngunsnply1chr2.2	$⊢ \underset{˙}{+} = +_{R}$
12		rngunsnply1chr2.3	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
13		rngunsnply1chr2.4	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{R}}$
14		rngunsnply1chr2.a	$⊢ φ \to A \in S$
15		rngunsnply1chr2.b	$⊢ φ \to B \in S$
16		rngunsnply1chr2.5	$⊢ φ \to 2 \underset{˙}{\times} X = (A \underset{˙}{\cdot} X) \underset{˙}{+} B$
17		rngunsnply1chr2lem.d	$⊢ D = \deg_{1} (R)$
18		rngunsnply1chr2lem.e	$⊢ E = {rem}_{1p} (R ↾_{𝑠} S)$
19		rngunsnply1chr2lem.g	$⊢ G = (2 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) -_{P} ((A \cdot_{P} {var}_{1} (R)) +_{P} algSc (P) (B))$
20		rngunsnply1chr2lem.h	$⊢ H = F E G$
21		rngunsnply1chr2lem.f	$⊢ φ \to F \in U$
22	20	fveq2i	$⊢ D (H) = D (F E G)$
23		eqid	$⊢ R ↾_{𝑠} S = R ↾_{𝑠} S$
24	23	subrgring	$⊢ S \in SubRing (R) \to R ↾_{𝑠} S \in Ring$
25	7 24	syl	$⊢ φ \to R ↾_{𝑠} S \in Ring$
26	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21	rngunsnply1chr2lem2	$⊢ φ \to G \in {Unic}_{1p} (R ↾_{𝑠} S)$
27		eqid	$⊢ {Unic}_{1p} (R ↾_{𝑠} S) = {Unic}_{1p} (R ↾_{𝑠} S)$
28	18 2 3 27	r1pcl	$⊢ (R ↾_{𝑠} S \in Ring \land F \in U \land G \in {Unic}_{1p} (R ↾_{𝑠} S)) \to F E G \in U$
29	25 21 26 28	syl3anc	$⊢ φ \to F E G \in U$
30	23 17 2 3 29 7	ressdeg1	$⊢ φ \to D (F E G) = \deg_{1} (R ↾_{𝑠} S) (F E G)$
31	22 30	eqtrid	$⊢ φ \to D (H) = \deg_{1} (R ↾_{𝑠} S) (F E G)$
32		simpr	$⊢ (φ \land \deg_{1} (R ↾_{𝑠} S) (F E G) \in ℕ_{0}) \to \deg_{1} (R ↾_{𝑠} S) (F E G) \in ℕ_{0}$
33		1nn0	$⊢ 1 \in ℕ_{0}$
34	33	a1i	$⊢ (φ \land \deg_{1} (R ↾_{𝑠} S) (F E G) \in ℕ_{0}) \to 1 \in ℕ_{0}$
35		eqid	$⊢ \deg_{1} (R ↾_{𝑠} S) = \deg_{1} (R ↾_{𝑠} S)$
36	18 2 3 27 35	r1pdeglt	$⊢ (R ↾_{𝑠} S \in Ring \land F \in U \land G \in {Unic}_{1p} (R ↾_{𝑠} S)) \to \deg_{1} (R ↾_{𝑠} S) (F E G) < \deg_{1} (R ↾_{𝑠} S) (G)$
37	25 21 26 36	syl3anc	$⊢ φ \to \deg_{1} (R ↾_{𝑠} S) (F E G) < \deg_{1} (R ↾_{𝑠} S) (G)$
38	37	adantr	$⊢ (φ \land \deg_{1} (R ↾_{𝑠} S) (F E G) \in ℕ_{0}) \to \deg_{1} (R ↾_{𝑠} S) (F E G) < \deg_{1} (R ↾_{𝑠} S) (G)$
39		1p1e2	$⊢ 1 + 1 = 2$
40	2 3 27	uc1pcl	$⊢ G \in {Unic}_{1p} (R ↾_{𝑠} S) \to G \in U$
41	26 40	syl	$⊢ φ \to G \in U$
42	23 17 2 3 41 7	ressdeg1	$⊢ φ \to D (G) = \deg_{1} (R ↾_{𝑠} S) (G)$
43	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21	rngunsnply1chr2lem1	$⊢ φ \to D (G) = 2$
44	42 43	eqtr3d	$⊢ φ \to \deg_{1} (R ↾_{𝑠} S) (G) = 2$
45	39 44	eqtr4id	$⊢ φ \to 1 + 1 = \deg_{1} (R ↾_{𝑠} S) (G)$
46	45	adantr	$⊢ (φ \land \deg_{1} (R ↾_{𝑠} S) (F E G) \in ℕ_{0}) \to 1 + 1 = \deg_{1} (R ↾_{𝑠} S) (G)$
47	38 46	breqtrrd	$⊢ (φ \land \deg_{1} (R ↾_{𝑠} S) (F E G) \in ℕ_{0}) \to \deg_{1} (R ↾_{𝑠} S) (F E G) < 1 + 1$
48		nn0leltp1	$⊢ (\deg_{1} (R ↾_{𝑠} S) (F E G) \in ℕ_{0} \land 1 \in ℕ_{0}) \to (\deg_{1} (R ↾_{𝑠} S) (F E G) \leq 1 \leftrightarrow \deg_{1} (R ↾_{𝑠} S) (F E G) < 1 + 1)$
49	48	biimpar	$⊢ ((\deg_{1} (R ↾_{𝑠} S) (F E G) \in ℕ_{0} \land 1 \in ℕ_{0}) \land \deg_{1} (R ↾_{𝑠} S) (F E G) < 1 + 1) \to \deg_{1} (R ↾_{𝑠} S) (F E G) \leq 1$
50	32 34 47 49	syl21anc	$⊢ (φ \land \deg_{1} (R ↾_{𝑠} S) (F E G) \in ℕ_{0}) \to \deg_{1} (R ↾_{𝑠} S) (F E G) \leq 1$
51		simpr	$⊢ (φ \land \deg_{1} (R ↾_{𝑠} S) (F E G) = −∞) \to \deg_{1} (R ↾_{𝑠} S) (F E G) = −∞$
52		1xr	$⊢ 1 \in ℝ^{*}$
53		mnfle	$⊢ 1 \in ℝ^{*} \to −∞ \leq 1$
54	52 53	ax-mp	$⊢ −∞ \leq 1$
55	51 54	eqbrtrdi	$⊢ (φ \land \deg_{1} (R ↾_{𝑠} S) (F E G) = −∞) \to \deg_{1} (R ↾_{𝑠} S) (F E G) \leq 1$
56	35 2 3	deg1cl	$⊢ F E G \in U \to \deg_{1} (R ↾_{𝑠} S) (F E G) \in (ℕ_{0} \cup \{−∞\})$
57	29 56	syl	$⊢ φ \to \deg_{1} (R ↾_{𝑠} S) (F E G) \in (ℕ_{0} \cup \{−∞\})$
58		fvex	$⊢ \deg_{1} (R ↾_{𝑠} S) (F E G) \in V$
59		elunsn	$⊢ \deg_{1} (R ↾_{𝑠} S) (F E G) \in V \to (\deg_{1} (R ↾_{𝑠} S) (F E G) \in (ℕ_{0} \cup \{−∞\}) \leftrightarrow (\deg_{1} (R ↾_{𝑠} S) (F E G) \in ℕ_{0} \lor \deg_{1} (R ↾_{𝑠} S) (F E G) = −∞))$
60	58 59	ax-mp	$⊢ \deg_{1} (R ↾_{𝑠} S) (F E G) \in (ℕ_{0} \cup \{−∞\}) \leftrightarrow (\deg_{1} (R ↾_{𝑠} S) (F E G) \in ℕ_{0} \lor \deg_{1} (R ↾_{𝑠} S) (F E G) = −∞)$
61	57 60	sylib	$⊢ φ \to (\deg_{1} (R ↾_{𝑠} S) (F E G) \in ℕ_{0} \lor \deg_{1} (R ↾_{𝑠} S) (F E G) = −∞)$
62	50 55 61	mpjaodan	$⊢ φ \to \deg_{1} (R ↾_{𝑠} S) (F E G) \leq 1$
63	31 62	eqbrtrd	$⊢ φ \to D (H) \leq 1$
64		eqid	$⊢ +_{P} = +_{P}$
65		eqid	$⊢ \cdot_{P} = \cdot_{P}$
66	2	ply1ring	$⊢ R ↾_{𝑠} S \in Ring \to P \in Ring$
67	25 66	syl	$⊢ φ \to P \in Ring$
68		eqid	$⊢ {quot}_{1p} (R ↾_{𝑠} S) = {quot}_{1p} (R ↾_{𝑠} S)$
69	68 2 3 27	q1pcl	$⊢ (R ↾_{𝑠} S \in Ring \land F \in U \land G \in {Unic}_{1p} (R ↾_{𝑠} S)) \to F {quot}_{1p} (R ↾_{𝑠} S) G \in U$
70	25 21 26 69	syl3anc	$⊢ φ \to F {quot}_{1p} (R ↾_{𝑠} S) G \in U$
71	3 65 67 70 41	ringcld	$⊢ φ \to (F {quot}_{1p} (R ↾_{𝑠} S) G) \cdot_{P} G \in U$
72	4 1 2 23 3 64 11 5 7 71 29 8	evls1addd	$⊢ φ \to Q (((F {quot}_{1p} (R ↾_{𝑠} S) G) \cdot_{P} G) +_{P} (F E G)) (X) = Q ((F {quot}_{1p} (R ↾_{𝑠} S) G) \cdot_{P} G) (X) \underset{˙}{+} Q (F E G) (X)$
73	4 1 2 23 3 65 12 5 7 70 41 8	evls1muld	$⊢ φ \to Q ((F {quot}_{1p} (R ↾_{𝑠} S) G) \cdot_{P} G) (X) = Q (F {quot}_{1p} (R ↾_{𝑠} S) G) (X) \underset{˙}{\cdot} Q (G) (X)$
74	19	fveq2i	$⊢ Q (G) = Q ((2 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) -_{P} ((A \cdot_{P} {var}_{1} (R)) +_{P} algSc (P) (B)))$
75	74	fveq1i	$⊢ Q (G) (X) = Q ((2 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) -_{P} ((A \cdot_{P} {var}_{1} (R)) +_{P} algSc (P) (B))) (X)$
76	75	a1i	$⊢ φ \to Q (G) (X) = Q ((2 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) -_{P} ((A \cdot_{P} {var}_{1} (R)) +_{P} algSc (P) (B))) (X)$
77		eqid	$⊢ -_{P} = -_{P}$
78		eqid	$⊢ -_{R} = -_{R}$
79		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
80	79 3	mgpbas	$⊢ U = {Base}_{{mulGrp}_{P}}$
81		eqid	$⊢ \cdot_{{mulGrp}_{P}} = \cdot_{{mulGrp}_{P}}$
82	79	ringmgp	$⊢ P \in Ring \to {mulGrp}_{P} \in Mnd$
83	67 82	syl	$⊢ φ \to {mulGrp}_{P} \in Mnd$
84		2nn0	$⊢ 2 \in ℕ_{0}$
85	84	a1i	$⊢ φ \to 2 \in ℕ_{0}$
86		eqid	$⊢ {var}_{1} (R) = {var}_{1} (R)$
87	86 7 23 2 3	subrgvr1cl	$⊢ φ \to {var}_{1} (R) \in U$
88	80 81 83 85 87	mulgnn0cld	$⊢ φ \to 2 \cdot_{{mulGrp}_{P}} {var}_{1} (R) \in U$
89	67	ringgrpd	$⊢ φ \to P \in Grp$
90		eqid	$⊢ Scalar (P) = Scalar (P)$
91		eqid	$⊢ \cdot_{P} = \cdot_{P}$
92		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
93	2	ply1lmod	$⊢ R ↾_{𝑠} S \in Ring \to P \in LMod$
94	25 93	syl	$⊢ φ \to P \in LMod$
95	23	subrgbas	$⊢ S \in SubRing (R) \to S = {Base}_{(R ↾_{𝑠} S)}$
96	7 95	syl	$⊢ φ \to S = {Base}_{(R ↾_{𝑠} S)}$
97		ovex	$⊢ R ↾_{𝑠} S \in V$
98	2	ply1sca	$⊢ R ↾_{𝑠} S \in V \to R ↾_{𝑠} S = Scalar (P)$
99	97 98	ax-mp	$⊢ R ↾_{𝑠} S = Scalar (P)$
100	99	fveq2i	$⊢ {Base}_{(R ↾_{𝑠} S)} = {Base}_{Scalar (P)}$
101	96 100	eqtrdi	$⊢ φ \to S = {Base}_{Scalar (P)}$
102	14 101	eleqtrd	$⊢ φ \to A \in {Base}_{Scalar (P)}$
103	3 90 91 92 94 102 87	lmodvscld	$⊢ φ \to A \cdot_{P} {var}_{1} (R) \in U$
104		eqid	$⊢ algSc (P) = algSc (P)$
105	2 23 104 3 5 7 15	ressasclcl	$⊢ φ \to algSc (P) (B) \in U$
106	3 64 89 103 105	grpcld	$⊢ φ \to (A \cdot_{P} {var}_{1} (R)) +_{P} algSc (P) (B) \in U$
107	4 1 2 23 3 77 78 5 7 88 106 8	evls1subd	$⊢ φ \to Q ((2 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) -_{P} ((A \cdot_{P} {var}_{1} (R)) +_{P} algSc (P) (B))) (X) = Q (2 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) (X) -_{R} Q ((A \cdot_{P} {var}_{1} (R)) +_{P} algSc (P) (B)) (X)$
108	4 1 2 23 3 5 7 81 13 85 87 8	evls1expd	$⊢ φ \to Q (2 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) (X) = 2 \underset{˙}{\times} Q ({var}_{1} (R)) (X)$
109	86 7 23	subrgvr1	$⊢ φ \to {var}_{1} (R) = {var}_{1} (R ↾_{𝑠} S)$
110	109	fveq2d	$⊢ φ \to Q ({var}_{1} (R)) = Q ({var}_{1} (R ↾_{𝑠} S))$
111	110	fveq1d	$⊢ φ \to Q ({var}_{1} (R)) (X) = Q ({var}_{1} (R ↾_{𝑠} S)) (X)$
112		eqid	$⊢ {var}_{1} (R ↾_{𝑠} S) = {var}_{1} (R ↾_{𝑠} S)$
113	4 112 23 1 5 7	evls1var	$⊢ φ \to Q ({var}_{1} (R ↾_{𝑠} S)) = {I ↾}_{V}$
114	113	fveq1d	$⊢ φ \to Q ({var}_{1} (R ↾_{𝑠} S)) (X) = ({I ↾}_{V}) (X)$
115		fvresi	$⊢ X \in V \to ({I ↾}_{V}) (X) = X$
116	8 115	syl	$⊢ φ \to ({I ↾}_{V}) (X) = X$
117	111 114 116	3eqtrd	$⊢ φ \to Q ({var}_{1} (R)) (X) = X$
118	117	oveq2d	$⊢ φ \to 2 \underset{˙}{\times} Q ({var}_{1} (R)) (X) = 2 \underset{˙}{\times} X$
119	108 118	eqtrd	$⊢ φ \to Q (2 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) (X) = 2 \underset{˙}{\times} X$
120	4 1 2 23 3 64 11 5 7 103 105 8	evls1addd	$⊢ φ \to Q ((A \cdot_{P} {var}_{1} (R)) +_{P} algSc (P) (B)) (X) = Q (A \cdot_{P} {var}_{1} (R)) (X) \underset{˙}{+} Q (algSc (P) (B)) (X)$
121	4 1 2 23 3 91 12 5 7 14 87 8	evls1vsca	$⊢ φ \to Q (A \cdot_{P} {var}_{1} (R)) (X) = A \underset{˙}{\cdot} Q ({var}_{1} (R)) (X)$
122	117	oveq2d	$⊢ φ \to A \underset{˙}{\cdot} Q ({var}_{1} (R)) (X) = A \underset{˙}{\cdot} X$
123	121 122	eqtrd	$⊢ φ \to Q (A \cdot_{P} {var}_{1} (R)) (X) = A \underset{˙}{\cdot} X$
124	4 2 23 1 104 5 7 15 8	evls1scafv	$⊢ φ \to Q (algSc (P) (B)) (X) = B$
125	123 124	oveq12d	$⊢ φ \to Q (A \cdot_{P} {var}_{1} (R)) (X) \underset{˙}{+} Q (algSc (P) (B)) (X) = (A \underset{˙}{\cdot} X) \underset{˙}{+} B$
126	120 125	eqtrd	$⊢ φ \to Q ((A \cdot_{P} {var}_{1} (R)) +_{P} algSc (P) (B)) (X) = (A \underset{˙}{\cdot} X) \underset{˙}{+} B$
127	119 126	oveq12d	$⊢ φ \to Q (2 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) (X) -_{R} Q ((A \cdot_{P} {var}_{1} (R)) +_{P} algSc (P) (B)) (X) = (2 \underset{˙}{\times} X) -_{R} ((A \underset{˙}{\cdot} X) \underset{˙}{+} B)$
128	5	crnggrpd	$⊢ φ \to R \in Grp$
129		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
130	129 1	mgpbas	$⊢ V = {Base}_{{mulGrp}_{R}}$
131	5	crngringd	$⊢ φ \to R \in Ring$
132	129	ringmgp	$⊢ R \in Ring \to {mulGrp}_{R} \in Mnd$
133	131 132	syl	$⊢ φ \to {mulGrp}_{R} \in Mnd$
134	130 13 133 85 8	mulgnn0cld	$⊢ φ \to 2 \underset{˙}{\times} X \in V$
135	16 134	eqeltrrd	$⊢ φ \to (A \underset{˙}{\cdot} X) \underset{˙}{+} B \in V$
136		eqid	$⊢ 0_{R} = 0_{R}$
137	1 136 78	grpsubeq0	$⊢ (R \in Grp \land 2 \underset{˙}{\times} X \in V \land (A \underset{˙}{\cdot} X) \underset{˙}{+} B \in V) \to ((2 \underset{˙}{\times} X) -_{R} ((A \underset{˙}{\cdot} X) \underset{˙}{+} B) = 0_{R} \leftrightarrow 2 \underset{˙}{\times} X = (A \underset{˙}{\cdot} X) \underset{˙}{+} B)$
138	137	biimpar	$⊢ ((R \in Grp \land 2 \underset{˙}{\times} X \in V \land (A \underset{˙}{\cdot} X) \underset{˙}{+} B \in V) \land 2 \underset{˙}{\times} X = (A \underset{˙}{\cdot} X) \underset{˙}{+} B) \to (2 \underset{˙}{\times} X) -_{R} ((A \underset{˙}{\cdot} X) \underset{˙}{+} B) = 0_{R}$
139	128 134 135 16 138	syl31anc	$⊢ φ \to (2 \underset{˙}{\times} X) -_{R} ((A \underset{˙}{\cdot} X) \underset{˙}{+} B) = 0_{R}$
140	127 139	eqtrd	$⊢ φ \to Q (2 \cdot_{{mulGrp}_{P}} {var}_{1} (R)) (X) -_{R} Q ((A \cdot_{P} {var}_{1} (R)) +_{P} algSc (P) (B)) (X) = 0_{R}$
141	76 107 140	3eqtrd	$⊢ φ \to Q (G) (X) = 0_{R}$
142	141	oveq2d	$⊢ φ \to Q (F {quot}_{1p} (R ↾_{𝑠} S) G) (X) \underset{˙}{\cdot} Q (G) (X) = Q (F {quot}_{1p} (R ↾_{𝑠} S) G) (X) \underset{˙}{\cdot} 0_{R}$
143	4 2 1 3 5 7 8 70	evls1fvcl	$⊢ φ \to Q (F {quot}_{1p} (R ↾_{𝑠} S) G) (X) \in V$
144	1 12 136 131 143	ringrzd	$⊢ φ \to Q (F {quot}_{1p} (R ↾_{𝑠} S) G) (X) \underset{˙}{\cdot} 0_{R} = 0_{R}$
145	73 142 144	3eqtrd	$⊢ φ \to Q ((F {quot}_{1p} (R ↾_{𝑠} S) G) \cdot_{P} G) (X) = 0_{R}$
146	145	oveq1d	$⊢ φ \to Q ((F {quot}_{1p} (R ↾_{𝑠} S) G) \cdot_{P} G) (X) \underset{˙}{+} Q (F E G) (X) = 0_{R} \underset{˙}{+} Q (F E G) (X)$
147	4 2 1 3 5 7 8 29	evls1fvcl	$⊢ φ \to Q (F E G) (X) \in V$
148	1 11 136 128 147	grplidd	$⊢ φ \to 0_{R} \underset{˙}{+} Q (F E G) (X) = Q (F E G) (X)$
149	72 146 148	3eqtrd	$⊢ φ \to Q (((F {quot}_{1p} (R ↾_{𝑠} S) G) \cdot_{P} G) +_{P} (F E G)) (X) = Q (F E G) (X)$
150	2 3 27 68 18 65 64	r1pid	$⊢ (R ↾_{𝑠} S \in Ring \land F \in U \land G \in {Unic}_{1p} (R ↾_{𝑠} S)) \to F = ((F {quot}_{1p} (R ↾_{𝑠} S) G) \cdot_{P} G) +_{P} (F E G)$
151	25 21 26 150	syl3anc	$⊢ φ \to F = ((F {quot}_{1p} (R ↾_{𝑠} S) G) \cdot_{P} G) +_{P} (F E G)$
152	151	fveq2d	$⊢ φ \to Q (F) = Q (((F {quot}_{1p} (R ↾_{𝑠} S) G) \cdot_{P} G) +_{P} (F E G))$
153	152	fveq1d	$⊢ φ \to Q (F) (X) = Q (((F {quot}_{1p} (R ↾_{𝑠} S) G) \cdot_{P} G) +_{P} (F E G)) (X)$
154	20	fveq2i	$⊢ Q (H) = Q (F E G)$
155	154	fveq1i	$⊢ Q (H) (X) = Q (F E G) (X)$
156	155	a1i	$⊢ φ \to Q (H) (X) = Q (F E G) (X)$
157	149 153 156	3eqtr4rd	$⊢ φ \to Q (H) (X) = Q (F) (X)$
158	63 157	jca	$⊢ φ \to (D (H) \leq 1 \land Q (H) (X) = Q (F) (X))$

Metamath Proof Explorer

Theorem rngunsnply1chr2lem3

Proof