Metamath Proof Explorer

Theorem pi1xfrcnvlem

Description: Given a path F between two basepoints, there is an induced group homomorphism on the fundamental groups. (Contributed by Mario Carneiro, 12-Feb-2015) (Proof shortened by Mario Carneiro, 23-Dec-2016)

Ref Expression
Hypotheses pi1xfr.p 
|- P = ( J pi1 ( F ` 0 ) )
pi1xfr.q 
|- Q = ( J pi1 ( F ` 1 ) )
pi1xfr.b 
|- B = ( Base ` P )
pi1xfr.g 
|- G = ran ( g e. U. B |-> <. [ g ] ( ~=ph ` J ) , [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) >. )
pi1xfr.j 
|- ( ph -> J e. ( TopOn ` X ) )
pi1xfr.f 
|- ( ph -> F e. ( II Cn J ) )
pi1xfr.i 
|- I = ( x e. ( 0 [,] 1 ) |-> ( F ` ( 1 - x ) ) )
pi1xfrcnv.h 
|- H = ran ( h e. U. ( Base ` Q ) |-> <. [ h ] ( ~=ph ` J ) , [ ( F ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. )
Assertion pi1xfrcnvlem 
|- ( ph -> `' G C_ H )

Proof

Step Hyp Ref Expression
1 pi1xfr.p 
 |-  P = ( J pi1 ( F ` 0 ) )
2 pi1xfr.q 
 |-  Q = ( J pi1 ( F ` 1 ) )
3 pi1xfr.b 
 |-  B = ( Base ` P )
4 pi1xfr.g 
 |-  G = ran ( g e. U. B |-> <. [ g ] ( ~=ph ` J ) , [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) >. )
5 pi1xfr.j 
 |-  ( ph -> J e. ( TopOn ` X ) )
6 pi1xfr.f 
 |-  ( ph -> F e. ( II Cn J ) )
7 pi1xfr.i 
 |-  I = ( x e. ( 0 [,] 1 ) |-> ( F ` ( 1 - x ) ) )
8 pi1xfrcnv.h 
 |-  H = ran ( h e. U. ( Base ` Q ) |-> <. [ h ] ( ~=ph ` J ) , [ ( F ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. )
9 fvex 
 |-  ( ~=ph ` J ) e. _V
10 ecexg 
 |-  ( ( ~=ph ` J ) e. _V -> [ g ] ( ~=ph ` J ) e. _V )
11 9 10 mp1i 
 |-  ( ( ph /\ g e. U. B ) -> [ g ] ( ~=ph ` J ) e. _V )
12 ecexg 
 |-  ( ( ~=ph ` J ) e. _V -> [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) e. _V )
13 9 12 mp1i 
 |-  ( ( ph /\ g e. U. B ) -> [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) e. _V )
14 4 11 13 fliftcnv 
 |-  ( ph -> `' G = ran ( g e. U. B |-> <. [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) , [ g ] ( ~=ph ` J ) >. ) )
15 7 pcorevcl 
 |-  ( F e. ( II Cn J ) -> ( I e. ( II Cn J ) /\ ( I ` 0 ) = ( F ` 1 ) /\ ( I ` 1 ) = ( F ` 0 ) ) )
16 6 15 syl 
 |-  ( ph -> ( I e. ( II Cn J ) /\ ( I ` 0 ) = ( F ` 1 ) /\ ( I ` 1 ) = ( F ` 0 ) ) )
17 16 simp1d 
 |-  ( ph -> I e. ( II Cn J ) )
18 17 adantr 
 |-  ( ( ph /\ g e. U. B ) -> I e. ( II Cn J ) )
19 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
20 cnf2 
 |-  ( ( II e. ( TopOn ` ( 0 [,] 1 ) ) /\ J e. ( TopOn ` X ) /\ F e. ( II Cn J ) ) -> F : ( 0 [,] 1 ) --> X )
21 19 5 6 20 mp3an2i 
 |-  ( ph -> F : ( 0 [,] 1 ) --> X )
22 0elunit 
 |-  0 e. ( 0 [,] 1 )
23 ffvelrn 
 |-  ( ( F : ( 0 [,] 1 ) --> X /\ 0 e. ( 0 [,] 1 ) ) -> ( F ` 0 ) e. X )
24 21 22 23 sylancl 
 |-  ( ph -> ( F ` 0 ) e. X )
25 3 a1i 
 |-  ( ph -> B = ( Base ` P ) )
26 1 5 24 25 pi1eluni 
 |-  ( ph -> ( g e. U. B <-> ( g e. ( II Cn J ) /\ ( g ` 0 ) = ( F ` 0 ) /\ ( g ` 1 ) = ( F ` 0 ) ) ) )
27 26 biimpa 
 |-  ( ( ph /\ g e. U. B ) -> ( g e. ( II Cn J ) /\ ( g ` 0 ) = ( F ` 0 ) /\ ( g ` 1 ) = ( F ` 0 ) ) )
28 27 simp1d 
 |-  ( ( ph /\ g e. U. B ) -> g e. ( II Cn J ) )
29 6 adantr 
 |-  ( ( ph /\ g e. U. B ) -> F e. ( II Cn J ) )
30 27 simp3d 
 |-  ( ( ph /\ g e. U. B ) -> ( g ` 1 ) = ( F ` 0 ) )
31 28 29 30 pcocn 
 |-  ( ( ph /\ g e. U. B ) -> ( g ( *p ` J ) F ) e. ( II Cn J ) )
32 16 simp3d 
 |-  ( ph -> ( I ` 1 ) = ( F ` 0 ) )
33 32 adantr 
 |-  ( ( ph /\ g e. U. B ) -> ( I ` 1 ) = ( F ` 0 ) )
34 27 simp2d 
 |-  ( ( ph /\ g e. U. B ) -> ( g ` 0 ) = ( F ` 0 ) )
35 33 34 eqtr4d 
 |-  ( ( ph /\ g e. U. B ) -> ( I ` 1 ) = ( g ` 0 ) )
36 28 29 pco0 
 |-  ( ( ph /\ g e. U. B ) -> ( ( g ( *p ` J ) F ) ` 0 ) = ( g ` 0 ) )
37 35 36 eqtr4d 
 |-  ( ( ph /\ g e. U. B ) -> ( I ` 1 ) = ( ( g ( *p ` J ) F ) ` 0 ) )
38 18 31 37 pcocn 
 |-  ( ( ph /\ g e. U. B ) -> ( I ( *p ` J ) ( g ( *p ` J ) F ) ) e. ( II Cn J ) )
39 18 31 pco0 
 |-  ( ( ph /\ g e. U. B ) -> ( ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ` 0 ) = ( I ` 0 ) )
40 16 simp2d 
 |-  ( ph -> ( I ` 0 ) = ( F ` 1 ) )
41 40 adantr 
 |-  ( ( ph /\ g e. U. B ) -> ( I ` 0 ) = ( F ` 1 ) )
42 39 41 eqtrd 
 |-  ( ( ph /\ g e. U. B ) -> ( ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ` 0 ) = ( F ` 1 ) )
43 18 31 pco1 
 |-  ( ( ph /\ g e. U. B ) -> ( ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ` 1 ) = ( ( g ( *p ` J ) F ) ` 1 ) )
44 28 29 pco1 
 |-  ( ( ph /\ g e. U. B ) -> ( ( g ( *p ` J ) F ) ` 1 ) = ( F ` 1 ) )
45 43 44 eqtrd 
 |-  ( ( ph /\ g e. U. B ) -> ( ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ` 1 ) = ( F ` 1 ) )
46 1elunit 
 |-  1 e. ( 0 [,] 1 )
47 ffvelrn 
 |-  ( ( F : ( 0 [,] 1 ) --> X /\ 1 e. ( 0 [,] 1 ) ) -> ( F ` 1 ) e. X )
48 21 46 47 sylancl 
 |-  ( ph -> ( F ` 1 ) e. X )
49 eqidd 
 |-  ( ph -> ( Base ` Q ) = ( Base ` Q ) )
50 2 5 48 49 pi1eluni 
 |-  ( ph -> ( ( I ( *p ` J ) ( g ( *p ` J ) F ) ) e. U. ( Base ` Q ) <-> ( ( I ( *p ` J ) ( g ( *p ` J ) F ) ) e. ( II Cn J ) /\ ( ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ` 0 ) = ( F ` 1 ) /\ ( ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ` 1 ) = ( F ` 1 ) ) ) )
51 50 adantr 
 |-  ( ( ph /\ g e. U. B ) -> ( ( I ( *p ` J ) ( g ( *p ` J ) F ) ) e. U. ( Base ` Q ) <-> ( ( I ( *p ` J ) ( g ( *p ` J ) F ) ) e. ( II Cn J ) /\ ( ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ` 0 ) = ( F ` 1 ) /\ ( ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ` 1 ) = ( F ` 1 ) ) ) )
52 38 42 45 51 mpbir3and 
 |-  ( ( ph /\ g e. U. B ) -> ( I ( *p ` J ) ( g ( *p ` J ) F ) ) e. U. ( Base ` Q ) )
53 eqidd 
 |-  ( ph -> ( g e. U. B |-> ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ) = ( g e. U. B |-> ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ) )
54 eqidd 
 |-  ( ph -> ( h e. U. ( Base ` Q ) |-> <. [ h ] ( ~=ph ` J ) , [ ( F ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. ) = ( h e. U. ( Base ` Q ) |-> <. [ h ] ( ~=ph ` J ) , [ ( F ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. ) )
55 eceq1 
 |-  ( h = ( I ( *p ` J ) ( g ( *p ` J ) F ) ) -> [ h ] ( ~=ph ` J ) = [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) )
56 oveq1 
 |-  ( h = ( I ( *p ` J ) ( g ( *p ` J ) F ) ) -> ( h ( *p ` J ) I ) = ( ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ( *p ` J ) I ) )
57 56 oveq2d 
 |-  ( h = ( I ( *p ` J ) ( g ( *p ` J ) F ) ) -> ( F ( *p ` J ) ( h ( *p ` J ) I ) ) = ( F ( *p ` J ) ( ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ( *p ` J ) I ) ) )
58 57 eceq1d 
 |-  ( h = ( I ( *p ` J ) ( g ( *p ` J ) F ) ) -> [ ( F ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) = [ ( F ( *p ` J ) ( ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ( *p ` J ) I ) ) ] ( ~=ph ` J ) )
59 55 58 opeq12d 
 |-  ( h = ( I ( *p ` J ) ( g ( *p ` J ) F ) ) -> <. [ h ] ( ~=ph ` J ) , [ ( F ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. = <. [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) , [ ( F ( *p ` J ) ( ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. )
60 52 53 54 59 fmptco 
 |-  ( ph -> ( ( h e. U. ( Base ` Q ) |-> <. [ h ] ( ~=ph ` J ) , [ ( F ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. ) o. ( g e. U. B |-> ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ) ) = ( g e. U. B |-> <. [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) , [ ( F ( *p ` J ) ( ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. ) )
61 phtpcer 
 |-  ( ~=ph ` J ) Er ( II Cn J )
62 61 a1i 
 |-  ( ( ph /\ g e. U. B ) -> ( ~=ph ` J ) Er ( II Cn J ) )
63 18 28 pco0 
 |-  ( ( ph /\ g e. U. B ) -> ( ( I ( *p ` J ) g ) ` 0 ) = ( I ` 0 ) )
64 63 41 eqtr2d 
 |-  ( ( ph /\ g e. U. B ) -> ( F ` 1 ) = ( ( I ( *p ` J ) g ) ` 0 ) )
65 62 29 erref 
 |-  ( ( ph /\ g e. U. B ) -> F ( ~=ph ` J ) F )
66 62 18 erref 
 |-  ( ( ph /\ g e. U. B ) -> I ( ~=ph ` J ) I )
67 eqid 
 |-  ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) = ( ( 0 [,] 1 ) X. { ( F ` 0 ) } )
68 67 pcopt2 
 |-  ( ( g e. ( II Cn J ) /\ ( g ` 1 ) = ( F ` 0 ) ) -> ( g ( *p ` J ) ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) ) ( ~=ph ` J ) g )
69 28 30 68 syl2anc 
 |-  ( ( ph /\ g e. U. B ) -> ( g ( *p ` J ) ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) ) ( ~=ph ` J ) g )
70 41 eqcomd 
 |-  ( ( ph /\ g e. U. B ) -> ( F ` 1 ) = ( I ` 0 ) )
71 eqid 
 |-  ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) ) = ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) )
72 28 29 18 30 70 71 pcoass 
 |-  ( ( ph /\ g e. U. B ) -> ( ( g ( *p ` J ) F ) ( *p ` J ) I ) ( ~=ph ` J ) ( g ( *p ` J ) ( F ( *p ` J ) I ) ) )
73 29 18 pco0 
 |-  ( ( ph /\ g e. U. B ) -> ( ( F ( *p ` J ) I ) ` 0 ) = ( F ` 0 ) )
74 30 73 eqtr4d 
 |-  ( ( ph /\ g e. U. B ) -> ( g ` 1 ) = ( ( F ( *p ` J ) I ) ` 0 ) )
75 62 28 erref 
 |-  ( ( ph /\ g e. U. B ) -> g ( ~=ph ` J ) g )
76 7 67 pcorev2 
 |-  ( F e. ( II Cn J ) -> ( F ( *p ` J ) I ) ( ~=ph ` J ) ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) )
77 29 76 syl 
 |-  ( ( ph /\ g e. U. B ) -> ( F ( *p ` J ) I ) ( ~=ph ` J ) ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) )
78 74 75 77 pcohtpy 
 |-  ( ( ph /\ g e. U. B ) -> ( g ( *p ` J ) ( F ( *p ` J ) I ) ) ( ~=ph ` J ) ( g ( *p ` J ) ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) ) )
79 62 72 78 ertr2d 
 |-  ( ( ph /\ g e. U. B ) -> ( g ( *p ` J ) ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) ) ( ~=ph ` J ) ( ( g ( *p ` J ) F ) ( *p ` J ) I ) )
80 62 69 79 ertr3d 
 |-  ( ( ph /\ g e. U. B ) -> g ( ~=ph ` J ) ( ( g ( *p ` J ) F ) ( *p ` J ) I ) )
81 35 66 80 pcohtpy 
 |-  ( ( ph /\ g e. U. B ) -> ( I ( *p ` J ) g ) ( ~=ph ` J ) ( I ( *p ` J ) ( ( g ( *p ` J ) F ) ( *p ` J ) I ) ) )
82 44 41 eqtr4d 
 |-  ( ( ph /\ g e. U. B ) -> ( ( g ( *p ` J ) F ) ` 1 ) = ( I ` 0 ) )
83 18 31 18 37 82 71 pcoass 
 |-  ( ( ph /\ g e. U. B ) -> ( ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ( *p ` J ) I ) ( ~=ph ` J ) ( I ( *p ` J ) ( ( g ( *p ` J ) F ) ( *p ` J ) I ) ) )
84 62 81 83 ertr4d 
 |-  ( ( ph /\ g e. U. B ) -> ( I ( *p ` J ) g ) ( ~=ph ` J ) ( ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ( *p ` J ) I ) )
85 64 65 84 pcohtpy 
 |-  ( ( ph /\ g e. U. B ) -> ( F ( *p ` J ) ( I ( *p ` J ) g ) ) ( ~=ph ` J ) ( F ( *p ` J ) ( ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ( *p ` J ) I ) ) )
86 29 18 28 70 35 71 pcoass 
 |-  ( ( ph /\ g e. U. B ) -> ( ( F ( *p ` J ) I ) ( *p ` J ) g ) ( ~=ph ` J ) ( F ( *p ` J ) ( I ( *p ` J ) g ) ) )
87 29 18 pco1 
 |-  ( ( ph /\ g e. U. B ) -> ( ( F ( *p ` J ) I ) ` 1 ) = ( I ` 1 ) )
88 87 35 eqtrd 
 |-  ( ( ph /\ g e. U. B ) -> ( ( F ( *p ` J ) I ) ` 1 ) = ( g ` 0 ) )
89 88 77 75 pcohtpy 
 |-  ( ( ph /\ g e. U. B ) -> ( ( F ( *p ` J ) I ) ( *p ` J ) g ) ( ~=ph ` J ) ( ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) ( *p ` J ) g ) )
90 67 pcopt 
 |-  ( ( g e. ( II Cn J ) /\ ( g ` 0 ) = ( F ` 0 ) ) -> ( ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) ( *p ` J ) g ) ( ~=ph ` J ) g )
91 28 34 90 syl2anc 
 |-  ( ( ph /\ g e. U. B ) -> ( ( ( 0 [,] 1 ) X. { ( F ` 0 ) } ) ( *p ` J ) g ) ( ~=ph ` J ) g )
92 62 89 91 ertrd 
 |-  ( ( ph /\ g e. U. B ) -> ( ( F ( *p ` J ) I ) ( *p ` J ) g ) ( ~=ph ` J ) g )
93 62 86 92 ertr3d 
 |-  ( ( ph /\ g e. U. B ) -> ( F ( *p ` J ) ( I ( *p ` J ) g ) ) ( ~=ph ` J ) g )
94 62 85 93 ertr3d 
 |-  ( ( ph /\ g e. U. B ) -> ( F ( *p ` J ) ( ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ( *p ` J ) I ) ) ( ~=ph ` J ) g )
95 62 94 erthi 
 |-  ( ( ph /\ g e. U. B ) -> [ ( F ( *p ` J ) ( ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ( *p ` J ) I ) ) ] ( ~=ph ` J ) = [ g ] ( ~=ph ` J ) )
96 95 opeq2d 
 |-  ( ( ph /\ g e. U. B ) -> <. [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) , [ ( F ( *p ` J ) ( ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. = <. [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) , [ g ] ( ~=ph ` J ) >. )
97 96 mpteq2dva 
 |-  ( ph -> ( g e. U. B |-> <. [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) , [ ( F ( *p ` J ) ( ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. ) = ( g e. U. B |-> <. [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) , [ g ] ( ~=ph ` J ) >. ) )
98 60 97 eqtrd 
 |-  ( ph -> ( ( h e. U. ( Base ` Q ) |-> <. [ h ] ( ~=ph ` J ) , [ ( F ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. ) o. ( g e. U. B |-> ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ) ) = ( g e. U. B |-> <. [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) , [ g ] ( ~=ph ` J ) >. ) )
99 98 rneqd 
 |-  ( ph -> ran ( ( h e. U. ( Base ` Q ) |-> <. [ h ] ( ~=ph ` J ) , [ ( F ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. ) o. ( g e. U. B |-> ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ) ) = ran ( g e. U. B |-> <. [ ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ] ( ~=ph ` J ) , [ g ] ( ~=ph ` J ) >. ) )
100 14 99 eqtr4d 
 |-  ( ph -> `' G = ran ( ( h e. U. ( Base ` Q ) |-> <. [ h ] ( ~=ph ` J ) , [ ( F ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. ) o. ( g e. U. B |-> ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ) ) )
101 rncoss 
 |-  ran ( ( h e. U. ( Base ` Q ) |-> <. [ h ] ( ~=ph ` J ) , [ ( F ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. ) o. ( g e. U. B |-> ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ) ) C_ ran ( h e. U. ( Base ` Q ) |-> <. [ h ] ( ~=ph ` J ) , [ ( F ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. )
102 101 8 sseqtrri 
 |-  ran ( ( h e. U. ( Base ` Q ) |-> <. [ h ] ( ~=ph ` J ) , [ ( F ( *p ` J ) ( h ( *p ` J ) I ) ) ] ( ~=ph ` J ) >. ) o. ( g e. U. B |-> ( I ( *p ` J ) ( g ( *p ` J ) F ) ) ) ) C_ H
103 100 102 eqsstrdi 
 |-  ( ph -> `' G C_ H )