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	6	subggrp	\|- ( B e. ( SubGrp ` S ) -> P e. Grp )
14	5 11 12 13	4syl	\|- ( ph -> P e. Grp )
15	1 2 3 4 5 6	ressply1bas	\|- ( ph -> B = ( Base ` P ) )
16	8 15	eleqtrd	\|- ( ph -> Y e. ( Base ` P ) )
17		eqid	\|- ( Base ` P ) = ( Base ` P )
18		eqid	\|- ( invg ` P ) = ( invg ` P )
19	17 18	grpinvcl	\|- ( ( P e. Grp /\ Y e. ( Base ` P ) ) -> ( ( invg ` P ) ` Y ) e. ( Base ` P ) )
20	14 16 19	syl2anc	\|- ( ph -> ( ( invg ` P ) ` Y ) e. ( Base ` P ) )
21	20 15	eleqtrrd	\|- ( ph -> ( ( invg ` P ) ` Y ) e. B )
22	7 21	jca	\|- ( ph -> ( X e. B /\ ( ( invg ` P ) ` Y ) e. B ) )
23	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 ) ) )
24	22 23	mpdan	\|- ( ph -> ( X ( +g ` U ) ( ( invg ` P ) ` Y ) ) = ( X ( +g ` P ) ( ( invg ` P ) ` Y ) ) )
25	10 24	eqtrd	\|- ( ph -> ( X ( +g ` U ) ( ( invg ` U ) ` Y ) ) = ( X ( +g ` P ) ( ( invg ` P ) ` Y ) ) )
26		eqid	\|- ( +g ` U ) = ( +g ` U )
27		eqid	\|- ( invg ` U ) = ( invg ` U )
28		eqid	\|- ( -g ` U ) = ( -g ` U )
29	4 26 27 28	grpsubval	\|- ( ( X e. B /\ Y e. B ) -> ( X ( -g ` U ) Y ) = ( X ( +g ` U ) ( ( invg ` U ) ` Y ) ) )
30	7 8 29	syl2anc	\|- ( ph -> ( X ( -g ` U ) Y ) = ( X ( +g ` U ) ( ( invg ` U ) ` Y ) ) )
31	7 15	eleqtrd	\|- ( ph -> X e. ( Base ` P ) )
32		eqid	\|- ( +g ` P ) = ( +g ` P )
33		eqid	\|- ( -g ` P ) = ( -g ` P )
34	17 32 18 33	grpsubval	\|- ( ( X e. ( Base ` P ) /\ Y e. ( Base ` P ) ) -> ( X ( -g ` P ) Y ) = ( X ( +g ` P ) ( ( invg ` P ) ` Y ) ) )
35	31 16 34	syl2anc	\|- ( ph -> ( X ( -g ` P ) Y ) = ( X ( +g ` P ) ( ( invg ` P ) ` Y ) ) )
36	25 30 35	3eqtr4d	\|- ( ph -> ( X ( -g ` U ) Y ) = ( X ( -g ` P ) Y ) )

Metamath Proof Explorer

Theorem ressply1sub

Proof