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		simplr	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to k \in D$
41		eqid	$⊢ \{y \in D \| y \leq_{f} k\} = \{y \in D \| y \leq_{f} k\}$
42	4 41	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\}$
43	40 16 42	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\}$
44	15 43	sseldi	$⊢ ((φ \land k \in D) \land x \in \{y \in D \| y \leq_{f} k\}) \to k -_{f} x \in D$
45	39 44	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	18 11 46	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))$
48	35 36 37 45 47	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))$
49	34 48	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))$
50	49	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)))$
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	18 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}$
54	35 36 45 53	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}$
55	18 46	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}$
56	35 37 45 55	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}$
57		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))$
58		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))$
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} 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)))$
60	50 59	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))$
61	60	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)))$
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} Z (k -_{f} x)) = (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \cdot_{R} Z (k -_{f} x))$
66		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))$
67	18 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} 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)))$
68	61 67	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)))$
69	68	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))))$
70		ringgrp	$⊢ R \in Ring \to R \in Grp$
71	3 70	syl	$⊢ φ \to R \in Grp$
72	1 6 10 71 7 8	psraddcl	$⊢ φ \to X \underset{˙}{+} Y \in B$
73	1 6 46 5 4 72 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)))$
74	1 6 5 3 7 9	psrmulcl	$⊢ φ \to X \underset{˙}{\times} Z \in B$
75	1 6 5 3 8 9	psrmulcl	$⊢ φ \to Y \underset{˙}{\times} Z \in B$
76	1 6 11 10 74 75	psradd	$⊢ φ \to (X \underset{˙}{\times} Z) \underset{˙}{+} (Y \underset{˙}{\times} Z) = (X \underset{˙}{\times} Z) {+_{R}}_{f} (Y \underset{˙}{\times} Z)$
77	26	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} Z (k -_{f} x)) \in V$
79		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$
80	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)))$
81	1 6 46 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)))$
82	77 78 79 80 81	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))))$
83	76 82	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))))$
84	69 73 83	3eqtr4d	$⊢ φ \to (X \underset{˙}{+} Y) \underset{˙}{\times} Z = (X \underset{˙}{\times} Z) \underset{˙}{+} (Y \underset{˙}{\times} Z)$

Metamath Proof Explorer

Theorem psrdir

Proof