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

Metamath Proof Explorer

Theorem psrass1

Proof