Metamath Proof Explorer

Theorem pl42N

Description: Law holding in a Hilbert lattice that fails in orthomodular lattice L42 (Figure 7 in MegPav2000 p. 2366). (Contributed by NM, 8-Apr-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pl42.b 
|- B = ( Base ` K )
pl42.l 
|- .<_ = ( le ` K )
pl42.j 
|- .\/ = ( join ` K )
pl42.m 
|- ./\ = ( meet ` K )
pl42.o 
|- ._|_ = ( oc ` K )
Assertion pl42N 
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( ( X .<_ ( ._|_ ` Y ) /\ Z .<_ ( ._|_ ` W ) ) -> ( ( ( ( X .\/ Y ) ./\ Z ) .\/ W ) ./\ V ) .<_ ( ( X .\/ Y ) .\/ ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pl42.b 
 |-  B = ( Base ` K )
2 pl42.l 
 |-  .<_ = ( le ` K )
3 pl42.j 
 |-  .\/ = ( join ` K )
4 pl42.m 
 |-  ./\ = ( meet ` K )
5 pl42.o 
 |-  ._|_ = ( oc ` K )
6 eqid 
 |-  ( pmap ` K ) = ( pmap ` K )
7 eqid 
 |-  ( +P ` K ) = ( +P ` K )
8 1 2 3 4 5 6 7 pl42lem4N 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( ( X .<_ ( ._|_ ` Y ) /\ Z .<_ ( ._|_ ` W ) ) -> ( ( pmap ` K ) ` ( ( ( ( X .\/ Y ) ./\ Z ) .\/ W ) ./\ V ) ) C_ ( ( pmap ` K ) ` ( ( X .\/ Y ) .\/ ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) ) ) )
9 simpl1 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> K e. HL )
10 9 hllatd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> K e. Lat )
11 simpl2 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> X e. B )
12 simpl3 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> Y e. B )
13 1 3 latjcl 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .\/ Y ) e. B )
14 10 11 12 13 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( X .\/ Y ) e. B )
15 simpr1 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> Z e. B )
16 1 4 latmcl 
 |-  ( ( K e. Lat /\ ( X .\/ Y ) e. B /\ Z e. B ) -> ( ( X .\/ Y ) ./\ Z ) e. B )
17 10 14 15 16 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( ( X .\/ Y ) ./\ Z ) e. B )
18 simpr2 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> W e. B )
19 1 3 latjcl 
 |-  ( ( K e. Lat /\ ( ( X .\/ Y ) ./\ Z ) e. B /\ W e. B ) -> ( ( ( X .\/ Y ) ./\ Z ) .\/ W ) e. B )
20 10 17 18 19 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( ( ( X .\/ Y ) ./\ Z ) .\/ W ) e. B )
21 simpr3 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> V e. B )
22 1 4 latmcl 
 |-  ( ( K e. Lat /\ ( ( ( X .\/ Y ) ./\ Z ) .\/ W ) e. B /\ V e. B ) -> ( ( ( ( X .\/ Y ) ./\ Z ) .\/ W ) ./\ V ) e. B )
23 10 20 21 22 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( ( ( ( X .\/ Y ) ./\ Z ) .\/ W ) ./\ V ) e. B )
24 1 3 latjcl 
 |-  ( ( K e. Lat /\ X e. B /\ W e. B ) -> ( X .\/ W ) e. B )
25 10 11 18 24 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( X .\/ W ) e. B )
26 1 3 latjcl 
 |-  ( ( K e. Lat /\ Y e. B /\ V e. B ) -> ( Y .\/ V ) e. B )
27 10 12 21 26 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( Y .\/ V ) e. B )
28 1 4 latmcl 
 |-  ( ( K e. Lat /\ ( X .\/ W ) e. B /\ ( Y .\/ V ) e. B ) -> ( ( X .\/ W ) ./\ ( Y .\/ V ) ) e. B )
29 10 25 27 28 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( ( X .\/ W ) ./\ ( Y .\/ V ) ) e. B )
30 1 3 latjcl 
 |-  ( ( K e. Lat /\ ( X .\/ Y ) e. B /\ ( ( X .\/ W ) ./\ ( Y .\/ V ) ) e. B ) -> ( ( X .\/ Y ) .\/ ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) e. B )
31 10 14 29 30 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( ( X .\/ Y ) .\/ ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) e. B )
32 1 2 6 pmaple 
 |-  ( ( K e. HL /\ ( ( ( ( X .\/ Y ) ./\ Z ) .\/ W ) ./\ V ) e. B /\ ( ( X .\/ Y ) .\/ ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) e. B ) -> ( ( ( ( ( X .\/ Y ) ./\ Z ) .\/ W ) ./\ V ) .<_ ( ( X .\/ Y ) .\/ ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) <-> ( ( pmap ` K ) ` ( ( ( ( X .\/ Y ) ./\ Z ) .\/ W ) ./\ V ) ) C_ ( ( pmap ` K ) ` ( ( X .\/ Y ) .\/ ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) ) ) )
33 9 23 31 32 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( ( ( ( ( X .\/ Y ) ./\ Z ) .\/ W ) ./\ V ) .<_ ( ( X .\/ Y ) .\/ ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) <-> ( ( pmap ` K ) ` ( ( ( ( X .\/ Y ) ./\ Z ) .\/ W ) ./\ V ) ) C_ ( ( pmap ` K ) ` ( ( X .\/ Y ) .\/ ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) ) ) )
34 8 33 sylibrd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( ( X .<_ ( ._|_ ` Y ) /\ Z .<_ ( ._|_ ` W ) ) -> ( ( ( ( X .\/ Y ) ./\ Z ) .\/ W ) ./\ V ) .<_ ( ( X .\/ Y ) .\/ ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) ) )