Theorem fprodabs2

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

	Ref	Expression
Hypotheses	fprodabs2.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fprodabs2.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
Assertion	fprodabs2	⊢ ( 𝜑 → ( abs ‘ ∏ 𝑘 ∈ 𝐴 𝐵 ) = ∏ 𝑘 ∈ 𝐴 ( abs ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		fprodabs2.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
2		fprodabs2.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
3		prodeq1	⊢ ( 𝑥 = ∅ → ∏ 𝑘 ∈ 𝑥 𝐵 = ∏ 𝑘 ∈ ∅ 𝐵 )
4	3	fveq2d	⊢ ( 𝑥 = ∅ → ( abs ‘ ∏ 𝑘 ∈ 𝑥 𝐵 ) = ( abs ‘ ∏ 𝑘 ∈ ∅ 𝐵 ) )
5		prodeq1	⊢ ( 𝑥 = ∅ → ∏ 𝑘 ∈ 𝑥 ( abs ‘ 𝐵 ) = ∏ 𝑘 ∈ ∅ ( abs ‘ 𝐵 ) )
6	4 5	eqeq12d	⊢ ( 𝑥 = ∅ → ( ( abs ‘ ∏ 𝑘 ∈ 𝑥 𝐵 ) = ∏ 𝑘 ∈ 𝑥 ( abs ‘ 𝐵 ) ↔ ( abs ‘ ∏ 𝑘 ∈ ∅ 𝐵 ) = ∏ 𝑘 ∈ ∅ ( abs ‘ 𝐵 ) ) )
7		prodeq1	⊢ ( 𝑥 = 𝑦 → ∏ 𝑘 ∈ 𝑥 𝐵 = ∏ 𝑘 ∈ 𝑦 𝐵 )
8	7	fveq2d	⊢ ( 𝑥 = 𝑦 → ( abs ‘ ∏ 𝑘 ∈ 𝑥 𝐵 ) = ( abs ‘ ∏ 𝑘 ∈ 𝑦 𝐵 ) )
9		prodeq1	⊢ ( 𝑥 = 𝑦 → ∏ 𝑘 ∈ 𝑥 ( abs ‘ 𝐵 ) = ∏ 𝑘 ∈ 𝑦 ( abs ‘ 𝐵 ) )
10	8 9	eqeq12d	⊢ ( 𝑥 = 𝑦 → ( ( abs ‘ ∏ 𝑘 ∈ 𝑥 𝐵 ) = ∏ 𝑘 ∈ 𝑥 ( abs ‘ 𝐵 ) ↔ ( abs ‘ ∏ 𝑘 ∈ 𝑦 𝐵 ) = ∏ 𝑘 ∈ 𝑦 ( abs ‘ 𝐵 ) ) )
11		prodeq1	⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ∏ 𝑘 ∈ 𝑥 𝐵 = ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 )
12	11	fveq2d	⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( abs ‘ ∏ 𝑘 ∈ 𝑥 𝐵 ) = ( abs ‘ ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) )
13		prodeq1	⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ∏ 𝑘 ∈ 𝑥 ( abs ‘ 𝐵 ) = ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( abs ‘ 𝐵 ) )
14	12 13	eqeq12d	⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( abs ‘ ∏ 𝑘 ∈ 𝑥 𝐵 ) = ∏ 𝑘 ∈ 𝑥 ( abs ‘ 𝐵 ) ↔ ( abs ‘ ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) = ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( abs ‘ 𝐵 ) ) )
15		prodeq1	⊢ ( 𝑥 = 𝐴 → ∏ 𝑘 ∈ 𝑥 𝐵 = ∏ 𝑘 ∈ 𝐴 𝐵 )
16	15	fveq2d	⊢ ( 𝑥 = 𝐴 → ( abs ‘ ∏ 𝑘 ∈ 𝑥 𝐵 ) = ( abs ‘ ∏ 𝑘 ∈ 𝐴 𝐵 ) )
17		prodeq1	⊢ ( 𝑥 = 𝐴 → ∏ 𝑘 ∈ 𝑥 ( abs ‘ 𝐵 ) = ∏ 𝑘 ∈ 𝐴 ( abs ‘ 𝐵 ) )
18	16 17	eqeq12d	⊢ ( 𝑥 = 𝐴 → ( ( abs ‘ ∏ 𝑘 ∈ 𝑥 𝐵 ) = ∏ 𝑘 ∈ 𝑥 ( abs ‘ 𝐵 ) ↔ ( abs ‘ ∏ 𝑘 ∈ 𝐴 𝐵 ) = ∏ 𝑘 ∈ 𝐴 ( abs ‘ 𝐵 ) ) )
19		abs1	⊢ ( abs ‘ 1 ) = 1
20		prod0	⊢ ∏ 𝑘 ∈ ∅ 𝐵 = 1
21	20	fveq2i	⊢ ( abs ‘ ∏ 𝑘 ∈ ∅ 𝐵 ) = ( abs ‘ 1 )
22		prod0	⊢ ∏ 𝑘 ∈ ∅ ( abs ‘ 𝐵 ) = 1
23	19 21 22	3eqtr4i	⊢ ( abs ‘ ∏ 𝑘 ∈ ∅ 𝐵 ) = ∏ 𝑘 ∈ ∅ ( abs ‘ 𝐵 )
24	23	a1i	⊢ ( 𝜑 → ( abs ‘ ∏ 𝑘 ∈ ∅ 𝐵 ) = ∏ 𝑘 ∈ ∅ ( abs ‘ 𝐵 ) )
25		eqidd	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ( abs ‘ ∏ 𝑘 ∈ 𝑦 𝐵 ) = ∏ 𝑘 ∈ 𝑦 ( abs ‘ 𝐵 ) ) → ( ∏ 𝑘 ∈ 𝑦 ( abs ‘ 𝐵 ) · ( abs ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) = ( ∏ 𝑘 ∈ 𝑦 ( abs ‘ 𝐵 ) · ( abs ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
26		nfv	⊢ Ⅎ 𝑘 ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) )
27		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝑧 / 𝑘 ⦌ 𝐵
28	1	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ) → 𝐴 ∈ Fin )
29		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ) → 𝑦 ⊆ 𝐴 )
30		ssfi	⊢ ( ( 𝐴 ∈ Fin ∧ 𝑦 ⊆ 𝐴 ) → 𝑦 ∈ Fin )
31	28 29 30	syl2anc	⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ) → 𝑦 ∈ Fin )
32	31	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → 𝑦 ∈ Fin )
33		simprr	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) )
34	33	eldifbd	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ¬ 𝑧 ∈ 𝑦 )
35		simpll	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝜑 )
36	29	sselda	⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑘 ∈ 𝑦 ) → 𝑘 ∈ 𝐴 )
37	36	adantlrr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝑘 ∈ 𝐴 )
38	35 37 2	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝐵 ∈ ℂ )
39		csbeq1a	⊢ ( 𝑘 = 𝑧 → 𝐵 = ⦋ 𝑧 / 𝑘 ⦌ 𝐵 )
40		simpl	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → 𝜑 )
41	33	eldifad	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → 𝑧 ∈ 𝐴 )
42		nfv	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑧 ∈ 𝐴 )
43	27	nfel1	⊢ Ⅎ 𝑘 ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℂ
44	42 43	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℂ )
45		eleq1w	⊢ ( 𝑘 = 𝑧 → ( 𝑘 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
46	45	anbi2d	⊢ ( 𝑘 = 𝑧 → ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ) )
47	39	eleq1d	⊢ ( 𝑘 = 𝑧 → ( 𝐵 ∈ ℂ ↔ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℂ ) )
48	46 47	imbi12d	⊢ ( 𝑘 = 𝑧 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℂ ) ) )
49	44 48 2	chvarfv	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℂ )
50	40 41 49	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℂ )
51	26 27 32 33 34 38 39 50	fprodsplitsn	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 = ( ∏ 𝑘 ∈ 𝑦 𝐵 · ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
52	51	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ( abs ‘ ∏ 𝑘 ∈ 𝑦 𝐵 ) = ∏ 𝑘 ∈ 𝑦 ( abs ‘ 𝐵 ) ) → ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 = ( ∏ 𝑘 ∈ 𝑦 𝐵 · ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
53	52	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ( abs ‘ ∏ 𝑘 ∈ 𝑦 𝐵 ) = ∏ 𝑘 ∈ 𝑦 ( abs ‘ 𝐵 ) ) → ( abs ‘ ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) = ( abs ‘ ( ∏ 𝑘 ∈ 𝑦 𝐵 · ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
54	26 32 38	fprodclf	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ∏ 𝑘 ∈ 𝑦 𝐵 ∈ ℂ )
55	54 50	absmuld	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( abs ‘ ( ∏ 𝑘 ∈ 𝑦 𝐵 · ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) = ( ( abs ‘ ∏ 𝑘 ∈ 𝑦 𝐵 ) · ( abs ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
56	55	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ( abs ‘ ∏ 𝑘 ∈ 𝑦 𝐵 ) = ∏ 𝑘 ∈ 𝑦 ( abs ‘ 𝐵 ) ) → ( abs ‘ ( ∏ 𝑘 ∈ 𝑦 𝐵 · ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) = ( ( abs ‘ ∏ 𝑘 ∈ 𝑦 𝐵 ) · ( abs ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
57		oveq1	⊢ ( ( abs ‘ ∏ 𝑘 ∈ 𝑦 𝐵 ) = ∏ 𝑘 ∈ 𝑦 ( abs ‘ 𝐵 ) → ( ( abs ‘ ∏ 𝑘 ∈ 𝑦 𝐵 ) · ( abs ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) = ( ∏ 𝑘 ∈ 𝑦 ( abs ‘ 𝐵 ) · ( abs ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
58	57	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ( abs ‘ ∏ 𝑘 ∈ 𝑦 𝐵 ) = ∏ 𝑘 ∈ 𝑦 ( abs ‘ 𝐵 ) ) → ( ( abs ‘ ∏ 𝑘 ∈ 𝑦 𝐵 ) · ( abs ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) = ( ∏ 𝑘 ∈ 𝑦 ( abs ‘ 𝐵 ) · ( abs ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
59	53 56 58	3eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ( abs ‘ ∏ 𝑘 ∈ 𝑦 𝐵 ) = ∏ 𝑘 ∈ 𝑦 ( abs ‘ 𝐵 ) ) → ( abs ‘ ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) = ( ∏ 𝑘 ∈ 𝑦 ( abs ‘ 𝐵 ) · ( abs ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
60		nfcv	⊢ Ⅎ 𝑘 abs
61	60 27	nffv	⊢ Ⅎ 𝑘 ( abs ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 )
62	38	abscld	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ 𝑦 ) → ( abs ‘ 𝐵 ) ∈ ℝ )
63	62	recnd	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ 𝑦 ) → ( abs ‘ 𝐵 ) ∈ ℂ )
64	39	fveq2d	⊢ ( 𝑘 = 𝑧 → ( abs ‘ 𝐵 ) = ( abs ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
65	50	abscld	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( abs ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ∈ ℝ )
66	65	recnd	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( abs ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ∈ ℂ )
67	26 61 32 33 34 63 64 66	fprodsplitsn	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( abs ‘ 𝐵 ) = ( ∏ 𝑘 ∈ 𝑦 ( abs ‘ 𝐵 ) · ( abs ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
68	67	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ( abs ‘ ∏ 𝑘 ∈ 𝑦 𝐵 ) = ∏ 𝑘 ∈ 𝑦 ( abs ‘ 𝐵 ) ) → ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( abs ‘ 𝐵 ) = ( ∏ 𝑘 ∈ 𝑦 ( abs ‘ 𝐵 ) · ( abs ‘ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ) )
69	25 59 68	3eqtr4d	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ( abs ‘ ∏ 𝑘 ∈ 𝑦 𝐵 ) = ∏ 𝑘 ∈ 𝑦 ( abs ‘ 𝐵 ) ) → ( abs ‘ ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) = ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( abs ‘ 𝐵 ) )
70	69	ex	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ( abs ‘ ∏ 𝑘 ∈ 𝑦 𝐵 ) = ∏ 𝑘 ∈ 𝑦 ( abs ‘ 𝐵 ) → ( abs ‘ ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ) = ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( abs ‘ 𝐵 ) ) )
71	6 10 14 18 24 70 1	findcard2d	⊢ ( 𝜑 → ( abs ‘ ∏ 𝑘 ∈ 𝐴 𝐵 ) = ∏ 𝑘 ∈ 𝐴 ( abs ‘ 𝐵 ) )