Metamath Proof Explorer

Theorem imasgrp2

Description: The image structure of a group is a group. (Contributed by Mario Carneiro, 24-Feb-2015) (Revised by Mario Carneiro, 5-Sep-2015)

Ref Expression
Hypotheses imasgrp.u 
|- ( ph -> U = ( F "s R ) )
imasgrp.v 
|- ( ph -> V = ( Base ` R ) )
imasgrp.p 
|- ( ph -> .+ = ( +g ` R ) )
imasgrp.f 
|- ( ph -> F : V -onto-> B )
imasgrp.e 
|- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .+ b ) ) = ( F ` ( p .+ q ) ) ) )
imasgrp2.r 
|- ( ph -> R e. W )
imasgrp2.1 
|- ( ( ph /\ x e. V /\ y e. V ) -> ( x .+ y ) e. V )
imasgrp2.2 
|- ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( F ` ( ( x .+ y ) .+ z ) ) = ( F ` ( x .+ ( y .+ z ) ) ) )
imasgrp2.3 
|- ( ph -> .0. e. V )
imasgrp2.4 
|- ( ( ph /\ x e. V ) -> ( F ` ( .0. .+ x ) ) = ( F ` x ) )
imasgrp2.5 
|- ( ( ph /\ x e. V ) -> N e. V )
imasgrp2.6 
|- ( ( ph /\ x e. V ) -> ( F ` ( N .+ x ) ) = ( F ` .0. ) )
Assertion imasgrp2 
|- ( ph -> ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) )

Proof

Step Hyp Ref Expression
1 imasgrp.u 
 |-  ( ph -> U = ( F "s R ) )
2 imasgrp.v 
 |-  ( ph -> V = ( Base ` R ) )
3 imasgrp.p 
 |-  ( ph -> .+ = ( +g ` R ) )
4 imasgrp.f 
 |-  ( ph -> F : V -onto-> B )
5 imasgrp.e 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .+ b ) ) = ( F ` ( p .+ q ) ) ) )
6 imasgrp2.r 
 |-  ( ph -> R e. W )
7 imasgrp2.1 
 |-  ( ( ph /\ x e. V /\ y e. V ) -> ( x .+ y ) e. V )
8 imasgrp2.2 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( F ` ( ( x .+ y ) .+ z ) ) = ( F ` ( x .+ ( y .+ z ) ) ) )
9 imasgrp2.3 
 |-  ( ph -> .0. e. V )
10 imasgrp2.4 
 |-  ( ( ph /\ x e. V ) -> ( F ` ( .0. .+ x ) ) = ( F ` x ) )
11 imasgrp2.5 
 |-  ( ( ph /\ x e. V ) -> N e. V )
12 imasgrp2.6 
 |-  ( ( ph /\ x e. V ) -> ( F ` ( N .+ x ) ) = ( F ` .0. ) )
13 1 2 4 6 imasbas 
 |-  ( ph -> B = ( Base ` U ) )
14 eqidd 
 |-  ( ph -> ( +g ` U ) = ( +g ` U ) )
15 3 oveqd 
 |-  ( ph -> ( a .+ b ) = ( a ( +g ` R ) b ) )
16 15 fveq2d 
 |-  ( ph -> ( F ` ( a .+ b ) ) = ( F ` ( a ( +g ` R ) b ) ) )
17 3 oveqd 
 |-  ( ph -> ( p .+ q ) = ( p ( +g ` R ) q ) )
18 17 fveq2d 
 |-  ( ph -> ( F ` ( p .+ q ) ) = ( F ` ( p ( +g ` R ) q ) ) )
19 16 18 eqeq12d 
 |-  ( ph -> ( ( F ` ( a .+ b ) ) = ( F ` ( p .+ q ) ) <-> ( F ` ( a ( +g ` R ) b ) ) = ( F ` ( p ( +g ` R ) q ) ) ) )
20 19 3ad2ant1 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( F ` ( a .+ b ) ) = ( F ` ( p .+ q ) ) <-> ( F ` ( a ( +g ` R ) b ) ) = ( F ` ( p ( +g ` R ) q ) ) ) )
21 5 20 sylibd 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a ( +g ` R ) b ) ) = ( F ` ( p ( +g ` R ) q ) ) ) )
22 eqid 
 |-  ( +g ` R ) = ( +g ` R )
23 eqid 
 |-  ( +g ` U ) = ( +g ` U )
24 17 adantr 
 |-  ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .+ q ) = ( p ( +g ` R ) q ) )
25 7 3expb 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> ( x .+ y ) e. V )
26 25 caovclg 
 |-  ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .+ q ) e. V )
27 24 26 eqeltrrd 
 |-  ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p ( +g ` R ) q ) e. V )
28 4 21 1 2 6 22 23 27 imasaddf 
 |-  ( ph -> ( +g ` U ) : ( B X. B ) --> B )
29 fovcdm 
 |-  ( ( ( +g ` U ) : ( B X. B ) --> B /\ u e. B /\ v e. B ) -> ( u ( +g ` U ) v ) e. B )
30 28 29 syl3an1 
 |-  ( ( ph /\ u e. B /\ v e. B ) -> ( u ( +g ` U ) v ) e. B )
31 forn 
 |-  ( F : V -onto-> B -> ran F = B )
32 4 31 syl 
 |-  ( ph -> ran F = B )
33 32 eleq2d 
 |-  ( ph -> ( u e. ran F <-> u e. B ) )
34 32 eleq2d 
 |-  ( ph -> ( v e. ran F <-> v e. B ) )
35 32 eleq2d 
 |-  ( ph -> ( w e. ran F <-> w e. B ) )
36 33 34 35 3anbi123d 
 |-  ( ph -> ( ( u e. ran F /\ v e. ran F /\ w e. ran F ) <-> ( u e. B /\ v e. B /\ w e. B ) ) )
37 fofn 
 |-  ( F : V -onto-> B -> F Fn V )
38 4 37 syl 
 |-  ( ph -> F Fn V )
39 fvelrnb 
 |-  ( F Fn V -> ( u e. ran F <-> E. x e. V ( F ` x ) = u ) )
40 fvelrnb 
 |-  ( F Fn V -> ( v e. ran F <-> E. y e. V ( F ` y ) = v ) )
41 fvelrnb 
 |-  ( F Fn V -> ( w e. ran F <-> E. z e. V ( F ` z ) = w ) )
42 39 40 41 3anbi123d 
 |-  ( F Fn V -> ( ( u e. ran F /\ v e. ran F /\ w e. ran F ) <-> ( E. x e. V ( F ` x ) = u /\ E. y e. V ( F ` y ) = v /\ E. z e. V ( F ` z ) = w ) ) )
43 38 42 syl 
 |-  ( ph -> ( ( u e. ran F /\ v e. ran F /\ w e. ran F ) <-> ( E. x e. V ( F ` x ) = u /\ E. y e. V ( F ` y ) = v /\ E. z e. V ( F ` z ) = w ) ) )
44 36 43 bitr3d 
 |-  ( ph -> ( ( u e. B /\ v e. B /\ w e. B ) <-> ( E. x e. V ( F ` x ) = u /\ E. y e. V ( F ` y ) = v /\ E. z e. V ( F ` z ) = w ) ) )
45 3reeanv 
 |-  ( E. x e. V E. y e. V E. z e. V ( ( F ` x ) = u /\ ( F ` y ) = v /\ ( F ` z ) = w ) <-> ( E. x e. V ( F ` x ) = u /\ E. y e. V ( F ` y ) = v /\ E. z e. V ( F ` z ) = w ) )
46 44 45 bitr4di 
 |-  ( ph -> ( ( u e. B /\ v e. B /\ w e. B ) <-> E. x e. V E. y e. V E. z e. V ( ( F ` x ) = u /\ ( F ` y ) = v /\ ( F ` z ) = w ) ) )
47 3 adantr 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> .+ = ( +g ` R ) )
48 47 oveqd 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( x .+ y ) .+ z ) = ( ( x .+ y ) ( +g ` R ) z ) )
49 48 fveq2d 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( F ` ( ( x .+ y ) .+ z ) ) = ( F ` ( ( x .+ y ) ( +g ` R ) z ) ) )
50 47 oveqd 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( x .+ ( y .+ z ) ) = ( x ( +g ` R ) ( y .+ z ) ) )
51 50 fveq2d 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( F ` ( x .+ ( y .+ z ) ) ) = ( F ` ( x ( +g ` R ) ( y .+ z ) ) ) )
52 8 49 51 3eqtr3d 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( F ` ( ( x .+ y ) ( +g ` R ) z ) ) = ( F ` ( x ( +g ` R ) ( y .+ z ) ) ) )
53 simpl 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ph )
54 7 3adant3r3 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( x .+ y ) e. V )
55 simpr3 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> z e. V )
56 4 21 1 2 6 22 23 imasaddval 
 |-  ( ( ph /\ ( x .+ y ) e. V /\ z e. V ) -> ( ( F ` ( x .+ y ) ) ( +g ` U ) ( F ` z ) ) = ( F ` ( ( x .+ y ) ( +g ` R ) z ) ) )
57 53 54 55 56 syl3anc 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( F ` ( x .+ y ) ) ( +g ` U ) ( F ` z ) ) = ( F ` ( ( x .+ y ) ( +g ` R ) z ) ) )
58 simpr1 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> x e. V )
59 26 caovclg 
 |-  ( ( ph /\ ( y e. V /\ z e. V ) ) -> ( y .+ z ) e. V )
60 59 3adantr1 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( y .+ z ) e. V )
61 4 21 1 2 6 22 23 imasaddval 
 |-  ( ( ph /\ x e. V /\ ( y .+ z ) e. V ) -> ( ( F ` x ) ( +g ` U ) ( F ` ( y .+ z ) ) ) = ( F ` ( x ( +g ` R ) ( y .+ z ) ) ) )
62 53 58 60 61 syl3anc 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( F ` x ) ( +g ` U ) ( F ` ( y .+ z ) ) ) = ( F ` ( x ( +g ` R ) ( y .+ z ) ) ) )
63 52 57 62 3eqtr4d 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( F ` ( x .+ y ) ) ( +g ` U ) ( F ` z ) ) = ( ( F ` x ) ( +g ` U ) ( F ` ( y .+ z ) ) ) )
64 4 21 1 2 6 22 23 imasaddval 
 |-  ( ( ph /\ x e. V /\ y e. V ) -> ( ( F ` x ) ( +g ` U ) ( F ` y ) ) = ( F ` ( x ( +g ` R ) y ) ) )
65 64 3adant3r3 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( F ` x ) ( +g ` U ) ( F ` y ) ) = ( F ` ( x ( +g ` R ) y ) ) )
66 47 oveqd 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( x .+ y ) = ( x ( +g ` R ) y ) )
67 66 fveq2d 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( F ` ( x .+ y ) ) = ( F ` ( x ( +g ` R ) y ) ) )
68 65 67 eqtr4d 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( F ` x ) ( +g ` U ) ( F ` y ) ) = ( F ` ( x .+ y ) ) )
69 68 oveq1d 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( ( F ` x ) ( +g ` U ) ( F ` y ) ) ( +g ` U ) ( F ` z ) ) = ( ( F ` ( x .+ y ) ) ( +g ` U ) ( F ` z ) ) )
70 4 21 1 2 6 22 23 imasaddval 
 |-  ( ( ph /\ y e. V /\ z e. V ) -> ( ( F ` y ) ( +g ` U ) ( F ` z ) ) = ( F ` ( y ( +g ` R ) z ) ) )
71 70 3adant3r1 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( F ` y ) ( +g ` U ) ( F ` z ) ) = ( F ` ( y ( +g ` R ) z ) ) )
72 47 oveqd 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( y .+ z ) = ( y ( +g ` R ) z ) )
73 72 fveq2d 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( F ` ( y .+ z ) ) = ( F ` ( y ( +g ` R ) z ) ) )
74 71 73 eqtr4d 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( F ` y ) ( +g ` U ) ( F ` z ) ) = ( F ` ( y .+ z ) ) )
75 74 oveq2d 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( F ` x ) ( +g ` U ) ( ( F ` y ) ( +g ` U ) ( F ` z ) ) ) = ( ( F ` x ) ( +g ` U ) ( F ` ( y .+ z ) ) ) )
76 63 69 75 3eqtr4d 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( ( F ` x ) ( +g ` U ) ( F ` y ) ) ( +g ` U ) ( F ` z ) ) = ( ( F ` x ) ( +g ` U ) ( ( F ` y ) ( +g ` U ) ( F ` z ) ) ) )
77 simp1 
 |-  ( ( ( F ` x ) = u /\ ( F ` y ) = v /\ ( F ` z ) = w ) -> ( F ` x ) = u )
78 simp2 
 |-  ( ( ( F ` x ) = u /\ ( F ` y ) = v /\ ( F ` z ) = w ) -> ( F ` y ) = v )
79 77 78 oveq12d 
 |-  ( ( ( F ` x ) = u /\ ( F ` y ) = v /\ ( F ` z ) = w ) -> ( ( F ` x ) ( +g ` U ) ( F ` y ) ) = ( u ( +g ` U ) v ) )
80 simp3 
 |-  ( ( ( F ` x ) = u /\ ( F ` y ) = v /\ ( F ` z ) = w ) -> ( F ` z ) = w )
81 79 80 oveq12d 
 |-  ( ( ( F ` x ) = u /\ ( F ` y ) = v /\ ( F ` z ) = w ) -> ( ( ( F ` x ) ( +g ` U ) ( F ` y ) ) ( +g ` U ) ( F ` z ) ) = ( ( u ( +g ` U ) v ) ( +g ` U ) w ) )
82 78 80 oveq12d 
 |-  ( ( ( F ` x ) = u /\ ( F ` y ) = v /\ ( F ` z ) = w ) -> ( ( F ` y ) ( +g ` U ) ( F ` z ) ) = ( v ( +g ` U ) w ) )
83 77 82 oveq12d 
 |-  ( ( ( F ` x ) = u /\ ( F ` y ) = v /\ ( F ` z ) = w ) -> ( ( F ` x ) ( +g ` U ) ( ( F ` y ) ( +g ` U ) ( F ` z ) ) ) = ( u ( +g ` U ) ( v ( +g ` U ) w ) ) )
84 81 83 eqeq12d 
 |-  ( ( ( F ` x ) = u /\ ( F ` y ) = v /\ ( F ` z ) = w ) -> ( ( ( ( F ` x ) ( +g ` U ) ( F ` y ) ) ( +g ` U ) ( F ` z ) ) = ( ( F ` x ) ( +g ` U ) ( ( F ` y ) ( +g ` U ) ( F ` z ) ) ) <-> ( ( u ( +g ` U ) v ) ( +g ` U ) w ) = ( u ( +g ` U ) ( v ( +g ` U ) w ) ) ) )
85 76 84 syl5ibcom 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( ( F ` x ) = u /\ ( F ` y ) = v /\ ( F ` z ) = w ) -> ( ( u ( +g ` U ) v ) ( +g ` U ) w ) = ( u ( +g ` U ) ( v ( +g ` U ) w ) ) ) )
86 85 3exp2 
 |-  ( ph -> ( x e. V -> ( y e. V -> ( z e. V -> ( ( ( F ` x ) = u /\ ( F ` y ) = v /\ ( F ` z ) = w ) -> ( ( u ( +g ` U ) v ) ( +g ` U ) w ) = ( u ( +g ` U ) ( v ( +g ` U ) w ) ) ) ) ) ) )
87 86 imp32 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> ( z e. V -> ( ( ( F ` x ) = u /\ ( F ` y ) = v /\ ( F ` z ) = w ) -> ( ( u ( +g ` U ) v ) ( +g ` U ) w ) = ( u ( +g ` U ) ( v ( +g ` U ) w ) ) ) ) )
88 87 rexlimdv 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> ( E. z e. V ( ( F ` x ) = u /\ ( F ` y ) = v /\ ( F ` z ) = w ) -> ( ( u ( +g ` U ) v ) ( +g ` U ) w ) = ( u ( +g ` U ) ( v ( +g ` U ) w ) ) ) )
89 88 rexlimdvva 
 |-  ( ph -> ( E. x e. V E. y e. V E. z e. V ( ( F ` x ) = u /\ ( F ` y ) = v /\ ( F ` z ) = w ) -> ( ( u ( +g ` U ) v ) ( +g ` U ) w ) = ( u ( +g ` U ) ( v ( +g ` U ) w ) ) ) )
90 46 89 sylbid 
 |-  ( ph -> ( ( u e. B /\ v e. B /\ w e. B ) -> ( ( u ( +g ` U ) v ) ( +g ` U ) w ) = ( u ( +g ` U ) ( v ( +g ` U ) w ) ) ) )
91 90 imp 
 |-  ( ( ph /\ ( u e. B /\ v e. B /\ w e. B ) ) -> ( ( u ( +g ` U ) v ) ( +g ` U ) w ) = ( u ( +g ` U ) ( v ( +g ` U ) w ) ) )
92 fof 
 |-  ( F : V -onto-> B -> F : V --> B )
93 4 92 syl 
 |-  ( ph -> F : V --> B )
94 93 9 ffvelcdmd 
 |-  ( ph -> ( F ` .0. ) e. B )
95 38 39 syl 
 |-  ( ph -> ( u e. ran F <-> E. x e. V ( F ` x ) = u ) )
96 33 95 bitr3d 
 |-  ( ph -> ( u e. B <-> E. x e. V ( F ` x ) = u ) )
97 simpl 
 |-  ( ( ph /\ x e. V ) -> ph )
98 9 adantr 
 |-  ( ( ph /\ x e. V ) -> .0. e. V )
99 simpr 
 |-  ( ( ph /\ x e. V ) -> x e. V )
100 4 21 1 2 6 22 23 imasaddval 
 |-  ( ( ph /\ .0. e. V /\ x e. V ) -> ( ( F ` .0. ) ( +g ` U ) ( F ` x ) ) = ( F ` ( .0. ( +g ` R ) x ) ) )
101 97 98 99 100 syl3anc 
 |-  ( ( ph /\ x e. V ) -> ( ( F ` .0. ) ( +g ` U ) ( F ` x ) ) = ( F ` ( .0. ( +g ` R ) x ) ) )
102 3 adantr 
 |-  ( ( ph /\ x e. V ) -> .+ = ( +g ` R ) )
103 102 oveqd 
 |-  ( ( ph /\ x e. V ) -> ( .0. .+ x ) = ( .0. ( +g ` R ) x ) )
104 103 fveq2d 
 |-  ( ( ph /\ x e. V ) -> ( F ` ( .0. .+ x ) ) = ( F ` ( .0. ( +g ` R ) x ) ) )
105 101 104 10 3eqtr2d 
 |-  ( ( ph /\ x e. V ) -> ( ( F ` .0. ) ( +g ` U ) ( F ` x ) ) = ( F ` x ) )
106 oveq2 
 |-  ( ( F ` x ) = u -> ( ( F ` .0. ) ( +g ` U ) ( F ` x ) ) = ( ( F ` .0. ) ( +g ` U ) u ) )
107 id 
 |-  ( ( F ` x ) = u -> ( F ` x ) = u )
108 106 107 eqeq12d 
 |-  ( ( F ` x ) = u -> ( ( ( F ` .0. ) ( +g ` U ) ( F ` x ) ) = ( F ` x ) <-> ( ( F ` .0. ) ( +g ` U ) u ) = u ) )
109 105 108 syl5ibcom 
 |-  ( ( ph /\ x e. V ) -> ( ( F ` x ) = u -> ( ( F ` .0. ) ( +g ` U ) u ) = u ) )
110 109 rexlimdva 
 |-  ( ph -> ( E. x e. V ( F ` x ) = u -> ( ( F ` .0. ) ( +g ` U ) u ) = u ) )
111 96 110 sylbid 
 |-  ( ph -> ( u e. B -> ( ( F ` .0. ) ( +g ` U ) u ) = u ) )
112 111 imp 
 |-  ( ( ph /\ u e. B ) -> ( ( F ` .0. ) ( +g ` U ) u ) = u )
113 93 adantr 
 |-  ( ( ph /\ x e. V ) -> F : V --> B )
114 113 11 ffvelcdmd 
 |-  ( ( ph /\ x e. V ) -> ( F ` N ) e. B )
115 4 21 1 2 6 22 23 imasaddval 
 |-  ( ( ph /\ N e. V /\ x e. V ) -> ( ( F ` N ) ( +g ` U ) ( F ` x ) ) = ( F ` ( N ( +g ` R ) x ) ) )
116 97 11 99 115 syl3anc 
 |-  ( ( ph /\ x e. V ) -> ( ( F ` N ) ( +g ` U ) ( F ` x ) ) = ( F ` ( N ( +g ` R ) x ) ) )
117 102 oveqd 
 |-  ( ( ph /\ x e. V ) -> ( N .+ x ) = ( N ( +g ` R ) x ) )
118 117 fveq2d 
 |-  ( ( ph /\ x e. V ) -> ( F ` ( N .+ x ) ) = ( F ` ( N ( +g ` R ) x ) ) )
119 116 118 12 3eqtr2d 
 |-  ( ( ph /\ x e. V ) -> ( ( F ` N ) ( +g ` U ) ( F ` x ) ) = ( F ` .0. ) )
120 oveq1 
 |-  ( v = ( F ` N ) -> ( v ( +g ` U ) ( F ` x ) ) = ( ( F ` N ) ( +g ` U ) ( F ` x ) ) )
121 120 eqeq1d 
 |-  ( v = ( F ` N ) -> ( ( v ( +g ` U ) ( F ` x ) ) = ( F ` .0. ) <-> ( ( F ` N ) ( +g ` U ) ( F ` x ) ) = ( F ` .0. ) ) )
122 121 rspcev 
 |-  ( ( ( F ` N ) e. B /\ ( ( F ` N ) ( +g ` U ) ( F ` x ) ) = ( F ` .0. ) ) -> E. v e. B ( v ( +g ` U ) ( F ` x ) ) = ( F ` .0. ) )
123 114 119 122 syl2anc 
 |-  ( ( ph /\ x e. V ) -> E. v e. B ( v ( +g ` U ) ( F ` x ) ) = ( F ` .0. ) )
124 oveq2 
 |-  ( ( F ` x ) = u -> ( v ( +g ` U ) ( F ` x ) ) = ( v ( +g ` U ) u ) )
125 124 eqeq1d 
 |-  ( ( F ` x ) = u -> ( ( v ( +g ` U ) ( F ` x ) ) = ( F ` .0. ) <-> ( v ( +g ` U ) u ) = ( F ` .0. ) ) )
126 125 rexbidv 
 |-  ( ( F ` x ) = u -> ( E. v e. B ( v ( +g ` U ) ( F ` x ) ) = ( F ` .0. ) <-> E. v e. B ( v ( +g ` U ) u ) = ( F ` .0. ) ) )
127 123 126 syl5ibcom 
 |-  ( ( ph /\ x e. V ) -> ( ( F ` x ) = u -> E. v e. B ( v ( +g ` U ) u ) = ( F ` .0. ) ) )
128 127 rexlimdva 
 |-  ( ph -> ( E. x e. V ( F ` x ) = u -> E. v e. B ( v ( +g ` U ) u ) = ( F ` .0. ) ) )
129 96 128 sylbid 
 |-  ( ph -> ( u e. B -> E. v e. B ( v ( +g ` U ) u ) = ( F ` .0. ) ) )
130 129 imp 
 |-  ( ( ph /\ u e. B ) -> E. v e. B ( v ( +g ` U ) u ) = ( F ` .0. ) )
131 13 14 30 91 94 112 130 isgrpde 
 |-  ( ph -> U e. Grp )
132 13 14 94 112 131 grpidd2 
 |-  ( ph -> ( F ` .0. ) = ( 0g ` U ) )
133 131 132 jca 
 |-  ( ph -> ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) )