Step |
Hyp |
Ref |
Expression |
1 |
|
ulmdv.z |
⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 ) |
2 |
|
ulmdv.s |
⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } ) |
3 |
|
ulmdv.m |
⊢ ( 𝜑 → 𝑀 ∈ ℤ ) |
4 |
|
ulmdv.f |
⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑋 ) ) |
5 |
|
ulmdv.g |
⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ℂ ) |
6 |
|
ulmdv.l |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ⇝ ( 𝐺 ‘ 𝑧 ) ) |
7 |
|
ulmdv.u |
⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ( ⇝𝑢 ‘ 𝑋 ) 𝐻 ) |
8 |
|
dvfg |
⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ ) |
9 |
2 8
|
syl |
⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ ) |
10 |
|
recnprss |
⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ ) |
11 |
2 10
|
syl |
⊢ ( 𝜑 → 𝑆 ⊆ ℂ ) |
12 |
|
biidd |
⊢ ( 𝑘 = 𝑀 → ( 𝑋 ⊆ 𝑆 ↔ 𝑋 ⊆ 𝑆 ) ) |
13 |
1 2 3 4 5 6 7
|
ulmdvlem2 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → dom ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) = 𝑋 ) |
14 |
|
dvbsss |
⊢ dom ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ⊆ 𝑆 |
15 |
13 14
|
eqsstrrdi |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑋 ⊆ 𝑆 ) |
16 |
15
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 𝑋 ⊆ 𝑆 ) |
17 |
|
uzid |
⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
18 |
3 17
|
syl |
⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
19 |
18 1
|
eleqtrrdi |
⊢ ( 𝜑 → 𝑀 ∈ 𝑍 ) |
20 |
12 16 19
|
rspcdva |
⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 ) |
21 |
11 5 20
|
dvbss |
⊢ ( 𝜑 → dom ( 𝑆 D 𝐺 ) ⊆ 𝑋 ) |
22 |
1 2 3 4 5 6 7
|
ulmdvlem3 |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ( 𝑆 D 𝐺 ) ( 𝐻 ‘ 𝑧 ) ) |
23 |
|
vex |
⊢ 𝑧 ∈ V |
24 |
|
fvex |
⊢ ( 𝐻 ‘ 𝑧 ) ∈ V |
25 |
23 24
|
breldm |
⊢ ( 𝑧 ( 𝑆 D 𝐺 ) ( 𝐻 ‘ 𝑧 ) → 𝑧 ∈ dom ( 𝑆 D 𝐺 ) ) |
26 |
22 25
|
syl |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ∈ dom ( 𝑆 D 𝐺 ) ) |
27 |
21 26
|
eqelssd |
⊢ ( 𝜑 → dom ( 𝑆 D 𝐺 ) = 𝑋 ) |
28 |
27
|
feq2d |
⊢ ( 𝜑 → ( ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ ↔ ( 𝑆 D 𝐺 ) : 𝑋 ⟶ ℂ ) ) |
29 |
9 28
|
mpbid |
⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) : 𝑋 ⟶ ℂ ) |
30 |
29
|
ffnd |
⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) Fn 𝑋 ) |
31 |
|
ulmcl |
⊢ ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ( ⇝𝑢 ‘ 𝑋 ) 𝐻 → 𝐻 : 𝑋 ⟶ ℂ ) |
32 |
7 31
|
syl |
⊢ ( 𝜑 → 𝐻 : 𝑋 ⟶ ℂ ) |
33 |
32
|
ffnd |
⊢ ( 𝜑 → 𝐻 Fn 𝑋 ) |
34 |
9
|
ffund |
⊢ ( 𝜑 → Fun ( 𝑆 D 𝐺 ) ) |
35 |
34
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → Fun ( 𝑆 D 𝐺 ) ) |
36 |
|
funbrfv |
⊢ ( Fun ( 𝑆 D 𝐺 ) → ( 𝑧 ( 𝑆 D 𝐺 ) ( 𝐻 ‘ 𝑧 ) → ( ( 𝑆 D 𝐺 ) ‘ 𝑧 ) = ( 𝐻 ‘ 𝑧 ) ) ) |
37 |
35 22 36
|
sylc |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑆 D 𝐺 ) ‘ 𝑧 ) = ( 𝐻 ‘ 𝑧 ) ) |
38 |
30 33 37
|
eqfnfvd |
⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) = 𝐻 ) |