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

Metamath Proof Explorer

Theorem ressply1sub

Description: A restricted polynomial algebra has the same subtraction operation. (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 𝐵 )
ressply1sub.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
ressply1sub.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion ressply1sub ( 𝜑 → ( 𝑋 ( -g ‘ 𝑈 ) 𝑌 ) = ( 𝑋 ( -g ‘ 𝑃 ) 𝑌 ) )

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 ressply1sub.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8 ressply1sub.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9 1 2 3 4 5 6 8 ressply1invg ⊢ ( 𝜑 → ( ( invg ‘ 𝑈 ) ‘ 𝑌 ) = ( ( invg ‘ 𝑃 ) ‘ 𝑌 ) )
10 9 oveq2d ⊢ ( 𝜑 → ( 𝑋 ( +g ‘ 𝑈 ) ( ( invg ‘ 𝑈 ) ‘ 𝑌 ) ) = ( 𝑋 ( +g ‘ 𝑈 ) ( ( invg ‘ 𝑃 ) ‘ 𝑌 ) ) )
11 1 2 3 4 subrgply1 ⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝐵 ∈ ( SubRing ‘ 𝑆 ) )
12 subrgsubg ⊢ ( 𝐵 ∈ ( SubRing ‘ 𝑆 ) → 𝐵 ∈ ( SubGrp ‘ 𝑆 ) )
13 6 subggrp ⊢ ( 𝐵 ∈ ( SubGrp ‘ 𝑆 ) → 𝑃 ∈ Grp )
14 5 11 12 13 4syl ⊢ ( 𝜑 → 𝑃 ∈ Grp )
15 1 2 3 4 5 6 ressply1bas ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑃 ) )
16 8 15 eleqtrd ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝑃 ) )
17 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
18 eqid ⊢ ( invg ‘ 𝑃 ) = ( invg ‘ 𝑃 )
19 17 18 grpinvcl ⊢ ( ( 𝑃 ∈ Grp ∧ 𝑌 ∈ ( Base ‘ 𝑃 ) ) → ( ( invg ‘ 𝑃 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝑃 ) )
20 14 16 19 syl2anc ⊢ ( 𝜑 → ( ( invg ‘ 𝑃 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝑃 ) )
21 20 15 eleqtrrd ⊢ ( 𝜑 → ( ( invg ‘ 𝑃 ) ‘ 𝑌 ) ∈ 𝐵 )
22 7 21 jca ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ ( ( invg ‘ 𝑃 ) ‘ 𝑌 ) ∈ 𝐵 ) )
23 1 2 3 4 5 6 ressply1add ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ ( ( invg ‘ 𝑃 ) ‘ 𝑌 ) ∈ 𝐵 ) ) → ( 𝑋 ( +g ‘ 𝑈 ) ( ( invg ‘ 𝑃 ) ‘ 𝑌 ) ) = ( 𝑋 ( +g ‘ 𝑃 ) ( ( invg ‘ 𝑃 ) ‘ 𝑌 ) ) )
24 22 23 mpdan ⊢ ( 𝜑 → ( 𝑋 ( +g ‘ 𝑈 ) ( ( invg ‘ 𝑃 ) ‘ 𝑌 ) ) = ( 𝑋 ( +g ‘ 𝑃 ) ( ( invg ‘ 𝑃 ) ‘ 𝑌 ) ) )
25 10 24 eqtrd ⊢ ( 𝜑 → ( 𝑋 ( +g ‘ 𝑈 ) ( ( invg ‘ 𝑈 ) ‘ 𝑌 ) ) = ( 𝑋 ( +g ‘ 𝑃 ) ( ( invg ‘ 𝑃 ) ‘ 𝑌 ) ) )
26 eqid ⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
27 eqid ⊢ ( invg ‘ 𝑈 ) = ( invg ‘ 𝑈 )
28 eqid ⊢ ( -g ‘ 𝑈 ) = ( -g ‘ 𝑈 )
29 4 26 27 28 grpsubval ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( -g ‘ 𝑈 ) 𝑌 ) = ( 𝑋 ( +g ‘ 𝑈 ) ( ( invg ‘ 𝑈 ) ‘ 𝑌 ) ) )
30 7 8 29 syl2anc ⊢ ( 𝜑 → ( 𝑋 ( -g ‘ 𝑈 ) 𝑌 ) = ( 𝑋 ( +g ‘ 𝑈 ) ( ( invg ‘ 𝑈 ) ‘ 𝑌 ) ) )
31 7 15 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑃 ) )
32 eqid ⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
33 eqid ⊢ ( -g ‘ 𝑃 ) = ( -g ‘ 𝑃 )
34 17 32 18 33 grpsubval ⊢ ( ( 𝑋 ∈ ( Base ‘ 𝑃 ) ∧ 𝑌 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑋 ( -g ‘ 𝑃 ) 𝑌 ) = ( 𝑋 ( +g ‘ 𝑃 ) ( ( invg ‘ 𝑃 ) ‘ 𝑌 ) ) )
35 31 16 34 syl2anc ⊢ ( 𝜑 → ( 𝑋 ( -g ‘ 𝑃 ) 𝑌 ) = ( 𝑋 ( +g ‘ 𝑃 ) ( ( invg ‘ 𝑃 ) ‘ 𝑌 ) ) )
36 25 30 35 3eqtr4d ⊢ ( 𝜑 → ( 𝑋 ( -g ‘ 𝑈 ) 𝑌 ) = ( 𝑋 ( -g ‘ 𝑃 ) 𝑌 ) )