Metamath Proof Explorer

Theorem cvmlift2lem8

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 9-Mar-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	cvmlift2lem8	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 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		cvmlift2.k	⊢ 𝐾 = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑥 ) ) ) ‘ 𝑦 ) )
8		simpr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → 𝑋 ∈ ( 0 [,] 1 ) )
9		0elunit	⊢ 0 ∈ ( 0 [,] 1 )
10	1 2 3 4 5 6 7	cvmlift2lem4	⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ 0 ∈ ( 0 [,] 1 ) ) → ( 𝑋 𝐾 0 ) = ( ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ) ‘ 0 ) )
11	8 9 10	sylancl	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( 𝑋 𝐾 0 ) = ( ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ) ‘ 0 ) )
12		eqid	⊢ ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ) = ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) )
13	1 2 3 4 5 6 12	cvmlift2lem3	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ) ∈ ( II Cn 𝐶 ) ∧ ( 𝐹 ∘ ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ) ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ) ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) )
14	13	simp3d	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ) ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) )
15	11 14	eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( 𝑋 𝐾 0 ) = ( 𝐻 ‘ 𝑋 ) )