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 ⊢φ→A∈Fin
fprodabs2.b ⊢φ∧k∈A→B∈ℂ
Assertion fprodabs2 ⊢φ→∏k∈AB=∏k∈AB

Proof

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