Metamath Proof Explorer


Theorem om1addcl

Description: Closure of the group operation of the loop space. (Contributed by Jeff Madsen, 11-Jun-2010) (Revised by Mario Carneiro, 5-Sep-2015)

Ref Expression
Hypotheses om1bas.o 𝑂 = ( 𝐽 Ω1 𝑌 )
om1bas.j ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
om1bas.y ( 𝜑𝑌𝑋 )
om1bas.b ( 𝜑𝐵 = ( Base ‘ 𝑂 ) )
om1addcl.h ( 𝜑𝐻𝐵 )
om1addcl.k ( 𝜑𝐾𝐵 )
Assertion om1addcl ( 𝜑 → ( 𝐻 ( *𝑝𝐽 ) 𝐾 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 om1bas.o 𝑂 = ( 𝐽 Ω1 𝑌 )
2 om1bas.j ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3 om1bas.y ( 𝜑𝑌𝑋 )
4 om1bas.b ( 𝜑𝐵 = ( Base ‘ 𝑂 ) )
5 om1addcl.h ( 𝜑𝐻𝐵 )
6 om1addcl.k ( 𝜑𝐾𝐵 )
7 1 2 3 4 om1elbas ( 𝜑 → ( 𝐻𝐵 ↔ ( 𝐻 ∈ ( II Cn 𝐽 ) ∧ ( 𝐻 ‘ 0 ) = 𝑌 ∧ ( 𝐻 ‘ 1 ) = 𝑌 ) ) )
8 5 7 mpbid ( 𝜑 → ( 𝐻 ∈ ( II Cn 𝐽 ) ∧ ( 𝐻 ‘ 0 ) = 𝑌 ∧ ( 𝐻 ‘ 1 ) = 𝑌 ) )
9 8 simp1d ( 𝜑𝐻 ∈ ( II Cn 𝐽 ) )
10 1 2 3 4 om1elbas ( 𝜑 → ( 𝐾𝐵 ↔ ( 𝐾 ∈ ( II Cn 𝐽 ) ∧ ( 𝐾 ‘ 0 ) = 𝑌 ∧ ( 𝐾 ‘ 1 ) = 𝑌 ) ) )
11 6 10 mpbid ( 𝜑 → ( 𝐾 ∈ ( II Cn 𝐽 ) ∧ ( 𝐾 ‘ 0 ) = 𝑌 ∧ ( 𝐾 ‘ 1 ) = 𝑌 ) )
12 11 simp1d ( 𝜑𝐾 ∈ ( II Cn 𝐽 ) )
13 8 simp3d ( 𝜑 → ( 𝐻 ‘ 1 ) = 𝑌 )
14 11 simp2d ( 𝜑 → ( 𝐾 ‘ 0 ) = 𝑌 )
15 13 14 eqtr4d ( 𝜑 → ( 𝐻 ‘ 1 ) = ( 𝐾 ‘ 0 ) )
16 9 12 15 pcocn ( 𝜑 → ( 𝐻 ( *𝑝𝐽 ) 𝐾 ) ∈ ( II Cn 𝐽 ) )
17 9 12 pco0 ( 𝜑 → ( ( 𝐻 ( *𝑝𝐽 ) 𝐾 ) ‘ 0 ) = ( 𝐻 ‘ 0 ) )
18 8 simp2d ( 𝜑 → ( 𝐻 ‘ 0 ) = 𝑌 )
19 17 18 eqtrd ( 𝜑 → ( ( 𝐻 ( *𝑝𝐽 ) 𝐾 ) ‘ 0 ) = 𝑌 )
20 9 12 pco1 ( 𝜑 → ( ( 𝐻 ( *𝑝𝐽 ) 𝐾 ) ‘ 1 ) = ( 𝐾 ‘ 1 ) )
21 11 simp3d ( 𝜑 → ( 𝐾 ‘ 1 ) = 𝑌 )
22 20 21 eqtrd ( 𝜑 → ( ( 𝐻 ( *𝑝𝐽 ) 𝐾 ) ‘ 1 ) = 𝑌 )
23 1 2 3 4 om1elbas ( 𝜑 → ( ( 𝐻 ( *𝑝𝐽 ) 𝐾 ) ∈ 𝐵 ↔ ( ( 𝐻 ( *𝑝𝐽 ) 𝐾 ) ∈ ( II Cn 𝐽 ) ∧ ( ( 𝐻 ( *𝑝𝐽 ) 𝐾 ) ‘ 0 ) = 𝑌 ∧ ( ( 𝐻 ( *𝑝𝐽 ) 𝐾 ) ‘ 1 ) = 𝑌 ) ) )
24 16 19 22 23 mpbir3and ( 𝜑 → ( 𝐻 ( *𝑝𝐽 ) 𝐾 ) ∈ 𝐵 )