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	5 14	syl	$$⊢\phi \to B\in \mathrm{SubRing}\left(S\right)$$
16		subrgrcl	$$⊢B\in \mathrm{SubRing}\left(S\right)\to S\in \mathrm{Ring}$$
17		ringmnd	$$⊢S\in \mathrm{Ring}\to S\in \mathrm{Mnd}$$
18	15 16 17	3syl	$$⊢\phi \to S\in \mathrm{Mnd}$$
19		subrgsubg	$$⊢B\in \mathrm{SubRing}\left(S\right)\to B\in \mathrm{SubGrp}\left(S\right)$$
20	12	subg0cl	$$⊢B\in \mathrm{SubGrp}\left(S\right)\to 0_S\in B$$
21	15 19 20	3syl	$$⊢\phi \to 0_S\in B$$
22		eqid	$$⊢{\mathrm{PwSer}}_1\left(H\right)={\mathrm{PwSer}}_1\left(H\right)$$
23		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(H\right)}={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(H\right)}$$
24		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
25	1 2 3 4 5 22 23 24	ressply1bas2	$$⊢\phi \to B={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(H\right)}\cap {\mathrm{Base}}_S$$
26		inss2	$$⊢{\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(H\right)}\cap {\mathrm{Base}}_S\subseteq {\mathrm{Base}}_S$$
27	25 26	eqsstrdi	$$⊢\phi \to B\subseteq {\mathrm{Base}}_S$$
28	6 24 12	ress0g	$$⊢\left(S\in \mathrm{Mnd}\wedge 0_S\in B\wedge B\subseteq {\mathrm{Base}}_S\right)\to 0_S=0_P$$
29	18 21 27 28	syl3anc	$$⊢\phi \to 0_S=0_P$$
30	13 29	eqtr3d	$$⊢\phi \to 0_U=0_P$$
31	30	adantr	$$⊢\left(\phi \wedge y\in B\right)\to 0_U=0_P$$
32	11 31	eqeq12d	$$⊢\left(\phi \wedge y\in B\right)\to \left(y{+}_{U}X=0_U\leftrightarrow y{+}_{P}X=0_P\right)$$
33	8 32	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)$$
34		eqid	$$⊢{+}_U={+}_U$$
35		eqid	$$⊢0_U=0_U$$
36		eqid	$$⊢{inv}_g\left(U\right)={inv}_g\left(U\right)$$
37	4 34 35 36	grpinvval	$$⊢X\in B\to {inv}_g\left(U\right)\left(X\right)=\left(\iota y\in B|y{+}_{U}X=0_U\right)$$
38	7 37	syl	$$⊢\phi \to {inv}_g\left(U\right)\left(X\right)=\left(\iota y\in B|y{+}_{U}X=0_U\right)$$
39	7 8	eleqtrd	$$⊢\phi \to X\in {\mathrm{Base}}_P$$
40		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
41		eqid	$$⊢{+}_P={+}_P$$
42		eqid	$$⊢0_P=0_P$$
43		eqid	$$⊢{inv}_g\left(P\right)={inv}_g\left(P\right)$$
44	40 41 42 43	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)$$
45	39 44	syl	$$⊢\phi \to {inv}_g\left(P\right)\left(X\right)=\left(\iota y\in {\mathrm{Base}}_P|y{+}_{P}X=0_P\right)$$
46	33 38 45	3eqtr4d	$$⊢\phi \to {inv}_g\left(U\right)\left(X\right)={inv}_g\left(P\right)\left(X\right)$$