Theorem ressply1sub

Description: A restricted polynomial algebra has the same subtraction operation. (Contributed by Thierry Arnoux, 30-Jan-2025)

	Ref	Expression
Hypotheses	ressply.1	$$⊢S={\mathrm{Poly}}_1\left(R\right)$$
	ressply.2	$$⊢H=R{\upharpoonright }_{𝑠}T$$
	ressply.3	$$⊢U={\mathrm{Poly}}_1\left(H\right)$$
	ressply.4	$$⊢B={\mathrm{Base}}_U$$
	ressply.5	$$⊢\phi \to T\in \mathrm{SubRing}\left(R\right)$$
	ressply1.1	$$⊢P=S{\upharpoonright }_{𝑠}B$$
	ressply1sub.1	$$⊢\phi \to X\in B$$
	ressply1sub.2	$$⊢\phi \to Y\in B$$
Assertion	ressply1sub	$$⊢\phi \to X{-}_{U}Y=X{-}_{P}Y$$

Proof

Step	Hyp	Ref	Expression
1		ressply.1	$$⊢S={\mathrm{Poly}}_1\left(R\right)$$
2		ressply.2	$$⊢H=R{\upharpoonright }_{𝑠}T$$
3		ressply.3	$$⊢U={\mathrm{Poly}}_1\left(H\right)$$
4		ressply.4	$$⊢B={\mathrm{Base}}_U$$
5		ressply.5	$$⊢\phi \to T\in \mathrm{SubRing}\left(R\right)$$
6		ressply1.1	$$⊢P=S{\upharpoonright }_{𝑠}B$$
7		ressply1sub.1	$$⊢\phi \to X\in B$$
8		ressply1sub.2	$$⊢\phi \to Y\in B$$
9	1 2 3 4 5 6 8	ressply1invg	$$⊢\phi \to {inv}_g\left(U\right)\left(Y\right)={inv}_g\left(P\right)\left(Y\right)$$
10	9	oveq2d	$$⊢\phi \to X{+}_U{inv}_g\left(U\right)\left(Y\right)=X{+}_U{inv}_g\left(P\right)\left(Y\right)$$
11	1 2 3 4	subrgply1	$$⊢T\in \mathrm{SubRing}\left(R\right)\to B\in \mathrm{SubRing}\left(S\right)$$
12		subrgsubg	$$⊢B\in \mathrm{SubRing}\left(S\right)\to B\in \mathrm{SubGrp}\left(S\right)$$
13	5 11 12	3syl	$$⊢\phi \to B\in \mathrm{SubGrp}\left(S\right)$$
14	6	subggrp	$$⊢B\in \mathrm{SubGrp}\left(S\right)\to P\in \mathrm{Grp}$$
15	13 14	syl	$$⊢\phi \to P\in \mathrm{Grp}$$
16	1 2 3 4 5 6	ressply1bas	$$⊢\phi \to B={\mathrm{Base}}_P$$
17	8 16	eleqtrd	$$⊢\phi \to Y\in {\mathrm{Base}}_P$$
18		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
19		eqid	$$⊢{inv}_g\left(P\right)={inv}_g\left(P\right)$$
20	18 19	grpinvcl	$$⊢\left(P\in \mathrm{Grp}\wedge Y\in {\mathrm{Base}}_P\right)\to {inv}_g\left(P\right)\left(Y\right)\in {\mathrm{Base}}_P$$
21	15 17 20	syl2anc	$$⊢\phi \to {inv}_g\left(P\right)\left(Y\right)\in {\mathrm{Base}}_P$$
22	21 16	eleqtrrd	$$⊢\phi \to {inv}_g\left(P\right)\left(Y\right)\in B$$
23	7 22	jca	$$⊢\phi \to \left(X\in B\wedge {inv}_g\left(P\right)\left(Y\right)\in B\right)$$
24	1 2 3 4 5 6	ressply1add	$$⊢\left(\phi \wedge \left(X\in B\wedge {inv}_g\left(P\right)\left(Y\right)\in B\right)\right)\to X{+}_U{inv}_g\left(P\right)\left(Y\right)=X{+}_P{inv}_g\left(P\right)\left(Y\right)$$
25	23 24	mpdan	$$⊢\phi \to X{+}_U{inv}_g\left(P\right)\left(Y\right)=X{+}_P{inv}_g\left(P\right)\left(Y\right)$$
26	10 25	eqtrd	$$⊢\phi \to X{+}_U{inv}_g\left(U\right)\left(Y\right)=X{+}_P{inv}_g\left(P\right)\left(Y\right)$$
27		eqid	$$⊢{+}_U={+}_U$$
28		eqid	$$⊢{inv}_g\left(U\right)={inv}_g\left(U\right)$$
29		eqid	$$⊢{-}_U={-}_U$$
30	4 27 28 29	grpsubval	$$⊢\left(X\in B\wedge Y\in B\right)\to X{-}_{U}Y=X{+}_U{inv}_g\left(U\right)\left(Y\right)$$
31	7 8 30	syl2anc	$$⊢\phi \to X{-}_{U}Y=X{+}_U{inv}_g\left(U\right)\left(Y\right)$$
32	7 16	eleqtrd	$$⊢\phi \to X\in {\mathrm{Base}}_P$$
33		eqid	$$⊢{+}_P={+}_P$$
34		eqid	$$⊢{-}_P={-}_P$$
35	18 33 19 34	grpsubval	$$⊢\left(X\in {\mathrm{Base}}_P\wedge Y\in {\mathrm{Base}}_P\right)\to X{-}_{P}Y=X{+}_P{inv}_g\left(P\right)\left(Y\right)$$
36	32 17 35	syl2anc	$$⊢\phi \to X{-}_{P}Y=X{+}_P{inv}_g\left(P\right)\left(Y\right)$$
37	26 31 36	3eqtr4d	$$⊢\phi \to X{-}_{U}Y=X{-}_{P}Y$$