Metamath Proof Explorer


Theorem fprodss

Description: Change the index set to a subset in a finite product. (Contributed by Scott Fenton, 16-Dec-2017)

Ref Expression
Hypotheses fprodss.1 ( 𝜑𝐴𝐵 )
fprodss.2 ( ( 𝜑𝑘𝐴 ) → 𝐶 ∈ ℂ )
fprodss.3 ( ( 𝜑𝑘 ∈ ( 𝐵𝐴 ) ) → 𝐶 = 1 )
fprodss.4 ( 𝜑𝐵 ∈ Fin )
Assertion fprodss ( 𝜑 → ∏ 𝑘𝐴 𝐶 = ∏ 𝑘𝐵 𝐶 )

Proof

Step Hyp Ref Expression
1 fprodss.1 ( 𝜑𝐴𝐵 )
2 fprodss.2 ( ( 𝜑𝑘𝐴 ) → 𝐶 ∈ ℂ )
3 fprodss.3 ( ( 𝜑𝑘 ∈ ( 𝐵𝐴 ) ) → 𝐶 = 1 )
4 fprodss.4 ( 𝜑𝐵 ∈ Fin )
5 sseq2 ( 𝐵 = ∅ → ( 𝐴𝐵𝐴 ⊆ ∅ ) )
6 ss0 ( 𝐴 ⊆ ∅ → 𝐴 = ∅ )
7 5 6 syl6bi ( 𝐵 = ∅ → ( 𝐴𝐵𝐴 = ∅ ) )
8 prodeq1 ( 𝐴 = ∅ → ∏ 𝑘𝐴 𝐶 = ∏ 𝑘 ∈ ∅ 𝐶 )
9 prodeq1 ( 𝐵 = ∅ → ∏ 𝑘𝐵 𝐶 = ∏ 𝑘 ∈ ∅ 𝐶 )
10 9 eqcomd ( 𝐵 = ∅ → ∏ 𝑘 ∈ ∅ 𝐶 = ∏ 𝑘𝐵 𝐶 )
11 8 10 sylan9eq ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) → ∏ 𝑘𝐴 𝐶 = ∏ 𝑘𝐵 𝐶 )
12 11 expcom ( 𝐵 = ∅ → ( 𝐴 = ∅ → ∏ 𝑘𝐴 𝐶 = ∏ 𝑘𝐵 𝐶 ) )
13 7 12 syld ( 𝐵 = ∅ → ( 𝐴𝐵 → ∏ 𝑘𝐴 𝐶 = ∏ 𝑘𝐵 𝐶 ) )
14 1 13 syl5com ( 𝜑 → ( 𝐵 = ∅ → ∏ 𝑘𝐴 𝐶 = ∏ 𝑘𝐵 𝐶 ) )
15 cnvimass ( 𝑓𝐴 ) ⊆ dom 𝑓
16 simprr ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 )
17 f1of ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) ⟶ 𝐵 )
18 16 17 syl ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) ⟶ 𝐵 )
19 15 18 fssdm ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( 𝑓𝐴 ) ⊆ ( 1 ... ( ♯ ‘ 𝐵 ) ) )
20 f1ofn ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵𝑓 Fn ( 1 ... ( ♯ ‘ 𝐵 ) ) )
21 elpreima ( 𝑓 Fn ( 1 ... ( ♯ ‘ 𝐵 ) ) → ( 𝑛 ∈ ( 𝑓𝐴 ) ↔ ( 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ ( 𝑓𝑛 ) ∈ 𝐴 ) ) )
22 16 20 21 3syl ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( 𝑛 ∈ ( 𝑓𝐴 ) ↔ ( 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ ( 𝑓𝑛 ) ∈ 𝐴 ) ) )
23 18 ffvelrnda ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) → ( 𝑓𝑛 ) ∈ 𝐵 )
24 23 ex ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) → ( 𝑓𝑛 ) ∈ 𝐵 ) )
25 24 adantrd ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( ( 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ ( 𝑓𝑛 ) ∈ 𝐴 ) → ( 𝑓𝑛 ) ∈ 𝐵 ) )
26 22 25 sylbid ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( 𝑛 ∈ ( 𝑓𝐴 ) → ( 𝑓𝑛 ) ∈ 𝐵 ) )
27 26 imp ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( 𝑓𝐴 ) ) → ( 𝑓𝑛 ) ∈ 𝐵 )
28 2 ex ( 𝜑 → ( 𝑘𝐴𝐶 ∈ ℂ ) )
29 28 adantr ( ( 𝜑𝑘𝐵 ) → ( 𝑘𝐴𝐶 ∈ ℂ ) )
30 eldif ( 𝑘 ∈ ( 𝐵𝐴 ) ↔ ( 𝑘𝐵 ∧ ¬ 𝑘𝐴 ) )
31 ax-1cn 1 ∈ ℂ
32 3 31 eqeltrdi ( ( 𝜑𝑘 ∈ ( 𝐵𝐴 ) ) → 𝐶 ∈ ℂ )
33 30 32 sylan2br ( ( 𝜑 ∧ ( 𝑘𝐵 ∧ ¬ 𝑘𝐴 ) ) → 𝐶 ∈ ℂ )
34 33 expr ( ( 𝜑𝑘𝐵 ) → ( ¬ 𝑘𝐴𝐶 ∈ ℂ ) )
35 29 34 pm2.61d ( ( 𝜑𝑘𝐵 ) → 𝐶 ∈ ℂ )
36 35 adantlr ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑘𝐵 ) → 𝐶 ∈ ℂ )
37 36 fmpttd ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( 𝑘𝐵𝐶 ) : 𝐵 ⟶ ℂ )
38 37 ffvelrnda ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ ( 𝑓𝑛 ) ∈ 𝐵 ) → ( ( 𝑘𝐵𝐶 ) ‘ ( 𝑓𝑛 ) ) ∈ ℂ )
39 27 38 syldan ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( 𝑓𝐴 ) ) → ( ( 𝑘𝐵𝐶 ) ‘ ( 𝑓𝑛 ) ) ∈ ℂ )
40 eqid ( ℤ ‘ 1 ) = ( ℤ ‘ 1 )
41 simprl ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( ♯ ‘ 𝐵 ) ∈ ℕ )
42 nnuz ℕ = ( ℤ ‘ 1 )
43 41 42 eleqtrdi ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( ♯ ‘ 𝐵 ) ∈ ( ℤ ‘ 1 ) )
44 ssidd ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( 1 ... ( ♯ ‘ 𝐵 ) ) ⊆ ( 1 ... ( ♯ ‘ 𝐵 ) ) )
45 40 43 44 fprodntriv ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ∃ 𝑚 ∈ ( ℤ ‘ 1 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑚 ( · , ( 𝑛 ∈ ( ℤ ‘ 1 ) ↦ if ( 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) , ( ( 𝑘𝐵𝐶 ) ‘ ( 𝑓𝑛 ) ) , 1 ) ) ) ⇝ 𝑦 ) )
46 eldifi ( 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( 𝑓𝐴 ) ) → 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) )
47 46 23 sylan2 ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( 𝑓𝐴 ) ) ) → ( 𝑓𝑛 ) ∈ 𝐵 )
48 eldifn ( 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( 𝑓𝐴 ) ) → ¬ 𝑛 ∈ ( 𝑓𝐴 ) )
49 48 adantl ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( 𝑓𝐴 ) ) ) → ¬ 𝑛 ∈ ( 𝑓𝐴 ) )
50 46 adantl ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( 𝑓𝐴 ) ) ) → 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) )
51 22 adantr ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( 𝑓𝐴 ) ) ) → ( 𝑛 ∈ ( 𝑓𝐴 ) ↔ ( 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ ( 𝑓𝑛 ) ∈ 𝐴 ) ) )
52 50 51 mpbirand ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( 𝑓𝐴 ) ) ) → ( 𝑛 ∈ ( 𝑓𝐴 ) ↔ ( 𝑓𝑛 ) ∈ 𝐴 ) )
53 49 52 mtbid ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( 𝑓𝐴 ) ) ) → ¬ ( 𝑓𝑛 ) ∈ 𝐴 )
54 47 53 eldifd ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( 𝑓𝐴 ) ) ) → ( 𝑓𝑛 ) ∈ ( 𝐵𝐴 ) )
55 difss ( 𝐵𝐴 ) ⊆ 𝐵
56 resmpt ( ( 𝐵𝐴 ) ⊆ 𝐵 → ( ( 𝑘𝐵𝐶 ) ↾ ( 𝐵𝐴 ) ) = ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 𝐶 ) )
57 55 56 ax-mp ( ( 𝑘𝐵𝐶 ) ↾ ( 𝐵𝐴 ) ) = ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 𝐶 )
58 57 fveq1i ( ( ( 𝑘𝐵𝐶 ) ↾ ( 𝐵𝐴 ) ) ‘ ( 𝑓𝑛 ) ) = ( ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 𝐶 ) ‘ ( 𝑓𝑛 ) )
59 fvres ( ( 𝑓𝑛 ) ∈ ( 𝐵𝐴 ) → ( ( ( 𝑘𝐵𝐶 ) ↾ ( 𝐵𝐴 ) ) ‘ ( 𝑓𝑛 ) ) = ( ( 𝑘𝐵𝐶 ) ‘ ( 𝑓𝑛 ) ) )
60 58 59 eqtr3id ( ( 𝑓𝑛 ) ∈ ( 𝐵𝐴 ) → ( ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 𝐶 ) ‘ ( 𝑓𝑛 ) ) = ( ( 𝑘𝐵𝐶 ) ‘ ( 𝑓𝑛 ) ) )
61 54 60 syl ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( 𝑓𝐴 ) ) ) → ( ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 𝐶 ) ‘ ( 𝑓𝑛 ) ) = ( ( 𝑘𝐵𝐶 ) ‘ ( 𝑓𝑛 ) ) )
62 1ex 1 ∈ V
63 62 elsn2 ( 𝐶 ∈ { 1 } ↔ 𝐶 = 1 )
64 3 63 sylibr ( ( 𝜑𝑘 ∈ ( 𝐵𝐴 ) ) → 𝐶 ∈ { 1 } )
65 64 fmpttd ( 𝜑 → ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 𝐶 ) : ( 𝐵𝐴 ) ⟶ { 1 } )
66 65 ad2antrr ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( 𝑓𝐴 ) ) ) → ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 𝐶 ) : ( 𝐵𝐴 ) ⟶ { 1 } )
67 66 54 ffvelrnd ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( 𝑓𝐴 ) ) ) → ( ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 𝐶 ) ‘ ( 𝑓𝑛 ) ) ∈ { 1 } )
68 elsni ( ( ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 𝐶 ) ‘ ( 𝑓𝑛 ) ) ∈ { 1 } → ( ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 𝐶 ) ‘ ( 𝑓𝑛 ) ) = 1 )
69 67 68 syl ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( 𝑓𝐴 ) ) ) → ( ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 𝐶 ) ‘ ( 𝑓𝑛 ) ) = 1 )
70 61 69 eqtr3d ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( 𝑓𝐴 ) ) ) → ( ( 𝑘𝐵𝐶 ) ‘ ( 𝑓𝑛 ) ) = 1 )
71 fzssuz ( 1 ... ( ♯ ‘ 𝐵 ) ) ⊆ ( ℤ ‘ 1 )
72 71 a1i ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( 1 ... ( ♯ ‘ 𝐵 ) ) ⊆ ( ℤ ‘ 1 ) )
73 19 39 45 70 72 prodss ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ∏ 𝑛 ∈ ( 𝑓𝐴 ) ( ( 𝑘𝐵𝐶 ) ‘ ( 𝑓𝑛 ) ) = ∏ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ( ( 𝑘𝐵𝐶 ) ‘ ( 𝑓𝑛 ) ) )
74 1 adantr ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → 𝐴𝐵 )
75 74 resmptd ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( ( 𝑘𝐵𝐶 ) ↾ 𝐴 ) = ( 𝑘𝐴𝐶 ) )
76 75 fveq1d ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( ( ( 𝑘𝐵𝐶 ) ↾ 𝐴 ) ‘ 𝑚 ) = ( ( 𝑘𝐴𝐶 ) ‘ 𝑚 ) )
77 fvres ( 𝑚𝐴 → ( ( ( 𝑘𝐵𝐶 ) ↾ 𝐴 ) ‘ 𝑚 ) = ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) )
78 76 77 sylan9req ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑚𝐴 ) → ( ( 𝑘𝐴𝐶 ) ‘ 𝑚 ) = ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) )
79 78 prodeq2dv ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ∏ 𝑚𝐴 ( ( 𝑘𝐴𝐶 ) ‘ 𝑚 ) = ∏ 𝑚𝐴 ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) )
80 fveq2 ( 𝑚 = ( 𝑓𝑛 ) → ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) = ( ( 𝑘𝐵𝐶 ) ‘ ( 𝑓𝑛 ) ) )
81 fzfid ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( 1 ... ( ♯ ‘ 𝐵 ) ) ∈ Fin )
82 81 18 fisuppfi ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( 𝑓𝐴 ) ∈ Fin )
83 f1of1 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1𝐵 )
84 16 83 syl ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1𝐵 )
85 f1ores ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1𝐵 ∧ ( 𝑓𝐴 ) ⊆ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) → ( 𝑓 ↾ ( 𝑓𝐴 ) ) : ( 𝑓𝐴 ) –1-1-onto→ ( 𝑓 “ ( 𝑓𝐴 ) ) )
86 84 19 85 syl2anc ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( 𝑓 ↾ ( 𝑓𝐴 ) ) : ( 𝑓𝐴 ) –1-1-onto→ ( 𝑓 “ ( 𝑓𝐴 ) ) )
87 f1ofo ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –onto𝐵 )
88 16 87 syl ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –onto𝐵 )
89 foimacnv ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –onto𝐵𝐴𝐵 ) → ( 𝑓 “ ( 𝑓𝐴 ) ) = 𝐴 )
90 88 74 89 syl2anc ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( 𝑓 “ ( 𝑓𝐴 ) ) = 𝐴 )
91 90 f1oeq3d ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( ( 𝑓 ↾ ( 𝑓𝐴 ) ) : ( 𝑓𝐴 ) –1-1-onto→ ( 𝑓 “ ( 𝑓𝐴 ) ) ↔ ( 𝑓 ↾ ( 𝑓𝐴 ) ) : ( 𝑓𝐴 ) –1-1-onto𝐴 ) )
92 86 91 mpbid ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( 𝑓 ↾ ( 𝑓𝐴 ) ) : ( 𝑓𝐴 ) –1-1-onto𝐴 )
93 fvres ( 𝑛 ∈ ( 𝑓𝐴 ) → ( ( 𝑓 ↾ ( 𝑓𝐴 ) ) ‘ 𝑛 ) = ( 𝑓𝑛 ) )
94 93 adantl ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( 𝑓𝐴 ) ) → ( ( 𝑓 ↾ ( 𝑓𝐴 ) ) ‘ 𝑛 ) = ( 𝑓𝑛 ) )
95 74 sselda ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑚𝐴 ) → 𝑚𝐵 )
96 37 ffvelrnda ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑚𝐵 ) → ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) ∈ ℂ )
97 95 96 syldan ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑚𝐴 ) → ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) ∈ ℂ )
98 80 82 92 94 97 fprodf1o ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ∏ 𝑚𝐴 ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) = ∏ 𝑛 ∈ ( 𝑓𝐴 ) ( ( 𝑘𝐵𝐶 ) ‘ ( 𝑓𝑛 ) ) )
99 79 98 eqtrd ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ∏ 𝑚𝐴 ( ( 𝑘𝐴𝐶 ) ‘ 𝑚 ) = ∏ 𝑛 ∈ ( 𝑓𝐴 ) ( ( 𝑘𝐵𝐶 ) ‘ ( 𝑓𝑛 ) ) )
100 eqidd ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) → ( 𝑓𝑛 ) = ( 𝑓𝑛 ) )
101 80 81 16 100 96 fprodf1o ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ∏ 𝑚𝐵 ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) = ∏ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ( ( 𝑘𝐵𝐶 ) ‘ ( 𝑓𝑛 ) ) )
102 73 99 101 3eqtr4d ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ∏ 𝑚𝐴 ( ( 𝑘𝐴𝐶 ) ‘ 𝑚 ) = ∏ 𝑚𝐵 ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) )
103 prodfc 𝑚𝐴 ( ( 𝑘𝐴𝐶 ) ‘ 𝑚 ) = ∏ 𝑘𝐴 𝐶
104 prodfc 𝑚𝐵 ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) = ∏ 𝑘𝐵 𝐶
105 102 103 104 3eqtr3g ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ∏ 𝑘𝐴 𝐶 = ∏ 𝑘𝐵 𝐶 )
106 105 expr ( ( 𝜑 ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ ) → ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 → ∏ 𝑘𝐴 𝐶 = ∏ 𝑘𝐵 𝐶 ) )
107 106 exlimdv ( ( 𝜑 ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ ) → ( ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 → ∏ 𝑘𝐴 𝐶 = ∏ 𝑘𝐵 𝐶 ) )
108 107 expimpd ( 𝜑 → ( ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) → ∏ 𝑘𝐴 𝐶 = ∏ 𝑘𝐵 𝐶 ) )
109 fz1f1o ( 𝐵 ∈ Fin → ( 𝐵 = ∅ ∨ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) )
110 4 109 syl ( 𝜑 → ( 𝐵 = ∅ ∨ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) )
111 14 108 110 mpjaod ( 𝜑 → ∏ 𝑘𝐴 𝐶 = ∏ 𝑘𝐵 𝐶 )