Metamath Proof Explorer

Theorem pl42lem4N

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 pl42lem4N 
|- ( ( ( 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 ) ) 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 1 2 3 4 5 6 7 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 ) ) ) )
9 8 3impia 
 |-  ( ( ( 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 ) ) )
10 1 2 3 4 5 6 7 pl42lem3N 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( ( ( ( ( F ` X ) .+ ( F ` Y ) ) i^i ( F ` Z ) ) .+ ( F ` W ) ) i^i ( F ` V ) ) C_ ( ( ( ( F ` X ) .+ ( F ` Y ) ) .+ ( F ` W ) ) i^i ( ( ( F ` X ) .+ ( F ` Y ) ) .+ ( F ` V ) ) ) )
11 simpl1 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> K e. HL )
12 11 hllatd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> K e. Lat )
13 simpl2 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> X e. B )
14 eqid 
 |-  ( PSubSp ` K ) = ( PSubSp ` K )
15 1 14 6 pmapsub 
 |-  ( ( K e. Lat /\ X e. B ) -> ( F ` X ) e. ( PSubSp ` K ) )
16 12 13 15 syl2anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( F ` X ) e. ( PSubSp ` K ) )
17 simpl3 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> Y e. B )
18 1 14 6 pmapsub 
 |-  ( ( K e. Lat /\ Y e. B ) -> ( F ` Y ) e. ( PSubSp ` K ) )
19 12 17 18 syl2anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( F ` Y ) e. ( PSubSp ` K ) )
20 simpr2 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> W e. B )
21 1 14 6 pmapsub 
 |-  ( ( K e. Lat /\ W e. B ) -> ( F ` W ) e. ( PSubSp ` K ) )
22 12 20 21 syl2anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( F ` W ) e. ( PSubSp ` K ) )
23 simpr3 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> V e. B )
24 1 14 6 pmapsub 
 |-  ( ( K e. Lat /\ V e. B ) -> ( F ` V ) e. ( PSubSp ` K ) )
25 12 23 24 syl2anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( F ` V ) e. ( PSubSp ` K ) )
26 14 7 pmodl42N 
 |-  ( ( ( K e. HL /\ ( F ` X ) e. ( PSubSp ` K ) /\ ( F ` Y ) e. ( PSubSp ` K ) ) /\ ( ( F ` W ) e. ( PSubSp ` K ) /\ ( F ` V ) e. ( PSubSp ` K ) ) ) -> ( ( ( ( F ` X ) .+ ( F ` Y ) ) .+ ( F ` W ) ) i^i ( ( ( F ` X ) .+ ( F ` Y ) ) .+ ( F ` V ) ) ) = ( ( ( F ` X ) .+ ( F ` Y ) ) .+ ( ( ( F ` X ) .+ ( F ` W ) ) i^i ( ( F ` Y ) .+ ( F ` V ) ) ) ) )
27 11 16 19 22 25 26 syl32anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( ( ( ( F ` X ) .+ ( F ` Y ) ) .+ ( F ` W ) ) i^i ( ( ( F ` X ) .+ ( F ` Y ) ) .+ ( F ` V ) ) ) = ( ( ( F ` X ) .+ ( F ` Y ) ) .+ ( ( ( F ` X ) .+ ( F ` W ) ) i^i ( ( F ` Y ) .+ ( F ` V ) ) ) ) )
28 1 2 3 4 5 6 7 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 ) ) ) ) )
29 27 28 eqsstrd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( ( ( ( F ` X ) .+ ( F ` Y ) ) .+ ( F ` W ) ) i^i ( ( ( F ` X ) .+ ( F ` Y ) ) .+ ( F ` V ) ) ) C_ ( F ` ( ( X .\/ Y ) .\/ ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) ) )
30 10 29 sstrd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( ( ( ( ( F ` X ) .+ ( F ` Y ) ) i^i ( F ` Z ) ) .+ ( F ` W ) ) i^i ( F ` V ) ) C_ ( F ` ( ( X .\/ Y ) .\/ ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) ) )
31 30 3adant3 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) /\ ( X .<_ ( ._|_ ` Y ) /\ Z .<_ ( ._|_ ` W ) ) ) -> ( ( ( ( ( F ` X ) .+ ( F ` Y ) ) i^i ( F ` Z ) ) .+ ( F ` W ) ) i^i ( F ` V ) ) C_ ( F ` ( ( X .\/ Y ) .\/ ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) ) )
32 9 31 eqsstrd 
 |-  ( ( ( 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 ) ) C_ ( F ` ( ( X .\/ Y ) .\/ ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) ) )
33 32 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 ) ) C_ ( F ` ( ( X .\/ Y ) .\/ ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) ) ) )