This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 subrgrcl ⊢ ( 𝐵 ∈ ( SubRing ‘ 𝑆 ) → 𝑆 ∈ Ring )
16 ringmnd ⊢ ( 𝑆 ∈ Ring → 𝑆 ∈ Mnd )
17 5 14 15 16 4syl ⊢ ( 𝜑 → 𝑆 ∈ Mnd )
18 subrgsubg ⊢ ( 𝐵 ∈ ( SubRing ‘ 𝑆 ) → 𝐵 ∈ ( SubGrp ‘ 𝑆 ) )
19 12 subg0cl ⊢ ( 𝐵 ∈ ( SubGrp ‘ 𝑆 ) → ( 0g ‘ 𝑆 ) ∈ 𝐵 )
20 5 14 18 19 4syl ⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) ∈ 𝐵 )
21 eqid ⊢ ( PwSer1 ‘ 𝐻 ) = ( PwSer1 ‘ 𝐻 )
22 eqid ⊢ ( Base ‘ ( PwSer1 ‘ 𝐻 ) ) = ( Base ‘ ( PwSer1 ‘ 𝐻 ) )
23 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
24 1 2 3 4 5 21 22 23 ressply1bas2 ⊢ ( 𝜑 → 𝐵 = ( ( Base ‘ ( PwSer1 ‘ 𝐻 ) ) ∩ ( Base ‘ 𝑆 ) ) )
25 inss2 ⊢ ( ( Base ‘ ( PwSer1 ‘ 𝐻 ) ) ∩ ( Base ‘ 𝑆 ) ) ⊆ ( Base ‘ 𝑆 )
26 24 25 eqsstrdi ⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ 𝑆 ) )
27 6 23 12 ress0g ⊢ ( ( 𝑆 ∈ Mnd ∧ ( 0g ‘ 𝑆 ) ∈ 𝐵 ∧ 𝐵 ⊆ ( Base ‘ 𝑆 ) ) → ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑃 ) )
28 17 20 26 27 syl3anc ⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑃 ) )
29 13 28 eqtr3d ⊢ ( 𝜑 → ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑃 ) )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑃 ) )
31 11 30 eqeq12d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑦 ( +g ‘ 𝑈 ) 𝑋 ) = ( 0g ‘ 𝑈 ) ↔ ( 𝑦 ( +g ‘ 𝑃 ) 𝑋 ) = ( 0g ‘ 𝑃 ) ) )
32 8 31 riotaeqbidva ⊢ ( 𝜑 → ( ℩ 𝑦 ∈ 𝐵 ( 𝑦 ( +g ‘ 𝑈 ) 𝑋 ) = ( 0g ‘ 𝑈 ) ) = ( ℩ 𝑦 ∈ ( Base ‘ 𝑃 ) ( 𝑦 ( +g ‘ 𝑃 ) 𝑋 ) = ( 0g ‘ 𝑃 ) ) )
33 eqid ⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
34 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
35 eqid ⊢ ( invg ‘ 𝑈 ) = ( invg ‘ 𝑈 )
36 4 33 34 35 grpinvval ⊢ ( 𝑋 ∈ 𝐵 → ( ( invg ‘ 𝑈 ) ‘ 𝑋 ) = ( ℩ 𝑦 ∈ 𝐵 ( 𝑦 ( +g ‘ 𝑈 ) 𝑋 ) = ( 0g ‘ 𝑈 ) ) )
37 7 36 syl ⊢ ( 𝜑 → ( ( invg ‘ 𝑈 ) ‘ 𝑋 ) = ( ℩ 𝑦 ∈ 𝐵 ( 𝑦 ( +g ‘ 𝑈 ) 𝑋 ) = ( 0g ‘ 𝑈 ) ) )
38 7 8 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑃 ) )
39 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
40 eqid ⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
41 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
42 eqid ⊢ ( invg ‘ 𝑃 ) = ( invg ‘ 𝑃 )
43 39 40 41 42 grpinvval ⊢ ( 𝑋 ∈ ( Base ‘ 𝑃 ) → ( ( invg ‘ 𝑃 ) ‘ 𝑋 ) = ( ℩ 𝑦 ∈ ( Base ‘ 𝑃 ) ( 𝑦 ( +g ‘ 𝑃 ) 𝑋 ) = ( 0g ‘ 𝑃 ) ) )
44 38 43 syl ⊢ ( 𝜑 → ( ( invg ‘ 𝑃 ) ‘ 𝑋 ) = ( ℩ 𝑦 ∈ ( Base ‘ 𝑃 ) ( 𝑦 ( +g ‘ 𝑃 ) 𝑋 ) = ( 0g ‘ 𝑃 ) ) )
45 32 37 44 3eqtr4d ⊢ ( 𝜑 → ( ( invg ‘ 𝑈 ) ‘ 𝑋 ) = ( ( invg ‘ 𝑃 ) ‘ 𝑋 ) )