Metamath Proof Explorer


Theorem fprodcl2lem

Description: Finite product closure lemma. (Contributed by Scott Fenton, 14-Dec-2017)

Ref Expression
Hypotheses fprodcllem.1 ( 𝜑𝑆 ⊆ ℂ )
fprodcllem.2 ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
fprodcllem.3 ( 𝜑𝐴 ∈ Fin )
fprodcllem.4 ( ( 𝜑𝑘𝐴 ) → 𝐵𝑆 )
fprodcl2lem.5 ( 𝜑𝐴 ≠ ∅ )
Assertion fprodcl2lem ( 𝜑 → ∏ 𝑘𝐴 𝐵𝑆 )

Proof

Step Hyp Ref Expression
1 fprodcllem.1 ( 𝜑𝑆 ⊆ ℂ )
2 fprodcllem.2 ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
3 fprodcllem.3 ( 𝜑𝐴 ∈ Fin )
4 fprodcllem.4 ( ( 𝜑𝑘𝐴 ) → 𝐵𝑆 )
5 fprodcl2lem.5 ( 𝜑𝐴 ≠ ∅ )
6 5 a1d ( 𝜑 → ( ¬ ∏ 𝑘𝐴 𝐵𝑆𝐴 ≠ ∅ ) )
7 6 necon4bd ( 𝜑 → ( 𝐴 = ∅ → ∏ 𝑘𝐴 𝐵𝑆 ) )
8 prodfc 𝑚𝐴 ( ( 𝑘𝐴𝐵 ) ‘ 𝑚 ) = ∏ 𝑘𝐴 𝐵
9 fveq2 ( 𝑚 = ( 𝑓𝑥 ) → ( ( 𝑘𝐴𝐵 ) ‘ 𝑚 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝑓𝑥 ) ) )
10 simprl ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℕ )
11 simprr ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 )
12 1 adantr ( ( 𝜑𝑘𝐴 ) → 𝑆 ⊆ ℂ )
13 12 4 sseldd ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℂ )
14 13 fmpttd ( 𝜑 → ( 𝑘𝐴𝐵 ) : 𝐴 ⟶ ℂ )
15 14 ffvelrnda ( ( 𝜑𝑚𝐴 ) → ( ( 𝑘𝐴𝐵 ) ‘ 𝑚 ) ∈ ℂ )
16 15 adantlr ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) ∧ 𝑚𝐴 ) → ( ( 𝑘𝐴𝐵 ) ‘ 𝑚 ) ∈ ℂ )
17 f1of ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
18 17 ad2antll ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
19 fvco3 ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘𝐴𝐵 ) ∘ 𝑓 ) ‘ 𝑥 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝑓𝑥 ) ) )
20 18 19 sylan ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘𝐴𝐵 ) ∘ 𝑓 ) ‘ 𝑥 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝑓𝑥 ) ) )
21 9 10 11 16 20 fprod ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) → ∏ 𝑚𝐴 ( ( 𝑘𝐴𝐵 ) ‘ 𝑚 ) = ( seq 1 ( · , ( ( 𝑘𝐴𝐵 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) )
22 8 21 eqtr3id ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) → ∏ 𝑘𝐴 𝐵 = ( seq 1 ( · , ( ( 𝑘𝐴𝐵 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) )
23 nnuz ℕ = ( ℤ ‘ 1 )
24 10 23 eleqtrdi ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) → ( ♯ ‘ 𝐴 ) ∈ ( ℤ ‘ 1 ) )
25 4 fmpttd ( 𝜑 → ( 𝑘𝐴𝐵 ) : 𝐴𝑆 )
26 fco ( ( ( 𝑘𝐴𝐵 ) : 𝐴𝑆𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 ) → ( ( 𝑘𝐴𝐵 ) ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝑆 )
27 25 18 26 syl2an2r ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) → ( ( 𝑘𝐴𝐵 ) ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝑆 )
28 27 ffvelrnda ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘𝐴𝐵 ) ∘ 𝑓 ) ‘ 𝑥 ) ∈ 𝑆 )
29 2 adantlr ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
30 24 28 29 seqcl ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) → ( seq 1 ( · , ( ( 𝑘𝐴𝐵 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) ∈ 𝑆 )
31 22 30 eqeltrd ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) → ∏ 𝑘𝐴 𝐵𝑆 )
32 31 expr ( ( 𝜑 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 → ∏ 𝑘𝐴 𝐵𝑆 ) )
33 32 exlimdv ( ( 𝜑 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) → ( ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 → ∏ 𝑘𝐴 𝐵𝑆 ) )
34 33 expimpd ( 𝜑 → ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) → ∏ 𝑘𝐴 𝐵𝑆 ) )
35 fz1f1o ( 𝐴 ∈ Fin → ( 𝐴 = ∅ ∨ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) )
36 3 35 syl ( 𝜑 → ( 𝐴 = ∅ ∨ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) )
37 7 34 36 mpjaod ( 𝜑 → ∏ 𝑘𝐴 𝐵𝑆 )