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

Metamath Proof Explorer

Theorem ressply1invg

Proof