psrdir

Description: Distributive law for the ring of power series (right-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	psrdir	$⊢ φ \to (X \underset{˙}{+} Y) \underset{˙}{\times} Z = (X \underset{˙}{\times} Z) \underset{˙}{+} (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		psrdi.a	$⊢ \underset{˙}{+} = +_{S}$
11		eqid	$⊢ +_{R} = +_{R}$
12	1 6 11 10 7 8	psradd	$⊢ φ \to X \underset{˙}{+} Y = X {+_{R}}_{f} Y$
13	12	fveq1d	$⊢ φ \to (X \underset{˙}{+} Y) (x) = (X {+_{R}}_{f} Y) (x)$
14	13	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to (X \underset{˙}{+} Y) (x) = (X {+_{R}}_{f} Y) (x)$
15		ssrab2	$⊢ \{y \in D \| y \leq_{f} k\} \subseteq D$
16		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\}$
17	15 16	sseldi	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to x \in D$
18		eqid	$⊢ {Base}_{R} = {Base}_{R}$
19	1 18 4 6 7	psrelbas	$⊢ φ \to X : D ⟶ {Base}_{R}$
20	19	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X : D ⟶ {Base}_{R}$
21	20	ffnd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X Fn D$
22	1 18 4 6 8	psrelbas	$⊢ φ \to Y : D ⟶ {Base}_{R}$
23	22	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Y : D ⟶ {Base}_{R}$
24	23	ffnd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Y Fn D$
25		ovex	$⊢ {ℕ_{0}}^{I} \in V$
26	4 25	rabex2	$⊢ D \in V$
27	26	a1i	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to D \in V$
28		inidm	$⊢ D \cap D = D$
29		eqidd	$⊢ (((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \land x \in D) \to X (x) = X (x)$
30		eqidd	$⊢ (((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \land x \in D) \to Y (x) = Y (x)$
31	21 24 27 27 28 29 30	ofval	$⊢ (((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \land x \in D) \to (X {+_{R}}_{f} Y) (x) = X (x) +_{R} Y (x)$
32	17 31	mpdan	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to (X {+_{R}}_{f} Y) (x) = X (x) +_{R} Y (x)$
33	14 32	eqtrd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to (X \underset{˙}{+} Y) (x) = X (x) +_{R} Y (x)$
34	33	oveq1d	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to (X \underset{˙}{+} Y) (x) \cdot_{R} Z (k -_{f} x) = (X (x) +_{R} Y (x)) \cdot_{R} Z (k -_{f} x)$
35	3	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to R \in Ring$
36	20 17	ffvelrnd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to X (x) \in {Base}_{R}$
37	23 17	ffvelrnd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Y (x) \in {Base}_{R}$
38	1 18 4 6 9	psrelbas	$⊢ φ \to Z : D ⟶ {Base}_{R}$
39	38	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Z : D ⟶ {Base}_{R}$
40	2	ad2antrr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to I \in V$
41		simplr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to k \in D$
42		eqid	$⊢ \{y \in D \| y \leq_{f} k\} = \{y \in D \| y \leq_{f} k\}$
43	4 42	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\}$
44	40 41 16 43	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\}$
45	15 44	sseldi	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to k -_{f} x \in D$
46	39 45	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	18 11 47	ringdir	$⊢ (R \in Ring \land (X (x) \in {Base}_{R} \land Y (x) \in {Base}_{R} \land Z (k -_{f} x) \in {Base}_{R})) \to (X (x) +_{R} Y (x)) \cdot_{R} Z (k -_{f} x) = (X (x) \cdot_{R} Z (k -_{f} x)) +_{R} (Y (x) \cdot_{R} Z (k -_{f} x))$
49	35 36 37 46 48	syl13anc	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to (X (x) +_{R} Y (x)) \cdot_{R} Z (k -_{f} x) = (X (x) \cdot_{R} Z (k -_{f} x)) +_{R} (Y (x) \cdot_{R} Z (k -_{f} x))$
50	34 49	eqtrd	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to (X \underset{˙}{+} Y) (x) \cdot_{R} Z (k -_{f} x) = (X (x) \cdot_{R} Z (k -_{f} x)) +_{R} (Y (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 \underset{˙}{+} Y) (x) \cdot_{R} Z (k -_{f} x)) = (x \in \{y \in D \| y \leq_{f} k\} ⟼ (X (x) \cdot_{R} Z (k -_{f} x)) +_{R} (Y (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	18 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}$
55	35 36 46 54	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}$
56	18 47	ringcl	$⊢ (R \in Ring \land Y (x) \in {Base}_{R} \land Z (k -_{f} x) \in {Base}_{R}) \to Y (x) \cdot_{R} Z (k -_{f} x) \in {Base}_{R}$
57	35 37 46 56	syl3anc	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to Y (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} Z (k -_{f} x)) = (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Z (k -_{f} x))$
59		eqidd	$⊢ (φ \land k \in D) \to (x \in \{y \in D \| y \leq_{f} k\} ⟼ Y (x) \cdot_{R} Z (k -_{f} x)) = (x \in \{y \in D \| y \leq_{f} k\} ⟼ Y (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} Z (k -_{f} x)) {+_{R}}_{f} (x \in \{y \in D \| y \leq_{f} k\} ⟼ Y (x) \cdot_{R} Z (k -_{f} x)) = (x \in \{y \in D \| y \leq_{f} k\} ⟼ (X (x) \cdot_{R} Z (k -_{f} x)) +_{R} (Y (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 \underset{˙}{+} Y) (x) \cdot_{R} Z (k -_{f} x)) = (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Z (k -_{f} x)) {+_{R}}_{f} (x \in \{y \in D \| y \leq_{f} k\} ⟼ Y (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 \underset{˙}{+} Y) (x) \cdot_{R} Z (k -_{f} x)) = \sum_{R} ((x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Z (k -_{f} x)) {+_{R}}_{f} (x \in \{y \in D \| y \leq_{f} k\} ⟼ Y (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} Z (k -_{f} x)) = (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Z (k -_{f} x))$
67		eqid	$⊢ (x \in \{y \in D \| y \leq_{f} k\} ⟼ Y (x) \cdot_{R} Z (k -_{f} x)) = (x \in \{y \in D \| y \leq_{f} k\} ⟼ Y (x) \cdot_{R} Z (k -_{f} x))$
68	18 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} Z (k -_{f} x)) {+_{R}}_{f} (x \in \{y \in D \| y \leq_{f} k\} ⟼ Y (x) \cdot_{R} Z (k -_{f} x))) = (\underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}}, (X (x) \cdot_{R} Z (k -_{f} x))) +_{R} (\underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}}, (Y (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 \underset{˙}{+} Y) (x) \cdot_{R} Z (k -_{f} x)) = (\underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}}, (X (x) \cdot_{R} Z (k -_{f} x))) +_{R} (\underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}}, (Y (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 \underset{˙}{+} Y) (x) \cdot_{R} Z (k -_{f} x))) = (k \in D ⟼ (\underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}}, (X (x) \cdot_{R} Z (k -_{f} x))) +_{R} (\underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}}, (Y (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 7 8	psraddcl	$⊢ φ \to X \underset{˙}{+} Y \in B$
74	1 6 47 5 4 73 9	psrmulfval	$⊢ φ \to (X \underset{˙}{+} Y) \underset{˙}{\times} Z = (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} ((X \underset{˙}{+} Y) (x) \cdot_{R} Z (k -_{f} x)))$
75	1 6 5 3 7 9	psrmulcl	$⊢ φ \to X \underset{˙}{\times} Z \in B$
76	1 6 5 3 8 9	psrmulcl	$⊢ φ \to Y \underset{˙}{\times} Z \in B$
77	1 6 11 10 75 76	psradd	$⊢ φ \to (X \underset{˙}{\times} Z) \underset{˙}{+} (Y \underset{˙}{\times} Z) = (X \underset{˙}{\times} Z) {+_{R}}_{f} (Y \underset{˙}{\times} Z)$
78	26	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} Z (k -_{f} x)) \in V$
80		ovexd	$⊢ (φ \land k \in D) \to \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (Y (x) \cdot_{R} Z (k -_{f} x)) \in V$
81	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)))$
82	1 6 47 5 4 8 9	psrmulfval	$⊢ φ \to Y \underset{˙}{\times} Z = (k \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (Y (x) \cdot_{R} Z (k -_{f} x)))$
83	78 79 80 81 82	offval2	$⊢ φ \to (X \underset{˙}{\times} Z) {+_{R}}_{f} (Y \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))) +_{R} (\underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}}, (Y (x) \cdot_{R} Z (k -_{f} x))))$
84	77 83	eqtrd	$⊢ φ \to (X \underset{˙}{\times} Z) \underset{˙}{+} (Y \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))) +_{R} (\underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}}, (Y (x) \cdot_{R} Z (k -_{f} x))))$
85	70 74 84	3eqtr4d	$⊢ φ \to (X \underset{˙}{+} Y) \underset{˙}{\times} Z = (X \underset{˙}{\times} Z) \underset{˙}{+} (Y \underset{˙}{\times} Z)$

Metamath Proof Explorer

Theorem psrdir

Proof