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 φ U = F 𝑠 R
imasgrp.v φ V = Base R
imasgrp.p φ + ˙ = + R
imasgrp.f φ F : V onto B
imasgrp.e φ a V b V p V q V F a = F p F b = F q F a + ˙ b = F p + ˙ q
imasgrp2.r φ R W
imasgrp2.1 φ x V y V x + ˙ y V
imasgrp2.2 φ x V y V z V F x + ˙ y + ˙ z = F x + ˙ y + ˙ z
imasgrp2.3 φ 0 ˙ V
imasgrp2.4 φ x V F 0 ˙ + ˙ x = F x
imasgrp2.5 φ x V N V
imasgrp2.6 φ x V F N + ˙ x = F 0 ˙
Assertion imasgrp2 φ U Grp F 0 ˙ = 0 U

Proof

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