Metamath Proof Explorer


Theorem cvmlift2lem7

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 ) = 𝑃 ) )
cvmlift2.k 𝐾 = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) ‘ 𝑦 ) )
Assertion cvmlift2lem7 ( 𝜑 → ( 𝐹𝐾 ) = 𝐺 )

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 cvmlift2.k 𝐾 = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) ‘ 𝑦 ) )
8 eqid ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) = ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) )
9 1 2 3 4 5 6 8 cvmlift2lem3 ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ) → ( ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) ∈ ( II Cn 𝐶 ) ∧ ( 𝐹 ∘ ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) ‘ 0 ) = ( 𝐻𝑥 ) ) )
10 9 adantrr ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) ∈ ( II Cn 𝐶 ) ∧ ( 𝐹 ∘ ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) ‘ 0 ) = ( 𝐻𝑥 ) ) )
11 10 simp2d ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ) → ( 𝐹 ∘ ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) )
12 11 fveq1d ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝐹 ∘ ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) ) ‘ 𝑦 ) = ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ‘ 𝑦 ) )
13 10 simp1d ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ) → ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) ∈ ( II Cn 𝐶 ) )
14 iiuni ( 0 [,] 1 ) = II
15 14 1 cnf ( ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) ∈ ( II Cn 𝐶 ) → ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) : ( 0 [,] 1 ) ⟶ 𝐵 )
16 13 15 syl ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ) → ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) : ( 0 [,] 1 ) ⟶ 𝐵 )
17 simprr ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ) → 𝑦 ∈ ( 0 [,] 1 ) )
18 fvco3 ( ( ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) : ( 0 [,] 1 ) ⟶ 𝐵𝑦 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ∘ ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝐹 ‘ ( ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) ‘ 𝑦 ) ) )
19 16 17 18 syl2anc ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝐹 ∘ ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) ) ‘ 𝑦 ) = ( 𝐹 ‘ ( ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) ‘ 𝑦 ) ) )
20 oveq2 ( 𝑧 = 𝑦 → ( 𝑥 𝐺 𝑧 ) = ( 𝑥 𝐺 𝑦 ) )
21 eqid ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) )
22 ovex ( 𝑥 𝐺 𝑦 ) ∈ V
23 20 21 22 fvmpt ( 𝑦 ∈ ( 0 [,] 1 ) → ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ‘ 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
24 17 23 syl ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ‘ 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
25 12 19 24 3eqtr3d ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ) → ( 𝐹 ‘ ( ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) ‘ 𝑦 ) ) = ( 𝑥 𝐺 𝑦 ) )
26 25 3impb ( ( 𝜑𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ ( ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) ‘ 𝑦 ) ) = ( 𝑥 𝐺 𝑦 ) )
27 26 mpoeq3dva ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) ‘ 𝑦 ) ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑦 ) ) )
28 16 17 ffvelrnd ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) ‘ 𝑦 ) ∈ 𝐵 )
29 7 a1i ( 𝜑𝐾 = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) ‘ 𝑦 ) ) )
30 cvmcn ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐹 ∈ ( 𝐶 Cn 𝐽 ) )
31 eqid 𝐽 = 𝐽
32 1 31 cnf ( 𝐹 ∈ ( 𝐶 Cn 𝐽 ) → 𝐹 : 𝐵 𝐽 )
33 2 30 32 3syl ( 𝜑𝐹 : 𝐵 𝐽 )
34 33 feqmptd ( 𝜑𝐹 = ( 𝑤𝐵 ↦ ( 𝐹𝑤 ) ) )
35 fveq2 ( 𝑤 = ( ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) ‘ 𝑦 ) → ( 𝐹𝑤 ) = ( 𝐹 ‘ ( ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) ‘ 𝑦 ) ) )
36 28 29 34 35 fmpoco ( 𝜑 → ( 𝐹𝐾 ) = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) ‘ 𝑦 ) ) ) )
37 iitop II ∈ Top
38 37 37 14 14 txunii ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) = ( II ×t II )
39 38 31 cnf ( 𝐺 ∈ ( ( II ×t II ) Cn 𝐽 ) → 𝐺 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐽 )
40 ffn ( 𝐺 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐽𝐺 Fn ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
41 3 39 40 3syl ( 𝜑𝐺 Fn ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
42 fnov ( 𝐺 Fn ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ↔ 𝐺 = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑦 ) ) )
43 41 42 sylib ( 𝜑𝐺 = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑦 ) ) )
44 27 36 43 3eqtr4d ( 𝜑 → ( 𝐹𝐾 ) = 𝐺 )