resspsrmul

Description: A restricted power series algebra has the same 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	resspsrmul	$⊢ (φ \land (X \in B \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		reldmpsr	$⊢ Rel dom mPwSer$
8	7 3 4	elbasov	$⊢ X \in B \to (I \in V \land H \in V)$
9	8	ad2antrl	$⊢ (φ \land (X \in B \land Y \in B)) \to (I \in V \land H \in V)$
10	9	simpld	$⊢ (φ \land (X \in B \land Y \in B)) \to I \in V$
11		eqid	$⊢ \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
12	11	psrbaglefi	$⊢ (I \in V \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\} \in Fin$
13	10 12	sylan	$⊢ ((φ \land (X \in B \land Y \in B)) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\} \in Fin$
14		subrgsubg	$⊢ T \in SubRing (R) \to T \in SubGrp (R)$
15	6 14	syl	$⊢ φ \to T \in SubGrp (R)$
16		subgsubm	$⊢ T \in SubGrp (R) \to T \in SubMnd (R)$
17	15 16	syl	$⊢ φ \to T \in SubMnd (R)$
18	17	ad2antrr	$⊢ ((φ \land (X \in B \land Y \in B)) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to T \in SubMnd (R)$
19	6	ad3antrrr	$⊢ (((φ \land (X \in B \land Y \in B)) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\}) \to T \in SubRing (R)$
20		eqid	$⊢ {Base}_{H} = {Base}_{H}$
21		simprl	$⊢ (φ \land (X \in B \land Y \in B)) \to X \in B$
22	3 20 11 4 21	psrelbas	$⊢ (φ \land (X \in B \land Y \in B)) \to X : \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟶ {Base}_{H}$
23	22	adantr	$⊢ ((φ \land (X \in B \land Y \in B)) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to X : \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟶ {Base}_{H}$
24		elrabi	$⊢ x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\} \to x \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
25		ffvelrn	$⊢ (X : \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟶ {Base}_{H} \land x \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to X (x) \in {Base}_{H}$
26	23 24 25	syl2an	$⊢ (((φ \land (X \in B \land Y \in B)) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\}) \to X (x) \in {Base}_{H}$
27	2	subrgbas	$⊢ T \in SubRing (R) \to T = {Base}_{H}$
28	19 27	syl	$⊢ (((φ \land (X \in B \land Y \in B)) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\}) \to T = {Base}_{H}$
29	26 28	eleqtrrd	$⊢ (((φ \land (X \in B \land Y \in B)) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\}) \to X (x) \in T$
30		simprr	$⊢ (φ \land (X \in B \land Y \in B)) \to Y \in B$
31	3 20 11 4 30	psrelbas	$⊢ (φ \land (X \in B \land Y \in B)) \to Y : \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟶ {Base}_{H}$
32	31	ad2antrr	$⊢ (((φ \land (X \in B \land Y \in B)) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\}) \to Y : \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟶ {Base}_{H}$
33		ssrab2	$⊢ \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\} \subseteq \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
34	10	ad2antrr	$⊢ (((φ \land (X \in B \land Y \in B)) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\}) \to I \in V$
35		simplr	$⊢ (((φ \land (X \in B \land Y \in B)) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\}) \to k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
36		simpr	$⊢ (((φ \land (X \in B \land Y \in B)) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\}) \to x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\}$
37		eqid	$⊢ \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\} = \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\}$
38	11 37	psrbagconcl	$⊢ (I \in V \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \land x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\}) \to k -_{f} x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\}$
39	34 35 36 38	syl3anc	$⊢ (((φ \land (X \in B \land Y \in B)) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\}) \to k -_{f} x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\}$
40	33 39	sseldi	$⊢ (((φ \land (X \in B \land Y \in B)) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\}) \to k -_{f} x \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
41	32 40	ffvelrnd	$⊢ (((φ \land (X \in B \land Y \in B)) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\}) \to Y (k -_{f} x) \in {Base}_{H}$
42	41 28	eleqtrrd	$⊢ (((φ \land (X \in B \land Y \in B)) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\}) \to Y (k -_{f} x) \in T$
43		eqid	$⊢ \cdot_{R} = \cdot_{R}$
44	43	subrgmcl	$⊢ (T \in SubRing (R) \land X (x) \in T \land Y (k -_{f} x) \in T) \to X (x) \cdot_{R} Y (k -_{f} x) \in T$
45	19 29 42 44	syl3anc	$⊢ (((φ \land (X \in B \land Y \in B)) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\}) \to X (x) \cdot_{R} Y (k -_{f} x) \in T$
46	45	fmpttd	$⊢ ((φ \land (X \in B \land Y \in B)) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to (x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x)) : \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\} ⟶ T$
47	13 18 46 2	gsumsubm	$⊢ ((φ \land (X \in B \land Y \in B)) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to \underset{x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\}}{\sum_{R}} (X (x) \cdot_{R} Y (k -_{f} x)) = \underset{x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\}}{\sum_{H}} (X (x) \cdot_{R} Y (k -_{f} x))$
48	2 43	ressmulr	$⊢ T \in SubRing (R) \to \cdot_{R} = \cdot_{H}$
49	6 48	syl	$⊢ φ \to \cdot_{R} = \cdot_{H}$
50	49	ad3antrrr	$⊢ (((φ \land (X \in B \land Y \in B)) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\}) \to \cdot_{R} = \cdot_{H}$
51	50	oveqd	$⊢ (((φ \land (X \in B \land Y \in B)) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\}) \to X (x) \cdot_{R} Y (k -_{f} x) = X (x) \cdot_{H} Y (k -_{f} x)$
52	51	mpteq2dva	$⊢ ((φ \land (X \in B \land Y \in B)) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to (x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x)) = (x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\} ⟼ X (x) \cdot_{H} Y (k -_{f} x))$
53	52	oveq2d	$⊢ ((φ \land (X \in B \land Y \in B)) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to \underset{x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\}}{\sum_{H}} (X (x) \cdot_{R} Y (k -_{f} x)) = \underset{x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\}}{\sum_{H}} (X (x) \cdot_{H} Y (k -_{f} x))$
54	47 53	eqtrd	$⊢ ((φ \land (X \in B \land Y \in B)) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to \underset{x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\}}{\sum_{R}} (X (x) \cdot_{R} Y (k -_{f} x)) = \underset{x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\}}{\sum_{H}} (X (x) \cdot_{H} Y (k -_{f} x))$
55	54	mpteq2dva	$⊢ (φ \land (X \in B \land Y \in B)) \to (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ \underset{x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\}}{\sum_{R}} (X (x) \cdot_{R} Y (k -_{f} x))) = (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ \underset{x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\}}{\sum_{H}} (X (x) \cdot_{H} Y (k -_{f} x)))$
56		eqid	$⊢ {Base}_{S} = {Base}_{S}$
57		eqid	$⊢ \cdot_{S} = \cdot_{S}$
58		fvex	$⊢ {Base}_{R} \in V$
59	6 27	syl	$⊢ φ \to T = {Base}_{H}$
60		eqid	$⊢ {Base}_{R} = {Base}_{R}$
61	60	subrgss	$⊢ T \in SubRing (R) \to T \subseteq {Base}_{R}$
62	6 61	syl	$⊢ φ \to T \subseteq {Base}_{R}$
63	59 62	eqsstrrd	$⊢ φ \to {Base}_{H} \subseteq {Base}_{R}$
64		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\}}$
65	58 63 64	sylancr	$⊢ φ \to {Base}_{H}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}} \subseteq {Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}$
66	65	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\}}$
67	3 20 11 4 10	psrbas	$⊢ (φ \land (X \in B \land Y \in B)) \to B = {Base}_{H}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}$
68	1 60 11 56 10	psrbas	$⊢ (φ \land (X \in B \land Y \in B)) \to {Base}_{S} = {Base}_{R}^{\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}$
69	66 67 68	3sstr4d	$⊢ (φ \land (X \in B \land Y \in B)) \to B \subseteq {Base}_{S}$
70	69 21	sseldd	$⊢ (φ \land (X \in B \land Y \in B)) \to X \in {Base}_{S}$
71	69 30	sseldd	$⊢ (φ \land (X \in B \land Y \in B)) \to Y \in {Base}_{S}$
72	1 56 43 57 11 70 71	psrmulfval	$⊢ (φ \land (X \in B \land Y \in B)) \to X \cdot_{S} Y = (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ \underset{x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\}}{\sum_{R}} (X (x) \cdot_{R} Y (k -_{f} x)))$
73		eqid	$⊢ \cdot_{H} = \cdot_{H}$
74		eqid	$⊢ \cdot_{U} = \cdot_{U}$
75	3 4 73 74 11 21 30	psrmulfval	$⊢ (φ \land (X \in B \land Y \in B)) \to X \cdot_{U} Y = (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ \underset{x \in \{y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| y \leq_{f} k\}}{\sum_{H}} (X (x) \cdot_{H} Y (k -_{f} x)))$
76	55 72 75	3eqtr4rd	$⊢ (φ \land (X \in B \land Y \in B)) \to X \cdot_{U} Y = X \cdot_{S} Y$
77	4	fvexi	$⊢ B \in V$
78	5 57	ressmulr	$⊢ B \in V \to \cdot_{S} = \cdot_{P}$
79	77 78	mp1i	$⊢ (φ \land (X \in B \land Y \in B)) \to \cdot_{S} = \cdot_{P}$
80	79	oveqd	$⊢ (φ \land (X \in B \land Y \in B)) \to X \cdot_{S} Y = X \cdot_{P} Y$
81	76 80	eqtrd	$⊢ (φ \land (X \in B \land Y \in B)) \to X \cdot_{U} Y = X \cdot_{P} Y$

Metamath Proof Explorer

Theorem resspsrmul

Proof