Theorem ressply1sub

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

	Ref	Expression
Hypotheses	ressply.1	⊢ 𝑆 = ( Poly1 ‘ 𝑅 )
	ressply.2	⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
	ressply.3	⊢ 𝑈 = ( Poly1 ‘ 𝐻 )
	ressply.4	⊢ 𝐵 = ( Base ‘ 𝑈 )
	ressply.5	⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
	ressply1.1	⊢ 𝑃 = ( 𝑆 ↾s 𝐵 )
	ressply1sub.1	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	ressply1sub.2	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	ressply1sub	⊢ ( 𝜑 → ( 𝑋 ( -g ‘ 𝑈 ) 𝑌 ) = ( 𝑋 ( -g ‘ 𝑃 ) 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		ressply.1	⊢ 𝑆 = ( Poly1 ‘ 𝑅 )
2		ressply.2	⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
3		ressply.3	⊢ 𝑈 = ( Poly1 ‘ 𝐻 )
4		ressply.4	⊢ 𝐵 = ( Base ‘ 𝑈 )
5		ressply.5	⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
6		ressply1.1	⊢ 𝑃 = ( 𝑆 ↾s 𝐵 )
7		ressply1sub.1	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8		ressply1sub.2	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9	1 2 3 4 5 6 8	ressply1invg	⊢ ( 𝜑 → ( ( invg ‘ 𝑈 ) ‘ 𝑌 ) = ( ( invg ‘ 𝑃 ) ‘ 𝑌 ) )
10	9	oveq2d	⊢ ( 𝜑 → ( 𝑋 ( +g ‘ 𝑈 ) ( ( invg ‘ 𝑈 ) ‘ 𝑌 ) ) = ( 𝑋 ( +g ‘ 𝑈 ) ( ( invg ‘ 𝑃 ) ‘ 𝑌 ) ) )
11	1 2 3 4	subrgply1	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝐵 ∈ ( SubRing ‘ 𝑆 ) )
12		subrgsubg	⊢ ( 𝐵 ∈ ( SubRing ‘ 𝑆 ) → 𝐵 ∈ ( SubGrp ‘ 𝑆 ) )
13	5 11 12	3syl	⊢ ( 𝜑 → 𝐵 ∈ ( SubGrp ‘ 𝑆 ) )
14	6	subggrp	⊢ ( 𝐵 ∈ ( SubGrp ‘ 𝑆 ) → 𝑃 ∈ Grp )
15	13 14	syl	⊢ ( 𝜑 → 𝑃 ∈ Grp )
16	1 2 3 4 5 6	ressply1bas	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑃 ) )
17	8 16	eleqtrd	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝑃 ) )
18		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
19		eqid	⊢ ( invg ‘ 𝑃 ) = ( invg ‘ 𝑃 )
20	18 19	grpinvcl	⊢ ( ( 𝑃 ∈ Grp ∧ 𝑌 ∈ ( Base ‘ 𝑃 ) ) → ( ( invg ‘ 𝑃 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝑃 ) )
21	15 17 20	syl2anc	⊢ ( 𝜑 → ( ( invg ‘ 𝑃 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝑃 ) )
22	21 16	eleqtrrd	⊢ ( 𝜑 → ( ( invg ‘ 𝑃 ) ‘ 𝑌 ) ∈ 𝐵 )
23	7 22	jca	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ ( ( invg ‘ 𝑃 ) ‘ 𝑌 ) ∈ 𝐵 ) )
24	1 2 3 4 5 6	ressply1add	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ ( ( invg ‘ 𝑃 ) ‘ 𝑌 ) ∈ 𝐵 ) ) → ( 𝑋 ( +g ‘ 𝑈 ) ( ( invg ‘ 𝑃 ) ‘ 𝑌 ) ) = ( 𝑋 ( +g ‘ 𝑃 ) ( ( invg ‘ 𝑃 ) ‘ 𝑌 ) ) )
25	23 24	mpdan	⊢ ( 𝜑 → ( 𝑋 ( +g ‘ 𝑈 ) ( ( invg ‘ 𝑃 ) ‘ 𝑌 ) ) = ( 𝑋 ( +g ‘ 𝑃 ) ( ( invg ‘ 𝑃 ) ‘ 𝑌 ) ) )
26	10 25	eqtrd	⊢ ( 𝜑 → ( 𝑋 ( +g ‘ 𝑈 ) ( ( invg ‘ 𝑈 ) ‘ 𝑌 ) ) = ( 𝑋 ( +g ‘ 𝑃 ) ( ( invg ‘ 𝑃 ) ‘ 𝑌 ) ) )
27		eqid	⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
28		eqid	⊢ ( invg ‘ 𝑈 ) = ( invg ‘ 𝑈 )
29		eqid	⊢ ( -g ‘ 𝑈 ) = ( -g ‘ 𝑈 )
30	4 27 28 29	grpsubval	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( -g ‘ 𝑈 ) 𝑌 ) = ( 𝑋 ( +g ‘ 𝑈 ) ( ( invg ‘ 𝑈 ) ‘ 𝑌 ) ) )
31	7 8 30	syl2anc	⊢ ( 𝜑 → ( 𝑋 ( -g ‘ 𝑈 ) 𝑌 ) = ( 𝑋 ( +g ‘ 𝑈 ) ( ( invg ‘ 𝑈 ) ‘ 𝑌 ) ) )
32	7 16	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑃 ) )
33		eqid	⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
34		eqid	⊢ ( -g ‘ 𝑃 ) = ( -g ‘ 𝑃 )
35	18 33 19 34	grpsubval	⊢ ( ( 𝑋 ∈ ( Base ‘ 𝑃 ) ∧ 𝑌 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑋 ( -g ‘ 𝑃 ) 𝑌 ) = ( 𝑋 ( +g ‘ 𝑃 ) ( ( invg ‘ 𝑃 ) ‘ 𝑌 ) ) )
36	32 17 35	syl2anc	⊢ ( 𝜑 → ( 𝑋 ( -g ‘ 𝑃 ) 𝑌 ) = ( 𝑋 ( +g ‘ 𝑃 ) ( ( invg ‘ 𝑃 ) ‘ 𝑌 ) ) )
37	26 31 36	3eqtr4d	⊢ ( 𝜑 → ( 𝑋 ( -g ‘ 𝑈 ) 𝑌 ) = ( 𝑋 ( -g ‘ 𝑃 ) 𝑌 ) )