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 
|- G = ( J pi1 Y )
pi1fval.b 
|- B = ( Base ` G )
pi1fval.3 
|- ( ph -> J e. ( TopOn ` X ) )
pi1fval.4 
|- ( ph -> Y e. X )
pi1grplem.z 
|- .0. = ( ( 0 [,] 1 ) X. { Y } )
Assertion pi1grplem 
|- ( ph -> ( G e. Grp /\ [ .0. ] ( ~=ph ` J ) = ( 0g ` G ) ) )

Proof

Step Hyp Ref Expression
1 pi1fval.g 
 |-  G = ( J pi1 Y )
2 pi1fval.b 
 |-  B = ( Base ` G )
3 pi1fval.3 
 |-  ( ph -> J e. ( TopOn ` X ) )
4 pi1fval.4 
 |-  ( ph -> Y e. X )
5 pi1grplem.z 
 |-  .0. = ( ( 0 [,] 1 ) X. { Y } )
6 eqid 
 |-  ( J Om1 Y ) = ( J Om1 Y )
7 1 3 4 6 pi1val 
 |-  ( ph -> G = ( ( J Om1 Y ) /s ( ~=ph ` J ) ) )
8 2 a1i 
 |-  ( ph -> B = ( Base ` G ) )
9 eqidd 
 |-  ( ph -> ( Base ` ( J Om1 Y ) ) = ( Base ` ( J Om1 Y ) ) )
10 1 3 4 6 8 9 pi1buni 
 |-  ( ph -> U. B = ( Base ` ( J Om1 Y ) ) )
11 fvexd 
 |-  ( ph -> ( ~=ph ` J ) e. _V )
12 ovexd 
 |-  ( ph -> ( J Om1 Y ) e. _V )
13 1 3 4 6 8 10 pi1blem 
 |-  ( ph -> ( ( ( ~=ph ` J ) " U. B ) C_ U. B /\ U. B C_ ( II Cn J ) ) )
14 13 simpld 
 |-  ( ph -> ( ( ~=ph ` J ) " U. B ) C_ U. B )
15 7 10 11 12 14 qusin 
 |-  ( ph -> G = ( ( J Om1 Y ) /s ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ) )
16 6 3 4 om1plusg 
 |-  ( ph -> ( *p ` J ) = ( +g ` ( J Om1 Y ) ) )
17 phtpcer 
 |-  ( ~=ph ` J ) Er ( II Cn J )
18 17 a1i 
 |-  ( ph -> ( ~=ph ` J ) Er ( II Cn J ) )
19 13 simprd 
 |-  ( ph -> U. B C_ ( II Cn J ) )
20 18 19 erinxp 
 |-  ( ph -> ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) Er U. B )
21 eqid 
 |-  ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) = ( ( ~=ph ` J ) i^i ( U. B X. U. B ) )
22 eqid 
 |-  ( +g ` ( J Om1 Y ) ) = ( +g ` ( J Om1 Y ) )
23 1 3 4 8 21 6 22 pi1cpbl 
 |-  ( ph -> ( ( a ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) c /\ b ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) d ) -> ( a ( +g ` ( J Om1 Y ) ) b ) ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ( c ( +g ` ( J Om1 Y ) ) d ) ) )
24 16 oveqd 
 |-  ( ph -> ( a ( *p ` J ) b ) = ( a ( +g ` ( J Om1 Y ) ) b ) )
25 16 oveqd 
 |-  ( ph -> ( c ( *p ` J ) d ) = ( c ( +g ` ( J Om1 Y ) ) d ) )
26 24 25 breq12d 
 |-  ( ph -> ( ( a ( *p ` J ) b ) ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ( c ( *p ` J ) d ) <-> ( a ( +g ` ( J Om1 Y ) ) b ) ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ( c ( +g ` ( J Om1 Y ) ) d ) ) )
27 23 26 sylibrd 
 |-  ( ph -> ( ( a ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) c /\ b ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) d ) -> ( a ( *p ` J ) b ) ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ( c ( *p ` J ) d ) ) )
28 3 3ad2ant1 
 |-  ( ( ph /\ x e. U. B /\ y e. U. B ) -> J e. ( TopOn ` X ) )
29 4 3ad2ant1 
 |-  ( ( ph /\ x e. U. B /\ y e. U. B ) -> Y e. X )
30 10 3ad2ant1 
 |-  ( ( ph /\ x e. U. B /\ y e. U. B ) -> U. B = ( Base ` ( J Om1 Y ) ) )
31 simp2 
 |-  ( ( ph /\ x e. U. B /\ y e. U. B ) -> x e. U. B )
32 simp3 
 |-  ( ( ph /\ x e. U. B /\ y e. U. B ) -> y e. U. B )
33 6 28 29 30 31 32 om1addcl 
 |-  ( ( ph /\ x e. U. B /\ y e. U. B ) -> ( x ( *p ` J ) y ) e. U. B )
34 3 adantr 
 |-  ( ( ph /\ ( x e. U. B /\ y e. U. B /\ z e. U. B ) ) -> J e. ( TopOn ` X ) )
35 4 adantr 
 |-  ( ( ph /\ ( x e. U. B /\ y e. U. B /\ z e. U. B ) ) -> Y e. X )
36 10 adantr 
 |-  ( ( ph /\ ( x e. U. B /\ y e. U. B /\ z e. U. B ) ) -> U. B = ( Base ` ( J Om1 Y ) ) )
37 33 3adant3r3 
 |-  ( ( ph /\ ( x e. U. B /\ y e. U. B /\ z e. U. B ) ) -> ( x ( *p ` J ) y ) e. U. B )
38 simpr3 
 |-  ( ( ph /\ ( x e. U. B /\ y e. U. B /\ z e. U. B ) ) -> z e. U. B )
39 6 34 35 36 37 38 om1addcl 
 |-  ( ( ph /\ ( x e. U. B /\ y e. U. B /\ z e. U. B ) ) -> ( ( x ( *p ` J ) y ) ( *p ` J ) z ) e. U. B )
40 simpr1 
 |-  ( ( ph /\ ( x e. U. B /\ y e. U. B /\ z e. U. B ) ) -> x e. U. B )
41 simpr2 
 |-  ( ( ph /\ ( x e. U. B /\ y e. U. B /\ z e. U. B ) ) -> y e. U. B )
42 6 34 35 36 41 38 om1addcl 
 |-  ( ( ph /\ ( x e. U. B /\ y e. U. B /\ z e. U. B ) ) -> ( y ( *p ` J ) z ) e. U. B )
43 6 34 35 36 40 42 om1addcl 
 |-  ( ( ph /\ ( x e. U. B /\ y e. U. B /\ z e. U. B ) ) -> ( x ( *p ` J ) ( y ( *p ` J ) z ) ) e. U. B )
44 1 3 4 8 pi1eluni 
 |-  ( ph -> ( x e. U. B <-> ( x e. ( II Cn J ) /\ ( x ` 0 ) = Y /\ ( x ` 1 ) = Y ) ) )
45 44 biimpa 
 |-  ( ( ph /\ x e. U. B ) -> ( x e. ( II Cn J ) /\ ( x ` 0 ) = Y /\ ( x ` 1 ) = Y ) )
46 45 3ad2antr1 
 |-  ( ( ph /\ ( x e. U. B /\ y e. U. B /\ z e. U. B ) ) -> ( x e. ( II Cn J ) /\ ( x ` 0 ) = Y /\ ( x ` 1 ) = Y ) )
47 46 simp1d 
 |-  ( ( ph /\ ( x e. U. B /\ y e. U. B /\ z e. U. B ) ) -> x e. ( II Cn J ) )
48 2 a1i 
 |-  ( ( ph /\ ( x e. U. B /\ y e. U. B /\ z e. U. B ) ) -> B = ( Base ` G ) )
49 1 34 35 48 pi1eluni 
 |-  ( ( ph /\ ( x e. U. B /\ y e. U. B /\ z e. U. B ) ) -> ( y e. U. B <-> ( y e. ( II Cn J ) /\ ( y ` 0 ) = Y /\ ( y ` 1 ) = Y ) ) )
50 41 49 mpbid 
 |-  ( ( ph /\ ( x e. U. B /\ y e. U. B /\ z e. U. B ) ) -> ( y e. ( II Cn J ) /\ ( y ` 0 ) = Y /\ ( y ` 1 ) = Y ) )
51 50 simp1d 
 |-  ( ( ph /\ ( x e. U. B /\ y e. U. B /\ z e. U. B ) ) -> y e. ( II Cn J ) )
52 1 34 35 48 pi1eluni 
 |-  ( ( ph /\ ( x e. U. B /\ y e. U. B /\ z e. U. B ) ) -> ( z e. U. B <-> ( z e. ( II Cn J ) /\ ( z ` 0 ) = Y /\ ( z ` 1 ) = Y ) ) )
53 38 52 mpbid 
 |-  ( ( ph /\ ( x e. U. B /\ y e. U. B /\ z e. U. B ) ) -> ( z e. ( II Cn J ) /\ ( z ` 0 ) = Y /\ ( z ` 1 ) = Y ) )
54 53 simp1d 
 |-  ( ( ph /\ ( x e. U. B /\ y e. U. B /\ z e. U. B ) ) -> z e. ( II Cn J ) )
55 46 simp3d 
 |-  ( ( ph /\ ( x e. U. B /\ y e. U. B /\ z e. U. B ) ) -> ( x ` 1 ) = Y )
56 50 simp2d 
 |-  ( ( ph /\ ( x e. U. B /\ y e. U. B /\ z e. U. B ) ) -> ( y ` 0 ) = Y )
57 55 56 eqtr4d 
 |-  ( ( ph /\ ( x e. U. B /\ y e. U. B /\ z e. U. B ) ) -> ( x ` 1 ) = ( y ` 0 ) )
58 50 simp3d 
 |-  ( ( ph /\ ( x e. U. B /\ y e. U. B /\ z e. U. B ) ) -> ( y ` 1 ) = Y )
59 53 simp2d 
 |-  ( ( ph /\ ( x e. U. B /\ y e. U. B /\ z e. U. B ) ) -> ( z ` 0 ) = Y )
60 58 59 eqtr4d 
 |-  ( ( ph /\ ( x e. U. B /\ y e. U. B /\ z e. U. B ) ) -> ( y ` 1 ) = ( z ` 0 ) )
61 eqid 
 |-  ( u e. ( 0 [,] 1 ) |-> if ( u <_ ( 1 / 2 ) , if ( u <_ ( 1 / 4 ) , ( 2 x. u ) , ( u + ( 1 / 4 ) ) ) , ( ( u / 2 ) + ( 1 / 2 ) ) ) ) = ( u e. ( 0 [,] 1 ) |-> if ( u <_ ( 1 / 2 ) , if ( u <_ ( 1 / 4 ) , ( 2 x. u ) , ( u + ( 1 / 4 ) ) ) , ( ( u / 2 ) + ( 1 / 2 ) ) ) )
62 47 51 54 57 60 61 pcoass 
 |-  ( ( ph /\ ( x e. U. B /\ y e. U. B /\ z e. U. B ) ) -> ( ( x ( *p ` J ) y ) ( *p ` J ) z ) ( ~=ph ` J ) ( x ( *p ` J ) ( y ( *p ` J ) z ) ) )
63 brinxp2 
 |-  ( ( ( x ( *p ` J ) y ) ( *p ` J ) z ) ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ( x ( *p ` J ) ( y ( *p ` J ) z ) ) <-> ( ( ( ( x ( *p ` J ) y ) ( *p ` J ) z ) e. U. B /\ ( x ( *p ` J ) ( y ( *p ` J ) z ) ) e. U. B ) /\ ( ( x ( *p ` J ) y ) ( *p ` J ) z ) ( ~=ph ` J ) ( x ( *p ` J ) ( y ( *p ` J ) z ) ) ) )
64 39 43 62 63 syl21anbrc 
 |-  ( ( ph /\ ( x e. U. B /\ y e. U. B /\ z e. U. B ) ) -> ( ( x ( *p ` J ) y ) ( *p ` J ) z ) ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) ( x ( *p ` J ) ( y ( *p ` J ) z ) ) )
65 5 pcoptcl 
 |-  ( ( J e. ( TopOn ` X ) /\ Y e. X ) -> ( .0. e. ( II Cn J ) /\ ( .0. ` 0 ) = Y /\ ( .0. ` 1 ) = Y ) )
66 3 4 65 syl2anc 
 |-  ( ph -> ( .0. e. ( II Cn J ) /\ ( .0. ` 0 ) = Y /\ ( .0. ` 1 ) = Y ) )
67 1 3 4 8 pi1eluni 
 |-  ( ph -> ( .0. e. U. B <-> ( .0. e. ( II Cn J ) /\ ( .0. ` 0 ) = Y /\ ( .0. ` 1 ) = Y ) ) )
68 66 67 mpbird 
 |-  ( ph -> .0. e. U. B )
69 3 adantr 
 |-  ( ( ph /\ x e. U. B ) -> J e. ( TopOn ` X ) )
70 4 adantr 
 |-  ( ( ph /\ x e. U. B ) -> Y e. X )
71 10 adantr 
 |-  ( ( ph /\ x e. U. B ) -> U. B = ( Base ` ( J Om1 Y ) ) )
72 68 adantr 
 |-  ( ( ph /\ x e. U. B ) -> .0. e. U. B )
73 simpr 
 |-  ( ( ph /\ x e. U. B ) -> x e. U. B )
74 6 69 70 71 72 73 om1addcl 
 |-  ( ( ph /\ x e. U. B ) -> ( .0. ( *p ` J ) x ) e. U. B )
75 19 sselda 
 |-  ( ( ph /\ x e. U. B ) -> x e. ( II Cn J ) )
76 45 simp2d 
 |-  ( ( ph /\ x e. U. B ) -> ( x ` 0 ) = Y )
77 5 pcopt 
 |-  ( ( x e. ( II Cn J ) /\ ( x ` 0 ) = Y ) -> ( .0. ( *p ` J ) x ) ( ~=ph ` J ) x )
78 75 76 77 syl2anc 
 |-  ( ( ph /\ x e. U. B ) -> ( .0. ( *p ` J ) x ) ( ~=ph ` J ) x )
79 brinxp2 
 |-  ( ( .0. ( *p ` J ) x ) ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) x <-> ( ( ( .0. ( *p ` J ) x ) e. U. B /\ x e. U. B ) /\ ( .0. ( *p ` J ) x ) ( ~=ph ` J ) x ) )
80 74 73 78 79 syl21anbrc 
 |-  ( ( ph /\ x e. U. B ) -> ( .0. ( *p ` J ) x ) ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) x )
81 eqid 
 |-  ( a e. ( 0 [,] 1 ) |-> ( x ` ( 1 - a ) ) ) = ( a e. ( 0 [,] 1 ) |-> ( x ` ( 1 - a ) ) )
82 81 pcorevcl 
 |-  ( x e. ( II Cn J ) -> ( ( a e. ( 0 [,] 1 ) |-> ( x ` ( 1 - a ) ) ) e. ( II Cn J ) /\ ( ( a e. ( 0 [,] 1 ) |-> ( x ` ( 1 - a ) ) ) ` 0 ) = ( x ` 1 ) /\ ( ( a e. ( 0 [,] 1 ) |-> ( x ` ( 1 - a ) ) ) ` 1 ) = ( x ` 0 ) ) )
83 75 82 syl 
 |-  ( ( ph /\ x e. U. B ) -> ( ( a e. ( 0 [,] 1 ) |-> ( x ` ( 1 - a ) ) ) e. ( II Cn J ) /\ ( ( a e. ( 0 [,] 1 ) |-> ( x ` ( 1 - a ) ) ) ` 0 ) = ( x ` 1 ) /\ ( ( a e. ( 0 [,] 1 ) |-> ( x ` ( 1 - a ) ) ) ` 1 ) = ( x ` 0 ) ) )
84 83 simp1d 
 |-  ( ( ph /\ x e. U. B ) -> ( a e. ( 0 [,] 1 ) |-> ( x ` ( 1 - a ) ) ) e. ( II Cn J ) )
85 83 simp2d 
 |-  ( ( ph /\ x e. U. B ) -> ( ( a e. ( 0 [,] 1 ) |-> ( x ` ( 1 - a ) ) ) ` 0 ) = ( x ` 1 ) )
86 45 simp3d 
 |-  ( ( ph /\ x e. U. B ) -> ( x ` 1 ) = Y )
87 85 86 eqtrd 
 |-  ( ( ph /\ x e. U. B ) -> ( ( a e. ( 0 [,] 1 ) |-> ( x ` ( 1 - a ) ) ) ` 0 ) = Y )
88 83 simp3d 
 |-  ( ( ph /\ x e. U. B ) -> ( ( a e. ( 0 [,] 1 ) |-> ( x ` ( 1 - a ) ) ) ` 1 ) = ( x ` 0 ) )
89 88 76 eqtrd 
 |-  ( ( ph /\ x e. U. B ) -> ( ( a e. ( 0 [,] 1 ) |-> ( x ` ( 1 - a ) ) ) ` 1 ) = Y )
90 1 3 4 8 pi1eluni 
 |-  ( ph -> ( ( a e. ( 0 [,] 1 ) |-> ( x ` ( 1 - a ) ) ) e. U. B <-> ( ( a e. ( 0 [,] 1 ) |-> ( x ` ( 1 - a ) ) ) e. ( II Cn J ) /\ ( ( a e. ( 0 [,] 1 ) |-> ( x ` ( 1 - a ) ) ) ` 0 ) = Y /\ ( ( a e. ( 0 [,] 1 ) |-> ( x ` ( 1 - a ) ) ) ` 1 ) = Y ) ) )
91 90 adantr 
 |-  ( ( ph /\ x e. U. B ) -> ( ( a e. ( 0 [,] 1 ) |-> ( x ` ( 1 - a ) ) ) e. U. B <-> ( ( a e. ( 0 [,] 1 ) |-> ( x ` ( 1 - a ) ) ) e. ( II Cn J ) /\ ( ( a e. ( 0 [,] 1 ) |-> ( x ` ( 1 - a ) ) ) ` 0 ) = Y /\ ( ( a e. ( 0 [,] 1 ) |-> ( x ` ( 1 - a ) ) ) ` 1 ) = Y ) ) )
92 84 87 89 91 mpbir3and 
 |-  ( ( ph /\ x e. U. B ) -> ( a e. ( 0 [,] 1 ) |-> ( x ` ( 1 - a ) ) ) e. U. B )
93 6 69 70 71 92 73 om1addcl 
 |-  ( ( ph /\ x e. U. B ) -> ( ( a e. ( 0 [,] 1 ) |-> ( x ` ( 1 - a ) ) ) ( *p ` J ) x ) e. U. B )
94 eqid 
 |-  ( ( 0 [,] 1 ) X. { ( x ` 1 ) } ) = ( ( 0 [,] 1 ) X. { ( x ` 1 ) } )
95 81 94 pcorev 
 |-  ( x e. ( II Cn J ) -> ( ( a e. ( 0 [,] 1 ) |-> ( x ` ( 1 - a ) ) ) ( *p ` J ) x ) ( ~=ph ` J ) ( ( 0 [,] 1 ) X. { ( x ` 1 ) } ) )
96 75 95 syl 
 |-  ( ( ph /\ x e. U. B ) -> ( ( a e. ( 0 [,] 1 ) |-> ( x ` ( 1 - a ) ) ) ( *p ` J ) x ) ( ~=ph ` J ) ( ( 0 [,] 1 ) X. { ( x ` 1 ) } ) )
97 86 sneqd 
 |-  ( ( ph /\ x e. U. B ) -> { ( x ` 1 ) } = { Y } )
98 97 xpeq2d 
 |-  ( ( ph /\ x e. U. B ) -> ( ( 0 [,] 1 ) X. { ( x ` 1 ) } ) = ( ( 0 [,] 1 ) X. { Y } ) )
99 5 98 eqtr4id 
 |-  ( ( ph /\ x e. U. B ) -> .0. = ( ( 0 [,] 1 ) X. { ( x ` 1 ) } ) )
100 96 99 breqtrrd 
 |-  ( ( ph /\ x e. U. B ) -> ( ( a e. ( 0 [,] 1 ) |-> ( x ` ( 1 - a ) ) ) ( *p ` J ) x ) ( ~=ph ` J ) .0. )
101 brinxp2 
 |-  ( ( ( a e. ( 0 [,] 1 ) |-> ( x ` ( 1 - a ) ) ) ( *p ` J ) x ) ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) .0. <-> ( ( ( ( a e. ( 0 [,] 1 ) |-> ( x ` ( 1 - a ) ) ) ( *p ` J ) x ) e. U. B /\ .0. e. U. B ) /\ ( ( a e. ( 0 [,] 1 ) |-> ( x ` ( 1 - a ) ) ) ( *p ` J ) x ) ( ~=ph ` J ) .0. ) )
102 93 72 100 101 syl21anbrc 
 |-  ( ( ph /\ x e. U. B ) -> ( ( a e. ( 0 [,] 1 ) |-> ( x ` ( 1 - a ) ) ) ( *p ` J ) x ) ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) .0. )
103 15 10 16 20 12 27 33 64 68 80 92 102 qusgrp2 
 |-  ( ph -> ( G e. Grp /\ [ .0. ] ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) = ( 0g ` G ) ) )
104 ecinxp 
 |-  ( ( ( ( ~=ph ` J ) " U. B ) C_ U. B /\ .0. e. U. B ) -> [ .0. ] ( ~=ph ` J ) = [ .0. ] ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) )
105 14 68 104 syl2anc 
 |-  ( ph -> [ .0. ] ( ~=ph ` J ) = [ .0. ] ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) )
106 105 eqeq1d 
 |-  ( ph -> ( [ .0. ] ( ~=ph ` J ) = ( 0g ` G ) <-> [ .0. ] ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) = ( 0g ` G ) ) )
107 106 anbi2d 
 |-  ( ph -> ( ( G e. Grp /\ [ .0. ] ( ~=ph ` J ) = ( 0g ` G ) ) <-> ( G e. Grp /\ [ .0. ] ( ( ~=ph ` J ) i^i ( U. B X. U. B ) ) = ( 0g ` G ) ) ) )
108 103 107 mpbird 
 |-  ( ph -> ( G e. Grp /\ [ .0. ] ( ~=ph ` J ) = ( 0g ` G ) ) )