Metamath Proof Explorer

Theorem imasmnd2

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

Ref Expression
Hypotheses imasmnd.u ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
imasmnd.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
imasmnd.p ⊢ + = ( +g ‘ 𝑅 )
imasmnd.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
imasmnd.e ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) ) )
imasmnd2.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
imasmnd2.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑥 + 𝑦 ) ∈ 𝑉 )
imasmnd2.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝐹 ‘ ( ( 𝑥 + 𝑦 ) + 𝑧 ) ) = ( 𝐹 ‘ ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) )
imasmnd2.3 ⊢ ( 𝜑 → 0 ∈ 𝑉 )
imasmnd2.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐹 ‘ ( 0 + 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
imasmnd2.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐹 ‘ ( 𝑥 + 0 ) ) = ( 𝐹 ‘ 𝑥 ) )
Assertion imasmnd2 ( 𝜑 → ( 𝑈 ∈ Mnd ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 imasmnd.u ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
2 imasmnd.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3 imasmnd.p ⊢ + = ( +g ‘ 𝑅 )
4 imasmnd.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
5 imasmnd.e ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) ) )
6 imasmnd2.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
7 imasmnd2.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑥 + 𝑦 ) ∈ 𝑉 )
8 imasmnd2.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝐹 ‘ ( ( 𝑥 + 𝑦 ) + 𝑧 ) ) = ( 𝐹 ‘ ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) )
9 imasmnd2.3 ⊢ ( 𝜑 → 0 ∈ 𝑉 )
10 imasmnd2.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐹 ‘ ( 0 + 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
11 imasmnd2.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐹 ‘ ( 𝑥 + 0 ) ) = ( 𝐹 ‘ 𝑥 ) )
12 1 2 4 6 imasbas ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑈 ) )
13 eqidd ⊢ ( 𝜑 → ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 ) )
14 eqid ⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
15 7 3expb ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑉 )
16 15 caovclg ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( 𝑝 + 𝑞 ) ∈ 𝑉 )
17 4 5 1 2 6 3 14 16 imasaddf ⊢ ( 𝜑 → ( +g ‘ 𝑈 ) : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )
18 fovrn ⊢ ( ( ( +g ‘ 𝑈 ) : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) → ( 𝑢 ( +g ‘ 𝑈 ) 𝑣 ) ∈ 𝐵 )
19 17 18 syl3an1 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) → ( 𝑢 ( +g ‘ 𝑈 ) 𝑣 ) ∈ 𝐵 )
20 forn ⊢ ( 𝐹 : 𝑉 –onto→ 𝐵 → ran 𝐹 = 𝐵 )
21 4 20 syl ⊢ ( 𝜑 → ran 𝐹 = 𝐵 )
22 21 eleq2d ⊢ ( 𝜑 → ( 𝑢 ∈ ran 𝐹 ↔ 𝑢 ∈ 𝐵 ) )
23 21 eleq2d ⊢ ( 𝜑 → ( 𝑣 ∈ ran 𝐹 ↔ 𝑣 ∈ 𝐵 ) )
24 21 eleq2d ⊢ ( 𝜑 → ( 𝑤 ∈ ran 𝐹 ↔ 𝑤 ∈ 𝐵 ) )
25 22 23 24 3anbi123d ⊢ ( 𝜑 → ( ( 𝑢 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹 ∧ 𝑤 ∈ ran 𝐹 ) ↔ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) )
26 fofn ⊢ ( 𝐹 : 𝑉 –onto→ 𝐵 → 𝐹 Fn 𝑉 )
27 4 26 syl ⊢ ( 𝜑 → 𝐹 Fn 𝑉 )
28 fvelrnb ⊢ ( 𝐹 Fn 𝑉 → ( 𝑢 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝑉 ( 𝐹 ‘ 𝑥 ) = 𝑢 ) )
29 fvelrnb ⊢ ( 𝐹 Fn 𝑉 → ( 𝑣 ∈ ran 𝐹 ↔ ∃ 𝑦 ∈ 𝑉 ( 𝐹 ‘ 𝑦 ) = 𝑣 ) )
30 fvelrnb ⊢ ( 𝐹 Fn 𝑉 → ( 𝑤 ∈ ran 𝐹 ↔ ∃ 𝑧 ∈ 𝑉 ( 𝐹 ‘ 𝑧 ) = 𝑤 ) )
31 28 29 30 3anbi123d ⊢ ( 𝐹 Fn 𝑉 → ( ( 𝑢 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹 ∧ 𝑤 ∈ ran 𝐹 ) ↔ ( ∃ 𝑥 ∈ 𝑉 ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ∃ 𝑦 ∈ 𝑉 ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ∃ 𝑧 ∈ 𝑉 ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ) )
32 27 31 syl ⊢ ( 𝜑 → ( ( 𝑢 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹 ∧ 𝑤 ∈ ran 𝐹 ) ↔ ( ∃ 𝑥 ∈ 𝑉 ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ∃ 𝑦 ∈ 𝑉 ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ∃ 𝑧 ∈ 𝑉 ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ) )
33 25 32 bitr3d ⊢ ( 𝜑 → ( ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ↔ ( ∃ 𝑥 ∈ 𝑉 ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ∃ 𝑦 ∈ 𝑉 ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ∃ 𝑧 ∈ 𝑉 ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ) )
34 3reeanv ⊢ ( ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ↔ ( ∃ 𝑥 ∈ 𝑉 ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ∃ 𝑦 ∈ 𝑉 ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ∃ 𝑧 ∈ 𝑉 ( 𝐹 ‘ 𝑧 ) = 𝑤 ) )
35 33 34 bitr4di ⊢ ( 𝜑 → ( ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ) )
36 simpl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝜑 )
37 7 3adant3r3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑉 )
38 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑧 ∈ 𝑉 )
39 4 5 1 2 6 3 14 imasaddval ⊢ ( ( 𝜑 ∧ ( 𝑥 + 𝑦 ) ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) → ( ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ ( ( 𝑥 + 𝑦 ) + 𝑧 ) ) )
40 36 37 38 39 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ ( ( 𝑥 + 𝑦 ) + 𝑧 ) ) )
41 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑥 ∈ 𝑉 )
42 16 caovclg ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑦 + 𝑧 ) ∈ 𝑉 )
43 42 3adantr1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑦 + 𝑧 ) ∈ 𝑉 )
44 4 5 1 2 6 3 14 imasaddval ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ ( 𝑦 + 𝑧 ) ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) ) = ( 𝐹 ‘ ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) )
45 36 41 43 44 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) ) = ( 𝐹 ‘ ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) )
46 8 40 45 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) ) )
47 4 5 1 2 6 3 14 imasaddval ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) )
48 47 3adant3r3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) )
49 48 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) )
50 4 5 1 2 6 3 14 imasaddval ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑦 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) )
51 50 3adant3r1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑦 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) )
52 51 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( ( 𝐹 ‘ 𝑦 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) ) )
53 46 49 52 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( ( 𝐹 ‘ 𝑦 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) ) )
54 simp1 ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝐹 ‘ 𝑥 ) = 𝑢 )
55 simp2 ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝐹 ‘ 𝑦 ) = 𝑣 )
56 54 55 oveq12d ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) = ( 𝑢 ( +g ‘ 𝑈 ) 𝑣 ) )
57 simp3 ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝐹 ‘ 𝑧 ) = 𝑤 )
58 56 57 oveq12d ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( ( 𝑢 ( +g ‘ 𝑈 ) 𝑣 ) ( +g ‘ 𝑈 ) 𝑤 ) )
59 55 57 oveq12d ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝐹 ‘ 𝑦 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝑣 ( +g ‘ 𝑈 ) 𝑤 ) )
60 54 59 oveq12d ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( ( 𝐹 ‘ 𝑦 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) ) = ( 𝑢 ( +g ‘ 𝑈 ) ( 𝑣 ( +g ‘ 𝑈 ) 𝑤 ) ) )
61 58 60 eqeq12d ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑦 ) ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( ( 𝐹 ‘ 𝑦 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑧 ) ) ) ↔ ( ( 𝑢 ( +g ‘ 𝑈 ) 𝑣 ) ( +g ‘ 𝑈 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝑈 ) ( 𝑣 ( +g ‘ 𝑈 ) 𝑤 ) ) ) )
62 53 61 syl5ibcom ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝑢 ( +g ‘ 𝑈 ) 𝑣 ) ( +g ‘ 𝑈 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝑈 ) ( 𝑣 ( +g ‘ 𝑈 ) 𝑤 ) ) ) )
63 62 3exp2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑉 → ( 𝑦 ∈ 𝑉 → ( 𝑧 ∈ 𝑉 → ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝑢 ( +g ‘ 𝑈 ) 𝑣 ) ( +g ‘ 𝑈 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝑈 ) ( 𝑣 ( +g ‘ 𝑈 ) 𝑤 ) ) ) ) ) ) )
64 63 imp32 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑧 ∈ 𝑉 → ( ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝑢 ( +g ‘ 𝑈 ) 𝑣 ) ( +g ‘ 𝑈 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝑈 ) ( 𝑣 ( +g ‘ 𝑈 ) 𝑤 ) ) ) ) )
65 64 rexlimdv ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ∃ 𝑧 ∈ 𝑉 ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝑢 ( +g ‘ 𝑈 ) 𝑣 ) ( +g ‘ 𝑈 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝑈 ) ( 𝑣 ( +g ‘ 𝑈 ) 𝑤 ) ) ) )
66 65 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( ( 𝐹 ‘ 𝑥 ) = 𝑢 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝑢 ( +g ‘ 𝑈 ) 𝑣 ) ( +g ‘ 𝑈 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝑈 ) ( 𝑣 ( +g ‘ 𝑈 ) 𝑤 ) ) ) )
67 35 66 sylbid ⊢ ( 𝜑 → ( ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) → ( ( 𝑢 ( +g ‘ 𝑈 ) 𝑣 ) ( +g ‘ 𝑈 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝑈 ) ( 𝑣 ( +g ‘ 𝑈 ) 𝑤 ) ) ) )
68 67 imp ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑢 ( +g ‘ 𝑈 ) 𝑣 ) ( +g ‘ 𝑈 ) 𝑤 ) = ( 𝑢 ( +g ‘ 𝑈 ) ( 𝑣 ( +g ‘ 𝑈 ) 𝑤 ) ) )
69 fof ⊢ ( 𝐹 : 𝑉 –onto→ 𝐵 → 𝐹 : 𝑉 ⟶ 𝐵 )
70 4 69 syl ⊢ ( 𝜑 → 𝐹 : 𝑉 ⟶ 𝐵 )
71 70 9 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) ∈ 𝐵 )
72 27 28 syl ⊢ ( 𝜑 → ( 𝑢 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝑉 ( 𝐹 ‘ 𝑥 ) = 𝑢 ) )
73 22 72 bitr3d ⊢ ( 𝜑 → ( 𝑢 ∈ 𝐵 ↔ ∃ 𝑥 ∈ 𝑉 ( 𝐹 ‘ 𝑥 ) = 𝑢 ) )
74 simpl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 𝜑 )
75 9 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 0 ∈ 𝑉 )
76 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 𝑥 ∈ 𝑉 )
77 4 5 1 2 6 3 14 imasaddval ⊢ ( ( 𝜑 ∧ 0 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐹 ‘ 0 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ ( 0 + 𝑥 ) ) )
78 74 75 76 77 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐹 ‘ 0 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ ( 0 + 𝑥 ) ) )
79 78 10 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐹 ‘ 0 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
80 oveq2 ⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑢 → ( ( 𝐹 ‘ 0 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 0 ) ( +g ‘ 𝑈 ) 𝑢 ) )
81 id ⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑢 → ( 𝐹 ‘ 𝑥 ) = 𝑢 )
82 80 81 eqeq12d ⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑢 → ( ( ( 𝐹 ‘ 0 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) ↔ ( ( 𝐹 ‘ 0 ) ( +g ‘ 𝑈 ) 𝑢 ) = 𝑢 ) )
83 79 82 syl5ibcom ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑢 → ( ( 𝐹 ‘ 0 ) ( +g ‘ 𝑈 ) 𝑢 ) = 𝑢 ) )
84 83 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑉 ( 𝐹 ‘ 𝑥 ) = 𝑢 → ( ( 𝐹 ‘ 0 ) ( +g ‘ 𝑈 ) 𝑢 ) = 𝑢 ) )
85 73 84 sylbid ⊢ ( 𝜑 → ( 𝑢 ∈ 𝐵 → ( ( 𝐹 ‘ 0 ) ( +g ‘ 𝑈 ) 𝑢 ) = 𝑢 ) )
86 85 imp ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) → ( ( 𝐹 ‘ 0 ) ( +g ‘ 𝑈 ) 𝑢 ) = 𝑢 )
87 4 5 1 2 6 3 14 imasaddval ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 0 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 0 ) ) = ( 𝐹 ‘ ( 𝑥 + 0 ) ) )
88 75 87 mpd3an3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 0 ) ) = ( 𝐹 ‘ ( 𝑥 + 0 ) ) )
89 88 11 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 0 ) ) = ( 𝐹 ‘ 𝑥 ) )
90 oveq1 ⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑢 → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 0 ) ) = ( 𝑢 ( +g ‘ 𝑈 ) ( 𝐹 ‘ 0 ) ) )
91 90 81 eqeq12d ⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑢 → ( ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 0 ) ) = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝑢 ( +g ‘ 𝑈 ) ( 𝐹 ‘ 0 ) ) = 𝑢 ) )
92 89 91 syl5ibcom ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑢 → ( 𝑢 ( +g ‘ 𝑈 ) ( 𝐹 ‘ 0 ) ) = 𝑢 ) )
93 92 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑉 ( 𝐹 ‘ 𝑥 ) = 𝑢 → ( 𝑢 ( +g ‘ 𝑈 ) ( 𝐹 ‘ 0 ) ) = 𝑢 ) )
94 73 93 sylbid ⊢ ( 𝜑 → ( 𝑢 ∈ 𝐵 → ( 𝑢 ( +g ‘ 𝑈 ) ( 𝐹 ‘ 0 ) ) = 𝑢 ) )
95 94 imp ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) → ( 𝑢 ( +g ‘ 𝑈 ) ( 𝐹 ‘ 0 ) ) = 𝑢 )
96 12 13 19 68 71 86 95 ismndd ⊢ ( 𝜑 → 𝑈 ∈ Mnd )
97 12 13 71 86 95 grpidd ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) )
98 96 97 jca ⊢ ( 𝜑 → ( 𝑈 ∈ Mnd ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) )