# Metamath Proof Explorer

## Theorem cvmlift2lem3

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 7-May-2015)

Ref Expression
Hypotheses cvmlift2.b 𝐵 = 𝐶
cvmlift2.f ( 𝜑𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
cvmlift2.g ( 𝜑𝐺 ∈ ( ( II ×t II ) Cn 𝐽 ) )
cvmlift2.p ( 𝜑𝑃𝐵 )
cvmlift2.i ( 𝜑 → ( 𝐹𝑃 ) = ( 0 𝐺 0 ) )
cvmlift2.h 𝐻 = ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) )
cvmlift2lem3.1 𝐾 = ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑋 ) ) )
Assertion cvmlift2lem3 ( ( 𝜑𝑋 ∈ ( 0 [,] 1 ) ) → ( 𝐾 ∈ ( II Cn 𝐶 ) ∧ ( 𝐹𝐾 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝐾 ‘ 0 ) = ( 𝐻𝑋 ) ) )

### Proof

Step Hyp Ref Expression
1 cvmlift2.b 𝐵 = 𝐶
2 cvmlift2.f ( 𝜑𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
3 cvmlift2.g ( 𝜑𝐺 ∈ ( ( II ×t II ) Cn 𝐽 ) )
4 cvmlift2.p ( 𝜑𝑃𝐵 )
5 cvmlift2.i ( 𝜑 → ( 𝐹𝑃 ) = ( 0 𝐺 0 ) )
6 cvmlift2.h 𝐻 = ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) )
7 cvmlift2lem3.1 𝐾 = ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑋 ) ) )
8 2 adantr ( ( 𝜑𝑋 ∈ ( 0 [,] 1 ) ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
9 iitopon II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
10 9 a1i ( ( 𝜑𝑋 ∈ ( 0 [,] 1 ) ) → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
11 simpr ( ( 𝜑𝑋 ∈ ( 0 [,] 1 ) ) → 𝑋 ∈ ( 0 [,] 1 ) )
12 10 10 11 cnmptc ( ( 𝜑𝑋 ∈ ( 0 [,] 1 ) ) → ( 𝑧 ∈ ( 0 [,] 1 ) ↦ 𝑋 ) ∈ ( II Cn II ) )
13 10 cnmptid ( ( 𝜑𝑋 ∈ ( 0 [,] 1 ) ) → ( 𝑧 ∈ ( 0 [,] 1 ) ↦ 𝑧 ) ∈ ( II Cn II ) )
14 3 adantr ( ( 𝜑𝑋 ∈ ( 0 [,] 1 ) ) → 𝐺 ∈ ( ( II ×t II ) Cn 𝐽 ) )
15 10 12 13 14 cnmpt12f ( ( 𝜑𝑋 ∈ ( 0 [,] 1 ) ) → ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∈ ( II Cn 𝐽 ) )
16 1 2 3 4 5 6 cvmlift2lem2 ( 𝜑 → ( 𝐻 ∈ ( II Cn 𝐶 ) ∧ ( 𝐹𝐻 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) ∧ ( 𝐻 ‘ 0 ) = 𝑃 ) )
17 16 simp1d ( 𝜑𝐻 ∈ ( II Cn 𝐶 ) )
18 iiuni ( 0 [,] 1 ) = II
19 18 1 cnf ( 𝐻 ∈ ( II Cn 𝐶 ) → 𝐻 : ( 0 [,] 1 ) ⟶ 𝐵 )
20 17 19 syl ( 𝜑𝐻 : ( 0 [,] 1 ) ⟶ 𝐵 )
21 20 ffvelrnda ( ( 𝜑𝑋 ∈ ( 0 [,] 1 ) ) → ( 𝐻𝑋 ) ∈ 𝐵 )
22 0elunit 0 ∈ ( 0 [,] 1 )
23 oveq2 ( 𝑧 = 0 → ( 𝑋 𝐺 𝑧 ) = ( 𝑋 𝐺 0 ) )
24 eqid ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) )
25 ovex ( 𝑋 𝐺 0 ) ∈ V
26 23 24 25 fvmpt ( 0 ∈ ( 0 [,] 1 ) → ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ‘ 0 ) = ( 𝑋 𝐺 0 ) )
27 22 26 mp1i ( ( 𝜑𝑋 ∈ ( 0 [,] 1 ) ) → ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ‘ 0 ) = ( 𝑋 𝐺 0 ) )
28 16 simp2d ( 𝜑 → ( 𝐹𝐻 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) )
29 28 fveq1d ( 𝜑 → ( ( 𝐹𝐻 ) ‘ 𝑋 ) = ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) ‘ 𝑋 ) )
30 oveq1 ( 𝑧 = 𝑋 → ( 𝑧 𝐺 0 ) = ( 𝑋 𝐺 0 ) )
31 eqid ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) )
32 30 31 25 fvmpt ( 𝑋 ∈ ( 0 [,] 1 ) → ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) ‘ 𝑋 ) = ( 𝑋 𝐺 0 ) )
33 29 32 sylan9eq ( ( 𝜑𝑋 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹𝐻 ) ‘ 𝑋 ) = ( 𝑋 𝐺 0 ) )
34 fvco3 ( ( 𝐻 : ( 0 [,] 1 ) ⟶ 𝐵𝑋 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹𝐻 ) ‘ 𝑋 ) = ( 𝐹 ‘ ( 𝐻𝑋 ) ) )
35 20 34 sylan ( ( 𝜑𝑋 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹𝐻 ) ‘ 𝑋 ) = ( 𝐹 ‘ ( 𝐻𝑋 ) ) )
36 27 33 35 3eqtr2rd ( ( 𝜑𝑋 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ ( 𝐻𝑋 ) ) = ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ‘ 0 ) )
37 1 7 8 15 21 36 cvmliftiota ( ( 𝜑𝑋 ∈ ( 0 [,] 1 ) ) → ( 𝐾 ∈ ( II Cn 𝐶 ) ∧ ( 𝐹𝐾 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝐾 ‘ 0 ) = ( 𝐻𝑋 ) ) )