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={\mathrm{Poly}}_1\left(R\right)$$
	ressply.2	$$⊢H=R{\upharpoonright }_{𝑠}T$$
	ressply.3	$$⊢U={\mathrm{Poly}}_1\left(H\right)$$
	ressply.4	$$⊢B={\mathrm{Base}}_U$$
	ressply.5	$$⊢\phi \to T\in \mathrm{SubRing}\left(R\right)$$
	ressply1.1	$$⊢P=S{\upharpoonright }_{𝑠}B$$
	ressply1invg.1	$$⊢\phi \to X\in B$$
Assertion	ressply1invg	$$⊢\phi \to {inv}_g\left(U\right)\left(X\right)={inv}_g\left(P\right)\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		ressply.1	$$⊢S={\mathrm{Poly}}_1\left(R\right)$$
2		ressply.2	$$⊢H=R{\upharpoonright }_{𝑠}T$$
3		ressply.3	$$⊢U={\mathrm{Poly}}_1\left(H\right)$$
4		ressply.4	$$⊢B={\mathrm{Base}}_U$$
5		ressply.5	$$⊢\phi \to T\in \mathrm{SubRing}\left(R\right)$$
6		ressply1.1	$$⊢P=S{\upharpoonright }_{𝑠}B$$
7		ressply1invg.1	$$⊢\phi \to X\in B$$
8	1 2 3 4 5 6	ressply1bas	$$⊢\phi \to B={\mathrm{Base}}_P$$
9	1 2 3 4 5 6	ressply1add	$$⊢\left(\phi \wedge \left(y\in B\wedge X\in B\right)\right)\to y{+}_{U}X=y{+}_{P}X$$
10	9	anassrs	$$⊢\left(\left(\phi \wedge y\in B\right)\wedge X\in B\right)\to y{+}_{U}X=y{+}_{P}X$$
11	7 10	mpidan	$$⊢\left(\phi \wedge y\in B\right)\to y{+}_{U}X=y{+}_{P}X$$
12		eqid	$$⊢0_S=0_S$$
13	1 2 3 4 5 12	ressply10g	$$⊢\phi \to 0_S=0_U$$
14	1 2 3 4	subrgply1	$$⊢T\in \mathrm{SubRing}\left(R\right)\to B\in \mathrm{SubRing}\left(S\right)$$
15		subrgrcl	$$⊢B\in \mathrm{SubRing}\left(S\right)\to S\in \mathrm{Ring}$$
16		ringmnd	$$⊢S\in \mathrm{Ring}\to S\in \mathrm{Mnd}$$
17	5 14 15 16	4syl	$$⊢\phi \to S\in \mathrm{Mnd}$$
18		subrgsubg	$$⊢B\in \mathrm{SubRing}\left(S\right)\to B\in \mathrm{SubGrp}\left(S\right)$$
19	12	subg0cl	$$⊢B\in \mathrm{SubGrp}\left(S\right)\to 0_S\in B$$
20	5 14 18 19	4syl	$$⊢\phi \to 0_S\in B$$
21		eqid	$$⊢{\mathrm{PwSer}}_1\left(H\right)={\mathrm{PwSer}}_1\left(H\right)$$
22		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(H\right)}={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(H\right)}$$
23		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
24	1 2 3 4 5 21 22 23	ressply1bas2	$$⊢\phi \to B={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(H\right)}\cap {\mathrm{Base}}_S$$
25		inss2	$$⊢{\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(H\right)}\cap {\mathrm{Base}}_S\subseteq {\mathrm{Base}}_S$$
26	24 25	eqsstrdi	$$⊢\phi \to B\subseteq {\mathrm{Base}}_S$$
27	6 23 12	ress0g	$$⊢\left(S\in \mathrm{Mnd}\wedge 0_S\in B\wedge B\subseteq {\mathrm{Base}}_S\right)\to 0_S=0_P$$
28	17 20 26 27	syl3anc	$$⊢\phi \to 0_S=0_P$$
29	13 28	eqtr3d	$$⊢\phi \to 0_U=0_P$$
30	29	adantr	$$⊢\left(\phi \wedge y\in B\right)\to 0_U=0_P$$
31	11 30	eqeq12d	$$⊢\left(\phi \wedge y\in B\right)\to \left(y{+}_{U}X=0_U\leftrightarrow y{+}_{P}X=0_P\right)$$
32	8 31	riotaeqbidva	$$⊢\phi \to \left(\iota y\in B|y{+}_{U}X=0_U\right)=\left(\iota y\in {\mathrm{Base}}_P|y{+}_{P}X=0_P\right)$$
33		eqid	$$⊢{+}_U={+}_U$$
34		eqid	$$⊢0_U=0_U$$
35		eqid	$$⊢{inv}_g\left(U\right)={inv}_g\left(U\right)$$
36	4 33 34 35	grpinvval	$$⊢X\in B\to {inv}_g\left(U\right)\left(X\right)=\left(\iota y\in B|y{+}_{U}X=0_U\right)$$
37	7 36	syl	$$⊢\phi \to {inv}_g\left(U\right)\left(X\right)=\left(\iota y\in B|y{+}_{U}X=0_U\right)$$
38	7 8	eleqtrd	$$⊢\phi \to X\in {\mathrm{Base}}_P$$
39		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
40		eqid	$$⊢{+}_P={+}_P$$
41		eqid	$$⊢0_P=0_P$$
42		eqid	$$⊢{inv}_g\left(P\right)={inv}_g\left(P\right)$$
43	39 40 41 42	grpinvval	$$⊢X\in {\mathrm{Base}}_P\to {inv}_g\left(P\right)\left(X\right)=\left(\iota y\in {\mathrm{Base}}_P|y{+}_{P}X=0_P\right)$$
44	38 43	syl	$$⊢\phi \to {inv}_g\left(P\right)\left(X\right)=\left(\iota y\in {\mathrm{Base}}_P|y{+}_{P}X=0_P\right)$$
45	32 37 44	3eqtr4d	$$⊢\phi \to {inv}_g\left(U\right)\left(X\right)={inv}_g\left(P\right)\left(X\right)$$