Metamath Proof Explorer

Theorem pmapojoinN

Description: For orthogonal elements, projective map of join equals projective sum. Compare pmapjoin where only one direction holds. (Contributed by NM, 11-Apr-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pmapojoin.b 
|- B = ( Base ` K )
pmapojoin.l 
|- .<_ = ( le ` K )
pmapojoin.j 
|- .\/ = ( join ` K )
pmapojoin.m 
|- M = ( pmap ` K )
pmapojoin.o 
|- ._|_ = ( oc ` K )
pmapojoin.p 
|- .+ = ( +P ` K )
Assertion pmapojoinN 
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .<_ ( ._|_ ` Y ) ) -> ( M ` ( X .\/ Y ) ) = ( ( M ` X ) .+ ( M ` Y ) ) )

Proof

Step Hyp Ref Expression
1 pmapojoin.b 
 |-  B = ( Base ` K )
2 pmapojoin.l 
 |-  .<_ = ( le ` K )
3 pmapojoin.j 
 |-  .\/ = ( join ` K )
4 pmapojoin.m 
 |-  M = ( pmap ` K )
5 pmapojoin.o 
 |-  ._|_ = ( oc ` K )
6 pmapojoin.p 
 |-  .+ = ( +P ` K )
7 eqid 
 |-  ( _|_P ` K ) = ( _|_P ` K )
8 1 3 4 6 7 pmapj2N 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( M ` ( X .\/ Y ) ) = ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` ( ( M ` X ) .+ ( M ` Y ) ) ) ) )
9 8 adantr 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .<_ ( ._|_ ` Y ) ) -> ( M ` ( X .\/ Y ) ) = ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` ( ( M ` X ) .+ ( M ` Y ) ) ) ) )
10 simpl1 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .<_ ( ._|_ ` Y ) ) -> K e. HL )
11 simpl2 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .<_ ( ._|_ ` Y ) ) -> X e. B )
12 eqid 
 |-  ( PSubCl ` K ) = ( PSubCl ` K )
13 1 4 12 pmapsubclN 
 |-  ( ( K e. HL /\ X e. B ) -> ( M ` X ) e. ( PSubCl ` K ) )
14 10 11 13 syl2anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .<_ ( ._|_ ` Y ) ) -> ( M ` X ) e. ( PSubCl ` K ) )
15 simpl3 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .<_ ( ._|_ ` Y ) ) -> Y e. B )
16 1 4 12 pmapsubclN 
 |-  ( ( K e. HL /\ Y e. B ) -> ( M ` Y ) e. ( PSubCl ` K ) )
17 10 15 16 syl2anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .<_ ( ._|_ ` Y ) ) -> ( M ` Y ) e. ( PSubCl ` K ) )
18 hlop 
 |-  ( K e. HL -> K e. OP )
19 18 3ad2ant1 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> K e. OP )
20 simp3 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> Y e. B )
21 1 5 opoccl 
 |-  ( ( K e. OP /\ Y e. B ) -> ( ._|_ ` Y ) e. B )
22 19 20 21 syl2anc 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ._|_ ` Y ) e. B )
23 1 2 4 pmaple 
 |-  ( ( K e. HL /\ X e. B /\ ( ._|_ ` Y ) e. B ) -> ( X .<_ ( ._|_ ` Y ) <-> ( M ` X ) C_ ( M ` ( ._|_ ` Y ) ) ) )
24 22 23 syld3an3 
 |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X .<_ ( ._|_ ` Y ) <-> ( M ` X ) C_ ( M ` ( ._|_ ` Y ) ) ) )
25 24 biimpa 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .<_ ( ._|_ ` Y ) ) -> ( M ` X ) C_ ( M ` ( ._|_ ` Y ) ) )
26 1 5 4 7 polpmapN 
 |-  ( ( K e. HL /\ Y e. B ) -> ( ( _|_P ` K ) ` ( M ` Y ) ) = ( M ` ( ._|_ ` Y ) ) )
27 10 15 26 syl2anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .<_ ( ._|_ ` Y ) ) -> ( ( _|_P ` K ) ` ( M ` Y ) ) = ( M ` ( ._|_ ` Y ) ) )
28 25 27 sseqtrrd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .<_ ( ._|_ ` Y ) ) -> ( M ` X ) C_ ( ( _|_P ` K ) ` ( M ` Y ) ) )
29 6 7 12 osumclN 
 |-  ( ( ( K e. HL /\ ( M ` X ) e. ( PSubCl ` K ) /\ ( M ` Y ) e. ( PSubCl ` K ) ) /\ ( M ` X ) C_ ( ( _|_P ` K ) ` ( M ` Y ) ) ) -> ( ( M ` X ) .+ ( M ` Y ) ) e. ( PSubCl ` K ) )
30 10 14 17 28 29 syl31anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .<_ ( ._|_ ` Y ) ) -> ( ( M ` X ) .+ ( M ` Y ) ) e. ( PSubCl ` K ) )
31 7 12 psubcli2N 
 |-  ( ( K e. HL /\ ( ( M ` X ) .+ ( M ` Y ) ) e. ( PSubCl ` K ) ) -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` ( ( M ` X ) .+ ( M ` Y ) ) ) ) = ( ( M ` X ) .+ ( M ` Y ) ) )
32 10 30 31 syl2anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .<_ ( ._|_ ` Y ) ) -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` ( ( M ` X ) .+ ( M ` Y ) ) ) ) = ( ( M ` X ) .+ ( M ` Y ) ) )
33 9 32 eqtrd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .<_ ( ._|_ ` Y ) ) -> ( M ` ( X .\/ Y ) ) = ( ( M ` X ) .+ ( M ` Y ) ) )