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

Metamath Proof Explorer

Theorem ressply1invg

Proof