Metamath Proof Explorer


Theorem pl42lem2N

Description: Lemma for pl42N . (Contributed by NM, 8-Apr-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pl42lem.b
|- B = ( Base ` K )
pl42lem.l
|- .<_ = ( le ` K )
pl42lem.j
|- .\/ = ( join ` K )
pl42lem.m
|- ./\ = ( meet ` K )
pl42lem.o
|- ._|_ = ( oc ` K )
pl42lem.f
|- F = ( pmap ` K )
pl42lem.p
|- .+ = ( +P ` K )
Assertion pl42lem2N
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( ( ( F ` X ) .+ ( F ` Y ) ) .+ ( ( ( F ` X ) .+ ( F ` W ) ) i^i ( ( F ` Y ) .+ ( F ` V ) ) ) ) C_ ( F ` ( ( X .\/ Y ) .\/ ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pl42lem.b
 |-  B = ( Base ` K )
2 pl42lem.l
 |-  .<_ = ( le ` K )
3 pl42lem.j
 |-  .\/ = ( join ` K )
4 pl42lem.m
 |-  ./\ = ( meet ` K )
5 pl42lem.o
 |-  ._|_ = ( oc ` K )
6 pl42lem.f
 |-  F = ( pmap ` K )
7 pl42lem.p
 |-  .+ = ( +P ` K )
8 simpl1
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> K e. HL )
9 8 hllatd
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> K e. Lat )
10 simpl2
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> X e. B )
11 simpl3
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> Y e. B )
12 1 3 latjcl
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .\/ Y ) e. B )
13 9 10 11 12 syl3anc
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( X .\/ Y ) e. B )
14 eqid
 |-  ( Atoms ` K ) = ( Atoms ` K )
15 1 14 6 pmapssat
 |-  ( ( K e. HL /\ ( X .\/ Y ) e. B ) -> ( F ` ( X .\/ Y ) ) C_ ( Atoms ` K ) )
16 8 13 15 syl2anc
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( F ` ( X .\/ Y ) ) C_ ( Atoms ` K ) )
17 simpr2
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> W e. B )
18 1 3 latjcl
 |-  ( ( K e. Lat /\ X e. B /\ W e. B ) -> ( X .\/ W ) e. B )
19 9 10 17 18 syl3anc
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( X .\/ W ) e. B )
20 simpr3
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> V e. B )
21 1 3 latjcl
 |-  ( ( K e. Lat /\ Y e. B /\ V e. B ) -> ( Y .\/ V ) e. B )
22 9 11 20 21 syl3anc
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( Y .\/ V ) e. B )
23 1 4 latmcl
 |-  ( ( K e. Lat /\ ( X .\/ W ) e. B /\ ( Y .\/ V ) e. B ) -> ( ( X .\/ W ) ./\ ( Y .\/ V ) ) e. B )
24 9 19 22 23 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 )
25 1 14 6 pmapssat
 |-  ( ( K e. HL /\ ( ( X .\/ W ) ./\ ( Y .\/ V ) ) e. B ) -> ( F ` ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) C_ ( Atoms ` K ) )
26 8 24 25 syl2anc
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( F ` ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) C_ ( Atoms ` K ) )
27 8 16 26 3jca
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( K e. HL /\ ( F ` ( X .\/ Y ) ) C_ ( Atoms ` K ) /\ ( F ` ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) C_ ( Atoms ` K ) ) )
28 1 3 6 7 pmapjoin
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( F ` X ) .+ ( F ` Y ) ) C_ ( F ` ( X .\/ Y ) ) )
29 9 10 11 28 syl3anc
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( ( F ` X ) .+ ( F ` Y ) ) C_ ( F ` ( X .\/ Y ) ) )
30 1 3 6 7 pmapjoin
 |-  ( ( K e. Lat /\ X e. B /\ W e. B ) -> ( ( F ` X ) .+ ( F ` W ) ) C_ ( F ` ( X .\/ W ) ) )
31 9 10 17 30 syl3anc
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( ( F ` X ) .+ ( F ` W ) ) C_ ( F ` ( X .\/ W ) ) )
32 1 3 6 7 pmapjoin
 |-  ( ( K e. Lat /\ Y e. B /\ V e. B ) -> ( ( F ` Y ) .+ ( F ` V ) ) C_ ( F ` ( Y .\/ V ) ) )
33 9 11 20 32 syl3anc
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( ( F ` Y ) .+ ( F ` V ) ) C_ ( F ` ( Y .\/ V ) ) )
34 ss2in
 |-  ( ( ( ( F ` X ) .+ ( F ` W ) ) C_ ( F ` ( X .\/ W ) ) /\ ( ( F ` Y ) .+ ( F ` V ) ) C_ ( F ` ( Y .\/ V ) ) ) -> ( ( ( F ` X ) .+ ( F ` W ) ) i^i ( ( F ` Y ) .+ ( F ` V ) ) ) C_ ( ( F ` ( X .\/ W ) ) i^i ( F ` ( Y .\/ V ) ) ) )
35 31 33 34 syl2anc
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( ( ( F ` X ) .+ ( F ` W ) ) i^i ( ( F ` Y ) .+ ( F ` V ) ) ) C_ ( ( F ` ( X .\/ W ) ) i^i ( F ` ( Y .\/ V ) ) ) )
36 1 4 14 6 pmapmeet
 |-  ( ( K e. HL /\ ( X .\/ W ) e. B /\ ( Y .\/ V ) e. B ) -> ( F ` ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) = ( ( F ` ( X .\/ W ) ) i^i ( F ` ( Y .\/ V ) ) ) )
37 8 19 22 36 syl3anc
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( F ` ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) = ( ( F ` ( X .\/ W ) ) i^i ( F ` ( Y .\/ V ) ) ) )
38 35 37 sseqtrrd
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( ( ( F ` X ) .+ ( F ` W ) ) i^i ( ( F ` Y ) .+ ( F ` V ) ) ) C_ ( F ` ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) )
39 29 38 jca
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( ( ( F ` X ) .+ ( F ` Y ) ) C_ ( F ` ( X .\/ Y ) ) /\ ( ( ( F ` X ) .+ ( F ` W ) ) i^i ( ( F ` Y ) .+ ( F ` V ) ) ) C_ ( F ` ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) ) )
40 14 7 paddss12
 |-  ( ( K e. HL /\ ( F ` ( X .\/ Y ) ) C_ ( Atoms ` K ) /\ ( F ` ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) C_ ( Atoms ` K ) ) -> ( ( ( ( F ` X ) .+ ( F ` Y ) ) C_ ( F ` ( X .\/ Y ) ) /\ ( ( ( F ` X ) .+ ( F ` W ) ) i^i ( ( F ` Y ) .+ ( F ` V ) ) ) C_ ( F ` ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) ) -> ( ( ( F ` X ) .+ ( F ` Y ) ) .+ ( ( ( F ` X ) .+ ( F ` W ) ) i^i ( ( F ` Y ) .+ ( F ` V ) ) ) ) C_ ( ( F ` ( X .\/ Y ) ) .+ ( F ` ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) ) ) )
41 27 39 40 sylc
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( ( ( F ` X ) .+ ( F ` Y ) ) .+ ( ( ( F ` X ) .+ ( F ` W ) ) i^i ( ( F ` Y ) .+ ( F ` V ) ) ) ) C_ ( ( F ` ( X .\/ Y ) ) .+ ( F ` ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) ) )
42 1 3 6 7 pmapjoin
 |-  ( ( K e. Lat /\ ( X .\/ Y ) e. B /\ ( ( X .\/ W ) ./\ ( Y .\/ V ) ) e. B ) -> ( ( F ` ( X .\/ Y ) ) .+ ( F ` ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) ) C_ ( F ` ( ( X .\/ Y ) .\/ ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) ) )
43 9 13 24 42 syl3anc
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( ( F ` ( X .\/ Y ) ) .+ ( F ` ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) ) C_ ( F ` ( ( X .\/ Y ) .\/ ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) ) )
44 41 43 sstrd
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( ( ( F ` X ) .+ ( F ` Y ) ) .+ ( ( ( F ` X ) .+ ( F ` W ) ) i^i ( ( F ` Y ) .+ ( F ` V ) ) ) ) C_ ( F ` ( ( X .\/ Y ) .\/ ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) ) )