Metamath Proof Explorer


Theorem ulm2

Description: Simplify ulmval when F and G are known to be functions. (Contributed by Mario Carneiro, 26-Feb-2015)

Ref Expression
Hypotheses ulm2.z 𝑍 = ( ℤ𝑀 )
ulm2.m ( 𝜑𝑀 ∈ ℤ )
ulm2.f ( 𝜑𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
ulm2.b ( ( 𝜑 ∧ ( 𝑘𝑍𝑧𝑆 ) ) → ( ( 𝐹𝑘 ) ‘ 𝑧 ) = 𝐵 )
ulm2.a ( ( 𝜑𝑧𝑆 ) → ( 𝐺𝑧 ) = 𝐴 )
ulm2.g ( 𝜑𝐺 : 𝑆 ⟶ ℂ )
ulm2.s ( 𝜑𝑆𝑉 )
Assertion ulm2 ( 𝜑 → ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺 ↔ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( 𝐵𝐴 ) ) < 𝑥 ) )

Proof

Step Hyp Ref Expression
1 ulm2.z 𝑍 = ( ℤ𝑀 )
2 ulm2.m ( 𝜑𝑀 ∈ ℤ )
3 ulm2.f ( 𝜑𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
4 ulm2.b ( ( 𝜑 ∧ ( 𝑘𝑍𝑧𝑆 ) ) → ( ( 𝐹𝑘 ) ‘ 𝑧 ) = 𝐵 )
5 ulm2.a ( ( 𝜑𝑧𝑆 ) → ( 𝐺𝑧 ) = 𝐴 )
6 ulm2.g ( 𝜑𝐺 : 𝑆 ⟶ ℂ )
7 ulm2.s ( 𝜑𝑆𝑉 )
8 ulmval ( 𝑆𝑉 → ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺 ↔ ∃ 𝑛 ∈ ℤ ( 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝐺 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑥 ) ) )
9 7 8 syl ( 𝜑 → ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺 ↔ ∃ 𝑛 ∈ ℤ ( 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝐺 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑥 ) ) )
10 3anan12 ( ( 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝐺 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑥 ) ↔ ( 𝐺 : 𝑆 ⟶ ℂ ∧ ( 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑥 ) ) )
11 3 fdmd ( 𝜑 → dom 𝐹 = 𝑍 )
12 fdm ( 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) → dom 𝐹 = ( ℤ𝑛 ) )
13 11 12 sylan9req ( ( 𝜑𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) → 𝑍 = ( ℤ𝑛 ) )
14 1 13 eqtr3id ( ( 𝜑𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) → ( ℤ𝑀 ) = ( ℤ𝑛 ) )
15 2 adantr ( ( 𝜑𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) → 𝑀 ∈ ℤ )
16 uz11 ( 𝑀 ∈ ℤ → ( ( ℤ𝑀 ) = ( ℤ𝑛 ) ↔ 𝑀 = 𝑛 ) )
17 15 16 syl ( ( 𝜑𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) → ( ( ℤ𝑀 ) = ( ℤ𝑛 ) ↔ 𝑀 = 𝑛 ) )
18 14 17 mpbid ( ( 𝜑𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) → 𝑀 = 𝑛 )
19 18 eqcomd ( ( 𝜑𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) → 𝑛 = 𝑀 )
20 fveq2 ( 𝑛 = 𝑀 → ( ℤ𝑛 ) = ( ℤ𝑀 ) )
21 20 1 eqtr4di ( 𝑛 = 𝑀 → ( ℤ𝑛 ) = 𝑍 )
22 21 feq2d ( 𝑛 = 𝑀 → ( 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ↔ 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) ) )
23 22 biimparc ( ( 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝑛 = 𝑀 ) → 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) )
24 3 23 sylan ( ( 𝜑𝑛 = 𝑀 ) → 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) )
25 19 24 impbida ( 𝜑 → ( 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ↔ 𝑛 = 𝑀 ) )
26 25 anbi1d ( 𝜑 → ( ( 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑥 ) ↔ ( 𝑛 = 𝑀 ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑥 ) ) )
27 6 biantrurd ( 𝜑 → ( ( 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑥 ) ↔ ( 𝐺 : 𝑆 ⟶ ℂ ∧ ( 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑥 ) ) ) )
28 simp-4l ( ( ( ( ( 𝜑𝑛 = 𝑀 ) ∧ 𝑗 ∈ ( ℤ𝑛 ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ∧ 𝑧𝑆 ) → 𝜑 )
29 simpr ( ( 𝜑𝑛 = 𝑀 ) → 𝑛 = 𝑀 )
30 uzid ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ𝑀 ) )
31 2 30 syl ( 𝜑𝑀 ∈ ( ℤ𝑀 ) )
32 31 1 eleqtrrdi ( 𝜑𝑀𝑍 )
33 32 adantr ( ( 𝜑𝑛 = 𝑀 ) → 𝑀𝑍 )
34 29 33 eqeltrd ( ( 𝜑𝑛 = 𝑀 ) → 𝑛𝑍 )
35 1 uztrn2 ( ( 𝑛𝑍𝑗 ∈ ( ℤ𝑛 ) ) → 𝑗𝑍 )
36 34 35 sylan ( ( ( 𝜑𝑛 = 𝑀 ) ∧ 𝑗 ∈ ( ℤ𝑛 ) ) → 𝑗𝑍 )
37 1 uztrn2 ( ( 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ) → 𝑘𝑍 )
38 36 37 sylan ( ( ( ( 𝜑𝑛 = 𝑀 ) ∧ 𝑗 ∈ ( ℤ𝑛 ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → 𝑘𝑍 )
39 38 adantr ( ( ( ( ( 𝜑𝑛 = 𝑀 ) ∧ 𝑗 ∈ ( ℤ𝑛 ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ∧ 𝑧𝑆 ) → 𝑘𝑍 )
40 simpr ( ( ( ( ( 𝜑𝑛 = 𝑀 ) ∧ 𝑗 ∈ ( ℤ𝑛 ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ∧ 𝑧𝑆 ) → 𝑧𝑆 )
41 28 39 40 4 syl12anc ( ( ( ( ( 𝜑𝑛 = 𝑀 ) ∧ 𝑗 ∈ ( ℤ𝑛 ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ∧ 𝑧𝑆 ) → ( ( 𝐹𝑘 ) ‘ 𝑧 ) = 𝐵 )
42 28 5 sylancom ( ( ( ( ( 𝜑𝑛 = 𝑀 ) ∧ 𝑗 ∈ ( ℤ𝑛 ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ∧ 𝑧𝑆 ) → ( 𝐺𝑧 ) = 𝐴 )
43 41 42 oveq12d ( ( ( ( ( 𝜑𝑛 = 𝑀 ) ∧ 𝑗 ∈ ( ℤ𝑛 ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ∧ 𝑧𝑆 ) → ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) = ( 𝐵𝐴 ) )
44 43 fveq2d ( ( ( ( ( 𝜑𝑛 = 𝑀 ) ∧ 𝑗 ∈ ( ℤ𝑛 ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ∧ 𝑧𝑆 ) → ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) = ( abs ‘ ( 𝐵𝐴 ) ) )
45 44 breq1d ( ( ( ( ( 𝜑𝑛 = 𝑀 ) ∧ 𝑗 ∈ ( ℤ𝑛 ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ∧ 𝑧𝑆 ) → ( ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑥 ↔ ( abs ‘ ( 𝐵𝐴 ) ) < 𝑥 ) )
46 45 ralbidva ( ( ( ( 𝜑𝑛 = 𝑀 ) ∧ 𝑗 ∈ ( ℤ𝑛 ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → ( ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑥 ↔ ∀ 𝑧𝑆 ( abs ‘ ( 𝐵𝐴 ) ) < 𝑥 ) )
47 46 ralbidva ( ( ( 𝜑𝑛 = 𝑀 ) ∧ 𝑗 ∈ ( ℤ𝑛 ) ) → ( ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( 𝐵𝐴 ) ) < 𝑥 ) )
48 47 rexbidva ( ( 𝜑𝑛 = 𝑀 ) → ( ∃ 𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑥 ↔ ∃ 𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( 𝐵𝐴 ) ) < 𝑥 ) )
49 48 ralbidv ( ( 𝜑𝑛 = 𝑀 ) → ( ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑥 ↔ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( 𝐵𝐴 ) ) < 𝑥 ) )
50 49 pm5.32da ( 𝜑 → ( ( 𝑛 = 𝑀 ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑥 ) ↔ ( 𝑛 = 𝑀 ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( 𝐵𝐴 ) ) < 𝑥 ) ) )
51 26 27 50 3bitr3d ( 𝜑 → ( ( 𝐺 : 𝑆 ⟶ ℂ ∧ ( 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑥 ) ) ↔ ( 𝑛 = 𝑀 ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( 𝐵𝐴 ) ) < 𝑥 ) ) )
52 10 51 syl5bb ( 𝜑 → ( ( 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝐺 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑥 ) ↔ ( 𝑛 = 𝑀 ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( 𝐵𝐴 ) ) < 𝑥 ) ) )
53 52 rexbidv ( 𝜑 → ( ∃ 𝑛 ∈ ℤ ( 𝐹 : ( ℤ𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝐺 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 𝑥 ) ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 = 𝑀 ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( 𝐵𝐴 ) ) < 𝑥 ) ) )
54 21 rexeqdv ( 𝑛 = 𝑀 → ( ∃ 𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( 𝐵𝐴 ) ) < 𝑥 ↔ ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( 𝐵𝐴 ) ) < 𝑥 ) )
55 54 ralbidv ( 𝑛 = 𝑀 → ( ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( 𝐵𝐴 ) ) < 𝑥 ↔ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( 𝐵𝐴 ) ) < 𝑥 ) )
56 55 ceqsrexv ( 𝑀 ∈ ℤ → ( ∃ 𝑛 ∈ ℤ ( 𝑛 = 𝑀 ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( 𝐵𝐴 ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( 𝐵𝐴 ) ) < 𝑥 ) )
57 2 56 syl ( 𝜑 → ( ∃ 𝑛 ∈ ℤ ( 𝑛 = 𝑀 ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ( ℤ𝑛 ) ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( 𝐵𝐴 ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( 𝐵𝐴 ) ) < 𝑥 ) )
58 9 53 57 3bitrd ( 𝜑 → ( 𝐹 ( ⇝𝑢𝑆 ) 𝐺 ↔ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( 𝐵𝐴 ) ) < 𝑥 ) )