Metamath Proof Explorer

Theorem pl42lem1N

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 pl42lem1N 
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( ( X .<_ ( ._|_ ` Y ) /\ Z .<_ ( ._|_ ` W ) ) -> ( F ` ( ( ( ( X .\/ Y ) ./\ Z ) .\/ W ) ./\ V ) ) = ( ( ( ( ( F ` X ) .+ ( F ` Y ) ) i^i ( F ` Z ) ) .+ ( F ` W ) ) i^i ( F ` 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 simp11 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) /\ ( X .<_ ( ._|_ ` Y ) /\ Z .<_ ( ._|_ ` W ) ) ) -> K e. HL )
9 8 hllatd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) /\ ( X .<_ ( ._|_ ` Y ) /\ Z .<_ ( ._|_ ` W ) ) ) -> K e. Lat )
10 simp12 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) /\ ( X .<_ ( ._|_ ` Y ) /\ Z .<_ ( ._|_ ` W ) ) ) -> X e. B )
11 simp13 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) /\ ( X .<_ ( ._|_ ` Y ) /\ Z .<_ ( ._|_ ` W ) ) ) -> 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 ) /\ Z .<_ ( ._|_ ` W ) ) ) -> ( X .\/ Y ) e. B )
14 simp21 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) /\ ( X .<_ ( ._|_ ` Y ) /\ Z .<_ ( ._|_ ` W ) ) ) -> Z e. B )
15 1 4 latmcl 
 |-  ( ( K e. Lat /\ ( X .\/ Y ) e. B /\ Z e. B ) -> ( ( X .\/ Y ) ./\ Z ) e. B )
16 9 13 14 15 syl3anc 
 |-  ( ( ( 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 ) e. B )
17 simp22 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) /\ ( X .<_ ( ._|_ ` Y ) /\ Z .<_ ( ._|_ ` W ) ) ) -> W e. B )
18 1 3 latjcl 
 |-  ( ( K e. Lat /\ ( ( X .\/ Y ) ./\ Z ) e. B /\ W e. B ) -> ( ( ( X .\/ Y ) ./\ Z ) .\/ W ) e. B )
19 9 16 17 18 syl3anc 
 |-  ( ( ( 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 ) e. B )
20 simp23 
 |-  ( ( ( 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 )
21 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
22 1 4 21 6 pmapmeet 
 |-  ( ( K e. HL /\ ( ( ( X .\/ Y ) ./\ Z ) .\/ W ) e. B /\ V e. B ) -> ( F ` ( ( ( ( X .\/ Y ) ./\ Z ) .\/ W ) ./\ V ) ) = ( ( F ` ( ( ( X .\/ Y ) ./\ Z ) .\/ W ) ) i^i ( F ` V ) ) )
23 8 19 20 22 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) /\ ( X .<_ ( ._|_ ` Y ) /\ Z .<_ ( ._|_ ` W ) ) ) -> ( F ` ( ( ( ( X .\/ Y ) ./\ Z ) .\/ W ) ./\ V ) ) = ( ( F ` ( ( ( X .\/ Y ) ./\ Z ) .\/ W ) ) i^i ( F ` V ) ) )
24 hlop 
 |-  ( K e. HL -> K e. OP )
25 8 24 syl 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) /\ ( X .<_ ( ._|_ ` Y ) /\ Z .<_ ( ._|_ ` W ) ) ) -> K e. OP )
26 1 5 opoccl 
 |-  ( ( K e. OP /\ W e. B ) -> ( ._|_ ` W ) e. B )
27 25 17 26 syl2anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) /\ ( X .<_ ( ._|_ ` Y ) /\ Z .<_ ( ._|_ ` W ) ) ) -> ( ._|_ ` W ) e. B )
28 1 2 4 latmle2 
 |-  ( ( K e. Lat /\ ( X .\/ Y ) e. B /\ Z e. B ) -> ( ( X .\/ Y ) ./\ Z ) .<_ Z )
29 9 13 14 28 syl3anc 
 |-  ( ( ( 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 ) .<_ Z )
30 simp3r 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) /\ ( X .<_ ( ._|_ ` Y ) /\ Z .<_ ( ._|_ ` W ) ) ) -> Z .<_ ( ._|_ ` W ) )
31 1 2 9 16 14 27 29 30 lattrd 
 |-  ( ( ( 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 ) )
32 1 2 3 6 5 7 pmapojoinN 
 |-  ( ( ( K e. HL /\ ( ( X .\/ Y ) ./\ Z ) e. B /\ W e. B ) /\ ( ( X .\/ Y ) ./\ Z ) .<_ ( ._|_ ` W ) ) -> ( F ` ( ( ( X .\/ Y ) ./\ Z ) .\/ W ) ) = ( ( F ` ( ( X .\/ Y ) ./\ Z ) ) .+ ( F ` W ) ) )
33 8 16 17 31 32 syl31anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) /\ ( X .<_ ( ._|_ ` Y ) /\ Z .<_ ( ._|_ ` W ) ) ) -> ( F ` ( ( ( X .\/ Y ) ./\ Z ) .\/ W ) ) = ( ( F ` ( ( X .\/ Y ) ./\ Z ) ) .+ ( F ` W ) ) )
34 1 4 21 6 pmapmeet 
 |-  ( ( K e. HL /\ ( X .\/ Y ) e. B /\ Z e. B ) -> ( F ` ( ( X .\/ Y ) ./\ Z ) ) = ( ( F ` ( X .\/ Y ) ) i^i ( F ` Z ) ) )
35 8 13 14 34 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) /\ ( X .<_ ( ._|_ ` Y ) /\ Z .<_ ( ._|_ ` W ) ) ) -> ( F ` ( ( X .\/ Y ) ./\ Z ) ) = ( ( F ` ( X .\/ Y ) ) i^i ( F ` Z ) ) )
36 simp3l 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) /\ ( X .<_ ( ._|_ ` Y ) /\ Z .<_ ( ._|_ ` W ) ) ) -> X .<_ ( ._|_ ` Y ) )
37 1 2 3 6 5 7 pmapojoinN 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .<_ ( ._|_ ` Y ) ) -> ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) )
38 8 10 11 36 37 syl31anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) /\ ( X .<_ ( ._|_ ` Y ) /\ Z .<_ ( ._|_ ` W ) ) ) -> ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .+ ( F ` Y ) ) )
39 38 ineq1d 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) /\ ( X .<_ ( ._|_ ` Y ) /\ Z .<_ ( ._|_ ` W ) ) ) -> ( ( F ` ( X .\/ Y ) ) i^i ( F ` Z ) ) = ( ( ( F ` X ) .+ ( F ` Y ) ) i^i ( F ` Z ) ) )
40 35 39 eqtrd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) /\ ( X .<_ ( ._|_ ` Y ) /\ Z .<_ ( ._|_ ` W ) ) ) -> ( F ` ( ( X .\/ Y ) ./\ Z ) ) = ( ( ( F ` X ) .+ ( F ` Y ) ) i^i ( F ` Z ) ) )
41 40 oveq1d 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) /\ ( X .<_ ( ._|_ ` Y ) /\ Z .<_ ( ._|_ ` W ) ) ) -> ( ( F ` ( ( X .\/ Y ) ./\ Z ) ) .+ ( F ` W ) ) = ( ( ( ( F ` X ) .+ ( F ` Y ) ) i^i ( F ` Z ) ) .+ ( F ` W ) ) )
42 33 41 eqtrd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) /\ ( X .<_ ( ._|_ ` Y ) /\ Z .<_ ( ._|_ ` W ) ) ) -> ( F ` ( ( ( X .\/ Y ) ./\ Z ) .\/ W ) ) = ( ( ( ( F ` X ) .+ ( F ` Y ) ) i^i ( F ` Z ) ) .+ ( F ` W ) ) )
43 42 ineq1d 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) /\ ( X .<_ ( ._|_ ` Y ) /\ Z .<_ ( ._|_ ` W ) ) ) -> ( ( F ` ( ( ( X .\/ Y ) ./\ Z ) .\/ W ) ) i^i ( F ` V ) ) = ( ( ( ( ( F ` X ) .+ ( F ` Y ) ) i^i ( F ` Z ) ) .+ ( F ` W ) ) i^i ( F ` V ) ) )
44 23 43 eqtrd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) /\ ( X .<_ ( ._|_ ` Y ) /\ Z .<_ ( ._|_ ` W ) ) ) -> ( F ` ( ( ( ( X .\/ Y ) ./\ Z ) .\/ W ) ./\ V ) ) = ( ( ( ( ( F ` X ) .+ ( F ` Y ) ) i^i ( F ` Z ) ) .+ ( F ` W ) ) i^i ( F ` V ) ) )
45 44 3expia 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( ( X .<_ ( ._|_ ` Y ) /\ Z .<_ ( ._|_ ` W ) ) -> ( F ` ( ( ( ( X .\/ Y ) ./\ Z ) .\/ W ) ./\ V ) ) = ( ( ( ( ( F ` X ) .+ ( F ` Y ) ) i^i ( F ` Z ) ) .+ ( F ` W ) ) i^i ( F ` V ) ) ) )