Metamath Proof Explorer


Theorem cvmlift2lem5

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 cvmlift2lem5 ( 𝜑𝐾 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐵 )

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 simp1d ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ) → ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) ∈ ( II Cn 𝐶 ) )
12 iiuni ( 0 [,] 1 ) = II
13 12 1 cnf ( ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) ∈ ( II Cn 𝐶 ) → ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) : ( 0 [,] 1 ) ⟶ 𝐵 )
14 11 13 syl ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ) → ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) : ( 0 [,] 1 ) ⟶ 𝐵 )
15 simprr ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ) → 𝑦 ∈ ( 0 [,] 1 ) )
16 14 15 ffvelrnd ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) ‘ 𝑦 ) ∈ 𝐵 )
17 16 ralrimivva ( 𝜑 → ∀ 𝑥 ∈ ( 0 [,] 1 ) ∀ 𝑦 ∈ ( 0 [,] 1 ) ( ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) ‘ 𝑦 ) ∈ 𝐵 )
18 7 fmpo ( ∀ 𝑥 ∈ ( 0 [,] 1 ) ∀ 𝑦 ∈ ( 0 [,] 1 ) ( ( 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻𝑥 ) ) ) ‘ 𝑦 ) ∈ 𝐵𝐾 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐵 )
19 17 18 sylib ( 𝜑𝐾 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐵 )