psrdi

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

	Ref	Expression
Hypotheses	psrring.s	$⊢ S = I mPwSer R$
	psrring.i	$⊢ φ \to I \in V$
	psrring.r	$⊢ φ \to R \in Ring$
	psrass.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	psrass.t	$⊢ \underset{˙}{\times} = \cdot_{S}$
	psrass.b	$⊢ B = {Base}_{S}$
	psrass.x	$⊢ φ \to X \in B$
	psrass.y	$⊢ φ \to Y \in B$
	psrass.z	$⊢ φ \to Z \in B$
	psrdi.a	$⊢ \underset{˙}{+} = +_{S}$
Assertion	psrdi	$⊢ φ \to X \underset{˙}{\times} (Y \underset{˙}{+} Z) = (X \underset{˙}{\times} Y) \underset{˙}{+} (X \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		psrdi.a	$⊢ \underset{˙}{+} = +_{S}$
11		eqid	$⊢ +_{R} = +_{R}$
12	1 6 11 10 8 9	psradd	$⊢ φ \to Y \underset{˙}{+} Z = Y {+_{R}}_{f} Z$
13	12	fveq1d	$⊢ φ \to (Y \underset{˙}{+} Z) (k -_{f} x) = (Y {+_{R}}_{f} Z) (k -_{f} x)$
14	13	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to (Y \underset{˙}{+} Z) (k -_{f} x) = (Y {+_{R}}_{f} Z) (k -_{f} x)$
15		ssrab2	$⊢ \{y \in D \| y \leq_{f} k\} \subseteq D$
16		eqid	$⊢ \{y \in D \| y \leq_{f} k\} = \{y \in D \| y \leq_{f} k\}$
17	4 16	psrbagconcl	$⊢ (k \in D \land x \in \{y \in D \| y \leq_{f} k\}) \to k -_{f} x \in \{y \in D \| y \leq_{f} k\}$
18	17	adantll	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to k -_{f} x \in \{y \in D \| y \leq_{f} k\}$
19	15 18	sselid	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to k -_{f} x \in D$
20		eqid	$⊢ {Base}_{R} = {Base}_{R}$
21	1 20 4 6 8	psrelbas	$⊢ φ \to Y : D ⟶ {Base}_{R}$
22	21	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Y : D ⟶ {Base}_{R}$
23	22	ffnd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Y Fn D$
24	1 20 4 6 9	psrelbas	$⊢ φ \to Z : D ⟶ {Base}_{R}$
25	24	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Z : D ⟶ {Base}_{R}$
26	25	ffnd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Z Fn D$
27		ovex	$⊢ {ℕ_{0}}^{I} \in V$
28	4 27	rabex2	$⊢ D \in V$
29	28	a1i	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to D \in V$
30		inidm	$⊢ D \cap D = D$
31		eqidd	$⊢ (((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \land k -_{f} x \in D) \to Y (k -_{f} x) = Y (k -_{f} x)$
32		eqidd	$⊢ (((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \land k -_{f} x \in D) \to Z (k -_{f} x) = Z (k -_{f} x)$
33	23 26 29 29 30 31 32	ofval	$⊢ (((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \land k -_{f} x \in D) \to (Y {+_{R}}_{f} Z) (k -_{f} x) = Y (k -_{f} x) +_{R} Z (k -_{f} x)$
34	19 33	mpdan	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to (Y {+_{R}}_{f} Z) (k -_{f} x) = Y (k -_{f} x) +_{R} Z (k -_{f} x)$
35	14 34	eqtrd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to (Y \underset{˙}{+} Z) (k -_{f} x) = Y (k -_{f} x) +_{R} Z (k -_{f} x)$
36	35	oveq2d	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X (x) \cdot_{R} (Y \underset{˙}{+} Z) (k -_{f} x) = X (x) \cdot_{R} (Y (k -_{f} x) +_{R} Z (k -_{f} x))$
37	3	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to R \in Ring$
38	1 20 4 6 7	psrelbas	$⊢ φ \to X : D ⟶ {Base}_{R}$
39	38	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X : D ⟶ {Base}_{R}$
40		simpr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to x \in \{y \in D \| y \leq_{f} k\}$
41	15 40	sselid	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to x \in D$
42	39 41	ffvelcdmd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X (x) \in {Base}_{R}$
43	22 19	ffvelcdmd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Y (k -_{f} x) \in {Base}_{R}$
44	25 19	ffvelcdmd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Z (k -_{f} x) \in {Base}_{R}$
45		eqid	$⊢ \cdot_{R} = \cdot_{R}$
46	20 11 45	ringdi	$⊢ (R \in Ring \land (X (x) \in {Base}_{R} \land Y (k -_{f} x) \in {Base}_{R} \land Z (k -_{f} x) \in {Base}_{R})) \to X (x) \cdot_{R} (Y (k -_{f} x) +_{R} Z (k -_{f} x)) = (X (x) \cdot_{R} Y (k -_{f} x)) +_{R} (X (x) \cdot_{R} Z (k -_{f} x))$
47	37 42 43 44 46	syl13anc	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X (x) \cdot_{R} (Y (k -_{f} x) +_{R} Z (k -_{f} x)) = (X (x) \cdot_{R} Y (k -_{f} x)) +_{R} (X (x) \cdot_{R} Z (k -_{f} x))$
48	36 47	eqtrd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X (x) \cdot_{R} (Y \underset{˙}{+} Z) (k -_{f} x) = (X (x) \cdot_{R} Y (k -_{f} x)) +_{R} (X (x) \cdot_{R} Z (k -_{f} x))$
49	48	mpteq2dva	$⊢ (φ \land k \in D) \to (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} (Y \underset{˙}{+} Z) (k -_{f} x)) = (x \in \{y \in D \| y \leq_{f} k\} ⟼ (X (x) \cdot_{R} Y (k -_{f} x)) +_{R} (X (x) \cdot_{R} Z (k -_{f} x)))$
50	4	psrbaglefi	$⊢ k \in D \to \{y \in D \| y \leq_{f} k\} \in Fin$
51	50	adantl	$⊢ (φ \land k \in D) \to \{y \in D \| y \leq_{f} k\} \in Fin$
52	20 45 37 42 43	ringcld	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X (x) \cdot_{R} Y (k -_{f} x) \in {Base}_{R}$
53	20 45 37 42 44	ringcld	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X (x) \cdot_{R} Z (k -_{f} x) \in {Base}_{R}$
54		eqidd	$⊢ (φ \land k \in D) \to (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x)) = (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x))$
55		eqidd	$⊢ (φ \land k \in D) \to (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Z (k -_{f} x)) = (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Z (k -_{f} x))$
56	51 52 53 54 55	offval2	$⊢ (φ \land k \in D) \to (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x)) {+_{R}}_{f} (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Z (k -_{f} x)) = (x \in \{y \in D \| y \leq_{f} k\} ⟼ (X (x) \cdot_{R} Y (k -_{f} x)) +_{R} (X (x) \cdot_{R} Z (k -_{f} x)))$
57	49 56	eqtr4d	$⊢ (φ \land k \in D) \to (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} (Y \underset{˙}{+} Z) (k -_{f} x)) = (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x)) {+_{R}}_{f} (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Z (k -_{f} x))$
58	57	oveq2d	$⊢ (φ \land k \in D) \to \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (X (x) \cdot_{R} (Y \underset{˙}{+} Z) (k -_{f} x)) = \sum_{R} ((x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x)) {+_{R}}_{f} (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Z (k -_{f} x)))$
59	3	adantr	$⊢ (φ \land k \in D) \to R \in Ring$
60	59	ringcmnd	$⊢ (φ \land k \in D) \to R \in CMnd$
61		eqid	$⊢ (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x)) = (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x))$
62		eqid	$⊢ (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Z (k -_{f} x)) = (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Z (k -_{f} x))$
63	20 11 60 51 52 53 61 62	gsummptfidmadd2	$⊢ (φ \land k \in D) \to \sum_{R} ((x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Y (k -_{f} x)) {+_{R}}_{f} (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Z (k -_{f} x))) = (\underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}}, (X (x) \cdot_{R} Y (k -_{f} x))) +_{R} (\underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}}, (X (x) \cdot_{R} Z (k -_{f} x)))$
64	58 63	eqtrd	$⊢ (φ \land k \in D) \to \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (X (x) \cdot_{R} (Y \underset{˙}{+} Z) (k -_{f} x)) = (\underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}}, (X (x) \cdot_{R} Y (k -_{f} x))) +_{R} (\underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}}, (X (x) \cdot_{R} Z (k -_{f} x)))$
65	64	mpteq2dva	$⊢ φ \to (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (X (x) \cdot_{R} (Y \underset{˙}{+} Z) (k -_{f} x))) = (k \in D ⟼ (\underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}}, (X (x) \cdot_{R} Y (k -_{f} x))) +_{R} (\underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}}, (X (x) \cdot_{R} Z (k -_{f} x))))$
66	3	ringgrpd	$⊢ φ \to R \in Grp$
67	66	grpmgmd	$⊢ φ \to R \in Mgm$
68	1 6 10 67 8 9	psraddcl	$⊢ φ \to Y \underset{˙}{+} Z \in B$
69	1 6 45 5 4 7 68	psrmulfval	$⊢ φ \to X \underset{˙}{\times} (Y \underset{˙}{+} Z) = (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (X (x) \cdot_{R} (Y \underset{˙}{+} Z) (k -_{f} x)))$
70	1 6 5 3 7 8	psrmulcl	$⊢ φ \to X \underset{˙}{\times} Y \in B$
71	1 6 5 3 7 9	psrmulcl	$⊢ φ \to X \underset{˙}{\times} Z \in B$
72	1 6 11 10 70 71	psradd	$⊢ φ \to (X \underset{˙}{\times} Y) \underset{˙}{+} (X \underset{˙}{\times} Z) = (X \underset{˙}{\times} Y) {+_{R}}_{f} (X \underset{˙}{\times} Z)$
73	28	a1i	$⊢ φ \to D \in V$
74		ovexd	$⊢ (φ \land k \in D) \to \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (X (x) \cdot_{R} Y (k -_{f} x)) \in V$
75		ovexd	$⊢ (φ \land k \in D) \to \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (X (x) \cdot_{R} Z (k -_{f} x)) \in V$
76	1 6 45 5 4 7 8	psrmulfval	$⊢ φ \to X \underset{˙}{\times} Y = (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (X (x) \cdot_{R} Y (k -_{f} x)))$
77	1 6 45 5 4 7 9	psrmulfval	$⊢ φ \to X \underset{˙}{\times} Z = (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (X (x) \cdot_{R} Z (k -_{f} x)))$
78	73 74 75 76 77	offval2	$⊢ φ \to (X \underset{˙}{\times} Y) {+_{R}}_{f} (X \underset{˙}{\times} Z) = (k \in D ⟼ (\underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}}, (X (x) \cdot_{R} Y (k -_{f} x))) +_{R} (\underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}}, (X (x) \cdot_{R} Z (k -_{f} x))))$
79	72 78	eqtrd	$⊢ φ \to (X \underset{˙}{\times} Y) \underset{˙}{+} (X \underset{˙}{\times} Z) = (k \in D ⟼ (\underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}}, (X (x) \cdot_{R} Y (k -_{f} x))) +_{R} (\underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}}, (X (x) \cdot_{R} Z (k -_{f} x))))$
80	65 69 79	3eqtr4d	$⊢ φ \to X \underset{˙}{\times} (Y \underset{˙}{+} Z) = (X \underset{˙}{\times} Y) \underset{˙}{+} (X \underset{˙}{\times} Z)$

Metamath Proof Explorer

Theorem psrdi

Proof