seqdistr

Description: The distributive property for series. (Contributed by Mario Carneiro, 28-Jul-2013) (Revised by Mario Carneiro, 27-May-2014)

	Ref	Expression
Hypotheses	seqdistr.1	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
	seqdistr.2	$⊢ (φ \land (x \in S \land y \in S)) \to C T (x \underset{˙}{+} y) = (C T x) \underset{˙}{+} (C T y)$
	seqdistr.3	$⊢ φ \to N \in ℤ_{\geq M}$
	seqdistr.4	$⊢ (φ \land x \in (M \dots N)) \to G (x) \in S$
	seqdistr.5	$⊢ (φ \land x \in (M \dots N)) \to F (x) = C T G (x)$
Assertion	seqdistr	$⊢ φ \to seq M (\underset{˙}{+}, F) (N) = C T seq M (\underset{˙}{+}, G) (N)$

Proof

Step	Hyp	Ref	Expression
1		seqdistr.1	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
2		seqdistr.2	$⊢ (φ \land (x \in S \land y \in S)) \to C T (x \underset{˙}{+} y) = (C T x) \underset{˙}{+} (C T y)$
3		seqdistr.3	$⊢ φ \to N \in ℤ_{\geq M}$
4		seqdistr.4	$⊢ (φ \land x \in (M \dots N)) \to G (x) \in S$
5		seqdistr.5	$⊢ (φ \land x \in (M \dots N)) \to F (x) = C T G (x)$
6		oveq2	$⊢ z = x \underset{˙}{+} y \to C T z = C T (x \underset{˙}{+} y)$
7		eqid	$⊢ (z \in S ⟼ C T z) = (z \in S ⟼ C T z)$
8		ovex	$⊢ C T (x \underset{˙}{+} y) \in V$
9	6 7 8	fvmpt	$⊢ x \underset{˙}{+} y \in S \to (z \in S ⟼ C T z) (x \underset{˙}{+} y) = C T (x \underset{˙}{+} y)$
10	1 9	syl	$⊢ (φ \land (x \in S \land y \in S)) \to (z \in S ⟼ C T z) (x \underset{˙}{+} y) = C T (x \underset{˙}{+} y)$
11		oveq2	$⊢ z = x \to C T z = C T x$
12		ovex	$⊢ C T x \in V$
13	11 7 12	fvmpt	$⊢ x \in S \to (z \in S ⟼ C T z) (x) = C T x$
14	13	ad2antrl	$⊢ (φ \land (x \in S \land y \in S)) \to (z \in S ⟼ C T z) (x) = C T x$
15		oveq2	$⊢ z = y \to C T z = C T y$
16		ovex	$⊢ C T y \in V$
17	15 7 16	fvmpt	$⊢ y \in S \to (z \in S ⟼ C T z) (y) = C T y$
18	17	ad2antll	$⊢ (φ \land (x \in S \land y \in S)) \to (z \in S ⟼ C T z) (y) = C T y$
19	14 18	oveq12d	$⊢ (φ \land (x \in S \land y \in S)) \to (z \in S ⟼ C T z) (x) \underset{˙}{+} (z \in S ⟼ C T z) (y) = (C T x) \underset{˙}{+} (C T y)$
20	2 10 19	3eqtr4d	$⊢ (φ \land (x \in S \land y \in S)) \to (z \in S ⟼ C T z) (x \underset{˙}{+} y) = (z \in S ⟼ C T z) (x) \underset{˙}{+} (z \in S ⟼ C T z) (y)$
21		oveq2	$⊢ z = G (x) \to C T z = C T G (x)$
22		ovex	$⊢ C T G (x) \in V$
23	21 7 22	fvmpt	$⊢ G (x) \in S \to (z \in S ⟼ C T z) (G (x)) = C T G (x)$
24	4 23	syl	$⊢ (φ \land x \in (M \dots N)) \to (z \in S ⟼ C T z) (G (x)) = C T G (x)$
25	24 5	eqtr4d	$⊢ (φ \land x \in (M \dots N)) \to (z \in S ⟼ C T z) (G (x)) = F (x)$
26	1 4 3 20 25	seqhomo	$⊢ φ \to (z \in S ⟼ C T z) (seq M (\underset{˙}{+}, G) (N)) = seq M (\underset{˙}{+}, F) (N)$
27	3 4 1	seqcl	$⊢ φ \to seq M (\underset{˙}{+}, G) (N) \in S$
28		oveq2	$⊢ z = seq M (\underset{˙}{+}, G) (N) \to C T z = C T seq M (\underset{˙}{+}, G) (N)$
29		ovex	$⊢ C T seq M (\underset{˙}{+}, G) (N) \in V$
30	28 7 29	fvmpt	$⊢ seq M (\underset{˙}{+}, G) (N) \in S \to (z \in S ⟼ C T z) (seq M (\underset{˙}{+}, G) (N)) = C T seq M (\underset{˙}{+}, G) (N)$
31	27 30	syl	$⊢ φ \to (z \in S ⟼ C T z) (seq M (\underset{˙}{+}, G) (N)) = C T seq M (\underset{˙}{+}, G) (N)$
32	26 31	eqtr3d	$⊢ φ \to seq M (\underset{˙}{+}, F) (N) = C T seq M (\underset{˙}{+}, G) (N)$

Metamath Proof Explorer

Theorem seqdistr

Proof