resspsrvsca

Description: A restricted power series algebra has the same scalar multiplication 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	resspsrvsca	$⊢ (φ \land (X \in T \land Y \in B)) \to X \cdot_{U} Y = X \cdot_{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	$⊢ \cdot_{U} = \cdot_{U}$
8		eqid	$⊢ {Base}_{H} = {Base}_{H}$
9		eqid	$⊢ \cdot_{H} = \cdot_{H}$
10		eqid	$⊢ \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
11		simprl	$⊢ (φ \land (X \in T \land Y \in B)) \to X \in T$
12	6	adantr	$⊢ (φ \land (X \in T \land Y \in B)) \to T \in SubRing (R)$
13	2	subrgbas	$⊢ T \in SubRing (R) \to T = {Base}_{H}$
14	12 13	syl	$⊢ (φ \land (X \in T \land Y \in B)) \to T = {Base}_{H}$
15	11 14	eleqtrd	$⊢ (φ \land (X \in T \land Y \in B)) \to X \in {Base}_{H}$
16		simprr	$⊢ (φ \land (X \in T \land Y \in B)) \to Y \in B$
17	3 7 8 4 9 10 15 16	psrvsca	$⊢ (φ \land (X \in T \land Y \in B)) \to X \cdot_{U} Y = (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{X\}) {\cdot_{H}}_{f} Y$
18		eqid	$⊢ \cdot_{S} = \cdot_{S}$
19		eqid	$⊢ {Base}_{R} = {Base}_{R}$
20		eqid	$⊢ {Base}_{S} = {Base}_{S}$
21		eqid	$⊢ \cdot_{R} = \cdot_{R}$
22	19	subrgss	$⊢ T \in SubRing (R) \to T \subseteq {Base}_{R}$
23	12 22	syl	$⊢ (φ \land (X \in T \land Y \in B)) \to T \subseteq {Base}_{R}$
24	23 11	sseldd	$⊢ (φ \land (X \in T \land Y \in B)) \to X \in {Base}_{R}$
25	1 2 3 4 5 6	resspsrbas	$⊢ φ \to B = {Base}_{P}$
26	5 20	ressbasss	$⊢ {Base}_{P} \subseteq {Base}_{S}$
27	25 26	eqsstrdi	$⊢ φ \to B \subseteq {Base}_{S}$
28	27	adantr	$⊢ (φ \land (X \in T \land Y \in B)) \to B \subseteq {Base}_{S}$
29	28 16	sseldd	$⊢ (φ \land (X \in T \land Y \in B)) \to Y \in {Base}_{S}$
30	1 18 19 20 21 10 24 29	psrvsca	$⊢ (φ \land (X \in T \land Y \in B)) \to X \cdot_{S} Y = (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{X\}) {\cdot_{R}}_{f} Y$
31	2 21	ressmulr	$⊢ T \in SubRing (R) \to \cdot_{R} = \cdot_{H}$
32		ofeq	$⊢ \cdot_{R} = \cdot_{H} \to \circ_{f} \cdot_{R} = \circ_{f} \cdot_{H}$
33	12 31 32	3syl	$⊢ (φ \land (X \in T \land Y \in B)) \to \circ_{f} \cdot_{R} = \circ_{f} \cdot_{H}$
34	33	oveqd	$⊢ (φ \land (X \in T \land Y \in B)) \to (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{X\}) {\cdot_{R}}_{f} Y = (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{X\}) {\cdot_{H}}_{f} Y$
35	30 34	eqtrd	$⊢ (φ \land (X \in T \land Y \in B)) \to X \cdot_{S} Y = (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \times \{X\}) {\cdot_{H}}_{f} Y$
36	4	fvexi	$⊢ B \in V$
37	5 18	ressvsca	$⊢ B \in V \to \cdot_{S} = \cdot_{P}$
38	36 37	mp1i	$⊢ (φ \land (X \in T \land Y \in B)) \to \cdot_{S} = \cdot_{P}$
39	38	oveqd	$⊢ (φ \land (X \in T \land Y \in B)) \to X \cdot_{S} Y = X \cdot_{P} Y$
40	17 35 39	3eqtr2d	$⊢ (φ \land (X \in T \land Y \in B)) \to X \cdot_{U} Y = X \cdot_{P} Y$

Metamath Proof Explorer

Theorem resspsrvsca

Proof