psrass1

Description: Associative identity for the ring of power series. (Contributed by Mario Carneiro, 5-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$
	psrass.z	$⊢ φ \to Z \in B$
Assertion	psrass1	$⊢ φ \to (X \underset{˙}{\times} Y) \underset{˙}{\times} Z = X \underset{˙}{\times} (Y \underset{˙}{\times} Z)$

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		psrass.z	$⊢ φ \to Z \in B$
10		eqid	$⊢ {Base}_{R} = {Base}_{R}$
11	1 6 5 3 7 8	psrmulcl	$⊢ φ \to X \underset{˙}{\times} Y \in B$
12	1 6 5 3 11 9	psrmulcl	$⊢ φ \to (X \underset{˙}{\times} Y) \underset{˙}{\times} Z \in B$
13	1 10 4 6 12	psrelbas	$⊢ φ \to ((X \underset{˙}{\times} Y) \underset{˙}{\times} Z) : D ⟶ {Base}_{R}$
14	13	ffnd	$⊢ φ \to ((X \underset{˙}{\times} Y) \underset{˙}{\times} Z) Fn D$
15	1 6 5 3 8 9	psrmulcl	$⊢ φ \to Y \underset{˙}{\times} Z \in B$
16	1 6 5 3 7 15	psrmulcl	$⊢ φ \to X \underset{˙}{\times} (Y \underset{˙}{\times} Z) \in B$
17	1 10 4 6 16	psrelbas	$⊢ φ \to (X \underset{˙}{\times} (Y \underset{˙}{\times} Z)) : D ⟶ {Base}_{R}$
18	17	ffnd	$⊢ φ \to (X \underset{˙}{\times} (Y \underset{˙}{\times} Z)) Fn D$
19		eqid	$⊢ \{g \in D \| g \leq_{f} x\} = \{g \in D \| g \leq_{f} x\}$
20		simpr	$⊢ (φ \land x \in D) \to x \in D$
21	3	ringcmnd	$⊢ φ \to R \in CMnd$
22	21	adantr	$⊢ (φ \land x \in D) \to R \in CMnd$
23		eqid	$⊢ \cdot_{R} = \cdot_{R}$
24	3	ad3antrrr	$⊢ (((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \land n \in \{h \in D \| h \leq_{f} (x -_{f} j)\}) \to R \in Ring$
25	1 10 4 6 7	psrelbas	$⊢ φ \to X : D ⟶ {Base}_{R}$
26	25	ad2antrr	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to X : D ⟶ {Base}_{R}$
27		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\}$
28		breq1	$⊢ g = j \to (g \leq_{f} x \leftrightarrow j \leq_{f} x)$
29	28	elrab	$⊢ j \in \{g \in D \| g \leq_{f} x\} \leftrightarrow (j \in D \land j \leq_{f} x)$
30	27 29	sylib	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to (j \in D \land j \leq_{f} x)$
31	30	simpld	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to j \in D$
32	26 31	ffvelcdmd	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to X (j) \in {Base}_{R}$
33	32	adantr	$⊢ (((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \land n \in \{h \in D \| h \leq_{f} (x -_{f} j)\}) \to X (j) \in {Base}_{R}$
34	1 10 4 6 8	psrelbas	$⊢ φ \to Y : D ⟶ {Base}_{R}$
35	34	ad3antrrr	$⊢ (((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \land n \in \{h \in D \| h \leq_{f} (x -_{f} j)\}) \to Y : D ⟶ {Base}_{R}$
36		simpr	$⊢ (((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \land n \in \{h \in D \| h \leq_{f} (x -_{f} j)\}) \to n \in \{h \in D \| h \leq_{f} (x -_{f} j)\}$
37		breq1	$⊢ h = n \to (h \leq_{f} (x -_{f} j) \leftrightarrow n \leq_{f} (x -_{f} j))$
38	37	elrab	$⊢ n \in \{h \in D \| h \leq_{f} (x -_{f} j)\} \leftrightarrow (n \in D \land n \leq_{f} (x -_{f} j))$
39	36 38	sylib	$⊢ (((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \land n \in \{h \in D \| h \leq_{f} (x -_{f} j)\}) \to (n \in D \land n \leq_{f} (x -_{f} j))$
40	39	simpld	$⊢ (((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \land n \in \{h \in D \| h \leq_{f} (x -_{f} j)\}) \to n \in D$
41	35 40	ffvelcdmd	$⊢ (((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \land n \in \{h \in D \| h \leq_{f} (x -_{f} j)\}) \to Y (n) \in {Base}_{R}$
42	1 10 4 6 9	psrelbas	$⊢ φ \to Z : D ⟶ {Base}_{R}$
43	42	ad3antrrr	$⊢ (((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \land n \in \{h \in D \| h \leq_{f} (x -_{f} j)\}) \to Z : D ⟶ {Base}_{R}$
44		simplr	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to x \in D$
45	4	psrbagf	$⊢ j \in D \to j : I ⟶ ℕ_{0}$
46	31 45	syl	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to j : I ⟶ ℕ_{0}$
47	30	simprd	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to j \leq_{f} x$
48	4	psrbagcon	$⊢ (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)$
49	44 46 47 48	syl3anc	$⊢ ((φ \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)$
50	49	simpld	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to x -_{f} j \in D$
51	50	adantr	$⊢ (((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \land n \in \{h \in D \| h \leq_{f} (x -_{f} j)\}) \to x -_{f} j \in D$
52	4	psrbagf	$⊢ n \in D \to n : I ⟶ ℕ_{0}$
53	40 52	syl	$⊢ (((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \land n \in \{h \in D \| h \leq_{f} (x -_{f} j)\}) \to n : I ⟶ ℕ_{0}$
54	39	simprd	$⊢ (((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \land n \in \{h \in D \| h \leq_{f} (x -_{f} j)\}) \to n \leq_{f} (x -_{f} j)$
55	4	psrbagcon	$⊢ (x -_{f} j \in D \land n : I ⟶ ℕ_{0} \land n \leq_{f} (x -_{f} j)) \to ((x -_{f} j) -_{f} n \in D \land ((x -_{f} j) -_{f} n) \leq_{f} (x -_{f} j))$
56	51 53 54 55	syl3anc	$⊢ (((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \land n \in \{h \in D \| h \leq_{f} (x -_{f} j)\}) \to ((x -_{f} j) -_{f} n \in D \land ((x -_{f} j) -_{f} n) \leq_{f} (x -_{f} j))$
57	56	simpld	$⊢ (((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \land n \in \{h \in D \| h \leq_{f} (x -_{f} j)\}) \to (x -_{f} j) -_{f} n \in D$
58	43 57	ffvelcdmd	$⊢ (((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \land n \in \{h \in D \| h \leq_{f} (x -_{f} j)\}) \to Z ((x -_{f} j) -_{f} n) \in {Base}_{R}$
59	10 23 24 41 58	ringcld	$⊢ (((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \land n \in \{h \in D \| h \leq_{f} (x -_{f} j)\}) \to Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n) \in {Base}_{R}$
60	10 23 24 33 59	ringcld	$⊢ (((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \land n \in \{h \in D \| h \leq_{f} (x -_{f} j)\}) \to X (j) \cdot_{R} (Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n)) \in {Base}_{R}$
61	60	anasss	$⊢ ((φ \land x \in D) \land (j \in \{g \in D \| g \leq_{f} x\} \land n \in \{h \in D \| h \leq_{f} (x -_{f} j)\})) \to X (j) \cdot_{R} (Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n)) \in {Base}_{R}$
62		fveq2	$⊢ n = k -_{f} j \to Y (n) = Y (k -_{f} j)$
63		oveq2	$⊢ n = k -_{f} j \to (x -_{f} j) -_{f} n = (x -_{f} j) -_{f} (k -_{f} j)$
64	63	fveq2d	$⊢ n = k -_{f} j \to Z ((x -_{f} j) -_{f} n) = Z ((x -_{f} j) -_{f} (k -_{f} j))$
65	62 64	oveq12d	$⊢ n = k -_{f} j \to Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n) = Y (k -_{f} j) \cdot_{R} Z ((x -_{f} j) -_{f} (k -_{f} j))$
66	65	oveq2d	$⊢ n = k -_{f} j \to X (j) \cdot_{R} (Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n)) = X (j) \cdot_{R} (Y (k -_{f} j) \cdot_{R} Z ((x -_{f} j) -_{f} (k -_{f} j)))$
67	4 19 20 10 22 61 66	psrass1lem	$⊢ (φ \land x \in D) \to \underset{k \in \{g \in D \| g \leq_{f} x\}}{\sum_{R}} (\underset{j \in \{h \in D \| h \leq_{f} k\}}{\sum_{R}}, (X (j) \cdot_{R} (Y (k -_{f} j) \cdot_{R} Z ((x -_{f} j) -_{f} (k -_{f} j))))) = \underset{j \in \{g \in D \| g \leq_{f} x\}}{\sum_{R}} (\underset{n \in \{h \in D \| h \leq_{f} (x -_{f} j)\}}{\sum_{R}}, (X (j) \cdot_{R} (Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n))))$
68	7	ad2antrr	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to X \in B$
69	8	ad2antrr	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to Y \in B$
70		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\}$
71		breq1	$⊢ g = k \to (g \leq_{f} x \leftrightarrow k \leq_{f} x)$
72	71	elrab	$⊢ k \in \{g \in D \| g \leq_{f} x\} \leftrightarrow (k \in D \land k \leq_{f} x)$
73	70 72	sylib	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to (k \in D \land k \leq_{f} x)$
74	73	simpld	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to k \in D$
75	1 6 23 5 4 68 69 74	psrmulval	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to (X \underset{˙}{\times} Y) (k) = \underset{j \in \{h \in D \| h \leq_{f} k\}}{\sum_{R}} (X (j) \cdot_{R} Y (k -_{f} j))$
76	75	oveq1d	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to (X \underset{˙}{\times} Y) (k) \cdot_{R} Z (x -_{f} k) = (\underset{j \in \{h \in D \| h \leq_{f} k\}}{\sum_{R}}, (X (j) \cdot_{R} Y (k -_{f} j))) \cdot_{R} Z (x -_{f} k)$
77		eqid	$⊢ 0_{R} = 0_{R}$
78	3	ad2antrr	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to R \in Ring$
79	4	psrbaglefi	$⊢ k \in D \to \{h \in D \| h \leq_{f} k\} \in Fin$
80	74 79	syl	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to \{h \in D \| h \leq_{f} k\} \in Fin$
81	42	ad2antrr	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to Z : D ⟶ {Base}_{R}$
82		simplr	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to x \in D$
83	4	psrbagf	$⊢ k \in D \to k : I ⟶ ℕ_{0}$
84	74 83	syl	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to k : I ⟶ ℕ_{0}$
85	73	simprd	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to k \leq_{f} x$
86	4	psrbagcon	$⊢ (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)$
87	82 84 85 86	syl3anc	$⊢ ((φ \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)$
88	87	simpld	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to x -_{f} k \in D$
89	81 88	ffvelcdmd	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to Z (x -_{f} k) \in {Base}_{R}$
90	3	ad3antrrr	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to R \in Ring$
91	25	ad3antrrr	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to X : D ⟶ {Base}_{R}$
92		simpr	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to j \in \{h \in D \| h \leq_{f} k\}$
93		breq1	$⊢ h = j \to (h \leq_{f} k \leftrightarrow j \leq_{f} k)$
94	93	elrab	$⊢ j \in \{h \in D \| h \leq_{f} k\} \leftrightarrow (j \in D \land j \leq_{f} k)$
95	92 94	sylib	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to (j \in D \land j \leq_{f} k)$
96	95	simpld	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to j \in D$
97	91 96	ffvelcdmd	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to X (j) \in {Base}_{R}$
98	34	ad3antrrr	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to Y : D ⟶ {Base}_{R}$
99	74	adantr	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to k \in D$
100	96 45	syl	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to j : I ⟶ ℕ_{0}$
101	95	simprd	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to j \leq_{f} k$
102	4	psrbagcon	$⊢ (k \in D \land j : I ⟶ ℕ_{0} \land j \leq_{f} k) \to (k -_{f} j \in D \land (k -_{f} j) \leq_{f} k)$
103	99 100 101 102	syl3anc	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to (k -_{f} j \in D \land (k -_{f} j) \leq_{f} k)$
104	103	simpld	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to k -_{f} j \in D$
105	98 104	ffvelcdmd	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to Y (k -_{f} j) \in {Base}_{R}$
106	10 23 90 97 105	ringcld	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to X (j) \cdot_{R} Y (k -_{f} j) \in {Base}_{R}$
107		eqid	$⊢ (j \in \{h \in D \| h \leq_{f} k\} ⟼ X (j) \cdot_{R} Y (k -_{f} j)) = (j \in \{h \in D \| h \leq_{f} k\} ⟼ X (j) \cdot_{R} Y (k -_{f} j))$
108		fvex	$⊢ 0_{R} \in V$
109	108	a1i	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to 0_{R} \in V$
110	107 80 106 109	fsuppmptdm	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to {finSupp}_{0_{R}} ((j \in \{h \in D \| h \leq_{f} k\} ⟼ X (j) \cdot_{R} Y (k -_{f} j)))$
111	10 77 23 78 80 89 106 110	gsummulc1	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to \underset{j \in \{h \in D \| h \leq_{f} k\}}{\sum_{R}} ((X (j) \cdot_{R} Y (k -_{f} j)) \cdot_{R} Z (x -_{f} k)) = (\underset{j \in \{h \in D \| h \leq_{f} k\}}{\sum_{R}}, (X (j) \cdot_{R} Y (k -_{f} j))) \cdot_{R} Z (x -_{f} k)$
112	89	adantr	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to Z (x -_{f} k) \in {Base}_{R}$
113	10 23	ringass	$⊢ (R \in Ring \land (X (j) \in {Base}_{R} \land Y (k -_{f} j) \in {Base}_{R} \land Z (x -_{f} k) \in {Base}_{R})) \to (X (j) \cdot_{R} Y (k -_{f} j)) \cdot_{R} Z (x -_{f} k) = X (j) \cdot_{R} (Y (k -_{f} j) \cdot_{R} Z (x -_{f} k))$
114	90 97 105 112 113	syl13anc	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to (X (j) \cdot_{R} Y (k -_{f} j)) \cdot_{R} Z (x -_{f} k) = X (j) \cdot_{R} (Y (k -_{f} j) \cdot_{R} Z (x -_{f} k))$
115	4	psrbagf	$⊢ x \in D \to x : I ⟶ ℕ_{0}$
116	115	ad3antlr	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to x : I ⟶ ℕ_{0}$
117	116	ffvelcdmda	$⊢ ((((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \land z \in I) \to x (z) \in ℕ_{0}$
118	84	adantr	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to k : I ⟶ ℕ_{0}$
119	118	ffvelcdmda	$⊢ ((((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \land z \in I) \to k (z) \in ℕ_{0}$
120	100	ffvelcdmda	$⊢ ((((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \land z \in I) \to j (z) \in ℕ_{0}$
121		nn0cn	$⊢ x (z) \in ℕ_{0} \to x (z) \in ℂ$
122		nn0cn	$⊢ k (z) \in ℕ_{0} \to k (z) \in ℂ$
123		nn0cn	$⊢ j (z) \in ℕ_{0} \to j (z) \in ℂ$
124		nnncan2	$⊢ (x (z) \in ℂ \land k (z) \in ℂ \land j (z) \in ℂ) \to x (z) - j (z) - (k (z) - j (z)) = x (z) - k (z)$
125	121 122 123 124	syl3an	$⊢ (x (z) \in ℕ_{0} \land k (z) \in ℕ_{0} \land j (z) \in ℕ_{0}) \to x (z) - j (z) - (k (z) - j (z)) = x (z) - k (z)$
126	117 119 120 125	syl3anc	$⊢ ((((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \land z \in I) \to x (z) - j (z) - (k (z) - j (z)) = x (z) - k (z)$
127	126	mpteq2dva	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to (z \in I ⟼ x (z) - j (z) - (k (z) - j (z))) = (z \in I ⟼ x (z) - k (z))$
128	2	ad3antrrr	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to I \in V$
129		ovexd	$⊢ ((((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \land z \in I) \to x (z) - j (z) \in V$
130		ovexd	$⊢ ((((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \land z \in I) \to k (z) - j (z) \in V$
131	116	feqmptd	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to x = (z \in I ⟼ x (z))$
132	100	feqmptd	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to j = (z \in I ⟼ j (z))$
133	128 117 120 131 132	offval2	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to x -_{f} j = (z \in I ⟼ x (z) - j (z))$
134	118	feqmptd	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to k = (z \in I ⟼ k (z))$
135	128 119 120 134 132	offval2	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to k -_{f} j = (z \in I ⟼ k (z) - j (z))$
136	128 129 130 133 135	offval2	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to (x -_{f} j) -_{f} (k -_{f} j) = (z \in I ⟼ x (z) - j (z) - (k (z) - j (z)))$
137	128 117 119 131 134	offval2	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to x -_{f} k = (z \in I ⟼ x (z) - k (z))$
138	127 136 137	3eqtr4d	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to (x -_{f} j) -_{f} (k -_{f} j) = x -_{f} k$
139	138	fveq2d	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to Z ((x -_{f} j) -_{f} (k -_{f} j)) = Z (x -_{f} k)$
140	139	oveq2d	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to Y (k -_{f} j) \cdot_{R} Z ((x -_{f} j) -_{f} (k -_{f} j)) = Y (k -_{f} j) \cdot_{R} Z (x -_{f} k)$
141	140	oveq2d	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to X (j) \cdot_{R} (Y (k -_{f} j) \cdot_{R} Z ((x -_{f} j) -_{f} (k -_{f} j))) = X (j) \cdot_{R} (Y (k -_{f} j) \cdot_{R} Z (x -_{f} k))$
142	114 141	eqtr4d	$⊢ (((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \land j \in \{h \in D \| h \leq_{f} k\}) \to (X (j) \cdot_{R} Y (k -_{f} j)) \cdot_{R} Z (x -_{f} k) = X (j) \cdot_{R} (Y (k -_{f} j) \cdot_{R} Z ((x -_{f} j) -_{f} (k -_{f} j)))$
143	142	mpteq2dva	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to (j \in \{h \in D \| h \leq_{f} k\} ⟼ (X (j) \cdot_{R} Y (k -_{f} j)) \cdot_{R} Z (x -_{f} k)) = (j \in \{h \in D \| h \leq_{f} k\} ⟼ X (j) \cdot_{R} (Y (k -_{f} j) \cdot_{R} Z ((x -_{f} j) -_{f} (k -_{f} j))))$
144	143	oveq2d	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to \underset{j \in \{h \in D \| h \leq_{f} k\}}{\sum_{R}} ((X (j) \cdot_{R} Y (k -_{f} j)) \cdot_{R} Z (x -_{f} k)) = \underset{j \in \{h \in D \| h \leq_{f} k\}}{\sum_{R}} (X (j) \cdot_{R} (Y (k -_{f} j) \cdot_{R} Z ((x -_{f} j) -_{f} (k -_{f} j))))$
145	76 111 144	3eqtr2d	$⊢ ((φ \land x \in D) \land k \in \{g \in D \| g \leq_{f} x\}) \to (X \underset{˙}{\times} Y) (k) \cdot_{R} Z (x -_{f} k) = \underset{j \in \{h \in D \| h \leq_{f} k\}}{\sum_{R}} (X (j) \cdot_{R} (Y (k -_{f} j) \cdot_{R} Z ((x -_{f} j) -_{f} (k -_{f} j))))$
146	145	mpteq2dva	$⊢ (φ \land x \in D) \to (k \in \{g \in D \| g \leq_{f} x\} ⟼ (X \underset{˙}{\times} Y) (k) \cdot_{R} Z (x -_{f} k)) = (k \in \{g \in D \| g \leq_{f} x\} ⟼ \underset{j \in \{h \in D \| h \leq_{f} k\}}{\sum_{R}} (X (j) \cdot_{R} (Y (k -_{f} j) \cdot_{R} Z ((x -_{f} j) -_{f} (k -_{f} j)))))$
147	146	oveq2d	$⊢ (φ \land x \in D) \to \underset{k \in \{g \in D \| g \leq_{f} x\}}{\sum_{R}} ((X \underset{˙}{\times} Y) (k) \cdot_{R} Z (x -_{f} k)) = \underset{k \in \{g \in D \| g \leq_{f} x\}}{\sum_{R}} (\underset{j \in \{h \in D \| h \leq_{f} k\}}{\sum_{R}}, (X (j) \cdot_{R} (Y (k -_{f} j) \cdot_{R} Z ((x -_{f} j) -_{f} (k -_{f} j)))))$
148	8	ad2antrr	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to Y \in B$
149	9	ad2antrr	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to Z \in B$
150	1 6 23 5 4 148 149 50	psrmulval	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to (Y \underset{˙}{\times} Z) (x -_{f} j) = \underset{n \in \{h \in D \| h \leq_{f} (x -_{f} j)\}}{\sum_{R}} (Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n))$
151	150	oveq2d	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to X (j) \cdot_{R} (Y \underset{˙}{\times} Z) (x -_{f} j) = X (j) \cdot_{R} (\underset{n \in \{h \in D \| h \leq_{f} (x -_{f} j)\}}{\sum_{R}}, (Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n)))$
152	3	ad2antrr	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to R \in Ring$
153	4	psrbaglefi	$⊢ x -_{f} j \in D \to \{h \in D \| h \leq_{f} (x -_{f} j)\} \in Fin$
154	50 153	syl	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to \{h \in D \| h \leq_{f} (x -_{f} j)\} \in Fin$
155		ovex	$⊢ {ℕ_{0}}^{I} \in V$
156	4 155	rab2ex	$⊢ \{h \in D \| h \leq_{f} (x -_{f} j)\} \in V$
157	156	mptex	$⊢ (n \in \{h \in D \| h \leq_{f} (x -_{f} j)\} ⟼ Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n)) \in V$
158		funmpt	$⊢ Fun (n \in \{h \in D \| h \leq_{f} (x -_{f} j)\} ⟼ Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n))$
159	157 158 108	3pm3.2i	$⊢ ((n \in \{h \in D \| h \leq_{f} (x -_{f} j)\} ⟼ Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n)) \in V \land Fun (n \in \{h \in D \| h \leq_{f} (x -_{f} j)\} ⟼ Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n)) \land 0_{R} \in V)$
160	159	a1i	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to ((n \in \{h \in D \| h \leq_{f} (x -_{f} j)\} ⟼ Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n)) \in V \land Fun (n \in \{h \in D \| h \leq_{f} (x -_{f} j)\} ⟼ Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n)) \land 0_{R} \in V)$
161		suppssdm	$⊢ (n \in \{h \in D \| h \leq_{f} (x -_{f} j)\} ⟼ Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n)) supp 0_{R} \subseteq dom (n \in \{h \in D \| h \leq_{f} (x -_{f} j)\} ⟼ Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n))$
162		eqid	$⊢ (n \in \{h \in D \| h \leq_{f} (x -_{f} j)\} ⟼ Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n)) = (n \in \{h \in D \| h \leq_{f} (x -_{f} j)\} ⟼ Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n))$
163	162	dmmptss	$⊢ dom (n \in \{h \in D \| h \leq_{f} (x -_{f} j)\} ⟼ Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n)) \subseteq \{h \in D \| h \leq_{f} (x -_{f} j)\}$
164	161 163	sstri	$⊢ (n \in \{h \in D \| h \leq_{f} (x -_{f} j)\} ⟼ Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n)) supp 0_{R} \subseteq \{h \in D \| h \leq_{f} (x -_{f} j)\}$
165	164	a1i	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to (n \in \{h \in D \| h \leq_{f} (x -_{f} j)\} ⟼ Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n)) supp 0_{R} \subseteq \{h \in D \| h \leq_{f} (x -_{f} j)\}$
166		suppssfifsupp	$⊢ (((n \in \{h \in D \| h \leq_{f} (x -_{f} j)\} ⟼ Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n)) \in V \land Fun (n \in \{h \in D \| h \leq_{f} (x -_{f} j)\} ⟼ Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n)) \land 0_{R} \in V) \land (\{h \in D \| h \leq_{f} (x -_{f} j)\} \in Fin \land (n \in \{h \in D \| h \leq_{f} (x -_{f} j)\} ⟼ Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n)) supp 0_{R} \subseteq \{h \in D \| h \leq_{f} (x -_{f} j)\})) \to {finSupp}_{0_{R}} ((n \in \{h \in D \| h \leq_{f} (x -_{f} j)\} ⟼ Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n)))$
167	160 154 165 166	syl12anc	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to {finSupp}_{0_{R}} ((n \in \{h \in D \| h \leq_{f} (x -_{f} j)\} ⟼ Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n)))$
168	10 77 23 152 154 32 59 167	gsummulc2	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to \underset{n \in \{h \in D \| h \leq_{f} (x -_{f} j)\}}{\sum_{R}} (X (j) \cdot_{R} (Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n))) = X (j) \cdot_{R} (\underset{n \in \{h \in D \| h \leq_{f} (x -_{f} j)\}}{\sum_{R}}, (Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n)))$
169	151 168	eqtr4d	$⊢ ((φ \land x \in D) \land j \in \{g \in D \| g \leq_{f} x\}) \to X (j) \cdot_{R} (Y \underset{˙}{\times} Z) (x -_{f} j) = \underset{n \in \{h \in D \| h \leq_{f} (x -_{f} j)\}}{\sum_{R}} (X (j) \cdot_{R} (Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n)))$
170	169	mpteq2dva	$⊢ (φ \land x \in D) \to (j \in \{g \in D \| g \leq_{f} x\} ⟼ X (j) \cdot_{R} (Y \underset{˙}{\times} Z) (x -_{f} j)) = (j \in \{g \in D \| g \leq_{f} x\} ⟼ \underset{n \in \{h \in D \| h \leq_{f} (x -_{f} j)\}}{\sum_{R}} (X (j) \cdot_{R} (Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n))))$
171	170	oveq2d	$⊢ (φ \land x \in D) \to \underset{j \in \{g \in D \| g \leq_{f} x\}}{\sum_{R}} (X (j) \cdot_{R} (Y \underset{˙}{\times} Z) (x -_{f} j)) = \underset{j \in \{g \in D \| g \leq_{f} x\}}{\sum_{R}} (\underset{n \in \{h \in D \| h \leq_{f} (x -_{f} j)\}}{\sum_{R}}, (X (j) \cdot_{R} (Y (n) \cdot_{R} Z ((x -_{f} j) -_{f} n))))$
172	67 147 171	3eqtr4d	$⊢ (φ \land x \in D) \to \underset{k \in \{g \in D \| g \leq_{f} x\}}{\sum_{R}} ((X \underset{˙}{\times} Y) (k) \cdot_{R} Z (x -_{f} k)) = \underset{j \in \{g \in D \| g \leq_{f} x\}}{\sum_{R}} (X (j) \cdot_{R} (Y \underset{˙}{\times} Z) (x -_{f} j))$
173	11	adantr	$⊢ (φ \land x \in D) \to X \underset{˙}{\times} Y \in B$
174	9	adantr	$⊢ (φ \land x \in D) \to Z \in B$
175	1 6 23 5 4 173 174 20	psrmulval	$⊢ (φ \land x \in D) \to ((X \underset{˙}{\times} Y) \underset{˙}{\times} Z) (x) = \underset{k \in \{g \in D \| g \leq_{f} x\}}{\sum_{R}} ((X \underset{˙}{\times} Y) (k) \cdot_{R} Z (x -_{f} k))$
176	7	adantr	$⊢ (φ \land x \in D) \to X \in B$
177	15	adantr	$⊢ (φ \land x \in D) \to Y \underset{˙}{\times} Z \in B$
178	1 6 23 5 4 176 177 20	psrmulval	$⊢ (φ \land x \in D) \to (X \underset{˙}{\times} (Y \underset{˙}{\times} Z)) (x) = \underset{j \in \{g \in D \| g \leq_{f} x\}}{\sum_{R}} (X (j) \cdot_{R} (Y \underset{˙}{\times} Z) (x -_{f} j))$
179	172 175 178	3eqtr4d	$⊢ (φ \land x \in D) \to ((X \underset{˙}{\times} Y) \underset{˙}{\times} Z) (x) = (X \underset{˙}{\times} (Y \underset{˙}{\times} Z)) (x)$
180	14 18 179	eqfnfvd	$⊢ φ \to (X \underset{˙}{\times} Y) \underset{˙}{\times} Z = X \underset{˙}{\times} (Y \underset{˙}{\times} Z)$

Metamath Proof Explorer

Theorem psrass1

Proof