Metamath Proof Explorer

Theorem pexmidlem6N

Description: Lemma for pexmidN . (Contributed by NM, 3-Feb-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pexmidlem.l 
|- .<_ = ( le ` K )
pexmidlem.j 
|- .\/ = ( join ` K )
pexmidlem.a 
|- A = ( Atoms ` K )
pexmidlem.p 
|- .+ = ( +P ` K )
pexmidlem.o 
|- ._|_ = ( _|_P ` K )
pexmidlem.m 
|- M = ( X .+ { p } )
Assertion pexmidlem6N 
|- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> M = X )

Proof

Step Hyp Ref Expression
1 pexmidlem.l 
 |-  .<_ = ( le ` K )
2 pexmidlem.j 
 |-  .\/ = ( join ` K )
3 pexmidlem.a 
 |-  A = ( Atoms ` K )
4 pexmidlem.p 
 |-  .+ = ( +P ` K )
5 pexmidlem.o 
 |-  ._|_ = ( _|_P ` K )
6 pexmidlem.m 
 |-  M = ( X .+ { p } )
7 1 2 3 4 5 6 pexmidlem5N 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( ( ._|_ ` X ) i^i M ) = (/) )
8 7 3adantr1 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( ( ._|_ ` X ) i^i M ) = (/) )
9 8 fveq2d 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( ._|_ ` ( ( ._|_ ` X ) i^i M ) ) = ( ._|_ ` (/) ) )
10 simpl1 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> K e. HL )
11 3 5 pol0N 
 |-  ( K e. HL -> ( ._|_ ` (/) ) = A )
12 10 11 syl 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( ._|_ ` (/) ) = A )
13 9 12 eqtrd 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( ._|_ ` ( ( ._|_ ` X ) i^i M ) ) = A )
14 13 ineq1d 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( ( ._|_ ` ( ( ._|_ ` X ) i^i M ) ) i^i M ) = ( A i^i M ) )
15 simpl2 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> X C_ A )
16 simpl3 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> p e. A )
17 16 snssd 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> { p } C_ A )
18 3 4 paddssat 
 |-  ( ( K e. HL /\ X C_ A /\ { p } C_ A ) -> ( X .+ { p } ) C_ A )
19 10 15 17 18 syl3anc 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( X .+ { p } ) C_ A )
20 6 19 eqsstrid 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> M C_ A )
21 10 15 20 3jca 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( K e. HL /\ X C_ A /\ M C_ A ) )
22 3 4 sspadd1 
 |-  ( ( K e. HL /\ X C_ A /\ { p } C_ A ) -> X C_ ( X .+ { p } ) )
23 10 15 17 22 syl3anc 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> X C_ ( X .+ { p } ) )
24 23 6 sseqtrrdi 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> X C_ M )
25 simpr1 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( ._|_ ` ( ._|_ ` X ) ) = X )
26 eqid 
 |-  ( PSubCl ` K ) = ( PSubCl ` K )
27 3 5 26 ispsubclN 
 |-  ( K e. HL -> ( X e. ( PSubCl ` K ) <-> ( X C_ A /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) ) )
28 10 27 syl 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( X e. ( PSubCl ` K ) <-> ( X C_ A /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) ) )
29 15 25 28 mpbir2and 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> X e. ( PSubCl ` K ) )
30 3 4 26 paddatclN 
 |-  ( ( K e. HL /\ X e. ( PSubCl ` K ) /\ p e. A ) -> ( X .+ { p } ) e. ( PSubCl ` K ) )
31 10 29 16 30 syl3anc 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( X .+ { p } ) e. ( PSubCl ` K ) )
32 6 31 eqeltrid 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> M e. ( PSubCl ` K ) )
33 5 26 psubcli2N 
 |-  ( ( K e. HL /\ M e. ( PSubCl ` K ) ) -> ( ._|_ ` ( ._|_ ` M ) ) = M )
34 10 32 33 syl2anc 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( ._|_ ` ( ._|_ ` M ) ) = M )
35 24 34 jca 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( X C_ M /\ ( ._|_ ` ( ._|_ ` M ) ) = M ) )
36 3 5 poml4N 
 |-  ( ( K e. HL /\ X C_ A /\ M C_ A ) -> ( ( X C_ M /\ ( ._|_ ` ( ._|_ ` M ) ) = M ) -> ( ( ._|_ ` ( ( ._|_ ` X ) i^i M ) ) i^i M ) = ( ._|_ ` ( ._|_ ` X ) ) ) )
37 21 35 36 sylc 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( ( ._|_ ` ( ( ._|_ ` X ) i^i M ) ) i^i M ) = ( ._|_ ` ( ._|_ ` X ) ) )
38 sseqin2 
 |-  ( M C_ A <-> ( A i^i M ) = M )
39 20 38 sylib 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( A i^i M ) = M )
40 14 37 39 3eqtr3rd 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> M = ( ._|_ ` ( ._|_ ` X ) ) )
41 40 25 eqtrd 
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> M = X )