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

Metamath Proof Explorer

Theorem ressply1invg

Description: An element of a restricted polynomial algebra has the same group inverse. (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 )
ressply1invg.1 
|- ( ph -> X e. B )
Assertion ressply1invg 
|- ( ph -> ( ( invg ` U ) ` X ) = ( ( invg ` P ) ` X ) )

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 ressply1invg.1 
 |-  ( ph -> X e. B )
8 1 2 3 4 5 6 ressply1bas 
 |-  ( ph -> B = ( Base ` P ) )
9 1 2 3 4 5 6 ressply1add 
 |-  ( ( ph /\ ( y e. B /\ X e. B ) ) -> ( y ( +g ` U ) X ) = ( y ( +g ` P ) X ) )
10 9 anassrs 
 |-  ( ( ( ph /\ y e. B ) /\ X e. B ) -> ( y ( +g ` U ) X ) = ( y ( +g ` P ) X ) )
11 7 10 mpidan 
 |-  ( ( ph /\ y e. B ) -> ( y ( +g ` U ) X ) = ( y ( +g ` P ) X ) )
12 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
13 1 2 3 4 5 12 ressply10g 
 |-  ( ph -> ( 0g ` S ) = ( 0g ` U ) )
14 1 2 3 4 subrgply1 
 |-  ( T e. ( SubRing ` R ) -> B e. ( SubRing ` S ) )
15 subrgrcl 
 |-  ( B e. ( SubRing ` S ) -> S e. Ring )
16 ringmnd 
 |-  ( S e. Ring -> S e. Mnd )
17 5 14 15 16 4syl 
 |-  ( ph -> S e. Mnd )
18 subrgsubg 
 |-  ( B e. ( SubRing ` S ) -> B e. ( SubGrp ` S ) )
19 12 subg0cl 
 |-  ( B e. ( SubGrp ` S ) -> ( 0g ` S ) e. B )
20 5 14 18 19 4syl 
 |-  ( ph -> ( 0g ` S ) e. B )
21 eqid 
 |-  ( PwSer1 ` H ) = ( PwSer1 ` H )
22 eqid 
 |-  ( Base ` ( PwSer1 ` H ) ) = ( Base ` ( PwSer1 ` H ) )
23 eqid 
 |-  ( Base ` S ) = ( Base ` S )
24 1 2 3 4 5 21 22 23 ressply1bas2 
 |-  ( ph -> B = ( ( Base ` ( PwSer1 ` H ) ) i^i ( Base ` S ) ) )
25 inss2 
 |-  ( ( Base ` ( PwSer1 ` H ) ) i^i ( Base ` S ) ) C_ ( Base ` S )
26 24 25 eqsstrdi 
 |-  ( ph -> B C_ ( Base ` S ) )
27 6 23 12 ress0g 
 |-  ( ( S e. Mnd /\ ( 0g ` S ) e. B /\ B C_ ( Base ` S ) ) -> ( 0g ` S ) = ( 0g ` P ) )
28 17 20 26 27 syl3anc 
 |-  ( ph -> ( 0g ` S ) = ( 0g ` P ) )
29 13 28 eqtr3d 
 |-  ( ph -> ( 0g ` U ) = ( 0g ` P ) )
30 29 adantr 
 |-  ( ( ph /\ y e. B ) -> ( 0g ` U ) = ( 0g ` P ) )
31 11 30 eqeq12d 
 |-  ( ( ph /\ y e. B ) -> ( ( y ( +g ` U ) X ) = ( 0g ` U ) <-> ( y ( +g ` P ) X ) = ( 0g ` P ) ) )
32 8 31 riotaeqbidva 
 |-  ( ph -> ( iota_ y e. B ( y ( +g ` U ) X ) = ( 0g ` U ) ) = ( iota_ y e. ( Base ` P ) ( y ( +g ` P ) X ) = ( 0g ` P ) ) )
33 eqid 
 |-  ( +g ` U ) = ( +g ` U )
34 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
35 eqid 
 |-  ( invg ` U ) = ( invg ` U )
36 4 33 34 35 grpinvval 
 |-  ( X e. B -> ( ( invg ` U ) ` X ) = ( iota_ y e. B ( y ( +g ` U ) X ) = ( 0g ` U ) ) )
37 7 36 syl 
 |-  ( ph -> ( ( invg ` U ) ` X ) = ( iota_ y e. B ( y ( +g ` U ) X ) = ( 0g ` U ) ) )
38 7 8 eleqtrd 
 |-  ( ph -> X e. ( Base ` P ) )
39 eqid 
 |-  ( Base ` P ) = ( Base ` P )
40 eqid 
 |-  ( +g ` P ) = ( +g ` P )
41 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
42 eqid 
 |-  ( invg ` P ) = ( invg ` P )
43 39 40 41 42 grpinvval 
 |-  ( X e. ( Base ` P ) -> ( ( invg ` P ) ` X ) = ( iota_ y e. ( Base ` P ) ( y ( +g ` P ) X ) = ( 0g ` P ) ) )
44 38 43 syl 
 |-  ( ph -> ( ( invg ` P ) ` X ) = ( iota_ y e. ( Base ` P ) ( y ( +g ` P ) X ) = ( 0g ` P ) ) )
45 32 37 44 3eqtr4d 
 |-  ( ph -> ( ( invg ` U ) ` X ) = ( ( invg ` P ) ` X ) )