Metamath Proof Explorer

Theorem paddasslem12

Description: Lemma for paddass . The case when x = y . (Contributed by NM, 11-Jan-2012)

Ref Expression
Hypotheses paddasslem.l 
|- .<_ = ( le ` K )
paddasslem.j 
|- .\/ = ( join ` K )
paddasslem.a 
|- A = ( Atoms ` K )
paddasslem.p 
|- .+ = ( +P ` K )
Assertion paddasslem12 
|- ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> p e. ( ( X .+ Y ) .+ Z ) )

Proof

Step Hyp Ref Expression
1 paddasslem.l 
 |-  .<_ = ( le ` K )
2 paddasslem.j 
 |-  .\/ = ( join ` K )
3 paddasslem.a 
 |-  A = ( Atoms ` K )
4 paddasslem.p 
 |-  .+ = ( +P ` K )
5 simpl1l 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> K e. HL )
6 simpl21 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> X C_ A )
7 simpl22 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> Y C_ A )
8 3 4 paddssat 
 |-  ( ( K e. HL /\ X C_ A /\ Y C_ A ) -> ( X .+ Y ) C_ A )
9 5 6 7 8 syl3anc 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> ( X .+ Y ) C_ A )
10 simpl23 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> Z C_ A )
11 5 9 10 3jca 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> ( K e. HL /\ ( X .+ Y ) C_ A /\ Z C_ A ) )
12 3 4 sspadd2 
 |-  ( ( K e. HL /\ Y C_ A /\ X C_ A ) -> Y C_ ( X .+ Y ) )
13 5 7 6 12 syl3anc 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> Y C_ ( X .+ Y ) )
14 3 4 paddss1 
 |-  ( ( K e. HL /\ ( X .+ Y ) C_ A /\ Z C_ A ) -> ( Y C_ ( X .+ Y ) -> ( Y .+ Z ) C_ ( ( X .+ Y ) .+ Z ) ) )
15 11 13 14 sylc 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> ( Y .+ Z ) C_ ( ( X .+ Y ) .+ Z ) )
16 5 hllatd 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> K e. Lat )
17 simprll 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> y e. Y )
18 simprlr 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> z e. Z )
19 simpl3l 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> p e. A )
20 eqid 
 |-  ( Base ` K ) = ( Base ` K )
21 20 3 atbase 
 |-  ( p e. A -> p e. ( Base ` K ) )
22 19 21 syl 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> p e. ( Base ` K ) )
23 7 17 sseldd 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> y e. A )
24 20 3 atbase 
 |-  ( y e. A -> y e. ( Base ` K ) )
25 23 24 syl 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> y e. ( Base ` K ) )
26 simpl3r 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> r e. A )
27 20 3 atbase 
 |-  ( r e. A -> r e. ( Base ` K ) )
28 26 27 syl 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> r e. ( Base ` K ) )
29 20 2 latjcl 
 |-  ( ( K e. Lat /\ y e. ( Base ` K ) /\ r e. ( Base ` K ) ) -> ( y .\/ r ) e. ( Base ` K ) )
30 16 25 28 29 syl3anc 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> ( y .\/ r ) e. ( Base ` K ) )
31 10 18 sseldd 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> z e. A )
32 20 3 atbase 
 |-  ( z e. A -> z e. ( Base ` K ) )
33 31 32 syl 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> z e. ( Base ` K ) )
34 20 2 latjcl 
 |-  ( ( K e. Lat /\ y e. ( Base ` K ) /\ z e. ( Base ` K ) ) -> ( y .\/ z ) e. ( Base ` K ) )
35 16 25 33 34 syl3anc 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> ( y .\/ z ) e. ( Base ` K ) )
36 simpl1r 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> x = y )
37 simprrl 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> p .<_ ( x .\/ r ) )
38 oveq1 
 |-  ( x = y -> ( x .\/ r ) = ( y .\/ r ) )
39 38 breq2d 
 |-  ( x = y -> ( p .<_ ( x .\/ r ) <-> p .<_ ( y .\/ r ) ) )
40 39 biimpa 
 |-  ( ( x = y /\ p .<_ ( x .\/ r ) ) -> p .<_ ( y .\/ r ) )
41 36 37 40 syl2anc 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> p .<_ ( y .\/ r ) )
42 20 1 2 latlej1 
 |-  ( ( K e. Lat /\ y e. ( Base ` K ) /\ z e. ( Base ` K ) ) -> y .<_ ( y .\/ z ) )
43 16 25 33 42 syl3anc 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> y .<_ ( y .\/ z ) )
44 simprrr 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> r .<_ ( y .\/ z ) )
45 20 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( y e. ( Base ` K ) /\ r e. ( Base ` K ) /\ ( y .\/ z ) e. ( Base ` K ) ) ) -> ( ( y .<_ ( y .\/ z ) /\ r .<_ ( y .\/ z ) ) <-> ( y .\/ r ) .<_ ( y .\/ z ) ) )
46 16 25 28 35 45 syl13anc 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> ( ( y .<_ ( y .\/ z ) /\ r .<_ ( y .\/ z ) ) <-> ( y .\/ r ) .<_ ( y .\/ z ) ) )
47 43 44 46 mpbi2and 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> ( y .\/ r ) .<_ ( y .\/ z ) )
48 20 1 16 22 30 35 41 47 lattrd 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> p .<_ ( y .\/ z ) )
49 1 2 3 4 elpaddri 
 |-  ( ( ( K e. Lat /\ Y C_ A /\ Z C_ A ) /\ ( y e. Y /\ z e. Z ) /\ ( p e. A /\ p .<_ ( y .\/ z ) ) ) -> p e. ( Y .+ Z ) )
50 16 7 10 17 18 19 48 49 syl322anc 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> p e. ( Y .+ Z ) )
51 15 50 sseldd 
 |-  ( ( ( ( K e. HL /\ x = y ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ ( p e. A /\ r e. A ) ) /\ ( ( y e. Y /\ z e. Z ) /\ ( p .<_ ( x .\/ r ) /\ r .<_ ( y .\/ z ) ) ) ) -> p e. ( ( X .+ Y ) .+ Z ) )