Metamath Proof Explorer

Theorem imasmgm2

Description: The image structure of a unital magma is a unital magma. (Contributed by Thierry Arnoux, 31-Aug-2026)

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

Proof

Step Hyp Ref Expression
1 imasmgm.u ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
2 imasmgm.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3 imasmgm.p ⊢ + = ( +g ‘ 𝑅 )
4 imasmgm.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
5 imasmgm.e ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) ) )
6 imasmgm2.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
7 imasmgm2.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑥 + 𝑦 ) ∈ 𝑉 )
8 imasmgm2.2 ⊢ ( 𝜑 → 0 ∈ 𝑉 )
9 imasmgm2.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐹 ‘ ( 0 + 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
10 imasmgm2.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐹 ‘ ( 𝑥 + 0 ) ) = ( 𝐹 ‘ 𝑥 ) )
11 1 2 4 6 imasbas ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑈 ) )
12 ovex ⊢ ( 𝐹 “s 𝑅 ) ∈ V
13 1 12 eqeltrdi ⊢ ( 𝜑 → 𝑈 ∈ V )
14 eqidd ⊢ ( 𝜑 → ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 ) )
15 eqid ⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
16 7 3expb ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑉 )
17 16 caovclg ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( 𝑝 + 𝑞 ) ∈ 𝑉 )
18 4 5 1 2 6 3 15 17 imasaddf ⊢ ( 𝜑 → ( +g ‘ 𝑈 ) : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )
19 18 fovcld ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) → ( 𝑢 ( +g ‘ 𝑈 ) 𝑣 ) ∈ 𝐵 )
20 11 13 14 19 ismgmd ⊢ ( 𝜑 → 𝑈 ∈ Mgm )
21 fof ⊢ ( 𝐹 : 𝑉 –onto→ 𝐵 → 𝐹 : 𝑉 ⟶ 𝐵 )
22 4 21 syl ⊢ ( 𝜑 → 𝐹 : 𝑉 ⟶ 𝐵 )
23 22 8 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) ∈ 𝐵 )
24 forn ⊢ ( 𝐹 : 𝑉 –onto→ 𝐵 → ran 𝐹 = 𝐵 )
25 4 24 syl ⊢ ( 𝜑 → ran 𝐹 = 𝐵 )
26 25 eleq2d ⊢ ( 𝜑 → ( 𝑢 ∈ ran 𝐹 ↔ 𝑢 ∈ 𝐵 ) )
27 fofn ⊢ ( 𝐹 : 𝑉 –onto→ 𝐵 → 𝐹 Fn 𝑉 )
28 fvelrnb ⊢ ( 𝐹 Fn 𝑉 → ( 𝑢 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝑉 ( 𝐹 ‘ 𝑥 ) = 𝑢 ) )
29 4 27 28 3syl ⊢ ( 𝜑 → ( 𝑢 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝑉 ( 𝐹 ‘ 𝑥 ) = 𝑢 ) )
30 26 29 bitr3d ⊢ ( 𝜑 → ( 𝑢 ∈ 𝐵 ↔ ∃ 𝑥 ∈ 𝑉 ( 𝐹 ‘ 𝑥 ) = 𝑢 ) )
31 simpl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 𝜑 )
32 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 0 ∈ 𝑉 )
33 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 𝑥 ∈ 𝑉 )
34 4 5 1 2 6 3 15 imasaddval ⊢ ( ( 𝜑 ∧ 0 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐹 ‘ 0 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ ( 0 + 𝑥 ) ) )
35 31 32 33 34 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐹 ‘ 0 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ ( 0 + 𝑥 ) ) )
36 35 9 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐹 ‘ 0 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
37 oveq2 ⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑢 → ( ( 𝐹 ‘ 0 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 0 ) ( +g ‘ 𝑈 ) 𝑢 ) )
38 id ⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑢 → ( 𝐹 ‘ 𝑥 ) = 𝑢 )
39 37 38 eqeq12d ⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑢 → ( ( ( 𝐹 ‘ 0 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) ↔ ( ( 𝐹 ‘ 0 ) ( +g ‘ 𝑈 ) 𝑢 ) = 𝑢 ) )
40 36 39 syl5ibcom ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑢 → ( ( 𝐹 ‘ 0 ) ( +g ‘ 𝑈 ) 𝑢 ) = 𝑢 ) )
41 40 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑉 ( 𝐹 ‘ 𝑥 ) = 𝑢 → ( ( 𝐹 ‘ 0 ) ( +g ‘ 𝑈 ) 𝑢 ) = 𝑢 ) )
42 30 41 sylbid ⊢ ( 𝜑 → ( 𝑢 ∈ 𝐵 → ( ( 𝐹 ‘ 0 ) ( +g ‘ 𝑈 ) 𝑢 ) = 𝑢 ) )
43 42 imp ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) → ( ( 𝐹 ‘ 0 ) ( +g ‘ 𝑈 ) 𝑢 ) = 𝑢 )
44 4 5 1 2 6 3 15 imasaddval ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 0 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 0 ) ) = ( 𝐹 ‘ ( 𝑥 + 0 ) ) )
45 32 44 mpd3an3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 0 ) ) = ( 𝐹 ‘ ( 𝑥 + 0 ) ) )
46 45 10 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 0 ) ) = ( 𝐹 ‘ 𝑥 ) )
47 oveq1 ⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑢 → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 0 ) ) = ( 𝑢 ( +g ‘ 𝑈 ) ( 𝐹 ‘ 0 ) ) )
48 47 38 eqeq12d ⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑢 → ( ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 0 ) ) = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝑢 ( +g ‘ 𝑈 ) ( 𝐹 ‘ 0 ) ) = 𝑢 ) )
49 46 48 syl5ibcom ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑢 → ( 𝑢 ( +g ‘ 𝑈 ) ( 𝐹 ‘ 0 ) ) = 𝑢 ) )
50 49 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑉 ( 𝐹 ‘ 𝑥 ) = 𝑢 → ( 𝑢 ( +g ‘ 𝑈 ) ( 𝐹 ‘ 0 ) ) = 𝑢 ) )
51 30 50 sylbid ⊢ ( 𝜑 → ( 𝑢 ∈ 𝐵 → ( 𝑢 ( +g ‘ 𝑈 ) ( 𝐹 ‘ 0 ) ) = 𝑢 ) )
52 51 imp ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) → ( 𝑢 ( +g ‘ 𝑈 ) ( 𝐹 ‘ 0 ) ) = 𝑢 )
53 11 14 23 43 52 grpidd ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) )
54 20 53 jca ⊢ ( 𝜑 → ( 𝑈 ∈ Mgm ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) )