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

Metamath Proof Explorer

Theorem psrass1

Proof