Metamath Proof Explorer

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 ‘ 𝐵 ) )