Metamath Proof Explorer

Theorem fproddiv

Description: The quotient of two finite products. (Contributed by Scott Fenton, 15-Jan-2018)

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

Proof

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