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	⊢ 𝑆 = ( Poly1 ‘ 𝑅 )
	ressply.2	⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
	ressply.3	⊢ 𝑈 = ( Poly1 ‘ 𝐻 )
	ressply.4	⊢ 𝐵 = ( Base ‘ 𝑈 )
	ressply.5	⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
	ressply1.1	⊢ 𝑃 = ( 𝑆 ↾s 𝐵 )
	ressply1invg.1	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	ressply1invg	⊢ ( 𝜑 → ( ( invg ‘ 𝑈 ) ‘ 𝑋 ) = ( ( invg ‘ 𝑃 ) ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		ressply.1	⊢ 𝑆 = ( Poly1 ‘ 𝑅 )
2		ressply.2	⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
3		ressply.3	⊢ 𝑈 = ( Poly1 ‘ 𝐻 )
4		ressply.4	⊢ 𝐵 = ( Base ‘ 𝑈 )
5		ressply.5	⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
6		ressply1.1	⊢ 𝑃 = ( 𝑆 ↾s 𝐵 )
7		ressply1invg.1	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8	1 2 3 4 5 6	ressply1bas	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑃 ) )
9	1 2 3 4 5 6	ressply1add	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑦 ( +g ‘ 𝑈 ) 𝑋 ) = ( 𝑦 ( +g ‘ 𝑃 ) 𝑋 ) )
10	9	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝑦 ( +g ‘ 𝑈 ) 𝑋 ) = ( 𝑦 ( +g ‘ 𝑃 ) 𝑋 ) )
11	7 10	mpidan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ( +g ‘ 𝑈 ) 𝑋 ) = ( 𝑦 ( +g ‘ 𝑃 ) 𝑋 ) )
12		eqid	⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
13	1 2 3 4 5 12	ressply10g	⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑈 ) )
14	1 2 3 4	subrgply1	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝐵 ∈ ( SubRing ‘ 𝑆 ) )
15	5 14	syl	⊢ ( 𝜑 → 𝐵 ∈ ( SubRing ‘ 𝑆 ) )
16		subrgrcl	⊢ ( 𝐵 ∈ ( SubRing ‘ 𝑆 ) → 𝑆 ∈ Ring )
17		ringmnd	⊢ ( 𝑆 ∈ Ring → 𝑆 ∈ Mnd )
18	15 16 17	3syl	⊢ ( 𝜑 → 𝑆 ∈ Mnd )
19		subrgsubg	⊢ ( 𝐵 ∈ ( SubRing ‘ 𝑆 ) → 𝐵 ∈ ( SubGrp ‘ 𝑆 ) )
20	12	subg0cl	⊢ ( 𝐵 ∈ ( SubGrp ‘ 𝑆 ) → ( 0g ‘ 𝑆 ) ∈ 𝐵 )
21	15 19 20	3syl	⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) ∈ 𝐵 )
22		eqid	⊢ ( PwSer1 ‘ 𝐻 ) = ( PwSer1 ‘ 𝐻 )
23		eqid	⊢ ( Base ‘ ( PwSer1 ‘ 𝐻 ) ) = ( Base ‘ ( PwSer1 ‘ 𝐻 ) )
24		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
25	1 2 3 4 5 22 23 24	ressply1bas2	⊢ ( 𝜑 → 𝐵 = ( ( Base ‘ ( PwSer1 ‘ 𝐻 ) ) ∩ ( Base ‘ 𝑆 ) ) )
26		inss2	⊢ ( ( Base ‘ ( PwSer1 ‘ 𝐻 ) ) ∩ ( Base ‘ 𝑆 ) ) ⊆ ( Base ‘ 𝑆 )
27	25 26	eqsstrdi	⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ 𝑆 ) )
28	6 24 12	ress0g	⊢ ( ( 𝑆 ∈ Mnd ∧ ( 0g ‘ 𝑆 ) ∈ 𝐵 ∧ 𝐵 ⊆ ( Base ‘ 𝑆 ) ) → ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑃 ) )
29	18 21 27 28	syl3anc	⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑃 ) )
30	13 29	eqtr3d	⊢ ( 𝜑 → ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑃 ) )
31	30	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑃 ) )
32	11 31	eqeq12d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑦 ( +g ‘ 𝑈 ) 𝑋 ) = ( 0g ‘ 𝑈 ) ↔ ( 𝑦 ( +g ‘ 𝑃 ) 𝑋 ) = ( 0g ‘ 𝑃 ) ) )
33	8 32	riotaeqbidva	⊢ ( 𝜑 → ( ℩ 𝑦 ∈ 𝐵 ( 𝑦 ( +g ‘ 𝑈 ) 𝑋 ) = ( 0g ‘ 𝑈 ) ) = ( ℩ 𝑦 ∈ ( Base ‘ 𝑃 ) ( 𝑦 ( +g ‘ 𝑃 ) 𝑋 ) = ( 0g ‘ 𝑃 ) ) )
34		eqid	⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
35		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
36		eqid	⊢ ( invg ‘ 𝑈 ) = ( invg ‘ 𝑈 )
37	4 34 35 36	grpinvval	⊢ ( 𝑋 ∈ 𝐵 → ( ( invg ‘ 𝑈 ) ‘ 𝑋 ) = ( ℩ 𝑦 ∈ 𝐵 ( 𝑦 ( +g ‘ 𝑈 ) 𝑋 ) = ( 0g ‘ 𝑈 ) ) )
38	7 37	syl	⊢ ( 𝜑 → ( ( invg ‘ 𝑈 ) ‘ 𝑋 ) = ( ℩ 𝑦 ∈ 𝐵 ( 𝑦 ( +g ‘ 𝑈 ) 𝑋 ) = ( 0g ‘ 𝑈 ) ) )
39	7 8	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑃 ) )
40		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
41		eqid	⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
42		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
43		eqid	⊢ ( invg ‘ 𝑃 ) = ( invg ‘ 𝑃 )
44	40 41 42 43	grpinvval	⊢ ( 𝑋 ∈ ( Base ‘ 𝑃 ) → ( ( invg ‘ 𝑃 ) ‘ 𝑋 ) = ( ℩ 𝑦 ∈ ( Base ‘ 𝑃 ) ( 𝑦 ( +g ‘ 𝑃 ) 𝑋 ) = ( 0g ‘ 𝑃 ) ) )
45	39 44	syl	⊢ ( 𝜑 → ( ( invg ‘ 𝑃 ) ‘ 𝑋 ) = ( ℩ 𝑦 ∈ ( Base ‘ 𝑃 ) ( 𝑦 ( +g ‘ 𝑃 ) 𝑋 ) = ( 0g ‘ 𝑃 ) ) )
46	33 38 45	3eqtr4d	⊢ ( 𝜑 → ( ( invg ‘ 𝑈 ) ‘ 𝑋 ) = ( ( invg ‘ 𝑃 ) ‘ 𝑋 ) )