Metamath Proof Explorer

Theorem pmodlem1

Description: Lemma for pmod1i . (Contributed by NM, 9-Mar-2012)

Ref Expression
Hypotheses pmodlem.l 
|- .<_ = ( le ` K )
pmodlem.j 
|- .\/ = ( join ` K )
pmodlem.a 
|- A = ( Atoms ` K )
pmodlem.s 
|- S = ( PSubSp ` K )
pmodlem.p 
|- .+ = ( +P ` K )
Assertion pmodlem1 
|- ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) -> p e. ( X .+ ( Y i^i Z ) ) )

Proof

Step Hyp Ref Expression
1 pmodlem.l 
 |-  .<_ = ( le ` K )
2 pmodlem.j 
 |-  .\/ = ( join ` K )
3 pmodlem.a 
 |-  A = ( Atoms ` K )
4 pmodlem.s 
 |-  S = ( PSubSp ` K )
5 pmodlem.p 
 |-  .+ = ( +P ` K )
6 simpl11 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) /\ p = q ) -> K e. HL )
7 simpl12 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) /\ p = q ) -> X C_ A )
8 simpl13 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) /\ p = q ) -> Y C_ A )
9 ssinss1 
 |-  ( Y C_ A -> ( Y i^i Z ) C_ A )
10 8 9 syl 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) /\ p = q ) -> ( Y i^i Z ) C_ A )
11 3 5 sspadd1 
 |-  ( ( K e. HL /\ X C_ A /\ ( Y i^i Z ) C_ A ) -> X C_ ( X .+ ( Y i^i Z ) ) )
12 6 7 10 11 syl3anc 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) /\ p = q ) -> X C_ ( X .+ ( Y i^i Z ) ) )
13 simpr 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) /\ p = q ) -> p = q )
14 simpl31 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) /\ p = q ) -> q e. X )
15 13 14 eqeltrd 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) /\ p = q ) -> p e. X )
16 12 15 sseldd 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) /\ p = q ) -> p e. ( X .+ ( Y i^i Z ) ) )
17 simpl11 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) /\ p =/= q ) -> K e. HL )
18 17 hllatd 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) /\ p =/= q ) -> K e. Lat )
19 simpl12 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) /\ p =/= q ) -> X C_ A )
20 simpl13 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) /\ p =/= q ) -> Y C_ A )
21 20 9 syl 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) /\ p =/= q ) -> ( Y i^i Z ) C_ A )
22 simpl31 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) /\ p =/= q ) -> q e. X )
23 simpl32 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) /\ p =/= q ) -> r e. Y )
24 simpl21 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) /\ p =/= q ) -> Z e. S )
25 simpl22 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) /\ p =/= q ) -> X C_ Z )
26 simpl23 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) /\ p =/= q ) -> p e. Z )
27 3 4 psubssat 
 |-  ( ( K e. HL /\ Z e. S ) -> Z C_ A )
28 17 24 27 syl2anc 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) /\ p =/= q ) -> Z C_ A )
29 28 26 sseldd 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) /\ p =/= q ) -> p e. A )
30 20 23 sseldd 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) /\ p =/= q ) -> r e. A )
31 19 22 sseldd 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) /\ p =/= q ) -> q e. A )
32 29 30 31 3jca 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) /\ p =/= q ) -> ( p e. A /\ r e. A /\ q e. A ) )
33 simpr 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) /\ p =/= q ) -> p =/= q )
34 simpl33 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) /\ p =/= q ) -> p .<_ ( q .\/ r ) )
35 1 2 3 hlatexch1 
 |-  ( ( K e. HL /\ ( p e. A /\ r e. A /\ q e. A ) /\ p =/= q ) -> ( p .<_ ( q .\/ r ) -> r .<_ ( q .\/ p ) ) )
36 35 imp 
 |-  ( ( ( K e. HL /\ ( p e. A /\ r e. A /\ q e. A ) /\ p =/= q ) /\ p .<_ ( q .\/ r ) ) -> r .<_ ( q .\/ p ) )
37 17 32 33 34 36 syl31anc 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) /\ p =/= q ) -> r .<_ ( q .\/ p ) )
38 simp31 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ r .<_ ( q .\/ p ) ) ) -> q e. X )
39 38 snssd 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ r .<_ ( q .\/ p ) ) ) -> { q } C_ X )
40 simp22 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ r .<_ ( q .\/ p ) ) ) -> X C_ Z )
41 39 40 sstrd 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ r .<_ ( q .\/ p ) ) ) -> { q } C_ Z )
42 simp23 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ r .<_ ( q .\/ p ) ) ) -> p e. Z )
43 42 snssd 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ r .<_ ( q .\/ p ) ) ) -> { p } C_ Z )
44 simp11 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ r .<_ ( q .\/ p ) ) ) -> K e. HL )
45 simp12 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ r .<_ ( q .\/ p ) ) ) -> X C_ A )
46 45 38 sseldd 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ r .<_ ( q .\/ p ) ) ) -> q e. A )
47 46 snssd 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ r .<_ ( q .\/ p ) ) ) -> { q } C_ A )
48 simp21 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ r .<_ ( q .\/ p ) ) ) -> Z e. S )
49 44 48 27 syl2anc 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ r .<_ ( q .\/ p ) ) ) -> Z C_ A )
50 49 42 sseldd 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ r .<_ ( q .\/ p ) ) ) -> p e. A )
51 50 snssd 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ r .<_ ( q .\/ p ) ) ) -> { p } C_ A )
52 3 4 5 paddss 
 |-  ( ( K e. HL /\ ( { q } C_ A /\ { p } C_ A /\ Z e. S ) ) -> ( ( { q } C_ Z /\ { p } C_ Z ) <-> ( { q } .+ { p } ) C_ Z ) )
53 44 47 51 48 52 syl13anc 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ r .<_ ( q .\/ p ) ) ) -> ( ( { q } C_ Z /\ { p } C_ Z ) <-> ( { q } .+ { p } ) C_ Z ) )
54 41 43 53 mpbi2and 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ r .<_ ( q .\/ p ) ) ) -> ( { q } .+ { p } ) C_ Z )
55 simp33 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ r .<_ ( q .\/ p ) ) ) -> r .<_ ( q .\/ p ) )
56 44 hllatd 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ r .<_ ( q .\/ p ) ) ) -> K e. Lat )
57 simp13 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ r .<_ ( q .\/ p ) ) ) -> Y C_ A )
58 simp32 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ r .<_ ( q .\/ p ) ) ) -> r e. Y )
59 57 58 sseldd 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ r .<_ ( q .\/ p ) ) ) -> r e. A )
60 1 2 3 5 elpadd2at2 
 |-  ( ( K e. Lat /\ ( q e. A /\ p e. A /\ r e. A ) ) -> ( r e. ( { q } .+ { p } ) <-> r .<_ ( q .\/ p ) ) )
61 56 46 50 59 60 syl13anc 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ r .<_ ( q .\/ p ) ) ) -> ( r e. ( { q } .+ { p } ) <-> r .<_ ( q .\/ p ) ) )
62 55 61 mpbird 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ r .<_ ( q .\/ p ) ) ) -> r e. ( { q } .+ { p } ) )
63 54 62 sseldd 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ r .<_ ( q .\/ p ) ) ) -> r e. Z )
64 17 19 20 24 25 26 22 23 37 63 syl333anc 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) /\ p =/= q ) -> r e. Z )
65 23 64 elind 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) /\ p =/= q ) -> r e. ( Y i^i Z ) )
66 1 2 3 5 elpaddri 
 |-  ( ( ( K e. Lat /\ X C_ A /\ ( Y i^i Z ) C_ A ) /\ ( q e. X /\ r e. ( Y i^i Z ) ) /\ ( p e. A /\ p .<_ ( q .\/ r ) ) ) -> p e. ( X .+ ( Y i^i Z ) ) )
67 18 19 21 22 65 29 34 66 syl322anc 
 |-  ( ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) /\ p =/= q ) -> p e. ( X .+ ( Y i^i Z ) ) )
68 16 67 pm2.61dane 
 |-  ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( Z e. S /\ X C_ Z /\ p e. Z ) /\ ( q e. X /\ r e. Y /\ p .<_ ( q .\/ r ) ) ) -> p e. ( X .+ ( Y i^i Z ) ) )