Metamath Proof Explorer

Theorem osumcllem3N

Description: Lemma for osumclN . (Contributed by NM, 23-Mar-2012) (New usage is discouraged.)

Ref Expression
Hypotheses osumcllem.l 
|- .<_ = ( le ` K )
osumcllem.j 
|- .\/ = ( join ` K )
osumcllem.a 
|- A = ( Atoms ` K )
osumcllem.p 
|- .+ = ( +P ` K )
osumcllem.o 
|- ._|_ = ( _|_P ` K )
osumcllem.c 
|- C = ( PSubCl ` K )
osumcllem.m 
|- M = ( X .+ { p } )
osumcllem.u 
|- U = ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) )
Assertion osumcllem3N 
|- ( ( K e. HL /\ Y e. C /\ X C_ ( ._|_ ` Y ) ) -> ( ( ._|_ ` X ) i^i U ) = Y )

Proof

Step Hyp Ref Expression
1 osumcllem.l 
 |-  .<_ = ( le ` K )
2 osumcllem.j 
 |-  .\/ = ( join ` K )
3 osumcllem.a 
 |-  A = ( Atoms ` K )
4 osumcllem.p 
 |-  .+ = ( +P ` K )
5 osumcllem.o 
 |-  ._|_ = ( _|_P ` K )
6 osumcllem.c 
 |-  C = ( PSubCl ` K )
7 osumcllem.m 
 |-  M = ( X .+ { p } )
8 osumcllem.u 
 |-  U = ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) )
9 incom 
 |-  ( ( ._|_ ` X ) i^i U ) = ( U i^i ( ._|_ ` X ) )
10 simp1 
 |-  ( ( K e. HL /\ Y e. C /\ X C_ ( ._|_ ` Y ) ) -> K e. HL )
11 simp3 
 |-  ( ( K e. HL /\ Y e. C /\ X C_ ( ._|_ ` Y ) ) -> X C_ ( ._|_ ` Y ) )
12 3 6 psubclssatN 
 |-  ( ( K e. HL /\ Y e. C ) -> Y C_ A )
13 12 3adant3 
 |-  ( ( K e. HL /\ Y e. C /\ X C_ ( ._|_ ` Y ) ) -> Y C_ A )
14 3 5 polssatN 
 |-  ( ( K e. HL /\ Y C_ A ) -> ( ._|_ ` Y ) C_ A )
15 10 13 14 syl2anc 
 |-  ( ( K e. HL /\ Y e. C /\ X C_ ( ._|_ ` Y ) ) -> ( ._|_ ` Y ) C_ A )
16 11 15 sstrd 
 |-  ( ( K e. HL /\ Y e. C /\ X C_ ( ._|_ ` Y ) ) -> X C_ A )
17 3 4 5 poldmj1N 
 |-  ( ( K e. HL /\ X C_ A /\ Y C_ A ) -> ( ._|_ ` ( X .+ Y ) ) = ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) )
18 10 16 13 17 syl3anc 
 |-  ( ( K e. HL /\ Y e. C /\ X C_ ( ._|_ ` Y ) ) -> ( ._|_ ` ( X .+ Y ) ) = ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) )
19 incom 
 |-  ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) = ( ( ._|_ ` Y ) i^i ( ._|_ ` X ) )
20 18 19 eqtrdi 
 |-  ( ( K e. HL /\ Y e. C /\ X C_ ( ._|_ ` Y ) ) -> ( ._|_ ` ( X .+ Y ) ) = ( ( ._|_ ` Y ) i^i ( ._|_ ` X ) ) )
21 20 fveq2d 
 |-  ( ( K e. HL /\ Y e. C /\ X C_ ( ._|_ ` Y ) ) -> ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) = ( ._|_ ` ( ( ._|_ ` Y ) i^i ( ._|_ ` X ) ) ) )
22 8 21 eqtrid 
 |-  ( ( K e. HL /\ Y e. C /\ X C_ ( ._|_ ` Y ) ) -> U = ( ._|_ ` ( ( ._|_ ` Y ) i^i ( ._|_ ` X ) ) ) )
23 22 ineq1d 
 |-  ( ( K e. HL /\ Y e. C /\ X C_ ( ._|_ ` Y ) ) -> ( U i^i ( ._|_ ` X ) ) = ( ( ._|_ ` ( ( ._|_ ` Y ) i^i ( ._|_ ` X ) ) ) i^i ( ._|_ ` X ) ) )
24 3 5 polcon2N 
 |-  ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) -> Y C_ ( ._|_ ` X ) )
25 13 24 syld3an2 
 |-  ( ( K e. HL /\ Y e. C /\ X C_ ( ._|_ ` Y ) ) -> Y C_ ( ._|_ ` X ) )
26 3 5 poml5N 
 |-  ( ( K e. HL /\ X C_ A /\ Y C_ ( ._|_ ` X ) ) -> ( ( ._|_ ` ( ( ._|_ ` Y ) i^i ( ._|_ ` X ) ) ) i^i ( ._|_ ` X ) ) = ( ._|_ ` ( ._|_ ` Y ) ) )
27 10 16 25 26 syl3anc 
 |-  ( ( K e. HL /\ Y e. C /\ X C_ ( ._|_ ` Y ) ) -> ( ( ._|_ ` ( ( ._|_ ` Y ) i^i ( ._|_ ` X ) ) ) i^i ( ._|_ ` X ) ) = ( ._|_ ` ( ._|_ ` Y ) ) )
28 5 6 psubcli2N 
 |-  ( ( K e. HL /\ Y e. C ) -> ( ._|_ ` ( ._|_ ` Y ) ) = Y )
29 28 3adant3 
 |-  ( ( K e. HL /\ Y e. C /\ X C_ ( ._|_ ` Y ) ) -> ( ._|_ ` ( ._|_ ` Y ) ) = Y )
30 23 27 29 3eqtrd 
 |-  ( ( K e. HL /\ Y e. C /\ X C_ ( ._|_ ` Y ) ) -> ( U i^i ( ._|_ ` X ) ) = Y )
31 9 30 eqtrid 
 |-  ( ( K e. HL /\ Y e. C /\ X C_ ( ._|_ ` Y ) ) -> ( ( ._|_ ` X ) i^i U ) = Y )