psrcom

Description: Commutative law for the ring of power series. (Contributed by Mario Carneiro, 7-Jan-2015)

	Ref	Expression
Hypotheses	psrring.s	$⊢ S = I mPwSer R$
	psrring.i	$⊢ φ \to I \in V$
	psrring.r	$⊢ φ \to R \in Ring$
	psrass.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	psrass.t	$⊢ \underset{˙}{\times} = \cdot_{S}$
	psrass.b	$⊢ B = {Base}_{S}$
	psrass.x	$⊢ φ \to X \in B$
	psrass.y	$⊢ φ \to Y \in B$
	psrcom.c	$⊢ φ \to R \in CRing$
Assertion	psrcom	$⊢ φ \to X \underset{˙}{\times} Y = Y \underset{˙}{\times} X$

Proof

Step	Hyp	Ref	Expression
1		psrring.s	$⊢ S = I mPwSer R$
2		psrring.i	$⊢ φ \to I \in V$
3		psrring.r	$⊢ φ \to R \in Ring$
4		psrass.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
5		psrass.t	$⊢ \underset{˙}{\times} = \cdot_{S}$
6		psrass.b	$⊢ B = {Base}_{S}$
7		psrass.x	$⊢ φ \to X \in B$
8		psrass.y	$⊢ φ \to Y \in B$
9		psrcom.c	$⊢ φ \to R \in CRing$
10		eqid	$⊢ {Base}_{R} = {Base}_{R}$
11		eqid	$⊢ 0_{R} = 0_{R}$
12		ringcmn	$⊢ R \in Ring \to R \in CMnd$
13	3 12	syl	$⊢ φ \to R \in CMnd$
14	13	adantr	$⊢ (φ \land x \in D) \to R \in CMnd$
15	4	psrbaglefi	$⊢ (I \in V \land x \in D) \to \{g \in D \| g \leq_{f} x\} \in Fin$
16	2 15	sylan	$⊢ (φ \land x \in D) \to \{g \in D \| g \leq_{f} x\} \in Fin$
17	3	ad2antrr	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to R \in Ring$
18	1 10 4 6 7	psrelbas	$⊢ φ \to X : D ⟶ {Base}_{R}$
19	18	ad2antrr	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to X : D ⟶ {Base}_{R}$
20		simpr	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to k \in \{g \in D \| g \leq_{f} x\}$
21		breq1	$⊢ g = k \to (g \leq_{f} x \leftrightarrow k \leq_{f} x)$
22	21	elrab	$⊢ k \in \{g \in D \| g \leq_{f} x\} \leftrightarrow (k \in D \land k \leq_{f} x)$
23	20 22	sylib	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to (k \in D \land k \leq_{f} x)$
24	23	simpld	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to k \in D$
25	19 24	ffvelrnd	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to X (k) \in {Base}_{R}$
26	1 10 4 6 8	psrelbas	$⊢ φ \to Y : D ⟶ {Base}_{R}$
27	26	ad2antrr	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to Y : D ⟶ {Base}_{R}$
28	2	ad2antrr	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to I \in V$
29		simplr	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to x \in D$
30	4	psrbagf	$⊢ (I \in V \land k \in D) \to k : I ⟶ ℕ_{0}$
31	28 24 30	syl2anc	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to k : I ⟶ ℕ_{0}$
32	23	simprd	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to k \leq_{f} x$
33	4	psrbagcon	$⊢ (I \in V \land (x \in D \land k : I ⟶ ℕ_{0} \land k \leq_{f} x)) \to (x -_{f} k \in D \land (x -_{f} k) \leq_{f} x)$
34	28 29 31 32 33	syl13anc	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to (x -_{f} k \in D \land (x -_{f} k) \leq_{f} x)$
35	34	simpld	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to x -_{f} k \in D$
36	27 35	ffvelrnd	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to Y (x -_{f} k) \in {Base}_{R}$
37		eqid	$⊢ \cdot_{R} = \cdot_{R}$
38	10 37	ringcl	$⊢ (R \in Ring \land X (k) \in {Base}_{R} \land Y (x -_{f} k) \in {Base}_{R}) \to X (k) \cdot_{R} Y (x -_{f} k) \in {Base}_{R}$
39	17 25 36 38	syl3anc	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to X (k) \cdot_{R} Y (x -_{f} k) \in {Base}_{R}$
40	39	fmpttd	$⊢ (φ \land x \in D) \to (k \in \{g \in D \| g \leq_{f} x\} ⟼ X (k) \cdot_{R} Y (x -_{f} k)) : \{g \in D \| g \leq_{f} x\} ⟶ {Base}_{R}$
41		ovex	$⊢ {ℕ_{0}}^{I} \in V$
42	4 41	rabex2	$⊢ D \in V$
43	42	a1i	$⊢ (φ \land x \in D) \to D \in V$
44		rabexg	$⊢ D \in V \to \{g \in D \| g \leq_{f} x\} \in V$
45	43 44	syl	$⊢ (φ \land x \in D) \to \{g \in D \| g \leq_{f} x\} \in V$
46	45	mptexd	$⊢ (φ \land x \in D) \to (k \in \{g \in D \| g \leq_{f} x\} ⟼ X (k) \cdot_{R} Y (x -_{f} k)) \in V$
47		funmpt	$⊢ Fun (k \in \{g \in D \| g \leq_{f} x\} ⟼ X (k) \cdot_{R} Y (x -_{f} k))$
48	47	a1i	$⊢ (φ \land x \in D) \to Fun (k \in \{g \in D \| g \leq_{f} x\} ⟼ X (k) \cdot_{R} Y (x -_{f} k))$
49		fvexd	$⊢ (φ \land x \in D) \to 0_{R} \in V$
50		suppssdm	$⊢ (k \in \{g \in D \| g \leq_{f} x\} ⟼ X (k) \cdot_{R} Y (x -_{f} k)) supp 0_{R} \subseteq dom (k \in \{g \in D \| g \leq_{f} x\} ⟼ X (k) \cdot_{R} Y (x -_{f} k))$
51		eqid	$⊢ (k \in \{g \in D \| g \leq_{f} x\} ⟼ X (k) \cdot_{R} Y (x -_{f} k)) = (k \in \{g \in D \| g \leq_{f} x\} ⟼ X (k) \cdot_{R} Y (x -_{f} k))$
52	51	dmmptss	$⊢ dom (k \in \{g \in D \| g \leq_{f} x\} ⟼ X (k) \cdot_{R} Y (x -_{f} k)) \subseteq \{g \in D \| g \leq_{f} x\}$
53	50 52	sstri	$⊢ (k \in \{g \in D \| g \leq_{f} x\} ⟼ X (k) \cdot_{R} Y (x -_{f} k)) supp 0_{R} \subseteq \{g \in D \| g \leq_{f} x\}$
54	53	a1i	$⊢ (φ \land x \in D) \to (k \in \{g \in D \| g \leq_{f} x\} ⟼ X (k) \cdot_{R} Y (x -_{f} k)) supp 0_{R} \subseteq \{g \in D \| g \leq_{f} x\}$
55		suppssfifsupp	$⊢ (((k \in \{g \in D \| g \leq_{f} x\} ⟼ X (k) \cdot_{R} Y (x -_{f} k)) \in V \land Fun (k \in \{g \in D \| g \leq_{f} x\} ⟼ X (k) \cdot_{R} Y (x -_{f} k)) \land 0_{R} \in V) \land (\{g \in D \| g \leq_{f} x\} \in Fin \land (k \in \{g \in D \| g \leq_{f} x\} ⟼ X (k) \cdot_{R} Y (x -_{f} k)) supp 0_{R} \subseteq \{g \in D \| g \leq_{f} x\})) \to {finSupp}_{0_{R}} ((k \in \{g \in D \| g \leq_{f} x\} ⟼ X (k) \cdot_{R} Y (x -_{f} k)))$
56	46 48 49 16 54 55	syl32anc	$⊢ (φ \land x \in D) \to {finSupp}_{0_{R}} ((k \in \{g \in D \| g \leq_{f} x\} ⟼ X (k) \cdot_{R} Y (x -_{f} k)))$
57		eqid	$⊢ \{g \in D \| g \leq_{f} x\} = \{g \in D \| g \leq_{f} x\}$
58	4 57	psrbagconf1o	$⊢ (I \in V \land x \in D) \to (j \in \{g \in D \| g \leq_{f} x\} ⟼ x -_{f} j) : \{g \in D \| g \leq_{f} x\} \underset{1-1 onto}{⟶} \{g \in D \| g \leq_{f} x\}$
59	2 58	sylan	$⊢ (φ \land x \in D) \to (j \in \{g \in D \| g \leq_{f} x\} ⟼ x -_{f} j) : \{g \in D \| g \leq_{f} x\} \underset{1-1 onto}{⟶} \{g \in D \| g \leq_{f} x\}$
60	10 11 14 16 40 56 59	gsumf1o	$⊢ (φ \land x \in D) \to \underset{k \in \{g \in D \| g \leq_{f} x\}}{\sum_{R}} (X (k) \cdot_{R} Y (x -_{f} k)) = \sum_{R} ((k \in \{g \in D \| g \leq_{f} x\} ⟼ X (k) \cdot_{R} Y (x -_{f} k)) \circ (j \in \{g \in D \| g \leq_{f} x\} ⟼ x -_{f} j))$
61	2	ad2antrr	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to I \in V$
62		simplr	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to x \in D$
63		simpr	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to j \in \{g \in D \| g \leq_{f} x\}$
64	4 57	psrbagconcl	$⊢ (I \in V \land x \in D \land j \in \{g \in D \| g \leq_{f} x\}) \to x -_{f} j \in \{g \in D \| g \leq_{f} x\}$
65	61 62 63 64	syl3anc	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to x -_{f} j \in \{g \in D \| g \leq_{f} x\}$
66		eqidd	$⊢ (φ \land x \in D) \to (j \in \{g \in D \| g \leq_{f} x\} ⟼ x -_{f} j) = (j \in \{g \in D \| g \leq_{f} x\} ⟼ x -_{f} j)$
67		eqidd	$⊢ (φ \land x \in D) \to (k \in \{g \in D \| g \leq_{f} x\} ⟼ X (k) \cdot_{R} Y (x -_{f} k)) = (k \in \{g \in D \| g \leq_{f} x\} ⟼ X (k) \cdot_{R} Y (x -_{f} k))$
68		fveq2	$⊢ k = x -_{f} j \to X (k) = X (x -_{f} j)$
69		oveq2	$⊢ k = x -_{f} j \to x -_{f} k = x -_{f} (x -_{f} j)$
70	69	fveq2d	$⊢ k = x -_{f} j \to Y (x -_{f} k) = Y (x -_{f} (x -_{f} j))$
71	68 70	oveq12d	$⊢ k = x -_{f} j \to X (k) \cdot_{R} Y (x -_{f} k) = X (x -_{f} j) \cdot_{R} Y (x -_{f} (x -_{f} j))$
72	65 66 67 71	fmptco	$⊢ (φ \land x \in D) \to (k \in \{g \in D \| g \leq_{f} x\} ⟼ X (k) \cdot_{R} Y (x -_{f} k)) \circ (j \in \{g \in D \| g \leq_{f} x\} ⟼ x -_{f} j) = (j \in \{g \in D \| g \leq_{f} x\} ⟼ X (x -_{f} j) \cdot_{R} Y (x -_{f} (x -_{f} j)))$
73	4	psrbagf	$⊢ (I \in V \land x \in D) \to x : I ⟶ ℕ_{0}$
74	2 73	sylan	$⊢ (φ \land x \in D) \to x : I ⟶ ℕ_{0}$
75	74	adantr	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to x : I ⟶ ℕ_{0}$
76	75	ffvelrnda	$⊢ (((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \land z \in I) \to x (z) \in ℕ_{0}$
77		breq1	$⊢ g = j \to (g \leq_{f} x \leftrightarrow j \leq_{f} x)$
78	77	elrab	$⊢ j \in \{g \in D \| g \leq_{f} x\} \leftrightarrow (j \in D \land j \leq_{f} x)$
79	63 78	sylib	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to (j \in D \land j \leq_{f} x)$
80	79	simpld	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to j \in D$
81	4	psrbagf	$⊢ (I \in V \land j \in D) \to j : I ⟶ ℕ_{0}$
82	61 80 81	syl2anc	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to j : I ⟶ ℕ_{0}$
83	82	ffvelrnda	$⊢ (((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \land z \in I) \to j (z) \in ℕ_{0}$
84		nn0cn	$⊢ x (z) \in ℕ_{0} \to x (z) \in ℂ$
85		nn0cn	$⊢ j (z) \in ℕ_{0} \to j (z) \in ℂ$
86		nncan	$⊢ (x (z) \in ℂ \land j (z) \in ℂ) \to x (z) - (x (z) - j (z)) = j (z)$
87	84 85 86	syl2an	$⊢ (x (z) \in ℕ_{0} \land j (z) \in ℕ_{0}) \to x (z) - (x (z) - j (z)) = j (z)$
88	76 83 87	syl2anc	$⊢ (((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \land z \in I) \to x (z) - (x (z) - j (z)) = j (z)$
89	88	mpteq2dva	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to (z \in I ⟼ x (z) - (x (z) - j (z))) = (z \in I ⟼ j (z))$
90		ovex	$⊢ x (z) - j (z) \in V$
91	90	a1i	$⊢ (((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \land z \in I) \to x (z) - j (z) \in V$
92	75	feqmptd	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to x = (z \in I ⟼ x (z))$
93	82	feqmptd	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to j = (z \in I ⟼ j (z))$
94	61 76 83 92 93	offval2	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to x -_{f} j = (z \in I ⟼ x (z) - j (z))$
95	61 76 91 92 94	offval2	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to x -_{f} (x -_{f} j) = (z \in I ⟼ x (z) - (x (z) - j (z)))$
96	89 95 93	3eqtr4d	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to x -_{f} (x -_{f} j) = j$
97	96	fveq2d	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to Y (x -_{f} (x -_{f} j)) = Y (j)$
98	97	oveq2d	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to X (x -_{f} j) \cdot_{R} Y (x -_{f} (x -_{f} j)) = X (x -_{f} j) \cdot_{R} Y (j)$
99	9	ad2antrr	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to R \in CRing$
100	18	ad2antrr	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to X : D ⟶ {Base}_{R}$
101	79	simprd	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to j \leq_{f} x$
102	4	psrbagcon	$⊢ (I \in V \land (x \in D \land j : I ⟶ ℕ_{0} \land j \leq_{f} x)) \to (x -_{f} j \in D \land (x -_{f} j) \leq_{f} x)$
103	61 62 82 101 102	syl13anc	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to (x -_{f} j \in D \land (x -_{f} j) \leq_{f} x)$
104	103	simpld	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to x -_{f} j \in D$
105	100 104	ffvelrnd	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to X (x -_{f} j) \in {Base}_{R}$
106	26	ad2antrr	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to Y : D ⟶ {Base}_{R}$
107	106 80	ffvelrnd	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to Y (j) \in {Base}_{R}$
108	10 37	crngcom	$⊢ (R \in CRing \land X (x -_{f} j) \in {Base}_{R} \land Y (j) \in {Base}_{R}) \to X (x -_{f} j) \cdot_{R} Y (j) = Y (j) \cdot_{R} X (x -_{f} j)$
109	99 105 107 108	syl3anc	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to X (x -_{f} j) \cdot_{R} Y (j) = Y (j) \cdot_{R} X (x -_{f} j)$
110	98 109	eqtrd	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to X (x -_{f} j) \cdot_{R} Y (x -_{f} (x -_{f} j)) = Y (j) \cdot_{R} X (x -_{f} j)$
111	110	mpteq2dva	$⊢ (φ \land x \in D) \to (j \in \{g \in D \| g \leq_{f} x\} ⟼ X (x -_{f} j) \cdot_{R} Y (x -_{f} (x -_{f} j))) = (j \in \{g \in D \| g \leq_{f} x\} ⟼ Y (j) \cdot_{R} X (x -_{f} j))$
112	72 111	eqtrd	$⊢ (φ \land x \in D) \to (k \in \{g \in D \| g \leq_{f} x\} ⟼ X (k) \cdot_{R} Y (x -_{f} k)) \circ (j \in \{g \in D \| g \leq_{f} x\} ⟼ x -_{f} j) = (j \in \{g \in D \| g \leq_{f} x\} ⟼ Y (j) \cdot_{R} X (x -_{f} j))$
113	112	oveq2d	$⊢ (φ \land x \in D) \to \sum_{R} ((k \in \{g \in D \| g \leq_{f} x\} ⟼ X (k) \cdot_{R} Y (x -_{f} k)) \circ (j \in \{g \in D \| g \leq_{f} x\} ⟼ x -_{f} j)) = \underset{j \in \{g \in D \| g \leq_{f} x\}}{\sum_{R}} (Y (j) \cdot_{R} X (x -_{f} j))$
114	60 113	eqtrd	$⊢ (φ \land x \in D) \to \underset{k \in \{g \in D \| g \leq_{f} x\}}{\sum_{R}} (X (k) \cdot_{R} Y (x -_{f} k)) = \underset{j \in \{g \in D \| g \leq_{f} x\}}{\sum_{R}} (Y (j) \cdot_{R} X (x -_{f} j))$
115	114	mpteq2dva	$⊢ φ \to (x \in D ⟼ \underset{k \in \{g \in D \| g \leq_{f} x\}}{\sum_{R}} (X (k) \cdot_{R} Y (x -_{f} k))) = (x \in D ⟼ \underset{j \in \{g \in D \| g \leq_{f} x\}}{\sum_{R}} (Y (j) \cdot_{R} X (x -_{f} j)))$
116	1 6 37 5 4 7 8	psrmulfval	$⊢ φ \to X \underset{˙}{\times} Y = (x \in D ⟼ \underset{k \in \{g \in D \| g \leq_{f} x\}}{\sum_{R}} (X (k) \cdot_{R} Y (x -_{f} k)))$
117	1 6 37 5 4 8 7	psrmulfval	$⊢ φ \to Y \underset{˙}{\times} X = (x \in D ⟼ \underset{j \in \{g \in D \| g \leq_{f} x\}}{\sum_{R}} (Y (j) \cdot_{R} X (x -_{f} j)))$
118	115 116 117	3eqtr4d	$⊢ φ \to X \underset{˙}{\times} Y = Y \underset{˙}{\times} X$

Metamath Proof Explorer

Theorem psrcom

Proof