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

Metamath Proof Explorer

Theorem mgmhmf1o

Description: A magma homomorphism is bijective iff its converse is also a magma homomorphism. (Contributed by AV, 25-Feb-2020)

Ref Expression
Hypotheses mgmhmf1o.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
mgmhmf1o.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
Assertion mgmhmf1o ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) → ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ↔ ◡ 𝐹 ∈ ( 𝑆 MgmHom 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 mgmhmf1o.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 mgmhmf1o.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
3 mgmhmrcl ⊢ ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) → ( 𝑅 ∈ Mgm ∧ 𝑆 ∈ Mgm ) )
4 3 ancomd ⊢ ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) → ( 𝑆 ∈ Mgm ∧ 𝑅 ∈ Mgm ) )
5 4 adantr ⊢ ( ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ( 𝑆 ∈ Mgm ∧ 𝑅 ∈ Mgm ) )
6 f1ocnv ⊢ ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 → ◡ 𝐹 : 𝐶 –1-1-onto→ 𝐵 )
7 6 adantl ⊢ ( ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ◡ 𝐹 : 𝐶 –1-1-onto→ 𝐵 )
8 f1of ⊢ ( ◡ 𝐹 : 𝐶 –1-1-onto→ 𝐵 → ◡ 𝐹 : 𝐶 ⟶ 𝐵 )
9 7 8 syl ⊢ ( ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ◡ 𝐹 : 𝐶 ⟶ 𝐵 )
10 simpll ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) )
11 9 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ◡ 𝐹 : 𝐶 ⟶ 𝐵 )
12 simprl ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → 𝑥 ∈ 𝐶 )
13 11 12 ffvelcdmd ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ◡ 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
14 simprr ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → 𝑦 ∈ 𝐶 )
15 11 14 ffvelcdmd ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝐵 )
16 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
17 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
18 1 16 17 mgmhmlin ⊢ ( ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) ∧ ( ◡ 𝐹 ‘ 𝑥 ) ∈ 𝐵 ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝐵 ) → ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ) = ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑦 ) ) ) )
19 10 13 15 18 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ) = ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑦 ) ) ) )
20 simplr ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → 𝐹 : 𝐵 –1-1-onto→ 𝐶 )
21 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ∧ 𝑥 ∈ 𝐶 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) = 𝑥 )
22 20 12 21 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) = 𝑥 )
23 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ∧ 𝑦 ∈ 𝐶 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑦 ) ) = 𝑦 )
24 20 14 23 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑦 ) ) = 𝑦 )
25 22 24 oveq12d ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑦 ) ) ) = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) )
26 19 25 eqtrd ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ) = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) )
27 3 simpld ⊢ ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) → 𝑅 ∈ Mgm )
28 27 adantr ⊢ ( ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → 𝑅 ∈ Mgm )
29 28 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → 𝑅 ∈ Mgm )
30 1 16 mgmcl ⊢ ( ( 𝑅 ∈ Mgm ∧ ( ◡ 𝐹 ‘ 𝑥 ) ∈ 𝐵 ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝐵 ) → ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ∈ 𝐵 )
31 29 13 15 30 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ∈ 𝐵 )
32 f1ocnvfv ⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ∈ 𝐵 ) → ( ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ) = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) → ( ◡ 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ) )
33 20 31 32 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ) = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) → ( ◡ 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ) )
34 26 33 mpd ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ◡ 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ◡ 𝐹 ‘ 𝑦 ) ) )
35 34 ralrimivva ⊢ ( ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐶 ( ◡ 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ◡ 𝐹 ‘ 𝑦 ) ) )
36 9 35 jca ⊢ ( ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ( ◡ 𝐹 : 𝐶 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐶 ( ◡ 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ) )
37 2 1 17 16 ismgmhm ⊢ ( ◡ 𝐹 ∈ ( 𝑆 MgmHom 𝑅 ) ↔ ( ( 𝑆 ∈ Mgm ∧ 𝑅 ∈ Mgm ) ∧ ( ◡ 𝐹 : 𝐶 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐶 ( ◡ 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ) ) )
38 5 36 37 sylanbrc ⊢ ( ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ◡ 𝐹 ∈ ( 𝑆 MgmHom 𝑅 ) )
39 1 2 mgmhmf ⊢ ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) → 𝐹 : 𝐵 ⟶ 𝐶 )
40 39 adantr ⊢ ( ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 MgmHom 𝑅 ) ) → 𝐹 : 𝐵 ⟶ 𝐶 )
41 40 ffnd ⊢ ( ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 MgmHom 𝑅 ) ) → 𝐹 Fn 𝐵 )
42 2 1 mgmhmf ⊢ ( ◡ 𝐹 ∈ ( 𝑆 MgmHom 𝑅 ) → ◡ 𝐹 : 𝐶 ⟶ 𝐵 )
43 42 adantl ⊢ ( ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 MgmHom 𝑅 ) ) → ◡ 𝐹 : 𝐶 ⟶ 𝐵 )
44 43 ffnd ⊢ ( ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 MgmHom 𝑅 ) ) → ◡ 𝐹 Fn 𝐶 )
45 dff1o4 ⊢ ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ↔ ( 𝐹 Fn 𝐵 ∧ ◡ 𝐹 Fn 𝐶 ) )
46 41 44 45 sylanbrc ⊢ ( ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 MgmHom 𝑅 ) ) → 𝐹 : 𝐵 –1-1-onto→ 𝐶 )
47 38 46 impbida ⊢ ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) → ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ↔ ◡ 𝐹 ∈ ( 𝑆 MgmHom 𝑅 ) ) )