Metamath Proof Explorer

Theorem fprodmul

Description: The product of two finite products. (Contributed by Scott Fenton, 14-Dec-2017)

Ref Expression
Hypotheses fprodmul.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fprodmul.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
fprodmul.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
Assertion fprodmul ( 𝜑 → ∏ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) = ( ∏ 𝑘 ∈ 𝐴 𝐵 · ∏ 𝑘 ∈ 𝐴 𝐶 ) )

Proof

Step Hyp Ref Expression
1 fprodmul.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
2 fprodmul.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
3 fprodmul.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
4 1t1e1 ⊢ ( 1 · 1 ) = 1
5 prod0 ⊢ ∏ 𝑘 ∈ ∅ 𝐵 = 1
6 prod0 ⊢ ∏ 𝑘 ∈ ∅ 𝐶 = 1
7 5 6 oveq12i ⊢ ( ∏ 𝑘 ∈ ∅ 𝐵 · ∏ 𝑘 ∈ ∅ 𝐶 ) = ( 1 · 1 )
8 prod0 ⊢ ∏ 𝑘 ∈ ∅ ( 𝐵 · 𝐶 ) = 1
9 4 7 8 3eqtr4ri ⊢ ∏ 𝑘 ∈ ∅ ( 𝐵 · 𝐶 ) = ( ∏ 𝑘 ∈ ∅ 𝐵 · ∏ 𝑘 ∈ ∅ 𝐶 )
10 prodeq1 ⊢ ( 𝐴 = ∅ → ∏ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) = ∏ 𝑘 ∈ ∅ ( 𝐵 · 𝐶 ) )
11 prodeq1 ⊢ ( 𝐴 = ∅ → ∏ 𝑘 ∈ 𝐴 𝐵 = ∏ 𝑘 ∈ ∅ 𝐵 )
12 prodeq1 ⊢ ( 𝐴 = ∅ → ∏ 𝑘 ∈ 𝐴 𝐶 = ∏ 𝑘 ∈ ∅ 𝐶 )
13 11 12 oveq12d ⊢ ( 𝐴 = ∅ → ( ∏ 𝑘 ∈ 𝐴 𝐵 · ∏ 𝑘 ∈ 𝐴 𝐶 ) = ( ∏ 𝑘 ∈ ∅ 𝐵 · ∏ 𝑘 ∈ ∅ 𝐶 ) )
14 9 10 13 3eqtr4a ⊢ ( 𝐴 = ∅ → ∏ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) = ( ∏ 𝑘 ∈ 𝐴 𝐵 · ∏ 𝑘 ∈ 𝐴 𝐶 ) )
15 14 a1i ⊢ ( 𝜑 → ( 𝐴 = ∅ → ∏ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) = ( ∏ 𝑘 ∈ 𝐴 𝐵 · ∏ 𝑘 ∈ 𝐴 𝐶 ) ) )
16 simprl ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℕ )
17 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
18 16 17 eleqtrdi ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) )
19 2 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ )
20 19 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ )
21 f1of ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
22 21 ad2antll ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
23 fco ⊢ ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ ℂ )
24 20 22 23 syl2anc ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ ℂ )
25 24 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑛 ) ∈ ℂ )
26 3 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 ⟶ ℂ )
27 26 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 ⟶ ℂ )
28 fco ⊢ ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 ⟶ ℂ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ ℂ )
29 27 22 28 syl2anc ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ ℂ )
30 29 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ∘ 𝑓 ) ‘ 𝑛 ) ∈ ℂ )
31 22 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝑓 ‘ 𝑛 ) ∈ 𝐴 )
32 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ 𝐴 )
33 2 3 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
34 eqid ⊢ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) = ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) )
35 34 fvmpt2 ⊢ ( ( 𝑘 ∈ 𝐴 ∧ ( 𝐵 · 𝐶 ) ∈ ℂ ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ‘ 𝑘 ) = ( 𝐵 · 𝐶 ) )
36 32 33 35 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ‘ 𝑘 ) = ( 𝐵 · 𝐶 ) )
37 eqid ⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
38 37 fvmpt2 ⊢ ( ( 𝑘 ∈ 𝐴 ∧ 𝐵 ∈ ℂ ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) = 𝐵 )
39 32 2 38 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) = 𝐵 )
40 eqid ⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐶 )
41 40 fvmpt2 ⊢ ( ( 𝑘 ∈ 𝐴 ∧ 𝐶 ∈ ℂ ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) = 𝐶 )
42 32 3 41 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) = 𝐶 )
43 39 42 oveq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) · ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) ) = ( 𝐵 · 𝐶 ) )
44 36 43 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ‘ 𝑘 ) = ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) · ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) ) )
45 44 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ‘ 𝑘 ) = ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) · ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) ) )
46 45 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ∀ 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ‘ 𝑘 ) = ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) · ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) ) )
47 nffvmpt1 ⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ‘ ( 𝑓 ‘ 𝑛 ) )
48 nffvmpt1 ⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) )
49 nfcv ⊢ Ⅎ 𝑘 ·
50 nffvmpt1 ⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) )
51 48 49 50 nfov ⊢ Ⅎ 𝑘 ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) · ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
52 47 51 nfeq ⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) = ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) · ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
53 fveq2 ⊢ ( 𝑘 = ( 𝑓 ‘ 𝑛 ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ‘ 𝑘 ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
54 fveq2 ⊢ ( 𝑘 = ( 𝑓 ‘ 𝑛 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
55 fveq2 ⊢ ( 𝑘 = ( 𝑓 ‘ 𝑛 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
56 54 55 oveq12d ⊢ ( 𝑘 = ( 𝑓 ‘ 𝑛 ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) · ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) ) = ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) · ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
57 53 56 eqeq12d ⊢ ( 𝑘 = ( 𝑓 ‘ 𝑛 ) → ( ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ‘ 𝑘 ) = ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) · ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) ) ↔ ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) = ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) · ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) )
58 52 57 rspc ⊢ ( ( 𝑓 ‘ 𝑛 ) ∈ 𝐴 → ( ∀ 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ‘ 𝑘 ) = ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) · ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) = ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) · ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) )
59 31 46 58 sylc ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) = ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) · ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
60 fvco3 ⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ∘ 𝑓 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
61 22 60 sylan ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ∘ 𝑓 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
62 fvco3 ⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
63 22 62 sylan ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
64 fvco3 ⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ∘ 𝑓 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
65 22 64 sylan ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ∘ 𝑓 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
66 63 65 oveq12d ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑛 ) · ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ∘ 𝑓 ) ‘ 𝑛 ) ) = ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) · ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
67 59 61 66 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ∘ 𝑓 ) ‘ 𝑛 ) = ( ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑛 ) · ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ∘ 𝑓 ) ‘ 𝑛 ) ) )
68 18 25 30 67 prodfmul ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( seq 1 ( · , ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) = ( ( seq 1 ( · , ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) · ( seq 1 ( · , ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) ) )
69 fveq2 ⊢ ( 𝑚 = ( 𝑓 ‘ 𝑛 ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
70 simprr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 )
71 33 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) : 𝐴 ⟶ ℂ )
72 71 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) : 𝐴 ⟶ ℂ )
73 72 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑚 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ‘ 𝑚 ) ∈ ℂ )
74 69 16 70 73 61 fprod ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ∏ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ‘ 𝑚 ) = ( seq 1 ( · , ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) )
75 fveq2 ⊢ ( 𝑚 = ( 𝑓 ‘ 𝑛 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
76 20 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑚 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) ∈ ℂ )
77 75 16 70 76 63 fprod ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ∏ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) = ( seq 1 ( · , ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) )
78 fveq2 ⊢ ( 𝑚 = ( 𝑓 ‘ 𝑛 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
79 27 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑚 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) ∈ ℂ )
80 78 16 70 79 65 fprod ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ∏ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) = ( seq 1 ( · , ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) )
81 77 80 oveq12d ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( ∏ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) · ∏ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) ) = ( ( seq 1 ( · , ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) · ( seq 1 ( · , ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) ) )
82 68 74 81 3eqtr4d ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ∏ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ‘ 𝑚 ) = ( ∏ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) · ∏ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) ) )
83 prodfc ⊢ ∏ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ‘ 𝑚 ) = ∏ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 )
84 prodfc ⊢ ∏ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) = ∏ 𝑘 ∈ 𝐴 𝐵
85 prodfc ⊢ ∏ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) = ∏ 𝑘 ∈ 𝐴 𝐶
86 84 85 oveq12i ⊢ ( ∏ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) · ∏ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) ) = ( ∏ 𝑘 ∈ 𝐴 𝐵 · ∏ 𝑘 ∈ 𝐴 𝐶 )
87 82 83 86 3eqtr3g ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ∏ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) = ( ∏ 𝑘 ∈ 𝐴 𝐵 · ∏ 𝑘 ∈ 𝐴 𝐶 ) )
88 87 expr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → ∏ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) = ( ∏ 𝑘 ∈ 𝐴 𝐵 · ∏ 𝑘 ∈ 𝐴 𝐶 ) ) )
89 88 exlimdv ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) → ( ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → ∏ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) = ( ∏ 𝑘 ∈ 𝐴 𝐵 · ∏ 𝑘 ∈ 𝐴 𝐶 ) ) )
90 89 expimpd ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ∏ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) = ( ∏ 𝑘 ∈ 𝐴 𝐵 · ∏ 𝑘 ∈ 𝐴 𝐶 ) ) )
91 fz1f1o ⊢ ( 𝐴 ∈ Fin → ( 𝐴 = ∅ ∨ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) )
92 1 91 syl ⊢ ( 𝜑 → ( 𝐴 = ∅ ∨ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) )
93 15 90 92 mpjaod ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 ( 𝐵 · 𝐶 ) = ( ∏ 𝑘 ∈ 𝐴 𝐵 · ∏ 𝑘 ∈ 𝐴 𝐶 ) )