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

Metamath Proof Explorer

Theorem psrass1

Proof