Metamath Proof Explorer

Theorem osumcllem11N

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

Ref Expression
Hypotheses osumcl.p 
|- .+ = ( +P ` K )
osumcl.o 
|- ._|_ = ( _|_P ` K )
osumcl.c 
|- C = ( PSubCl ` K )
Assertion osumcllem11N 
|- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) ) ) -> ( X .+ Y ) = ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) )

Proof

Step Hyp Ref Expression
1 osumcl.p 
 |-  .+ = ( +P ` K )
2 osumcl.o 
 |-  ._|_ = ( _|_P ` K )
3 osumcl.c 
 |-  C = ( PSubCl ` K )
4 nonconne 
 |-  -. ( X = X /\ X =/= X )
5 simpl1 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) ) ) -> K e. HL )
6 simpl2 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) ) ) -> X e. C )
7 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
8 7 3 psubclssatN 
 |-  ( ( K e. HL /\ X e. C ) -> X C_ ( Atoms ` K ) )
9 5 6 8 syl2anc 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) ) ) -> X C_ ( Atoms ` K ) )
10 simpl3 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) ) ) -> Y e. C )
11 7 3 psubclssatN 
 |-  ( ( K e. HL /\ Y e. C ) -> Y C_ ( Atoms ` K ) )
12 5 10 11 syl2anc 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) ) ) -> Y C_ ( Atoms ` K ) )
13 7 1 paddssat 
 |-  ( ( K e. HL /\ X C_ ( Atoms ` K ) /\ Y C_ ( Atoms ` K ) ) -> ( X .+ Y ) C_ ( Atoms ` K ) )
14 5 9 12 13 syl3anc 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) ) ) -> ( X .+ Y ) C_ ( Atoms ` K ) )
15 7 2 2polssN 
 |-  ( ( K e. HL /\ ( X .+ Y ) C_ ( Atoms ` K ) ) -> ( X .+ Y ) C_ ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) )
16 5 14 15 syl2anc 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) ) ) -> ( X .+ Y ) C_ ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) )
17 df-pss 
 |-  ( ( X .+ Y ) C. ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) <-> ( ( X .+ Y ) C_ ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) /\ ( X .+ Y ) =/= ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) ) )
18 pssnel 
 |-  ( ( X .+ Y ) C. ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) -> E. p ( p e. ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) /\ -. p e. ( X .+ Y ) ) )
19 17 18 sylbir 
 |-  ( ( ( X .+ Y ) C_ ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) /\ ( X .+ Y ) =/= ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) ) -> E. p ( p e. ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) /\ -. p e. ( X .+ Y ) ) )
20 df-rex 
 |-  ( E. p e. ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) -. p e. ( X .+ Y ) <-> E. p ( p e. ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) /\ -. p e. ( X .+ Y ) ) )
21 19 20 sylibr 
 |-  ( ( ( X .+ Y ) C_ ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) /\ ( X .+ Y ) =/= ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) ) -> E. p e. ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) -. p e. ( X .+ Y ) )
22 eqid 
 |-  ( le ` K ) = ( le ` K )
23 eqid 
 |-  ( join ` K ) = ( join ` K )
24 eqid 
 |-  ( X .+ { p } ) = ( X .+ { p } )
25 eqid 
 |-  ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) = ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) )
26 22 23 7 1 2 3 24 25 osumcllem9N 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) ) /\ -. p e. ( X .+ Y ) ) -> ( X .+ { p } ) = X )
27 simp11 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) ) /\ -. p e. ( X .+ Y ) ) -> K e. HL )
28 simp12 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) ) /\ -. p e. ( X .+ Y ) ) -> X e. C )
29 27 28 8 syl2anc 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) ) /\ -. p e. ( X .+ Y ) ) -> X C_ ( Atoms ` K ) )
30 simp13 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) ) /\ -. p e. ( X .+ Y ) ) -> Y e. C )
31 27 30 11 syl2anc 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) ) /\ -. p e. ( X .+ Y ) ) -> Y C_ ( Atoms ` K ) )
32 14 3adantr3 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) ) ) -> ( X .+ Y ) C_ ( Atoms ` K ) )
33 32 3adant3 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) ) /\ -. p e. ( X .+ Y ) ) -> ( X .+ Y ) C_ ( Atoms ` K ) )
34 7 2 polssatN 
 |-  ( ( K e. HL /\ ( X .+ Y ) C_ ( Atoms ` K ) ) -> ( ._|_ ` ( X .+ Y ) ) C_ ( Atoms ` K ) )
35 27 33 34 syl2anc 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) ) /\ -. p e. ( X .+ Y ) ) -> ( ._|_ ` ( X .+ Y ) ) C_ ( Atoms ` K ) )
36 7 2 polssatN 
 |-  ( ( K e. HL /\ ( ._|_ ` ( X .+ Y ) ) C_ ( Atoms ` K ) ) -> ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) C_ ( Atoms ` K ) )
37 27 35 36 syl2anc 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) ) /\ -. p e. ( X .+ Y ) ) -> ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) C_ ( Atoms ` K ) )
38 simp23 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) ) /\ -. p e. ( X .+ Y ) ) -> p e. ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) )
39 37 38 sseldd 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) ) /\ -. p e. ( X .+ Y ) ) -> p e. ( Atoms ` K ) )
40 simp3 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) ) /\ -. p e. ( X .+ Y ) ) -> -. p e. ( X .+ Y ) )
41 22 23 7 1 2 3 24 25 osumcllem10N 
 |-  ( ( ( K e. HL /\ X C_ ( Atoms ` K ) /\ Y C_ ( Atoms ` K ) ) /\ p e. ( Atoms ` K ) /\ -. p e. ( X .+ Y ) ) -> ( X .+ { p } ) =/= X )
42 27 29 31 39 40 41 syl311anc 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) ) /\ -. p e. ( X .+ Y ) ) -> ( X .+ { p } ) =/= X )
43 26 42 pm2.21ddne 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) ) /\ -. p e. ( X .+ Y ) ) -> ( X = X /\ X =/= X ) )
44 43 3exp 
 |-  ( ( K e. HL /\ X e. C /\ Y e. C ) -> ( ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) ) -> ( -. p e. ( X .+ Y ) -> ( X = X /\ X =/= X ) ) ) )
45 44 3expd 
 |-  ( ( K e. HL /\ X e. C /\ Y e. C ) -> ( X C_ ( ._|_ ` Y ) -> ( X =/= (/) -> ( p e. ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) -> ( -. p e. ( X .+ Y ) -> ( X = X /\ X =/= X ) ) ) ) ) )
46 45 imp32 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) ) ) -> ( p e. ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) -> ( -. p e. ( X .+ Y ) -> ( X = X /\ X =/= X ) ) ) )
47 46 rexlimdv 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) ) ) -> ( E. p e. ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) -. p e. ( X .+ Y ) -> ( X = X /\ X =/= X ) ) )
48 21 47 syl5 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) ) ) -> ( ( ( X .+ Y ) C_ ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) /\ ( X .+ Y ) =/= ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) ) -> ( X = X /\ X =/= X ) ) )
49 16 48 mpand 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) ) ) -> ( ( X .+ Y ) =/= ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) -> ( X = X /\ X =/= X ) ) )
50 49 necon1bd 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) ) ) -> ( -. ( X = X /\ X =/= X ) -> ( X .+ Y ) = ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) ) )
51 4 50 mpi 
 |-  ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) ) ) -> ( X .+ Y ) = ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) )