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

Metamath Proof Explorer

Theorem resspsrmul

Proof