This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = ( 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 ) )