Metamath Proof Explorer

Theorem imasgrp

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 ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
imasgrp.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
imasgrp.p ⊢ ( 𝜑 → + = ( +g ‘ 𝑅 ) )
imasgrp.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
imasgrp.e ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) ) )
imasgrp.r ⊢ ( 𝜑 → 𝑅 ∈ Grp )
imasgrp.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion imasgrp ( 𝜑 → ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 imasgrp.u ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
2 imasgrp.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3 imasgrp.p ⊢ ( 𝜑 → + = ( +g ‘ 𝑅 ) )
4 imasgrp.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
5 imasgrp.e ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) ) )
6 imasgrp.r ⊢ ( 𝜑 → 𝑅 ∈ Grp )
7 imasgrp.z ⊢ 0 = ( 0g ‘ 𝑅 )
8 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → 𝑅 ∈ Grp )
9 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → 𝑥 ∈ 𝑉 )
10 2 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → 𝑉 = ( Base ‘ 𝑅 ) )
11 9 10 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
12 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → 𝑦 ∈ 𝑉 )
13 12 10 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
14 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
15 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
16 14 15 grpcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
17 8 11 13 16 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
18 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → + = ( +g ‘ 𝑅 ) )
19 18 oveqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑥 + 𝑦 ) = ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) )
20 17 19 10 3eltr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑥 + 𝑦 ) ∈ 𝑉 )
21 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑅 ∈ Grp )
22 11 3adant3r3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
23 13 3adant3r3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
24 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑧 ∈ 𝑉 )
25 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑉 = ( Base ‘ 𝑅 ) )
26 24 25 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑧 ∈ ( Base ‘ 𝑅 ) )
27 14 15 grpass ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ( +g ‘ 𝑅 ) 𝑧 ) = ( 𝑥 ( +g ‘ 𝑅 ) ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) )
28 21 22 23 26 27 syl13anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ( +g ‘ 𝑅 ) 𝑧 ) = ( 𝑥 ( +g ‘ 𝑅 ) ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) )
29 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → + = ( +g ‘ 𝑅 ) )
30 19 3adant3r3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) )
31 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑧 = 𝑧 )
32 29 30 31 oveq123d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ( +g ‘ 𝑅 ) 𝑧 ) )
33 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑥 = 𝑥 )
34 29 oveqd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑦 + 𝑧 ) = ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) )
35 29 33 34 oveq123d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑥 + ( 𝑦 + 𝑧 ) ) = ( 𝑥 ( +g ‘ 𝑅 ) ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) )
36 28 32 35 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
37 36 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝐹 ‘ ( ( 𝑥 + 𝑦 ) + 𝑧 ) ) = ( 𝐹 ‘ ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) )
38 14 7 grpidcl ⊢ ( 𝑅 ∈ Grp → 0 ∈ ( Base ‘ 𝑅 ) )
39 6 38 syl ⊢ ( 𝜑 → 0 ∈ ( Base ‘ 𝑅 ) )
40 39 2 eleqtrrd ⊢ ( 𝜑 → 0 ∈ 𝑉 )
41 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → + = ( +g ‘ 𝑅 ) )
42 41 oveqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 0 + 𝑥 ) = ( 0 ( +g ‘ 𝑅 ) 𝑥 ) )
43 2 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑉 ↔ 𝑥 ∈ ( Base ‘ 𝑅 ) ) )
44 43 biimpa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
45 14 15 7 grplid ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 0 ( +g ‘ 𝑅 ) 𝑥 ) = 𝑥 )
46 6 44 45 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 0 ( +g ‘ 𝑅 ) 𝑥 ) = 𝑥 )
47 42 46 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 0 + 𝑥 ) = 𝑥 )
48 47 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐹 ‘ ( 0 + 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
49 eqid ⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 )
50 14 49 grpinvcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
51 6 44 50 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
52 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 𝑉 = ( Base ‘ 𝑅 ) )
53 51 52 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝑉 )
54 41 oveqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) + 𝑥 ) = ( ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) ( +g ‘ 𝑅 ) 𝑥 ) )
55 14 15 7 49 grplinv ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) ( +g ‘ 𝑅 ) 𝑥 ) = 0 )
56 6 44 55 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) ( +g ‘ 𝑅 ) 𝑥 ) = 0 )
57 54 56 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) + 𝑥 ) = 0 )
58 57 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐹 ‘ ( ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) + 𝑥 ) ) = ( 𝐹 ‘ 0 ) )
59 1 2 3 4 5 6 20 37 40 48 53 58 imasgrp2 ⊢ ( 𝜑 → ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) )