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	2	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to I \in V$
17		simplr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to k \in D$
18		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\}$
19		eqid	$⊢ \{y \in D \| y \leq_{f} k\} = \{y \in D \| y \leq_{f} k\}$
20	4 19	psrbagconcl	$⊢ (I \in V \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\}$
21	16 17 18 20	syl3anc	$⊢ ((φ \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\}$
22	15 21	sseldi	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to k -_{f} x \in D$
23		eqid	$⊢ {Base}_{R} = {Base}_{R}$
24	1 23 4 6 8	psrelbas	$⊢ φ \to Y : D ⟶ {Base}_{R}$
25	24	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Y : D ⟶ {Base}_{R}$
26	25	ffnd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Y Fn D$
27	1 23 4 6 9	psrelbas	$⊢ φ \to Z : D ⟶ {Base}_{R}$
28	27	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Z : D ⟶ {Base}_{R}$
29	28	ffnd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Z Fn D$
30		ovex	$⊢ {ℕ_{0}}^{I} \in V$
31	4 30	rabex2	$⊢ D \in V$
32	31	a1i	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to D \in V$
33		inidm	$⊢ D \cap D = D$
34		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)$
35		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)$
36	26 29 32 32 33 34 35	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)$
37	22 36	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)$
38	14 37	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)$
39	38	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))$
40	3	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to R \in Ring$
41	1 23 4 6 7	psrelbas	$⊢ φ \to X : D ⟶ {Base}_{R}$
42	41	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X : D ⟶ {Base}_{R}$
43	15 18	sseldi	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to x \in D$
44	42 43	ffvelrnd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X (x) \in {Base}_{R}$
45	25 22	ffvelrnd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Y (k -_{f} x) \in {Base}_{R}$
46	28 22	ffvelrnd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Z (k -_{f} x) \in {Base}_{R}$
47		eqid	$⊢ \cdot_{R} = \cdot_{R}$
48	23 11 47	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))$
49	40 44 45 46 48	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))$
50	39 49	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))$
51	50	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)))$
52	4	psrbaglefi	$⊢ (I \in V \land k \in D) \to \{y \in D \| y \leq_{f} k\} \in Fin$
53	2 52	sylan	$⊢ (φ \land k \in D) \to \{y \in D \| y \leq_{f} k\} \in Fin$
54	23 47	ringcl	$⊢ (R \in Ring \land X (x) \in {Base}_{R} \land Y (k -_{f} x) \in {Base}_{R}) \to X (x) \cdot_{R} Y (k -_{f} x) \in {Base}_{R}$
55	40 44 45 54	syl3anc	$⊢ ((φ \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}$
56	23 47	ringcl	$⊢ (R \in Ring \land X (x) \in {Base}_{R} \land Z (k -_{f} x) \in {Base}_{R}) \to X (x) \cdot_{R} Z (k -_{f} x) \in {Base}_{R}$
57	40 44 46 56	syl3anc	$⊢ ((φ \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}$
58		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))$
59		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))$
60	53 55 57 58 59	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)))$
61	51 60	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))$
62	61	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)))$
63	3	adantr	$⊢ (φ \land k \in D) \to R \in Ring$
64		ringcmn	$⊢ R \in Ring \to R \in CMnd$
65	63 64	syl	$⊢ (φ \land k \in D) \to R \in CMnd$
66		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))$
67		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))$
68	23 11 65 53 55 57 66 67	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)))$
69	62 68	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)))$
70	69	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))))$
71		ringgrp	$⊢ R \in Ring \to R \in Grp$
72	3 71	syl	$⊢ φ \to R \in Grp$
73	1 6 10 72 8 9	psraddcl	$⊢ φ \to Y \underset{˙}{+} Z \in B$
74	1 6 47 5 4 7 73	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)))$
75	1 6 5 3 7 8	psrmulcl	$⊢ φ \to X \underset{˙}{\times} Y \in B$
76	1 6 5 3 7 9	psrmulcl	$⊢ φ \to X \underset{˙}{\times} Z \in B$
77	1 6 11 10 75 76	psradd	$⊢ φ \to (X \underset{˙}{\times} Y) \underset{˙}{+} (X \underset{˙}{\times} Z) = (X \underset{˙}{\times} Y) {+_{R}}_{f} (X \underset{˙}{\times} Z)$
78	31	a1i	$⊢ φ \to D \in V$
79		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$
80		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$
81	1 6 47 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)))$
82	1 6 47 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)))$
83	78 79 80 81 82	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))))$
84	77 83	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))))$
85	70 74 84	3eqtr4d	$⊢ φ \to X \underset{˙}{\times} (Y \underset{˙}{+} Z) = (X \underset{˙}{\times} Y) \underset{˙}{+} (X \underset{˙}{\times} Z)$

Metamath Proof Explorer

Theorem psrdi

Proof