Metamath Proof Explorer


Theorem mgcval

Description: Monotone Galois connection between two functions F and G . If this relation is satisfied, F is called the lower adjoint of G , and G is called the upper adjoint of F .

Technically, this is implemented as an operation taking a pair of structures V and W , expected to be posets, which gives a relation between pairs of functions F and G .

If such a relation exists, it can be proven to be unique.

Galois connections generalize the fundamental theorem of Galois theory about the correspondence between subgroups and subfields. (Contributed by Thierry Arnoux, 23-Apr-2024)

Ref Expression
Hypotheses mgcoval.1 A = Base V
mgcoval.2 B = Base W
mgcoval.3 ˙ = V
mgcoval.4 No typesetting found for |- .c_ = ( le ` W ) with typecode |-
mgcval.1 No typesetting found for |- H = ( V MGalConn W ) with typecode |-
mgcval.2 φ V Proset
mgcval.3 φ W Proset
Assertion mgcval Could not format assertion : No typesetting found for |- ( ph -> ( F H G <-> ( ( F : A --> B /\ G : B --> A ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 mgcoval.1 A = Base V
2 mgcoval.2 B = Base W
3 mgcoval.3 ˙ = V
4 mgcoval.4 Could not format .c_ = ( le ` W ) : No typesetting found for |- .c_ = ( le ` W ) with typecode |-
5 mgcval.1 Could not format H = ( V MGalConn W ) : No typesetting found for |- H = ( V MGalConn W ) with typecode |-
6 mgcval.2 φ V Proset
7 mgcval.3 φ W Proset
8 1 2 3 4 mgcoval Could not format ( ( V e. Proset /\ W e. Proset ) -> ( V MGalConn W ) = { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } ) : No typesetting found for |- ( ( V e. Proset /\ W e. Proset ) -> ( V MGalConn W ) = { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } ) with typecode |-
9 6 7 8 syl2anc Could not format ( ph -> ( V MGalConn W ) = { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } ) : No typesetting found for |- ( ph -> ( V MGalConn W ) = { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } ) with typecode |-
10 5 9 syl5eq Could not format ( ph -> H = { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } ) : No typesetting found for |- ( ph -> H = { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } ) with typecode |-
11 10 breqd Could not format ( ph -> ( F H G <-> F { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } G ) ) : No typesetting found for |- ( ph -> ( F H G <-> F { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } G ) ) with typecode |-
12 fveq1 f = F f x = F x
13 12 adantr f = F g = G f x = F x
14 13 breq1d Could not format ( ( f = F /\ g = G ) -> ( ( f ` x ) .c_ y <-> ( F ` x ) .c_ y ) ) : No typesetting found for |- ( ( f = F /\ g = G ) -> ( ( f ` x ) .c_ y <-> ( F ` x ) .c_ y ) ) with typecode |-
15 fveq1 g = G g y = G y
16 15 adantl f = F g = G g y = G y
17 16 breq2d f = F g = G x ˙ g y x ˙ G y
18 14 17 bibi12d Could not format ( ( f = F /\ g = G ) -> ( ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) <-> ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) : No typesetting found for |- ( ( f = F /\ g = G ) -> ( ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) <-> ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) with typecode |-
19 18 2ralbidv Could not format ( ( f = F /\ g = G ) -> ( A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) <-> A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) : No typesetting found for |- ( ( f = F /\ g = G ) -> ( A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) <-> A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) with typecode |-
20 eqid Could not format { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } = { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } : No typesetting found for |- { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } = { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } with typecode |-
21 19 20 brab2a Could not format ( F { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } G <-> ( ( F e. ( B ^m A ) /\ G e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) : No typesetting found for |- ( F { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } G <-> ( ( F e. ( B ^m A ) /\ G e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) with typecode |-
22 2 fvexi B V
23 1 fvexi A V
24 22 23 elmap F B A F : A B
25 23 22 elmap G A B G : B A
26 24 25 anbi12i F B A G A B F : A B G : B A
27 26 anbi1i Could not format ( ( ( F e. ( B ^m A ) /\ G e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) <-> ( ( F : A --> B /\ G : B --> A ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) : No typesetting found for |- ( ( ( F e. ( B ^m A ) /\ G e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) <-> ( ( F : A --> B /\ G : B --> A ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) with typecode |-
28 21 27 bitr2i Could not format ( ( ( F : A --> B /\ G : B --> A ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) <-> F { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } G ) : No typesetting found for |- ( ( ( F : A --> B /\ G : B --> A ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) <-> F { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } G ) with typecode |-
29 11 28 bitr4di Could not format ( ph -> ( F H G <-> ( ( F : A --> B /\ G : B --> A ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) ) : No typesetting found for |- ( ph -> ( F H G <-> ( ( F : A --> B /\ G : B --> A ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) ) with typecode |-