Metamath Proof Explorer

Theorem pi1grplem

Description: Lemma for pi1grp . (Contributed by Jeff Madsen, 11-Jun-2010) (Revised by Mario Carneiro, 10-Aug-2015)

Ref Expression
Hypotheses pi1fval.g ⊢ 𝐺 = ( 𝐽 π1 𝑌 )
pi1fval.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
pi1fval.3 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
pi1fval.4 ⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
pi1grplem.z ⊢ 0 = ( ( 0 [,] 1 ) × { 𝑌 } )
Assertion pi1grplem ( 𝜑 → ( 𝐺 ∈ Grp ∧ [ 0 ] ( ≃ph ‘ 𝐽 ) = ( 0g ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 pi1fval.g ⊢ 𝐺 = ( 𝐽 π1 𝑌 )
2 pi1fval.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
3 pi1fval.3 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
4 pi1fval.4 ⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
5 pi1grplem.z ⊢ 0 = ( ( 0 [,] 1 ) × { 𝑌 } )
6 eqid ⊢ ( 𝐽 Ω1 𝑌 ) = ( 𝐽 Ω1 𝑌 )
7 1 3 4 6 pi1val ⊢ ( 𝜑 → 𝐺 = ( ( 𝐽 Ω1 𝑌 ) /s ( ≃ph ‘ 𝐽 ) ) )
8 2 a1i ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
9 eqidd ⊢ ( 𝜑 → ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) = ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) )
10 1 3 4 6 8 9 pi1buni ⊢ ( 𝜑 → ∪ 𝐵 = ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) )
11 fvexd ⊢ ( 𝜑 → ( ≃ph ‘ 𝐽 ) ∈ V )
12 ovexd ⊢ ( 𝜑 → ( 𝐽 Ω1 𝑌 ) ∈ V )
13 1 3 4 6 8 10 pi1blem ⊢ ( 𝜑 → ( ( ( ≃ph ‘ 𝐽 ) “ ∪ 𝐵 ) ⊆ ∪ 𝐵 ∧ ∪ 𝐵 ⊆ ( II Cn 𝐽 ) ) )
14 13 simpld ⊢ ( 𝜑 → ( ( ≃ph ‘ 𝐽 ) “ ∪ 𝐵 ) ⊆ ∪ 𝐵 )
15 7 10 11 12 14 qusin ⊢ ( 𝜑 → 𝐺 = ( ( 𝐽 Ω1 𝑌 ) /s ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) ) )
16 6 3 4 om1plusg ⊢ ( 𝜑 → ( *𝑝 ‘ 𝐽 ) = ( +g ‘ ( 𝐽 Ω1 𝑌 ) ) )
17 phtpcer ⊢ ( ≃ph ‘ 𝐽 ) Er ( II Cn 𝐽 )
18 17 a1i ⊢ ( 𝜑 → ( ≃ph ‘ 𝐽 ) Er ( II Cn 𝐽 ) )
19 13 simprd ⊢ ( 𝜑 → ∪ 𝐵 ⊆ ( II Cn 𝐽 ) )
20 18 19 erinxp ⊢ ( 𝜑 → ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) Er ∪ 𝐵 )
21 eqid ⊢ ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) = ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) )
22 eqid ⊢ ( +g ‘ ( 𝐽 Ω1 𝑌 ) ) = ( +g ‘ ( 𝐽 Ω1 𝑌 ) )
23 1 3 4 8 21 6 22 pi1cpbl ⊢ ( 𝜑 → ( ( 𝑎 ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) 𝑐 ∧ 𝑏 ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) 𝑑 ) → ( 𝑎 ( +g ‘ ( 𝐽 Ω1 𝑌 ) ) 𝑏 ) ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) ( 𝑐 ( +g ‘ ( 𝐽 Ω1 𝑌 ) ) 𝑑 ) ) )
24 16 oveqd ⊢ ( 𝜑 → ( 𝑎 ( *𝑝 ‘ 𝐽 ) 𝑏 ) = ( 𝑎 ( +g ‘ ( 𝐽 Ω1 𝑌 ) ) 𝑏 ) )
25 16 oveqd ⊢ ( 𝜑 → ( 𝑐 ( *𝑝 ‘ 𝐽 ) 𝑑 ) = ( 𝑐 ( +g ‘ ( 𝐽 Ω1 𝑌 ) ) 𝑑 ) )
26 24 25 breq12d ⊢ ( 𝜑 → ( ( 𝑎 ( *𝑝 ‘ 𝐽 ) 𝑏 ) ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) ( 𝑐 ( *𝑝 ‘ 𝐽 ) 𝑑 ) ↔ ( 𝑎 ( +g ‘ ( 𝐽 Ω1 𝑌 ) ) 𝑏 ) ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) ( 𝑐 ( +g ‘ ( 𝐽 Ω1 𝑌 ) ) 𝑑 ) ) )
27 23 26 sylibrd ⊢ ( 𝜑 → ( ( 𝑎 ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) 𝑐 ∧ 𝑏 ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) 𝑑 ) → ( 𝑎 ( *𝑝 ‘ 𝐽 ) 𝑏 ) ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) ( 𝑐 ( *𝑝 ‘ 𝐽 ) 𝑑 ) ) )
28 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
29 4 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ) → 𝑌 ∈ 𝑋 )
30 10 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ) → ∪ 𝐵 = ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) )
31 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ) → 𝑥 ∈ ∪ 𝐵 )
32 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ) → 𝑦 ∈ ∪ 𝐵 )
33 6 28 29 30 31 32 om1addcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ) → ( 𝑥 ( *𝑝 ‘ 𝐽 ) 𝑦 ) ∈ ∪ 𝐵 )
34 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
35 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵 ) ) → 𝑌 ∈ 𝑋 )
36 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵 ) ) → ∪ 𝐵 = ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) )
37 33 3adant3r3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵 ) ) → ( 𝑥 ( *𝑝 ‘ 𝐽 ) 𝑦 ) ∈ ∪ 𝐵 )
38 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵 ) ) → 𝑧 ∈ ∪ 𝐵 )
39 6 34 35 36 37 38 om1addcl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵 ) ) → ( ( 𝑥 ( *𝑝 ‘ 𝐽 ) 𝑦 ) ( *𝑝 ‘ 𝐽 ) 𝑧 ) ∈ ∪ 𝐵 )
40 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵 ) ) → 𝑥 ∈ ∪ 𝐵 )
41 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵 ) ) → 𝑦 ∈ ∪ 𝐵 )
42 6 34 35 36 41 38 om1addcl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵 ) ) → ( 𝑦 ( *𝑝 ‘ 𝐽 ) 𝑧 ) ∈ ∪ 𝐵 )
43 6 34 35 36 40 42 om1addcl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵 ) ) → ( 𝑥 ( *𝑝 ‘ 𝐽 ) ( 𝑦 ( *𝑝 ‘ 𝐽 ) 𝑧 ) ) ∈ ∪ 𝐵 )
44 1 3 4 8 pi1eluni ⊢ ( 𝜑 → ( 𝑥 ∈ ∪ 𝐵 ↔ ( 𝑥 ∈ ( II Cn 𝐽 ) ∧ ( 𝑥 ‘ 0 ) = 𝑌 ∧ ( 𝑥 ‘ 1 ) = 𝑌 ) ) )
45 44 biimpa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ) → ( 𝑥 ∈ ( II Cn 𝐽 ) ∧ ( 𝑥 ‘ 0 ) = 𝑌 ∧ ( 𝑥 ‘ 1 ) = 𝑌 ) )
46 45 3ad2antr1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵 ) ) → ( 𝑥 ∈ ( II Cn 𝐽 ) ∧ ( 𝑥 ‘ 0 ) = 𝑌 ∧ ( 𝑥 ‘ 1 ) = 𝑌 ) )
47 46 simp1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵 ) ) → 𝑥 ∈ ( II Cn 𝐽 ) )
48 2 a1i ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵 ) ) → 𝐵 = ( Base ‘ 𝐺 ) )
49 1 34 35 48 pi1eluni ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵 ) ) → ( 𝑦 ∈ ∪ 𝐵 ↔ ( 𝑦 ∈ ( II Cn 𝐽 ) ∧ ( 𝑦 ‘ 0 ) = 𝑌 ∧ ( 𝑦 ‘ 1 ) = 𝑌 ) ) )
50 41 49 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵 ) ) → ( 𝑦 ∈ ( II Cn 𝐽 ) ∧ ( 𝑦 ‘ 0 ) = 𝑌 ∧ ( 𝑦 ‘ 1 ) = 𝑌 ) )
51 50 simp1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵 ) ) → 𝑦 ∈ ( II Cn 𝐽 ) )
52 1 34 35 48 pi1eluni ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵 ) ) → ( 𝑧 ∈ ∪ 𝐵 ↔ ( 𝑧 ∈ ( II Cn 𝐽 ) ∧ ( 𝑧 ‘ 0 ) = 𝑌 ∧ ( 𝑧 ‘ 1 ) = 𝑌 ) ) )
53 38 52 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵 ) ) → ( 𝑧 ∈ ( II Cn 𝐽 ) ∧ ( 𝑧 ‘ 0 ) = 𝑌 ∧ ( 𝑧 ‘ 1 ) = 𝑌 ) )
54 53 simp1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵 ) ) → 𝑧 ∈ ( II Cn 𝐽 ) )
55 46 simp3d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵 ) ) → ( 𝑥 ‘ 1 ) = 𝑌 )
56 50 simp2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵 ) ) → ( 𝑦 ‘ 0 ) = 𝑌 )
57 55 56 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵 ) ) → ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 0 ) )
58 50 simp3d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵 ) ) → ( 𝑦 ‘ 1 ) = 𝑌 )
59 53 simp2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵 ) ) → ( 𝑧 ‘ 0 ) = 𝑌 )
60 58 59 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵 ) ) → ( 𝑦 ‘ 1 ) = ( 𝑧 ‘ 0 ) )
61 eqid ⊢ ( 𝑢 ∈ ( 0 [,] 1 ) ↦ if ( 𝑢 ≤ ( 1 / 2 ) , if ( 𝑢 ≤ ( 1 / 4 ) , ( 2 · 𝑢 ) , ( 𝑢 + ( 1 / 4 ) ) ) , ( ( 𝑢 / 2 ) + ( 1 / 2 ) ) ) ) = ( 𝑢 ∈ ( 0 [,] 1 ) ↦ if ( 𝑢 ≤ ( 1 / 2 ) , if ( 𝑢 ≤ ( 1 / 4 ) , ( 2 · 𝑢 ) , ( 𝑢 + ( 1 / 4 ) ) ) , ( ( 𝑢 / 2 ) + ( 1 / 2 ) ) ) )
62 47 51 54 57 60 61 pcoass ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵 ) ) → ( ( 𝑥 ( *𝑝 ‘ 𝐽 ) 𝑦 ) ( *𝑝 ‘ 𝐽 ) 𝑧 ) ( ≃ph ‘ 𝐽 ) ( 𝑥 ( *𝑝 ‘ 𝐽 ) ( 𝑦 ( *𝑝 ‘ 𝐽 ) 𝑧 ) ) )
63 brinxp2 ⊢ ( ( ( 𝑥 ( *𝑝 ‘ 𝐽 ) 𝑦 ) ( *𝑝 ‘ 𝐽 ) 𝑧 ) ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) ( 𝑥 ( *𝑝 ‘ 𝐽 ) ( 𝑦 ( *𝑝 ‘ 𝐽 ) 𝑧 ) ) ↔ ( ( ( ( 𝑥 ( *𝑝 ‘ 𝐽 ) 𝑦 ) ( *𝑝 ‘ 𝐽 ) 𝑧 ) ∈ ∪ 𝐵 ∧ ( 𝑥 ( *𝑝 ‘ 𝐽 ) ( 𝑦 ( *𝑝 ‘ 𝐽 ) 𝑧 ) ) ∈ ∪ 𝐵 ) ∧ ( ( 𝑥 ( *𝑝 ‘ 𝐽 ) 𝑦 ) ( *𝑝 ‘ 𝐽 ) 𝑧 ) ( ≃ph ‘ 𝐽 ) ( 𝑥 ( *𝑝 ‘ 𝐽 ) ( 𝑦 ( *𝑝 ‘ 𝐽 ) 𝑧 ) ) ) )
64 39 43 62 63 syl21anbrc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ 𝐵 ∧ 𝑧 ∈ ∪ 𝐵 ) ) → ( ( 𝑥 ( *𝑝 ‘ 𝐽 ) 𝑦 ) ( *𝑝 ‘ 𝐽 ) 𝑧 ) ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) ( 𝑥 ( *𝑝 ‘ 𝐽 ) ( 𝑦 ( *𝑝 ‘ 𝐽 ) 𝑧 ) ) )
65 5 pcoptcl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑋 ) → ( 0 ∈ ( II Cn 𝐽 ) ∧ ( 0 ‘ 0 ) = 𝑌 ∧ ( 0 ‘ 1 ) = 𝑌 ) )
66 3 4 65 syl2anc ⊢ ( 𝜑 → ( 0 ∈ ( II Cn 𝐽 ) ∧ ( 0 ‘ 0 ) = 𝑌 ∧ ( 0 ‘ 1 ) = 𝑌 ) )
67 1 3 4 8 pi1eluni ⊢ ( 𝜑 → ( 0 ∈ ∪ 𝐵 ↔ ( 0 ∈ ( II Cn 𝐽 ) ∧ ( 0 ‘ 0 ) = 𝑌 ∧ ( 0 ‘ 1 ) = 𝑌 ) ) )
68 66 67 mpbird ⊢ ( 𝜑 → 0 ∈ ∪ 𝐵 )
69 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
70 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ) → 𝑌 ∈ 𝑋 )
71 10 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ) → ∪ 𝐵 = ( Base ‘ ( 𝐽 Ω1 𝑌 ) ) )
72 68 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ) → 0 ∈ ∪ 𝐵 )
73 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ) → 𝑥 ∈ ∪ 𝐵 )
74 6 69 70 71 72 73 om1addcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ) → ( 0 ( *𝑝 ‘ 𝐽 ) 𝑥 ) ∈ ∪ 𝐵 )
75 19 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ) → 𝑥 ∈ ( II Cn 𝐽 ) )
76 45 simp2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ) → ( 𝑥 ‘ 0 ) = 𝑌 )
77 5 pcopt ⊢ ( ( 𝑥 ∈ ( II Cn 𝐽 ) ∧ ( 𝑥 ‘ 0 ) = 𝑌 ) → ( 0 ( *𝑝 ‘ 𝐽 ) 𝑥 ) ( ≃ph ‘ 𝐽 ) 𝑥 )
78 75 76 77 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ) → ( 0 ( *𝑝 ‘ 𝐽 ) 𝑥 ) ( ≃ph ‘ 𝐽 ) 𝑥 )
79 brinxp2 ⊢ ( ( 0 ( *𝑝 ‘ 𝐽 ) 𝑥 ) ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) 𝑥 ↔ ( ( ( 0 ( *𝑝 ‘ 𝐽 ) 𝑥 ) ∈ ∪ 𝐵 ∧ 𝑥 ∈ ∪ 𝐵 ) ∧ ( 0 ( *𝑝 ‘ 𝐽 ) 𝑥 ) ( ≃ph ‘ 𝐽 ) 𝑥 ) )
80 74 73 78 79 syl21anbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ) → ( 0 ( *𝑝 ‘ 𝐽 ) 𝑥 ) ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) 𝑥 )
81 eqid ⊢ ( 𝑎 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ ( 1 − 𝑎 ) ) ) = ( 𝑎 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ ( 1 − 𝑎 ) ) )
82 81 pcorevcl ⊢ ( 𝑥 ∈ ( II Cn 𝐽 ) → ( ( 𝑎 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ ( 1 − 𝑎 ) ) ) ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑎 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ ( 1 − 𝑎 ) ) ) ‘ 0 ) = ( 𝑥 ‘ 1 ) ∧ ( ( 𝑎 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ ( 1 − 𝑎 ) ) ) ‘ 1 ) = ( 𝑥 ‘ 0 ) ) )
83 75 82 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ) → ( ( 𝑎 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ ( 1 − 𝑎 ) ) ) ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑎 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ ( 1 − 𝑎 ) ) ) ‘ 0 ) = ( 𝑥 ‘ 1 ) ∧ ( ( 𝑎 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ ( 1 − 𝑎 ) ) ) ‘ 1 ) = ( 𝑥 ‘ 0 ) ) )
84 83 simp1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ) → ( 𝑎 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ ( 1 − 𝑎 ) ) ) ∈ ( II Cn 𝐽 ) )
85 83 simp2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ) → ( ( 𝑎 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ ( 1 − 𝑎 ) ) ) ‘ 0 ) = ( 𝑥 ‘ 1 ) )
86 45 simp3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ) → ( 𝑥 ‘ 1 ) = 𝑌 )
87 85 86 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ) → ( ( 𝑎 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ ( 1 − 𝑎 ) ) ) ‘ 0 ) = 𝑌 )
88 83 simp3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ) → ( ( 𝑎 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ ( 1 − 𝑎 ) ) ) ‘ 1 ) = ( 𝑥 ‘ 0 ) )
89 88 76 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ) → ( ( 𝑎 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ ( 1 − 𝑎 ) ) ) ‘ 1 ) = 𝑌 )
90 1 3 4 8 pi1eluni ⊢ ( 𝜑 → ( ( 𝑎 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ ( 1 − 𝑎 ) ) ) ∈ ∪ 𝐵 ↔ ( ( 𝑎 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ ( 1 − 𝑎 ) ) ) ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑎 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ ( 1 − 𝑎 ) ) ) ‘ 0 ) = 𝑌 ∧ ( ( 𝑎 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ ( 1 − 𝑎 ) ) ) ‘ 1 ) = 𝑌 ) ) )
91 90 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ) → ( ( 𝑎 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ ( 1 − 𝑎 ) ) ) ∈ ∪ 𝐵 ↔ ( ( 𝑎 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ ( 1 − 𝑎 ) ) ) ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑎 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ ( 1 − 𝑎 ) ) ) ‘ 0 ) = 𝑌 ∧ ( ( 𝑎 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ ( 1 − 𝑎 ) ) ) ‘ 1 ) = 𝑌 ) ) )
92 84 87 89 91 mpbir3and ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ) → ( 𝑎 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ ( 1 − 𝑎 ) ) ) ∈ ∪ 𝐵 )
93 6 69 70 71 92 73 om1addcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ) → ( ( 𝑎 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ ( 1 − 𝑎 ) ) ) ( *𝑝 ‘ 𝐽 ) 𝑥 ) ∈ ∪ 𝐵 )
94 eqid ⊢ ( ( 0 [,] 1 ) × { ( 𝑥 ‘ 1 ) } ) = ( ( 0 [,] 1 ) × { ( 𝑥 ‘ 1 ) } )
95 81 94 pcorev ⊢ ( 𝑥 ∈ ( II Cn 𝐽 ) → ( ( 𝑎 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ ( 1 − 𝑎 ) ) ) ( *𝑝 ‘ 𝐽 ) 𝑥 ) ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝑥 ‘ 1 ) } ) )
96 75 95 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ) → ( ( 𝑎 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ ( 1 − 𝑎 ) ) ) ( *𝑝 ‘ 𝐽 ) 𝑥 ) ( ≃ph ‘ 𝐽 ) ( ( 0 [,] 1 ) × { ( 𝑥 ‘ 1 ) } ) )
97 86 sneqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ) → { ( 𝑥 ‘ 1 ) } = { 𝑌 } )
98 97 xpeq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ) → ( ( 0 [,] 1 ) × { ( 𝑥 ‘ 1 ) } ) = ( ( 0 [,] 1 ) × { 𝑌 } ) )
99 5 98 eqtr4id ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ) → 0 = ( ( 0 [,] 1 ) × { ( 𝑥 ‘ 1 ) } ) )
100 96 99 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ) → ( ( 𝑎 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ ( 1 − 𝑎 ) ) ) ( *𝑝 ‘ 𝐽 ) 𝑥 ) ( ≃ph ‘ 𝐽 ) 0 )
101 brinxp2 ⊢ ( ( ( 𝑎 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ ( 1 − 𝑎 ) ) ) ( *𝑝 ‘ 𝐽 ) 𝑥 ) ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) 0 ↔ ( ( ( ( 𝑎 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ ( 1 − 𝑎 ) ) ) ( *𝑝 ‘ 𝐽 ) 𝑥 ) ∈ ∪ 𝐵 ∧ 0 ∈ ∪ 𝐵 ) ∧ ( ( 𝑎 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ ( 1 − 𝑎 ) ) ) ( *𝑝 ‘ 𝐽 ) 𝑥 ) ( ≃ph ‘ 𝐽 ) 0 ) )
102 93 72 100 101 syl21anbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝐵 ) → ( ( 𝑎 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ‘ ( 1 − 𝑎 ) ) ) ( *𝑝 ‘ 𝐽 ) 𝑥 ) ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) 0 )
103 15 10 16 20 12 27 33 64 68 80 92 102 qusgrp2 ⊢ ( 𝜑 → ( 𝐺 ∈ Grp ∧ [ 0 ] ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) = ( 0g ‘ 𝐺 ) ) )
104 ecinxp ⊢ ( ( ( ( ≃ph ‘ 𝐽 ) “ ∪ 𝐵 ) ⊆ ∪ 𝐵 ∧ 0 ∈ ∪ 𝐵 ) → [ 0 ] ( ≃ph ‘ 𝐽 ) = [ 0 ] ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) )
105 14 68 104 syl2anc ⊢ ( 𝜑 → [ 0 ] ( ≃ph ‘ 𝐽 ) = [ 0 ] ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) )
106 105 eqeq1d ⊢ ( 𝜑 → ( [ 0 ] ( ≃ph ‘ 𝐽 ) = ( 0g ‘ 𝐺 ) ↔ [ 0 ] ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) = ( 0g ‘ 𝐺 ) ) )
107 106 anbi2d ⊢ ( 𝜑 → ( ( 𝐺 ∈ Grp ∧ [ 0 ] ( ≃ph ‘ 𝐽 ) = ( 0g ‘ 𝐺 ) ) ↔ ( 𝐺 ∈ Grp ∧ [ 0 ] ( ( ≃ph ‘ 𝐽 ) ∩ ( ∪ 𝐵 × ∪ 𝐵 ) ) = ( 0g ‘ 𝐺 ) ) ) )
108 103 107 mpbird ⊢ ( 𝜑 → ( 𝐺 ∈ Grp ∧ [ 0 ] ( ≃ph ‘ 𝐽 ) = ( 0g ‘ 𝐺 ) ) )