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	6	subggrp	$$⊢B\in \mathrm{SubGrp}\left(S\right)\to P\in \mathrm{Grp}$$
14	5 11 12 13	4syl	$$⊢\phi \to P\in \mathrm{Grp}$$
15	1 2 3 4 5 6	ressply1bas	$$⊢\phi \to B={\mathrm{Base}}_P$$
16	8 15	eleqtrd	$$⊢\phi \to Y\in {\mathrm{Base}}_P$$
17		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
18		eqid	$$⊢{inv}_g\left(P\right)={inv}_g\left(P\right)$$
19	17 18	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$$
20	14 16 19	syl2anc	$$⊢\phi \to {inv}_g\left(P\right)\left(Y\right)\in {\mathrm{Base}}_P$$
21	20 15	eleqtrrd	$$⊢\phi \to {inv}_g\left(P\right)\left(Y\right)\in B$$
22	7 21	jca	$$⊢\phi \to \left(X\in B\wedge {inv}_g\left(P\right)\left(Y\right)\in B\right)$$
23	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)$$
24	22 23	mpdan	$$⊢\phi \to X{+}_U{inv}_g\left(P\right)\left(Y\right)=X{+}_P{inv}_g\left(P\right)\left(Y\right)$$
25	10 24	eqtrd	$$⊢\phi \to X{+}_U{inv}_g\left(U\right)\left(Y\right)=X{+}_P{inv}_g\left(P\right)\left(Y\right)$$
26		eqid	$$⊢{+}_U={+}_U$$
27		eqid	$$⊢{inv}_g\left(U\right)={inv}_g\left(U\right)$$
28		eqid	$$⊢{-}_U={-}_U$$
29	4 26 27 28	grpsubval	$$⊢\left(X\in B\wedge Y\in B\right)\to X{-}_{U}Y=X{+}_U{inv}_g\left(U\right)\left(Y\right)$$
30	7 8 29	syl2anc	$$⊢\phi \to X{-}_{U}Y=X{+}_U{inv}_g\left(U\right)\left(Y\right)$$
31	7 15	eleqtrd	$$⊢\phi \to X\in {\mathrm{Base}}_P$$
32		eqid	$$⊢{+}_P={+}_P$$
33		eqid	$$⊢{-}_P={-}_P$$
34	17 32 18 33	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)$$
35	31 16 34	syl2anc	$$⊢\phi \to X{-}_{P}Y=X{+}_P{inv}_g\left(P\right)\left(Y\right)$$
36	25 30 35	3eqtr4d	$$⊢\phi \to X{-}_{U}Y=X{-}_{P}Y$$