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

Metamath Proof Explorer

Theorem psrdi

Proof