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 ( 𝜑𝑈 = ( 𝐹s 𝑅 ) )
imasgrp.v ( 𝜑𝑉 = ( Base ‘ 𝑅 ) )
imasgrp.p ( 𝜑+ = ( +g𝑅 ) )
imasgrp.f ( 𝜑𝐹 : 𝑉onto𝐵 )
imasgrp.e ( ( 𝜑 ∧ ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑝𝑉𝑞𝑉 ) ) → ( ( ( 𝐹𝑎 ) = ( 𝐹𝑝 ) ∧ ( 𝐹𝑏 ) = ( 𝐹𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) ) )
imasgrp2.r ( 𝜑𝑅𝑊 )
imasgrp2.1 ( ( 𝜑𝑥𝑉𝑦𝑉 ) → ( 𝑥 + 𝑦 ) ∈ 𝑉 )
imasgrp2.2 ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( 𝐹 ‘ ( ( 𝑥 + 𝑦 ) + 𝑧 ) ) = ( 𝐹 ‘ ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) )
imasgrp2.3 ( 𝜑0𝑉 )
imasgrp2.4 ( ( 𝜑𝑥𝑉 ) → ( 𝐹 ‘ ( 0 + 𝑥 ) ) = ( 𝐹𝑥 ) )
imasgrp2.5 ( ( 𝜑𝑥𝑉 ) → 𝑁𝑉 )
imasgrp2.6 ( ( 𝜑𝑥𝑉 ) → ( 𝐹 ‘ ( 𝑁 + 𝑥 ) ) = ( 𝐹0 ) )
Assertion imasgrp2 ( 𝜑 → ( 𝑈 ∈ 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 imasgrp2.r ( 𝜑𝑅𝑊 )
7 imasgrp2.1 ( ( 𝜑𝑥𝑉𝑦𝑉 ) → ( 𝑥 + 𝑦 ) ∈ 𝑉 )
8 imasgrp2.2 ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( 𝐹 ‘ ( ( 𝑥 + 𝑦 ) + 𝑧 ) ) = ( 𝐹 ‘ ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) )
9 imasgrp2.3 ( 𝜑0𝑉 )
10 imasgrp2.4 ( ( 𝜑𝑥𝑉 ) → ( 𝐹 ‘ ( 0 + 𝑥 ) ) = ( 𝐹𝑥 ) )
11 imasgrp2.5 ( ( 𝜑𝑥𝑉 ) → 𝑁𝑉 )
12 imasgrp2.6 ( ( 𝜑𝑥𝑉 ) → ( 𝐹 ‘ ( 𝑁 + 𝑥 ) ) = ( 𝐹0 ) )
13 1 2 4 6 imasbas ( 𝜑𝐵 = ( Base ‘ 𝑈 ) )
14 eqidd ( 𝜑 → ( +g𝑈 ) = ( +g𝑈 ) )
15 3 oveqd ( 𝜑 → ( 𝑎 + 𝑏 ) = ( 𝑎 ( +g𝑅 ) 𝑏 ) )
16 15 fveq2d ( 𝜑 → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑎 ( +g𝑅 ) 𝑏 ) ) )
17 3 oveqd ( 𝜑 → ( 𝑝 + 𝑞 ) = ( 𝑝 ( +g𝑅 ) 𝑞 ) )
18 17 fveq2d ( 𝜑 → ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) = ( 𝐹 ‘ ( 𝑝 ( +g𝑅 ) 𝑞 ) ) )
19 16 18 eqeq12d ( 𝜑 → ( ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) ↔ ( 𝐹 ‘ ( 𝑎 ( +g𝑅 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 ( +g𝑅 ) 𝑞 ) ) ) )
20 19 3ad2ant1 ( ( 𝜑 ∧ ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑝𝑉𝑞𝑉 ) ) → ( ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) ↔ ( 𝐹 ‘ ( 𝑎 ( +g𝑅 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 ( +g𝑅 ) 𝑞 ) ) ) )
21 5 20 sylibd ( ( 𝜑 ∧ ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑝𝑉𝑞𝑉 ) ) → ( ( ( 𝐹𝑎 ) = ( 𝐹𝑝 ) ∧ ( 𝐹𝑏 ) = ( 𝐹𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g𝑅 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 ( +g𝑅 ) 𝑞 ) ) ) )
22 eqid ( +g𝑅 ) = ( +g𝑅 )
23 eqid ( +g𝑈 ) = ( +g𝑈 )
24 17 adantr ( ( 𝜑 ∧ ( 𝑝𝑉𝑞𝑉 ) ) → ( 𝑝 + 𝑞 ) = ( 𝑝 ( +g𝑅 ) 𝑞 ) )
25 7 3expb ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑉 )
26 25 caovclg ( ( 𝜑 ∧ ( 𝑝𝑉𝑞𝑉 ) ) → ( 𝑝 + 𝑞 ) ∈ 𝑉 )
27 24 26 eqeltrrd ( ( 𝜑 ∧ ( 𝑝𝑉𝑞𝑉 ) ) → ( 𝑝 ( +g𝑅 ) 𝑞 ) ∈ 𝑉 )
28 4 21 1 2 6 22 23 27 imasaddf ( 𝜑 → ( +g𝑈 ) : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )
29 fovrn ( ( ( +g𝑈 ) : ( 𝐵 × 𝐵 ) ⟶ 𝐵𝑢𝐵𝑣𝐵 ) → ( 𝑢 ( +g𝑈 ) 𝑣 ) ∈ 𝐵 )
30 28 29 syl3an1 ( ( 𝜑𝑢𝐵𝑣𝐵 ) → ( 𝑢 ( +g𝑈 ) 𝑣 ) ∈ 𝐵 )
31 forn ( 𝐹 : 𝑉onto𝐵 → ran 𝐹 = 𝐵 )
32 4 31 syl ( 𝜑 → ran 𝐹 = 𝐵 )
33 32 eleq2d ( 𝜑 → ( 𝑢 ∈ ran 𝐹𝑢𝐵 ) )
34 32 eleq2d ( 𝜑 → ( 𝑣 ∈ ran 𝐹𝑣𝐵 ) )
35 32 eleq2d ( 𝜑 → ( 𝑤 ∈ ran 𝐹𝑤𝐵 ) )
36 33 34 35 3anbi123d ( 𝜑 → ( ( 𝑢 ∈ ran 𝐹𝑣 ∈ ran 𝐹𝑤 ∈ ran 𝐹 ) ↔ ( 𝑢𝐵𝑣𝐵𝑤𝐵 ) ) )
37 fofn ( 𝐹 : 𝑉onto𝐵𝐹 Fn 𝑉 )
38 4 37 syl ( 𝜑𝐹 Fn 𝑉 )
39 fvelrnb ( 𝐹 Fn 𝑉 → ( 𝑢 ∈ ran 𝐹 ↔ ∃ 𝑥𝑉 ( 𝐹𝑥 ) = 𝑢 ) )
40 fvelrnb ( 𝐹 Fn 𝑉 → ( 𝑣 ∈ ran 𝐹 ↔ ∃ 𝑦𝑉 ( 𝐹𝑦 ) = 𝑣 ) )
41 fvelrnb ( 𝐹 Fn 𝑉 → ( 𝑤 ∈ ran 𝐹 ↔ ∃ 𝑧𝑉 ( 𝐹𝑧 ) = 𝑤 ) )
42 39 40 41 3anbi123d ( 𝐹 Fn 𝑉 → ( ( 𝑢 ∈ ran 𝐹𝑣 ∈ ran 𝐹𝑤 ∈ ran 𝐹 ) ↔ ( ∃ 𝑥𝑉 ( 𝐹𝑥 ) = 𝑢 ∧ ∃ 𝑦𝑉 ( 𝐹𝑦 ) = 𝑣 ∧ ∃ 𝑧𝑉 ( 𝐹𝑧 ) = 𝑤 ) ) )
43 38 42 syl ( 𝜑 → ( ( 𝑢 ∈ ran 𝐹𝑣 ∈ ran 𝐹𝑤 ∈ ran 𝐹 ) ↔ ( ∃ 𝑥𝑉 ( 𝐹𝑥 ) = 𝑢 ∧ ∃ 𝑦𝑉 ( 𝐹𝑦 ) = 𝑣 ∧ ∃ 𝑧𝑉 ( 𝐹𝑧 ) = 𝑤 ) ) )
44 36 43 bitr3d ( 𝜑 → ( ( 𝑢𝐵𝑣𝐵𝑤𝐵 ) ↔ ( ∃ 𝑥𝑉 ( 𝐹𝑥 ) = 𝑢 ∧ ∃ 𝑦𝑉 ( 𝐹𝑦 ) = 𝑣 ∧ ∃ 𝑧𝑉 ( 𝐹𝑧 ) = 𝑤 ) ) )
45 3reeanv ( ∃ 𝑥𝑉𝑦𝑉𝑧𝑉 ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) ↔ ( ∃ 𝑥𝑉 ( 𝐹𝑥 ) = 𝑢 ∧ ∃ 𝑦𝑉 ( 𝐹𝑦 ) = 𝑣 ∧ ∃ 𝑧𝑉 ( 𝐹𝑧 ) = 𝑤 ) )
46 44 45 bitr4di ( 𝜑 → ( ( 𝑢𝐵𝑣𝐵𝑤𝐵 ) ↔ ∃ 𝑥𝑉𝑦𝑉𝑧𝑉 ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) ) )
47 3 adantr ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → + = ( +g𝑅 ) )
48 47 oveqd ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( ( 𝑥 + 𝑦 ) ( +g𝑅 ) 𝑧 ) )
49 48 fveq2d ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( 𝐹 ‘ ( ( 𝑥 + 𝑦 ) + 𝑧 ) ) = ( 𝐹 ‘ ( ( 𝑥 + 𝑦 ) ( +g𝑅 ) 𝑧 ) ) )
50 47 oveqd ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( 𝑥 + ( 𝑦 + 𝑧 ) ) = ( 𝑥 ( +g𝑅 ) ( 𝑦 + 𝑧 ) ) )
51 50 fveq2d ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( 𝐹 ‘ ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) = ( 𝐹 ‘ ( 𝑥 ( +g𝑅 ) ( 𝑦 + 𝑧 ) ) ) )
52 8 49 51 3eqtr3d ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( 𝐹 ‘ ( ( 𝑥 + 𝑦 ) ( +g𝑅 ) 𝑧 ) ) = ( 𝐹 ‘ ( 𝑥 ( +g𝑅 ) ( 𝑦 + 𝑧 ) ) ) )
53 simpl ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → 𝜑 )
54 7 3adant3r3 ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑉 )
55 simpr3 ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → 𝑧𝑉 )
56 4 21 1 2 6 22 23 imasaddval ( ( 𝜑 ∧ ( 𝑥 + 𝑦 ) ∈ 𝑉𝑧𝑉 ) → ( ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ( +g𝑈 ) ( 𝐹𝑧 ) ) = ( 𝐹 ‘ ( ( 𝑥 + 𝑦 ) ( +g𝑅 ) 𝑧 ) ) )
57 53 54 55 56 syl3anc ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ( +g𝑈 ) ( 𝐹𝑧 ) ) = ( 𝐹 ‘ ( ( 𝑥 + 𝑦 ) ( +g𝑅 ) 𝑧 ) ) )
58 simpr1 ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → 𝑥𝑉 )
59 26 caovclg ( ( 𝜑 ∧ ( 𝑦𝑉𝑧𝑉 ) ) → ( 𝑦 + 𝑧 ) ∈ 𝑉 )
60 59 3adantr1 ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( 𝑦 + 𝑧 ) ∈ 𝑉 )
61 4 21 1 2 6 22 23 imasaddval ( ( 𝜑𝑥𝑉 ∧ ( 𝑦 + 𝑧 ) ∈ 𝑉 ) → ( ( 𝐹𝑥 ) ( +g𝑈 ) ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) ) = ( 𝐹 ‘ ( 𝑥 ( +g𝑅 ) ( 𝑦 + 𝑧 ) ) ) )
62 53 58 60 61 syl3anc ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( 𝐹𝑥 ) ( +g𝑈 ) ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) ) = ( 𝐹 ‘ ( 𝑥 ( +g𝑅 ) ( 𝑦 + 𝑧 ) ) ) )
63 52 57 62 3eqtr4d ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ( +g𝑈 ) ( 𝐹𝑧 ) ) = ( ( 𝐹𝑥 ) ( +g𝑈 ) ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) ) )
64 4 21 1 2 6 22 23 imasaddval ( ( 𝜑𝑥𝑉𝑦𝑉 ) → ( ( 𝐹𝑥 ) ( +g𝑈 ) ( 𝐹𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 ( +g𝑅 ) 𝑦 ) ) )
65 64 3adant3r3 ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( 𝐹𝑥 ) ( +g𝑈 ) ( 𝐹𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 ( +g𝑅 ) 𝑦 ) ) )
66 47 oveqd ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑥 ( +g𝑅 ) 𝑦 ) )
67 66 fveq2d ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 ( +g𝑅 ) 𝑦 ) ) )
68 65 67 eqtr4d ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( 𝐹𝑥 ) ( +g𝑈 ) ( 𝐹𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) )
69 68 oveq1d ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( ( 𝐹𝑥 ) ( +g𝑈 ) ( 𝐹𝑦 ) ) ( +g𝑈 ) ( 𝐹𝑧 ) ) = ( ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ( +g𝑈 ) ( 𝐹𝑧 ) ) )
70 4 21 1 2 6 22 23 imasaddval ( ( 𝜑𝑦𝑉𝑧𝑉 ) → ( ( 𝐹𝑦 ) ( +g𝑈 ) ( 𝐹𝑧 ) ) = ( 𝐹 ‘ ( 𝑦 ( +g𝑅 ) 𝑧 ) ) )
71 70 3adant3r1 ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( 𝐹𝑦 ) ( +g𝑈 ) ( 𝐹𝑧 ) ) = ( 𝐹 ‘ ( 𝑦 ( +g𝑅 ) 𝑧 ) ) )
72 47 oveqd ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( 𝑦 + 𝑧 ) = ( 𝑦 ( +g𝑅 ) 𝑧 ) )
73 72 fveq2d ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) = ( 𝐹 ‘ ( 𝑦 ( +g𝑅 ) 𝑧 ) ) )
74 71 73 eqtr4d ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( 𝐹𝑦 ) ( +g𝑈 ) ( 𝐹𝑧 ) ) = ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) )
75 74 oveq2d ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( 𝐹𝑥 ) ( +g𝑈 ) ( ( 𝐹𝑦 ) ( +g𝑈 ) ( 𝐹𝑧 ) ) ) = ( ( 𝐹𝑥 ) ( +g𝑈 ) ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) ) )
76 63 69 75 3eqtr4d ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( ( 𝐹𝑥 ) ( +g𝑈 ) ( 𝐹𝑦 ) ) ( +g𝑈 ) ( 𝐹𝑧 ) ) = ( ( 𝐹𝑥 ) ( +g𝑈 ) ( ( 𝐹𝑦 ) ( +g𝑈 ) ( 𝐹𝑧 ) ) ) )
77 simp1 ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( 𝐹𝑥 ) = 𝑢 )
78 simp2 ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( 𝐹𝑦 ) = 𝑣 )
79 77 78 oveq12d ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( 𝐹𝑥 ) ( +g𝑈 ) ( 𝐹𝑦 ) ) = ( 𝑢 ( +g𝑈 ) 𝑣 ) )
80 simp3 ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( 𝐹𝑧 ) = 𝑤 )
81 79 80 oveq12d ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( ( 𝐹𝑥 ) ( +g𝑈 ) ( 𝐹𝑦 ) ) ( +g𝑈 ) ( 𝐹𝑧 ) ) = ( ( 𝑢 ( +g𝑈 ) 𝑣 ) ( +g𝑈 ) 𝑤 ) )
82 78 80 oveq12d ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( 𝐹𝑦 ) ( +g𝑈 ) ( 𝐹𝑧 ) ) = ( 𝑣 ( +g𝑈 ) 𝑤 ) )
83 77 82 oveq12d ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( 𝐹𝑥 ) ( +g𝑈 ) ( ( 𝐹𝑦 ) ( +g𝑈 ) ( 𝐹𝑧 ) ) ) = ( 𝑢 ( +g𝑈 ) ( 𝑣 ( +g𝑈 ) 𝑤 ) ) )
84 81 83 eqeq12d ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( ( ( 𝐹𝑥 ) ( +g𝑈 ) ( 𝐹𝑦 ) ) ( +g𝑈 ) ( 𝐹𝑧 ) ) = ( ( 𝐹𝑥 ) ( +g𝑈 ) ( ( 𝐹𝑦 ) ( +g𝑈 ) ( 𝐹𝑧 ) ) ) ↔ ( ( 𝑢 ( +g𝑈 ) 𝑣 ) ( +g𝑈 ) 𝑤 ) = ( 𝑢 ( +g𝑈 ) ( 𝑣 ( +g𝑈 ) 𝑤 ) ) ) )
85 76 84 syl5ibcom ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( 𝑢 ( +g𝑈 ) 𝑣 ) ( +g𝑈 ) 𝑤 ) = ( 𝑢 ( +g𝑈 ) ( 𝑣 ( +g𝑈 ) 𝑤 ) ) ) )
86 85 3exp2 ( 𝜑 → ( 𝑥𝑉 → ( 𝑦𝑉 → ( 𝑧𝑉 → ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( 𝑢 ( +g𝑈 ) 𝑣 ) ( +g𝑈 ) 𝑤 ) = ( 𝑢 ( +g𝑈 ) ( 𝑣 ( +g𝑈 ) 𝑤 ) ) ) ) ) ) )
87 86 imp32 ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉 ) ) → ( 𝑧𝑉 → ( ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( 𝑢 ( +g𝑈 ) 𝑣 ) ( +g𝑈 ) 𝑤 ) = ( 𝑢 ( +g𝑈 ) ( 𝑣 ( +g𝑈 ) 𝑤 ) ) ) ) )
88 87 rexlimdv ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉 ) ) → ( ∃ 𝑧𝑉 ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( 𝑢 ( +g𝑈 ) 𝑣 ) ( +g𝑈 ) 𝑤 ) = ( 𝑢 ( +g𝑈 ) ( 𝑣 ( +g𝑈 ) 𝑤 ) ) ) )
89 88 rexlimdvva ( 𝜑 → ( ∃ 𝑥𝑉𝑦𝑉𝑧𝑉 ( ( 𝐹𝑥 ) = 𝑢 ∧ ( 𝐹𝑦 ) = 𝑣 ∧ ( 𝐹𝑧 ) = 𝑤 ) → ( ( 𝑢 ( +g𝑈 ) 𝑣 ) ( +g𝑈 ) 𝑤 ) = ( 𝑢 ( +g𝑈 ) ( 𝑣 ( +g𝑈 ) 𝑤 ) ) ) )
90 46 89 sylbid ( 𝜑 → ( ( 𝑢𝐵𝑣𝐵𝑤𝐵 ) → ( ( 𝑢 ( +g𝑈 ) 𝑣 ) ( +g𝑈 ) 𝑤 ) = ( 𝑢 ( +g𝑈 ) ( 𝑣 ( +g𝑈 ) 𝑤 ) ) ) )
91 90 imp ( ( 𝜑 ∧ ( 𝑢𝐵𝑣𝐵𝑤𝐵 ) ) → ( ( 𝑢 ( +g𝑈 ) 𝑣 ) ( +g𝑈 ) 𝑤 ) = ( 𝑢 ( +g𝑈 ) ( 𝑣 ( +g𝑈 ) 𝑤 ) ) )
92 fof ( 𝐹 : 𝑉onto𝐵𝐹 : 𝑉𝐵 )
93 4 92 syl ( 𝜑𝐹 : 𝑉𝐵 )
94 93 9 ffvelrnd ( 𝜑 → ( 𝐹0 ) ∈ 𝐵 )
95 38 39 syl ( 𝜑 → ( 𝑢 ∈ ran 𝐹 ↔ ∃ 𝑥𝑉 ( 𝐹𝑥 ) = 𝑢 ) )
96 33 95 bitr3d ( 𝜑 → ( 𝑢𝐵 ↔ ∃ 𝑥𝑉 ( 𝐹𝑥 ) = 𝑢 ) )
97 simpl ( ( 𝜑𝑥𝑉 ) → 𝜑 )
98 9 adantr ( ( 𝜑𝑥𝑉 ) → 0𝑉 )
99 simpr ( ( 𝜑𝑥𝑉 ) → 𝑥𝑉 )
100 4 21 1 2 6 22 23 imasaddval ( ( 𝜑0𝑉𝑥𝑉 ) → ( ( 𝐹0 ) ( +g𝑈 ) ( 𝐹𝑥 ) ) = ( 𝐹 ‘ ( 0 ( +g𝑅 ) 𝑥 ) ) )
101 97 98 99 100 syl3anc ( ( 𝜑𝑥𝑉 ) → ( ( 𝐹0 ) ( +g𝑈 ) ( 𝐹𝑥 ) ) = ( 𝐹 ‘ ( 0 ( +g𝑅 ) 𝑥 ) ) )
102 3 adantr ( ( 𝜑𝑥𝑉 ) → + = ( +g𝑅 ) )
103 102 oveqd ( ( 𝜑𝑥𝑉 ) → ( 0 + 𝑥 ) = ( 0 ( +g𝑅 ) 𝑥 ) )
104 103 fveq2d ( ( 𝜑𝑥𝑉 ) → ( 𝐹 ‘ ( 0 + 𝑥 ) ) = ( 𝐹 ‘ ( 0 ( +g𝑅 ) 𝑥 ) ) )
105 101 104 10 3eqtr2d ( ( 𝜑𝑥𝑉 ) → ( ( 𝐹0 ) ( +g𝑈 ) ( 𝐹𝑥 ) ) = ( 𝐹𝑥 ) )
106 oveq2 ( ( 𝐹𝑥 ) = 𝑢 → ( ( 𝐹0 ) ( +g𝑈 ) ( 𝐹𝑥 ) ) = ( ( 𝐹0 ) ( +g𝑈 ) 𝑢 ) )
107 id ( ( 𝐹𝑥 ) = 𝑢 → ( 𝐹𝑥 ) = 𝑢 )
108 106 107 eqeq12d ( ( 𝐹𝑥 ) = 𝑢 → ( ( ( 𝐹0 ) ( +g𝑈 ) ( 𝐹𝑥 ) ) = ( 𝐹𝑥 ) ↔ ( ( 𝐹0 ) ( +g𝑈 ) 𝑢 ) = 𝑢 ) )
109 105 108 syl5ibcom ( ( 𝜑𝑥𝑉 ) → ( ( 𝐹𝑥 ) = 𝑢 → ( ( 𝐹0 ) ( +g𝑈 ) 𝑢 ) = 𝑢 ) )
110 109 rexlimdva ( 𝜑 → ( ∃ 𝑥𝑉 ( 𝐹𝑥 ) = 𝑢 → ( ( 𝐹0 ) ( +g𝑈 ) 𝑢 ) = 𝑢 ) )
111 96 110 sylbid ( 𝜑 → ( 𝑢𝐵 → ( ( 𝐹0 ) ( +g𝑈 ) 𝑢 ) = 𝑢 ) )
112 111 imp ( ( 𝜑𝑢𝐵 ) → ( ( 𝐹0 ) ( +g𝑈 ) 𝑢 ) = 𝑢 )
113 93 adantr ( ( 𝜑𝑥𝑉 ) → 𝐹 : 𝑉𝐵 )
114 113 11 ffvelrnd ( ( 𝜑𝑥𝑉 ) → ( 𝐹𝑁 ) ∈ 𝐵 )
115 4 21 1 2 6 22 23 imasaddval ( ( 𝜑𝑁𝑉𝑥𝑉 ) → ( ( 𝐹𝑁 ) ( +g𝑈 ) ( 𝐹𝑥 ) ) = ( 𝐹 ‘ ( 𝑁 ( +g𝑅 ) 𝑥 ) ) )
116 97 11 99 115 syl3anc ( ( 𝜑𝑥𝑉 ) → ( ( 𝐹𝑁 ) ( +g𝑈 ) ( 𝐹𝑥 ) ) = ( 𝐹 ‘ ( 𝑁 ( +g𝑅 ) 𝑥 ) ) )
117 102 oveqd ( ( 𝜑𝑥𝑉 ) → ( 𝑁 + 𝑥 ) = ( 𝑁 ( +g𝑅 ) 𝑥 ) )
118 117 fveq2d ( ( 𝜑𝑥𝑉 ) → ( 𝐹 ‘ ( 𝑁 + 𝑥 ) ) = ( 𝐹 ‘ ( 𝑁 ( +g𝑅 ) 𝑥 ) ) )
119 116 118 12 3eqtr2d ( ( 𝜑𝑥𝑉 ) → ( ( 𝐹𝑁 ) ( +g𝑈 ) ( 𝐹𝑥 ) ) = ( 𝐹0 ) )
120 oveq1 ( 𝑣 = ( 𝐹𝑁 ) → ( 𝑣 ( +g𝑈 ) ( 𝐹𝑥 ) ) = ( ( 𝐹𝑁 ) ( +g𝑈 ) ( 𝐹𝑥 ) ) )
121 120 eqeq1d ( 𝑣 = ( 𝐹𝑁 ) → ( ( 𝑣 ( +g𝑈 ) ( 𝐹𝑥 ) ) = ( 𝐹0 ) ↔ ( ( 𝐹𝑁 ) ( +g𝑈 ) ( 𝐹𝑥 ) ) = ( 𝐹0 ) ) )
122 121 rspcev ( ( ( 𝐹𝑁 ) ∈ 𝐵 ∧ ( ( 𝐹𝑁 ) ( +g𝑈 ) ( 𝐹𝑥 ) ) = ( 𝐹0 ) ) → ∃ 𝑣𝐵 ( 𝑣 ( +g𝑈 ) ( 𝐹𝑥 ) ) = ( 𝐹0 ) )
123 114 119 122 syl2anc ( ( 𝜑𝑥𝑉 ) → ∃ 𝑣𝐵 ( 𝑣 ( +g𝑈 ) ( 𝐹𝑥 ) ) = ( 𝐹0 ) )
124 oveq2 ( ( 𝐹𝑥 ) = 𝑢 → ( 𝑣 ( +g𝑈 ) ( 𝐹𝑥 ) ) = ( 𝑣 ( +g𝑈 ) 𝑢 ) )
125 124 eqeq1d ( ( 𝐹𝑥 ) = 𝑢 → ( ( 𝑣 ( +g𝑈 ) ( 𝐹𝑥 ) ) = ( 𝐹0 ) ↔ ( 𝑣 ( +g𝑈 ) 𝑢 ) = ( 𝐹0 ) ) )
126 125 rexbidv ( ( 𝐹𝑥 ) = 𝑢 → ( ∃ 𝑣𝐵 ( 𝑣 ( +g𝑈 ) ( 𝐹𝑥 ) ) = ( 𝐹0 ) ↔ ∃ 𝑣𝐵 ( 𝑣 ( +g𝑈 ) 𝑢 ) = ( 𝐹0 ) ) )
127 123 126 syl5ibcom ( ( 𝜑𝑥𝑉 ) → ( ( 𝐹𝑥 ) = 𝑢 → ∃ 𝑣𝐵 ( 𝑣 ( +g𝑈 ) 𝑢 ) = ( 𝐹0 ) ) )
128 127 rexlimdva ( 𝜑 → ( ∃ 𝑥𝑉 ( 𝐹𝑥 ) = 𝑢 → ∃ 𝑣𝐵 ( 𝑣 ( +g𝑈 ) 𝑢 ) = ( 𝐹0 ) ) )
129 96 128 sylbid ( 𝜑 → ( 𝑢𝐵 → ∃ 𝑣𝐵 ( 𝑣 ( +g𝑈 ) 𝑢 ) = ( 𝐹0 ) ) )
130 129 imp ( ( 𝜑𝑢𝐵 ) → ∃ 𝑣𝐵 ( 𝑣 ( +g𝑈 ) 𝑢 ) = ( 𝐹0 ) )
131 13 14 30 91 94 112 130 isgrpde ( 𝜑𝑈 ∈ Grp )
132 13 14 94 112 131 grpidd2 ( 𝜑 → ( 𝐹0 ) = ( 0g𝑈 ) )
133 131 132 jca ( 𝜑 → ( 𝑈 ∈ Grp ∧ ( 𝐹0 ) = ( 0g𝑈 ) ) )