Metamath Proof Explorer

Theorem poml4N

Description: Orthomodular law for projective lattices. Lemma 3.3(1) in Holland95 p. 215. (Contributed by NM, 25-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses poml4.a 
|- A = ( Atoms ` K )
poml4.p 
|- ._|_ = ( _|_P ` K )
Assertion poml4N 
|- ( ( K e. HL /\ X C_ A /\ Y C_ A ) -> ( ( X C_ Y /\ ( ._|_ ` ( ._|_ ` Y ) ) = Y ) -> ( ( ._|_ ` ( ( ._|_ ` X ) i^i Y ) ) i^i Y ) = ( ._|_ ` ( ._|_ ` X ) ) ) )

Proof

Step Hyp Ref Expression
1 poml4.a 
 |-  A = ( Atoms ` K )
2 poml4.p 
 |-  ._|_ = ( _|_P ` K )
3 eqcom 
 |-  ( ( ._|_ ` ( ._|_ ` Y ) ) = Y <-> Y = ( ._|_ ` ( ._|_ ` Y ) ) )
4 eqid 
 |-  ( lub ` K ) = ( lub ` K )
5 eqid 
 |-  ( pmap ` K ) = ( pmap ` K )
6 4 1 5 2 2polvalN 
 |-  ( ( K e. HL /\ Y C_ A ) -> ( ._|_ ` ( ._|_ ` Y ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) )
7 6 3adant2 
 |-  ( ( K e. HL /\ X C_ A /\ Y C_ A ) -> ( ._|_ ` ( ._|_ ` Y ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) )
8 7 eqeq2d 
 |-  ( ( K e. HL /\ X C_ A /\ Y C_ A ) -> ( Y = ( ._|_ ` ( ._|_ ` Y ) ) <-> Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) )
9 8 biimpd 
 |-  ( ( K e. HL /\ X C_ A /\ Y C_ A ) -> ( Y = ( ._|_ ` ( ._|_ ` Y ) ) -> Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) )
10 3 9 biimtrid 
 |-  ( ( K e. HL /\ X C_ A /\ Y C_ A ) -> ( ( ._|_ ` ( ._|_ ` Y ) ) = Y -> Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) )
11 simpl1 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> K e. HL )
12 hloml 
 |-  ( K e. HL -> K e. OML )
13 11 12 syl 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> K e. OML )
14 hlclat 
 |-  ( K e. HL -> K e. CLat )
15 11 14 syl 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> K e. CLat )
16 simpl2 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> X C_ A )
17 eqid 
 |-  ( Base ` K ) = ( Base ` K )
18 17 1 atssbase 
 |-  A C_ ( Base ` K )
19 16 18 sstrdi 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> X C_ ( Base ` K ) )
20 17 4 clatlubcl 
 |-  ( ( K e. CLat /\ X C_ ( Base ` K ) ) -> ( ( lub ` K ) ` X ) e. ( Base ` K ) )
21 15 19 20 syl2anc 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> ( ( lub ` K ) ` X ) e. ( Base ` K ) )
22 simpl3 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> Y C_ A )
23 22 18 sstrdi 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> Y C_ ( Base ` K ) )
24 17 4 clatlubcl 
 |-  ( ( K e. CLat /\ Y C_ ( Base ` K ) ) -> ( ( lub ` K ) ` Y ) e. ( Base ` K ) )
25 15 23 24 syl2anc 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> ( ( lub ` K ) ` Y ) e. ( Base ` K ) )
26 13 21 25 3jca 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> ( K e. OML /\ ( ( lub ` K ) ` X ) e. ( Base ` K ) /\ ( ( lub ` K ) ` Y ) e. ( Base ` K ) ) )
27 simprl 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> X C_ Y )
28 eqid 
 |-  ( le ` K ) = ( le ` K )
29 17 28 4 lubss 
 |-  ( ( K e. CLat /\ Y C_ ( Base ` K ) /\ X C_ Y ) -> ( ( lub ` K ) ` X ) ( le ` K ) ( ( lub ` K ) ` Y ) )
30 15 23 27 29 syl3anc 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> ( ( lub ` K ) ` X ) ( le ` K ) ( ( lub ` K ) ` Y ) )
31 eqid 
 |-  ( meet ` K ) = ( meet ` K )
32 eqid 
 |-  ( oc ` K ) = ( oc ` K )
33 17 28 31 32 omllaw4 
 |-  ( ( K e. OML /\ ( ( lub ` K ) ` X ) e. ( Base ` K ) /\ ( ( lub ` K ) ` Y ) e. ( Base ` K ) ) -> ( ( ( lub ` K ) ` X ) ( le ` K ) ( ( lub ` K ) ` Y ) -> ( ( ( oc ` K ) ` ( ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) = ( ( lub ` K ) ` X ) ) )
34 26 30 33 sylc 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> ( ( ( oc ` K ) ` ( ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) = ( ( lub ` K ) ` X ) )
35 34 fveq2d 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> ( ( pmap ` K ) ` ( ( ( oc ` K ) ` ( ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` X ) ) )
36 4 32 1 5 2 polval2N 
 |-  ( ( K e. HL /\ X C_ A ) -> ( ._|_ ` X ) = ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) )
37 11 16 36 syl2anc 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> ( ._|_ ` X ) = ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) )
38 simprr 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) )
39 37 38 ineq12d 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> ( ( ._|_ ` X ) i^i Y ) = ( ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) i^i ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) )
40 hlop 
 |-  ( K e. HL -> K e. OP )
41 11 40 syl 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> K e. OP )
42 17 32 opoccl 
 |-  ( ( K e. OP /\ ( ( lub ` K ) ` X ) e. ( Base ` K ) ) -> ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) e. ( Base ` K ) )
43 41 21 42 syl2anc 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) e. ( Base ` K ) )
44 17 31 1 5 pmapmeet 
 |-  ( ( K e. HL /\ ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) e. ( Base ` K ) /\ ( ( lub ` K ) ` Y ) e. ( Base ` K ) ) -> ( ( pmap ` K ) ` ( ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) ) = ( ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) i^i ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) )
45 11 43 25 44 syl3anc 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> ( ( pmap ` K ) ` ( ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) ) = ( ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) i^i ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) )
46 39 45 eqtr4d 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> ( ( ._|_ ` X ) i^i Y ) = ( ( pmap ` K ) ` ( ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) ) )
47 46 fveq2d 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> ( ._|_ ` ( ( ._|_ ` X ) i^i Y ) ) = ( ._|_ ` ( ( pmap ` K ) ` ( ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) ) ) )
48 11 hllatd 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> K e. Lat )
49 17 31 latmcl 
 |-  ( ( K e. Lat /\ ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) e. ( Base ` K ) /\ ( ( lub ` K ) ` Y ) e. ( Base ` K ) ) -> ( ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) e. ( Base ` K ) )
50 48 43 25 49 syl3anc 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> ( ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) e. ( Base ` K ) )
51 17 32 5 2 polpmapN 
 |-  ( ( K e. HL /\ ( ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) e. ( Base ` K ) ) -> ( ._|_ ` ( ( pmap ` K ) ` ( ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) ) ) = ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) ) ) )
52 11 50 51 syl2anc 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> ( ._|_ ` ( ( pmap ` K ) ` ( ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) ) ) = ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) ) ) )
53 47 52 eqtrd 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> ( ._|_ ` ( ( ._|_ ` X ) i^i Y ) ) = ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) ) ) )
54 53 38 ineq12d 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> ( ( ._|_ ` ( ( ._|_ ` X ) i^i Y ) ) i^i Y ) = ( ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) ) ) i^i ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) )
55 17 32 opoccl 
 |-  ( ( K e. OP /\ ( ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) e. ( Base ` K ) ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) ) e. ( Base ` K ) )
56 41 50 55 syl2anc 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) ) e. ( Base ` K ) )
57 17 31 1 5 pmapmeet 
 |-  ( ( K e. HL /\ ( ( oc ` K ) ` ( ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) ) e. ( Base ` K ) /\ ( ( lub ` K ) ` Y ) e. ( Base ` K ) ) -> ( ( pmap ` K ) ` ( ( ( oc ` K ) ` ( ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) ) = ( ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) ) ) i^i ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) )
58 11 56 25 57 syl3anc 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> ( ( pmap ` K ) ` ( ( ( oc ` K ) ` ( ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) ) = ( ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) ) ) i^i ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) )
59 54 58 eqtr4d 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> ( ( ._|_ ` ( ( ._|_ ` X ) i^i Y ) ) i^i Y ) = ( ( pmap ` K ) ` ( ( ( oc ` K ) ` ( ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) ) ( meet ` K ) ( ( lub ` K ) ` Y ) ) ) )
60 4 1 5 2 2polvalN 
 |-  ( ( K e. HL /\ X C_ A ) -> ( ._|_ ` ( ._|_ ` X ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` X ) ) )
61 11 16 60 syl2anc 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> ( ._|_ ` ( ._|_ ` X ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` X ) ) )
62 35 59 61 3eqtr4d 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) ) -> ( ( ._|_ ` ( ( ._|_ ` X ) i^i Y ) ) i^i Y ) = ( ._|_ ` ( ._|_ ` X ) ) )
63 62 ex 
 |-  ( ( K e. HL /\ X C_ A /\ Y C_ A ) -> ( ( X C_ Y /\ Y = ( ( pmap ` K ) ` ( ( lub ` K ) ` Y ) ) ) -> ( ( ._|_ ` ( ( ._|_ ` X ) i^i Y ) ) i^i Y ) = ( ._|_ ` ( ._|_ ` X ) ) ) )
64 10 63 sylan2d 
 |-  ( ( K e. HL /\ X C_ A /\ Y C_ A ) -> ( ( X C_ Y /\ ( ._|_ ` ( ._|_ ` Y ) ) = Y ) -> ( ( ._|_ ` ( ( ._|_ ` X ) i^i Y ) ) i^i Y ) = ( ._|_ ` ( ._|_ ` X ) ) ) )