Metamath Proof Explorer

Theorem mhmf1o

Description: A monoid homomorphism is bijective iff its converse is also a monoid homomorphism. (Contributed by AV, 22-Oct-2019)

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

Proof

Step Hyp Ref Expression
1 mhmf1o.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 mhmf1o.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
3 mhmrcl2 ⊢ ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) → 𝑆 ∈ Mnd )
4 mhmrcl1 ⊢ ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) → 𝑅 ∈ Mnd )
5 3 4 jca ⊢ ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) → ( 𝑆 ∈ Mnd ∧ 𝑅 ∈ Mnd ) )
6 5 adantr ⊢ ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ( 𝑆 ∈ Mnd ∧ 𝑅 ∈ Mnd ) )
7 f1ocnv ⊢ ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 → ◡ 𝐹 : 𝐶 –1-1-onto→ 𝐵 )
8 7 adantl ⊢ ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ◡ 𝐹 : 𝐶 –1-1-onto→ 𝐵 )
9 f1of ⊢ ( ◡ 𝐹 : 𝐶 –1-1-onto→ 𝐵 → ◡ 𝐹 : 𝐶 ⟶ 𝐵 )
10 8 9 syl ⊢ ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ◡ 𝐹 : 𝐶 ⟶ 𝐵 )
11 simpll ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) )
12 10 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ◡ 𝐹 : 𝐶 ⟶ 𝐵 )
13 simprl ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → 𝑥 ∈ 𝐶 )
14 12 13 ffvelrnd ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ◡ 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
15 simprr ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → 𝑦 ∈ 𝐶 )
16 12 15 ffvelrnd ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝐵 )
17 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
18 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
19 1 17 18 mhmlin ⊢ ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ ( ◡ 𝐹 ‘ 𝑥 ) ∈ 𝐵 ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝐵 ) → ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ) = ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑦 ) ) ) )
20 11 14 16 19 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ) = ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑦 ) ) ) )
21 simpr ⊢ ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → 𝐹 : 𝐵 –1-1-onto→ 𝐶 )
22 21 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → 𝐹 : 𝐵 –1-1-onto→ 𝐶 )
23 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ∧ 𝑥 ∈ 𝐶 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) = 𝑥 )
24 22 13 23 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) = 𝑥 )
25 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ∧ 𝑦 ∈ 𝐶 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑦 ) ) = 𝑦 )
26 22 15 25 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑦 ) ) = 𝑦 )
27 24 26 oveq12d ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑦 ) ) ) = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) )
28 20 27 eqtrd ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ) = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) )
29 4 adantr ⊢ ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → 𝑅 ∈ Mnd )
30 29 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → 𝑅 ∈ Mnd )
31 1 17 mndcl ⊢ ( ( 𝑅 ∈ Mnd ∧ ( ◡ 𝐹 ‘ 𝑥 ) ∈ 𝐵 ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝐵 ) → ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ∈ 𝐵 )
32 30 14 16 31 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ∈ 𝐵 )
33 f1ocnvfv ⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ∈ 𝐵 ) → ( ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ) = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) → ( ◡ 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ) )
34 22 32 33 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝐹 ‘ ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ) = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) → ( ◡ 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ) )
35 28 34 mpd ⊢ ( ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ◡ 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ◡ 𝐹 ‘ 𝑦 ) ) )
36 35 ralrimivva ⊢ ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐶 ( ◡ 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ◡ 𝐹 ‘ 𝑦 ) ) )
37 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
38 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
39 37 38 mhm0 ⊢ ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) → ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑆 ) )
40 39 adantr ⊢ ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑆 ) )
41 40 eqcomd ⊢ ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ( 0g ‘ 𝑆 ) = ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) )
42 41 fveq2d ⊢ ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ( ◡ 𝐹 ‘ ( 0g ‘ 𝑆 ) ) = ( ◡ 𝐹 ‘ ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) ) )
43 1 37 mndidcl ⊢ ( 𝑅 ∈ Mnd → ( 0g ‘ 𝑅 ) ∈ 𝐵 )
44 4 43 syl ⊢ ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) → ( 0g ‘ 𝑅 ) ∈ 𝐵 )
45 44 adantr ⊢ ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ( 0g ‘ 𝑅 ) ∈ 𝐵 )
46 f1ocnvfv1 ⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ∧ ( 0g ‘ 𝑅 ) ∈ 𝐵 ) → ( ◡ 𝐹 ‘ ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑅 ) )
47 21 45 46 syl2anc ⊢ ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ( ◡ 𝐹 ‘ ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑅 ) )
48 42 47 eqtrd ⊢ ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ( ◡ 𝐹 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑅 ) )
49 10 36 48 3jca ⊢ ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ( ◡ 𝐹 : 𝐶 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐶 ( ◡ 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ∧ ( ◡ 𝐹 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑅 ) ) )
50 2 1 18 17 38 37 ismhm ⊢ ( ◡ 𝐹 ∈ ( 𝑆 MndHom 𝑅 ) ↔ ( ( 𝑆 ∈ Mnd ∧ 𝑅 ∈ Mnd ) ∧ ( ◡ 𝐹 : 𝐶 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐶 ( ◡ 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ◡ 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ∧ ( ◡ 𝐹 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑅 ) ) ) )
51 6 49 50 sylanbrc ⊢ ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) → ◡ 𝐹 ∈ ( 𝑆 MndHom 𝑅 ) )
52 1 2 mhmf ⊢ ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) → 𝐹 : 𝐵 ⟶ 𝐶 )
53 52 adantr ⊢ ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 MndHom 𝑅 ) ) → 𝐹 : 𝐵 ⟶ 𝐶 )
54 53 ffnd ⊢ ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 MndHom 𝑅 ) ) → 𝐹 Fn 𝐵 )
55 2 1 mhmf ⊢ ( ◡ 𝐹 ∈ ( 𝑆 MndHom 𝑅 ) → ◡ 𝐹 : 𝐶 ⟶ 𝐵 )
56 55 adantl ⊢ ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 MndHom 𝑅 ) ) → ◡ 𝐹 : 𝐶 ⟶ 𝐵 )
57 56 ffnd ⊢ ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 MndHom 𝑅 ) ) → ◡ 𝐹 Fn 𝐶 )
58 dff1o4 ⊢ ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ↔ ( 𝐹 Fn 𝐵 ∧ ◡ 𝐹 Fn 𝐶 ) )
59 54 57 58 sylanbrc ⊢ ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 MndHom 𝑅 ) ) → 𝐹 : 𝐵 –1-1-onto→ 𝐶 )
60 51 59 impbida ⊢ ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) → ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ↔ ◡ 𝐹 ∈ ( 𝑆 MndHom 𝑅 ) ) )