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𝑈 ) ) )