ressply1sub

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

	Ref	Expression
Hypotheses	ressply.1	\|- S = ( Poly1 ` R )
	ressply.2	\|- H = ( R \|`s T )
	ressply.3	\|- U = ( Poly1 ` H )
	ressply.4	\|- B = ( Base ` U )
	ressply.5	\|- ( ph -> T e. ( SubRing ` R ) )
	ressply1.1	\|- P = ( S \|`s B )
	ressply1sub.1	\|- ( ph -> X e. B )
	ressply1sub.2	\|- ( ph -> Y e. B )
Assertion	ressply1sub	\|- ( ph -> ( X ( -g ` U ) Y ) = ( X ( -g ` P ) Y ) )

Proof

Step	Hyp	Ref	Expression
1		ressply.1	\|- S = ( Poly1 ` R )
2		ressply.2	\|- H = ( R \|`s T )
3		ressply.3	\|- U = ( Poly1 ` H )
4		ressply.4	\|- B = ( Base ` U )
5		ressply.5	\|- ( ph -> T e. ( SubRing ` R ) )
6		ressply1.1	\|- P = ( S \|`s B )
7		ressply1sub.1	\|- ( ph -> X e. B )
8		ressply1sub.2	\|- ( ph -> Y e. B )
9	1 2 3 4 5 6 8	ressply1invg	\|- ( ph -> ( ( invg ` U ) ` Y ) = ( ( invg ` P ) ` Y ) )
10	9	oveq2d	\|- ( ph -> ( X ( +g ` U ) ( ( invg ` U ) ` Y ) ) = ( X ( +g ` U ) ( ( invg ` P ) ` Y ) ) )
11	1 2 3 4	subrgply1	\|- ( T e. ( SubRing ` R ) -> B e. ( SubRing ` S ) )
12		subrgsubg	\|- ( B e. ( SubRing ` S ) -> B e. ( SubGrp ` S ) )
13	5 11 12	3syl	\|- ( ph -> B e. ( SubGrp ` S ) )
14	6	subggrp	\|- ( B e. ( SubGrp ` S ) -> P e. Grp )
15	13 14	syl	\|- ( ph -> P e. Grp )
16	1 2 3 4 5 6	ressply1bas	\|- ( ph -> B = ( Base ` P ) )
17	8 16	eleqtrd	\|- ( ph -> Y e. ( Base ` P ) )
18		eqid	\|- ( Base ` P ) = ( Base ` P )
19		eqid	\|- ( invg ` P ) = ( invg ` P )
20	18 19	grpinvcl	\|- ( ( P e. Grp /\ Y e. ( Base ` P ) ) -> ( ( invg ` P ) ` Y ) e. ( Base ` P ) )
21	15 17 20	syl2anc	\|- ( ph -> ( ( invg ` P ) ` Y ) e. ( Base ` P ) )
22	21 16	eleqtrrd	\|- ( ph -> ( ( invg ` P ) ` Y ) e. B )
23	7 22	jca	\|- ( ph -> ( X e. B /\ ( ( invg ` P ) ` Y ) e. B ) )
24	1 2 3 4 5 6	ressply1add	\|- ( ( ph /\ ( X e. B /\ ( ( invg ` P ) ` Y ) e. B ) ) -> ( X ( +g ` U ) ( ( invg ` P ) ` Y ) ) = ( X ( +g ` P ) ( ( invg ` P ) ` Y ) ) )
25	23 24	mpdan	\|- ( ph -> ( X ( +g ` U ) ( ( invg ` P ) ` Y ) ) = ( X ( +g ` P ) ( ( invg ` P ) ` Y ) ) )
26	10 25	eqtrd	\|- ( ph -> ( X ( +g ` U ) ( ( invg ` U ) ` Y ) ) = ( X ( +g ` P ) ( ( invg ` P ) ` Y ) ) )
27		eqid	\|- ( +g ` U ) = ( +g ` U )
28		eqid	\|- ( invg ` U ) = ( invg ` U )
29		eqid	\|- ( -g ` U ) = ( -g ` U )
30	4 27 28 29	grpsubval	\|- ( ( X e. B /\ Y e. B ) -> ( X ( -g ` U ) Y ) = ( X ( +g ` U ) ( ( invg ` U ) ` Y ) ) )
31	7 8 30	syl2anc	\|- ( ph -> ( X ( -g ` U ) Y ) = ( X ( +g ` U ) ( ( invg ` U ) ` Y ) ) )
32	7 16	eleqtrd	\|- ( ph -> X e. ( Base ` P ) )
33		eqid	\|- ( +g ` P ) = ( +g ` P )
34		eqid	\|- ( -g ` P ) = ( -g ` P )
35	18 33 19 34	grpsubval	\|- ( ( X e. ( Base ` P ) /\ Y e. ( Base ` P ) ) -> ( X ( -g ` P ) Y ) = ( X ( +g ` P ) ( ( invg ` P ) ` Y ) ) )
36	32 17 35	syl2anc	\|- ( ph -> ( X ( -g ` P ) Y ) = ( X ( +g ` P ) ( ( invg ` P ) ` Y ) ) )
37	26 31 36	3eqtr4d	\|- ( ph -> ( X ( -g ` U ) Y ) = ( X ( -g ` P ) Y ) )

Metamath Proof Explorer

Theorem ressply1sub

Proof