resspsradd

Description: A restricted power series algebra has the same addition operation. (Contributed by Mario Carneiro, 3-Jul-2015)

	Ref	Expression
Hypotheses	resspsr.s	$⊢ S = I mPwSer R$
	resspsr.h	$⊢ H = R ↾_{𝑠} T$
	resspsr.u	$⊢ U = I mPwSer H$
	resspsr.b	$⊢ B = {Base}_{U}$
	resspsr.p	$⊢ P = S ↾_{𝑠} B$
	resspsr.2	$⊢ φ \to T \in SubRing (R)$
Assertion	resspsradd	$⊢ (φ \land (X \in B \land Y \in B)) \to X +_{U} Y = X +_{P} Y$

Proof

Step	Hyp	Ref	Expression
1		resspsr.s	$⊢ S = I mPwSer R$
2		resspsr.h	$⊢ H = R ↾_{𝑠} T$
3		resspsr.u	$⊢ U = I mPwSer H$
4		resspsr.b	$⊢ B = {Base}_{U}$
5		resspsr.p	$⊢ P = S ↾_{𝑠} B$
6		resspsr.2	$⊢ φ \to T \in SubRing (R)$
7		eqid	$⊢ +_{H} = +_{H}$
8		eqid	$⊢ +_{U} = +_{U}$
9		simprl	$⊢ (φ \land (X \in B \land Y \in B)) \to X \in B$
10		simprr	$⊢ (φ \land (X \in B \land Y \in B)) \to Y \in B$
11	3 4 7 8 9 10	psradd	$⊢ (φ \land (X \in B \land Y \in B)) \to X +_{U} Y = X {+_{H}}_{f} Y$
12		eqid	$⊢ {Base}_{S} = {Base}_{S}$
13		eqid	$⊢ +_{R} = +_{R}$
14		eqid	$⊢ +_{S} = +_{S}$
15		fvex	$⊢ {Base}_{R} \in V$
16	2	subrgbas	$⊢ T \in SubRing (R) \to T = {Base}_{H}$
17	6 16	syl	$⊢ φ \to T = {Base}_{H}$
18		eqid	$⊢ {Base}_{R} = {Base}_{R}$
19	18	subrgss	$⊢ T \in SubRing (R) \to T \subseteq {Base}_{R}$
20	6 19	syl	$⊢ φ \to T \subseteq {Base}_{R}$
21	17 20	eqsstrrd	$⊢ φ \to {Base}_{H} \subseteq {Base}_{R}$
22		mapss	$⊢ ({Base}_{R} \in V \land {Base}_{H} \subseteq {Base}_{R}) \to {Base}_{H}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}} \subseteq {Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}$
23	15 21 22	sylancr	$⊢ φ \to {Base}_{H}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}} \subseteq {Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}$
24	23	adantr	$⊢ (φ \land (X \in B \land Y \in B)) \to {Base}_{H}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}} \subseteq {Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}$
25		eqid	$⊢ {Base}_{H} = {Base}_{H}$
26		eqid	$⊢ \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
27		reldmpsr	$⊢ Rel dom mPwSer$
28	27 3 4	elbasov	$⊢ X \in B \to (I \in V \land H \in V)$
29	28	ad2antrl	$⊢ (φ \land (X \in B \land Y \in B)) \to (I \in V \land H \in V)$
30	29	simpld	$⊢ (φ \land (X \in B \land Y \in B)) \to I \in V$
31	3 25 26 4 30	psrbas	$⊢ (φ \land (X \in B \land Y \in B)) \to B = {Base}_{H}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}$
32	1 18 26 12 30	psrbas	$⊢ (φ \land (X \in B \land Y \in B)) \to {Base}_{S} = {Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}$
33	24 31 32	3sstr4d	$⊢ (φ \land (X \in B \land Y \in B)) \to B \subseteq {Base}_{S}$
34	33 9	sseldd	$⊢ (φ \land (X \in B \land Y \in B)) \to X \in {Base}_{S}$
35	33 10	sseldd	$⊢ (φ \land (X \in B \land Y \in B)) \to Y \in {Base}_{S}$
36	1 12 13 14 34 35	psradd	$⊢ (φ \land (X \in B \land Y \in B)) \to X +_{S} Y = X {+_{R}}_{f} Y$
37	2 13	ressplusg	$⊢ T \in SubRing (R) \to +_{R} = +_{H}$
38	6 37	syl	$⊢ φ \to +_{R} = +_{H}$
39	38	adantr	$⊢ (φ \land (X \in B \land Y \in B)) \to +_{R} = +_{H}$
40		ofeq	$⊢ +_{R} = +_{H} \to \circ_{f} +_{R} = \circ_{f} +_{H}$
41	39 40	syl	$⊢ (φ \land (X \in B \land Y \in B)) \to \circ_{f} +_{R} = \circ_{f} +_{H}$
42	41	oveqd	$⊢ (φ \land (X \in B \land Y \in B)) \to X {+_{R}}_{f} Y = X {+_{H}}_{f} Y$
43	36 42	eqtrd	$⊢ (φ \land (X \in B \land Y \in B)) \to X +_{S} Y = X {+_{H}}_{f} Y$
44	4	fvexi	$⊢ B \in V$
45	5 14	ressplusg	$⊢ B \in V \to +_{S} = +_{P}$
46	44 45	mp1i	$⊢ (φ \land (X \in B \land Y \in B)) \to +_{S} = +_{P}$
47	46	oveqd	$⊢ (φ \land (X \in B \land Y \in B)) \to X +_{S} Y = X +_{P} Y$
48	11 43 47	3eqtr2d	$⊢ (φ \land (X \in B \land Y \in B)) \to X +_{U} Y = X +_{P} Y$

Metamath Proof Explorer

Theorem resspsradd

Proof