Metamath Proof Explorer

Theorem mgccnv

Description: The inverse Galois connection is the Galois connection of the dual orders. (Contributed by Thierry Arnoux, 26-Apr-2024)

Ref Expression
Hypotheses mgccnv.1 No typesetting found for |- H = ( V MGalConn W ) with typecode |-
mgccnv.2 No typesetting found for |- M = ( ( ODual ` W ) MGalConn ( ODual ` V ) ) with typecode |-
Assertion mgccnv ⊢ V ∈ Proset ∧ W ∈ Proset → F H G ↔ G M F

Proof

Step Hyp Ref Expression
1 mgccnv.1 Could not format H = ( V MGalConn W ) : No typesetting found for |- H = ( V MGalConn W ) with typecode |-
2 mgccnv.2 Could not format M = ( ( ODual ` W ) MGalConn ( ODual ` V ) ) : No typesetting found for |- M = ( ( ODual ` W ) MGalConn ( ODual ` V ) ) with typecode |-
3 ancom ⊢ F : Base V ⟶ Base W ∧ G : Base W ⟶ Base V ↔ G : Base W ⟶ Base V ∧ F : Base V ⟶ Base W
4 3 a1i ⊢ V ∈ Proset ∧ W ∈ Proset → F : Base V ⟶ Base W ∧ G : Base W ⟶ Base V ↔ G : Base W ⟶ Base V ∧ F : Base V ⟶ Base W
5 ralcom ⊢ ∀ x ∈ Base V ∀ y ∈ Base W F ⁡ x ≤ W y ↔ x ≤ V G ⁡ y ↔ ∀ y ∈ Base W ∀ x ∈ Base V F ⁡ x ≤ W y ↔ x ≤ V G ⁡ y
6 bicom ⊢ F ⁡ x ≤ W y ↔ x ≤ V G ⁡ y ↔ x ≤ V G ⁡ y ↔ F ⁡ x ≤ W y
7 fvex ⊢ G ⁡ y ∈ V
8 vex ⊢ x ∈ V
9 7 8 brcnv ⊢ G ⁡ y ≤ V -1 x ↔ x ≤ V G ⁡ y
10 9 bicomi ⊢ x ≤ V G ⁡ y ↔ G ⁡ y ≤ V -1 x
11 10 a1i ⊢ V ∈ Proset ∧ W ∈ Proset ∧ y ∈ Base W ∧ x ∈ Base V → x ≤ V G ⁡ y ↔ G ⁡ y ≤ V -1 x
12 vex ⊢ y ∈ V
13 fvex ⊢ F ⁡ x ∈ V
14 12 13 brcnv ⊢ y ≤ W -1 F ⁡ x ↔ F ⁡ x ≤ W y
15 14 bicomi ⊢ F ⁡ x ≤ W y ↔ y ≤ W -1 F ⁡ x
16 15 a1i ⊢ V ∈ Proset ∧ W ∈ Proset ∧ y ∈ Base W ∧ x ∈ Base V → F ⁡ x ≤ W y ↔ y ≤ W -1 F ⁡ x
17 11 16 bibi12d ⊢ V ∈ Proset ∧ W ∈ Proset ∧ y ∈ Base W ∧ x ∈ Base V → x ≤ V G ⁡ y ↔ F ⁡ x ≤ W y ↔ G ⁡ y ≤ V -1 x ↔ y ≤ W -1 F ⁡ x
18 6 17 syl5bb ⊢ V ∈ Proset ∧ W ∈ Proset ∧ y ∈ Base W ∧ x ∈ Base V → F ⁡ x ≤ W y ↔ x ≤ V G ⁡ y ↔ G ⁡ y ≤ V -1 x ↔ y ≤ W -1 F ⁡ x
19 18 ralbidva ⊢ V ∈ Proset ∧ W ∈ Proset ∧ y ∈ Base W → ∀ x ∈ Base V F ⁡ x ≤ W y ↔ x ≤ V G ⁡ y ↔ ∀ x ∈ Base V G ⁡ y ≤ V -1 x ↔ y ≤ W -1 F ⁡ x
20 19 ralbidva ⊢ V ∈ Proset ∧ W ∈ Proset → ∀ y ∈ Base W ∀ x ∈ Base V F ⁡ x ≤ W y ↔ x ≤ V G ⁡ y ↔ ∀ y ∈ Base W ∀ x ∈ Base V G ⁡ y ≤ V -1 x ↔ y ≤ W -1 F ⁡ x
21 5 20 syl5bb ⊢ V ∈ Proset ∧ W ∈ Proset → ∀ x ∈ Base V ∀ y ∈ Base W F ⁡ x ≤ W y ↔ x ≤ V G ⁡ y ↔ ∀ y ∈ Base W ∀ x ∈ Base V G ⁡ y ≤ V -1 x ↔ y ≤ W -1 F ⁡ x
22 4 21 anbi12d ⊢ V ∈ Proset ∧ W ∈ Proset → F : Base V ⟶ Base W ∧ G : Base W ⟶ Base V ∧ ∀ x ∈ Base V ∀ y ∈ Base W F ⁡ x ≤ W y ↔ x ≤ V G ⁡ y ↔ G : Base W ⟶ Base V ∧ F : Base V ⟶ Base W ∧ ∀ y ∈ Base W ∀ x ∈ Base V G ⁡ y ≤ V -1 x ↔ y ≤ W -1 F ⁡ x
23 eqid ⊢ Base V = Base V
24 eqid ⊢ Base W = Base W
25 eqid ⊢ ≤ V = ≤ V
26 eqid ⊢ ≤ W = ≤ W
27 simpl ⊢ V ∈ Proset ∧ W ∈ Proset → V ∈ Proset
28 simpr ⊢ V ∈ Proset ∧ W ∈ Proset → W ∈ Proset
29 23 24 25 26 1 27 28 mgcval ⊢ V ∈ Proset ∧ W ∈ Proset → F H G ↔ F : Base V ⟶ Base W ∧ G : Base W ⟶ Base V ∧ ∀ x ∈ Base V ∀ y ∈ Base W F ⁡ x ≤ W y ↔ x ≤ V G ⁡ y
30 eqid ⊢ ODual ⁡ W = ODual ⁡ W
31 30 24 odubas ⊢ Base W = Base ODual ⁡ W
32 eqid ⊢ ODual ⁡ V = ODual ⁡ V
33 32 23 odubas ⊢ Base V = Base ODual ⁡ V
34 30 26 oduleval ⊢ ≤ W -1 = ≤ ODual ⁡ W
35 32 25 oduleval ⊢ ≤ V -1 = ≤ ODual ⁡ V
36 30 oduprs ⊢ W ∈ Proset → ODual ⁡ W ∈ Proset
37 28 36 syl ⊢ V ∈ Proset ∧ W ∈ Proset → ODual ⁡ W ∈ Proset
38 32 oduprs ⊢ V ∈ Proset → ODual ⁡ V ∈ Proset
39 27 38 syl ⊢ V ∈ Proset ∧ W ∈ Proset → ODual ⁡ V ∈ Proset
40 31 33 34 35 2 37 39 mgcval ⊢ V ∈ Proset ∧ W ∈ Proset → G M F ↔ G : Base W ⟶ Base V ∧ F : Base V ⟶ Base W ∧ ∀ y ∈ Base W ∀ x ∈ Base V G ⁡ y ≤ V -1 x ↔ y ≤ W -1 F ⁡ x
41 22 29 40 3bitr4d ⊢ V ∈ Proset ∧ W ∈ Proset → F H G ↔ G M F