ressply1sub

Description: A restricted polynomial algebra has the same subtraction operation. (Contributed by Thierry Arnoux, 30-Jan-2025)

	Ref	Expression
Hypotheses	ressply.1	$⊢ S = {Poly}_{1} (R)$
	ressply.2	$⊢ H = R ↾_{𝑠} T$
	ressply.3	$⊢ U = {Poly}_{1} (H)$
	ressply.4	$⊢ B = {Base}_{U}$
	ressply.5	$⊢ φ \to T \in SubRing (R)$
	ressply1.1	$⊢ P = S ↾_{𝑠} B$
	ressply1sub.1	$⊢ φ \to X \in B$
	ressply1sub.2	$⊢ φ \to Y \in B$
Assertion	ressply1sub	$⊢ φ \to X -_{U} Y = X -_{P} Y$

Proof

Step	Hyp	Ref	Expression
1		ressply.1	$⊢ S = {Poly}_{1} (R)$
2		ressply.2	$⊢ H = R ↾_{𝑠} T$
3		ressply.3	$⊢ U = {Poly}_{1} (H)$
4		ressply.4	$⊢ B = {Base}_{U}$
5		ressply.5	$⊢ φ \to T \in SubRing (R)$
6		ressply1.1	$⊢ P = S ↾_{𝑠} B$
7		ressply1sub.1	$⊢ φ \to X \in B$
8		ressply1sub.2	$⊢ φ \to Y \in B$
9	1 2 3 4 5 6 8	ressply1invg	$⊢ φ \to {inv}_{g} (U) (Y) = {inv}_{g} (P) (Y)$
10	9	oveq2d	$⊢ φ \to X +_{U} {inv}_{g} (U) (Y) = X +_{U} {inv}_{g} (P) (Y)$
11	1 2 3 4	subrgply1	$⊢ T \in SubRing (R) \to B \in SubRing (S)$
12		subrgsubg	$⊢ B \in SubRing (S) \to B \in SubGrp (S)$
13	5 11 12	3syl	$⊢ φ \to B \in SubGrp (S)$
14	6	subggrp	$⊢ B \in SubGrp (S) \to P \in Grp$
15	13 14	syl	$⊢ φ \to P \in Grp$
16	1 2 3 4 5 6	ressply1bas	$⊢ φ \to B = {Base}_{P}$
17	8 16	eleqtrd	$⊢ φ \to Y \in {Base}_{P}$
18		eqid	$⊢ {Base}_{P} = {Base}_{P}$
19		eqid	$⊢ {inv}_{g} (P) = {inv}_{g} (P)$
20	18 19	grpinvcl	$⊢ (P \in Grp \land Y \in {Base}_{P}) \to {inv}_{g} (P) (Y) \in {Base}_{P}$
21	15 17 20	syl2anc	$⊢ φ \to {inv}_{g} (P) (Y) \in {Base}_{P}$
22	21 16	eleqtrrd	$⊢ φ \to {inv}_{g} (P) (Y) \in B$
23	7 22	jca	$⊢ φ \to (X \in B \land {inv}_{g} (P) (Y) \in B)$
24	1 2 3 4 5 6	ressply1add	$⊢ (φ \land (X \in B \land {inv}_{g} (P) (Y) \in B)) \to X +_{U} {inv}_{g} (P) (Y) = X +_{P} {inv}_{g} (P) (Y)$
25	23 24	mpdan	$⊢ φ \to X +_{U} {inv}_{g} (P) (Y) = X +_{P} {inv}_{g} (P) (Y)$
26	10 25	eqtrd	$⊢ φ \to X +_{U} {inv}_{g} (U) (Y) = X +_{P} {inv}_{g} (P) (Y)$
27		eqid	$⊢ +_{U} = +_{U}$
28		eqid	$⊢ {inv}_{g} (U) = {inv}_{g} (U)$
29		eqid	$⊢ -_{U} = -_{U}$
30	4 27 28 29	grpsubval	$⊢ (X \in B \land Y \in B) \to X -_{U} Y = X +_{U} {inv}_{g} (U) (Y)$
31	7 8 30	syl2anc	$⊢ φ \to X -_{U} Y = X +_{U} {inv}_{g} (U) (Y)$
32	7 16	eleqtrd	$⊢ φ \to X \in {Base}_{P}$
33		eqid	$⊢ +_{P} = +_{P}$
34		eqid	$⊢ -_{P} = -_{P}$
35	18 33 19 34	grpsubval	$⊢ (X \in {Base}_{P} \land Y \in {Base}_{P}) \to X -_{P} Y = X +_{P} {inv}_{g} (P) (Y)$
36	32 17 35	syl2anc	$⊢ φ \to X -_{P} Y = X +_{P} {inv}_{g} (P) (Y)$
37	26 31 36	3eqtr4d	$⊢ φ \to X -_{U} Y = X -_{P} Y$

Metamath Proof Explorer

Theorem ressply1sub

Proof