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 ) ) ) ) )