This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 fovcdm ⊢ ( ( ( +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 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 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 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑁 ) ∈ 𝐵 )
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 ‘ 𝑈 ) ) )