fprodabs2

Description: The absolute value of a finite product . (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	fprodabs2.a	$⊢ φ \to A \in Fin$
	fprodabs2.b	$⊢ (φ \land k \in A) \to B \in ℂ$
Assertion	fprodabs2	$⊢ φ \to \|\prod_{k \in A} B\| = \prod_{k \in A} \|B\|$

Proof

Step	Hyp	Ref	Expression
1		fprodabs2.a	$⊢ φ \to A \in Fin$
2		fprodabs2.b	$⊢ (φ \land k \in A) \to B \in ℂ$
3		prodeq1	$⊢ x = \emptyset \to \prod_{k \in x} B = \prod_{k \in \emptyset} B$
4	3	fveq2d	$⊢ x = \emptyset \to \|\prod_{k \in x} B\| = \|\prod_{k \in \emptyset} B\|$
5		prodeq1	$⊢ x = \emptyset \to \prod_{k \in x} \|B\| = \prod_{k \in \emptyset} \|B\|$
6	4 5	eqeq12d	$⊢ x = \emptyset \to (\|\prod_{k \in x} B\| = \prod_{k \in x} \|B\| \leftrightarrow \|\prod_{k \in \emptyset} B\| = \prod_{k \in \emptyset} \|B\|)$
7		prodeq1	$⊢ x = y \to \prod_{k \in x} B = \prod_{k \in y} B$
8	7	fveq2d	$⊢ x = y \to \|\prod_{k \in x} B\| = \|\prod_{k \in y} B\|$
9		prodeq1	$⊢ x = y \to \prod_{k \in x} \|B\| = \prod_{k \in y} \|B\|$
10	8 9	eqeq12d	$⊢ x = y \to (\|\prod_{k \in x} B\| = \prod_{k \in x} \|B\| \leftrightarrow \|\prod_{k \in y} B\| = \prod_{k \in y} \|B\|)$
11		prodeq1	$⊢ x = y \cup \{z\} \to \prod_{k \in x} B = \prod_{k \in y \cup \{z\}} B$
12	11	fveq2d	$⊢ x = y \cup \{z\} \to \|\prod_{k \in x} B\| = \|\prod_{k \in y \cup \{z\}} B\|$
13		prodeq1	$⊢ x = y \cup \{z\} \to \prod_{k \in x} \|B\| = \prod_{k \in y \cup \{z\}} \|B\|$
14	12 13	eqeq12d	$⊢ x = y \cup \{z\} \to (\|\prod_{k \in x} B\| = \prod_{k \in x} \|B\| \leftrightarrow \|\prod_{k \in y \cup \{z\}} B\| = \prod_{k \in y \cup \{z\}} \|B\|)$
15		prodeq1	$⊢ x = A \to \prod_{k \in x} B = \prod_{k \in A} B$
16	15	fveq2d	$⊢ x = A \to \|\prod_{k \in x} B\| = \|\prod_{k \in A} B\|$
17		prodeq1	$⊢ x = A \to \prod_{k \in x} \|B\| = \prod_{k \in A} \|B\|$
18	16 17	eqeq12d	$⊢ x = A \to (\|\prod_{k \in x} B\| = \prod_{k \in x} \|B\| \leftrightarrow \|\prod_{k \in A} B\| = \prod_{k \in A} \|B\|)$
19		abs1	$⊢ \|1\| = 1$
20		prod0	$⊢ \prod_{k \in \emptyset} B = 1$
21	20	fveq2i	$⊢ \|\prod_{k \in \emptyset} B\| = \|1\|$
22		prod0	$⊢ \prod_{k \in \emptyset} \|B\| = 1$
23	19 21 22	3eqtr4i	$⊢ \|\prod_{k \in \emptyset} B\| = \prod_{k \in \emptyset} \|B\|$
24	23	a1i	$⊢ φ \to \|\prod_{k \in \emptyset} B\| = \prod_{k \in \emptyset} \|B\|$
25		eqidd	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land \|\prod_{k \in y} B\| = \prod_{k \in y} \|B\|) \to \prod_{k \in y} \|B\| \|⦋ z / k ⦌ B\| = \prod_{k \in y} \|B\| \|⦋ z / k ⦌ B\|$
26		nfv	$⊢ Ⅎ k (φ \land (y \subseteq A \land z \in (A ∖ y)))$
27		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ z / k ⦌ B$
28	1	adantr	$⊢ (φ \land y \subseteq A) \to A \in Fin$
29		simpr	$⊢ (φ \land y \subseteq A) \to y \subseteq A$
30		ssfi	$⊢ (A \in Fin \land y \subseteq A) \to y \in Fin$
31	28 29 30	syl2anc	$⊢ (φ \land y \subseteq A) \to y \in Fin$
32	31	adantrr	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to y \in Fin$
33		simprr	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to z \in (A ∖ y)$
34	33	eldifbd	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to \neg z \in y$
35		simpll	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land k \in y) \to φ$
36	29	sselda	$⊢ ((φ \land y \subseteq A) \land k \in y) \to k \in A$
37	36	adantlrr	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land k \in y) \to k \in A$
38	35 37 2	syl2anc	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land k \in y) \to B \in ℂ$
39		csbeq1a	$⊢ k = z \to B = ⦋ z / k ⦌ B$
40		simpl	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to φ$
41	33	eldifad	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to z \in A$
42		nfv	$⊢ Ⅎ k (φ \land z \in A)$
43	27	nfel1	$⊢ Ⅎ k ⦋ z / k ⦌ B \in ℂ$
44	42 43	nfim	$⊢ Ⅎ k ((φ \land z \in A) \to ⦋ z / k ⦌ B \in ℂ)$
45		eleq1w	$⊢ k = z \to (k \in A \leftrightarrow z \in A)$
46	45	anbi2d	$⊢ k = z \to ((φ \land k \in A) \leftrightarrow (φ \land z \in A))$
47	39	eleq1d	$⊢ k = z \to (B \in ℂ \leftrightarrow ⦋ z / k ⦌ B \in ℂ)$
48	46 47	imbi12d	$⊢ k = z \to (((φ \land k \in A) \to B \in ℂ) \leftrightarrow ((φ \land z \in A) \to ⦋ z / k ⦌ B \in ℂ))$
49	44 48 2	chvarfv	$⊢ (φ \land z \in A) \to ⦋ z / k ⦌ B \in ℂ$
50	40 41 49	syl2anc	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to ⦋ z / k ⦌ B \in ℂ$
51	26 27 32 33 34 38 39 50	fprodsplitsn	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to \prod_{k \in y \cup \{z\}} B = \prod_{k \in y} B ⦋ z / k ⦌ B$
52	51	adantr	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land \|\prod_{k \in y} B\| = \prod_{k \in y} \|B\|) \to \prod_{k \in y \cup \{z\}} B = \prod_{k \in y} B ⦋ z / k ⦌ B$
53	52	fveq2d	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land \|\prod_{k \in y} B\| = \prod_{k \in y} \|B\|) \to \|\prod_{k \in y \cup \{z\}} B\| = \|\prod_{k \in y} B ⦋ z / k ⦌ B\|$
54	26 32 38	fprodclf	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to \prod_{k \in y} B \in ℂ$
55	54 50	absmuld	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to \|\prod_{k \in y} B ⦋ z / k ⦌ B\| = \|\prod_{k \in y} B\| \|⦋ z / k ⦌ B\|$
56	55	adantr	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land \|\prod_{k \in y} B\| = \prod_{k \in y} \|B\|) \to \|\prod_{k \in y} B ⦋ z / k ⦌ B\| = \|\prod_{k \in y} B\| \|⦋ z / k ⦌ B\|$
57		oveq1	$⊢ \|\prod_{k \in y} B\| = \prod_{k \in y} \|B\| \to \|\prod_{k \in y} B\| \|⦋ z / k ⦌ B\| = \prod_{k \in y} \|B\| \|⦋ z / k ⦌ B\|$
58	57	adantl	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land \|\prod_{k \in y} B\| = \prod_{k \in y} \|B\|) \to \|\prod_{k \in y} B\| \|⦋ z / k ⦌ B\| = \prod_{k \in y} \|B\| \|⦋ z / k ⦌ B\|$
59	53 56 58	3eqtrd	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land \|\prod_{k \in y} B\| = \prod_{k \in y} \|B\|) \to \|\prod_{k \in y \cup \{z\}} B\| = \prod_{k \in y} \|B\| \|⦋ z / k ⦌ B\|$
60		nfcv	$⊢ \underline{Ⅎ} k abs$
61	60 27	nffv	$⊢ \underline{Ⅎ} k \|⦋ z / k ⦌ B\|$
62	38	abscld	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land k \in y) \to \|B\| \in ℝ$
63	62	recnd	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land k \in y) \to \|B\| \in ℂ$
64	39	fveq2d	$⊢ k = z \to \|B\| = \|⦋ z / k ⦌ B\|$
65	50	abscld	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to \|⦋ z / k ⦌ B\| \in ℝ$
66	65	recnd	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to \|⦋ z / k ⦌ B\| \in ℂ$
67	26 61 32 33 34 63 64 66	fprodsplitsn	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to \prod_{k \in y \cup \{z\}} \|B\| = \prod_{k \in y} \|B\| \|⦋ z / k ⦌ B\|$
68	67	adantr	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land \|\prod_{k \in y} B\| = \prod_{k \in y} \|B\|) \to \prod_{k \in y \cup \{z\}} \|B\| = \prod_{k \in y} \|B\| \|⦋ z / k ⦌ B\|$
69	25 59 68	3eqtr4d	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land \|\prod_{k \in y} B\| = \prod_{k \in y} \|B\|) \to \|\prod_{k \in y \cup \{z\}} B\| = \prod_{k \in y \cup \{z\}} \|B\|$
70	69	ex	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to (\|\prod_{k \in y} B\| = \prod_{k \in y} \|B\| \to \|\prod_{k \in y \cup \{z\}} B\| = \prod_{k \in y \cup \{z\}} \|B\|)$
71	6 10 14 18 24 70 1	findcard2d	$⊢ φ \to \|\prod_{k \in A} B\| = \prod_{k \in A} \|B\|$

Metamath Proof Explorer

Theorem fprodabs2

Proof