Metamath Proof Explorer

Theorem paddasslem17

Description: Lemma for paddass . The case when at least one sum argument is empty. (Contributed by NM, 12-Jan-2012)

Ref Expression
Hypotheses paddass.a 
|- A = ( Atoms ` K )
paddass.p 
|- .+ = ( +P ` K )
Assertion paddasslem17 
|- ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ -. ( ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) ) -> ( X .+ ( Y .+ Z ) ) C_ ( ( X .+ Y ) .+ Z ) )

Proof

Step Hyp Ref Expression
1 paddass.a 
 |-  A = ( Atoms ` K )
2 paddass.p 
 |-  .+ = ( +P ` K )
3 ianor 
 |-  ( -. ( ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) <-> ( -. ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) \/ -. ( Y =/= (/) /\ Z =/= (/) ) ) )
4 ianor 
 |-  ( -. ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) <-> ( -. X =/= (/) \/ -. ( Y .+ Z ) =/= (/) ) )
5 nne 
 |-  ( -. X =/= (/) <-> X = (/) )
6 nne 
 |-  ( -. ( Y .+ Z ) =/= (/) <-> ( Y .+ Z ) = (/) )
7 5 6 orbi12i 
 |-  ( ( -. X =/= (/) \/ -. ( Y .+ Z ) =/= (/) ) <-> ( X = (/) \/ ( Y .+ Z ) = (/) ) )
8 4 7 bitri 
 |-  ( -. ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) <-> ( X = (/) \/ ( Y .+ Z ) = (/) ) )
9 ianor 
 |-  ( -. ( Y =/= (/) /\ Z =/= (/) ) <-> ( -. Y =/= (/) \/ -. Z =/= (/) ) )
10 nne 
 |-  ( -. Y =/= (/) <-> Y = (/) )
11 nne 
 |-  ( -. Z =/= (/) <-> Z = (/) )
12 10 11 orbi12i 
 |-  ( ( -. Y =/= (/) \/ -. Z =/= (/) ) <-> ( Y = (/) \/ Z = (/) ) )
13 9 12 bitri 
 |-  ( -. ( Y =/= (/) /\ Z =/= (/) ) <-> ( Y = (/) \/ Z = (/) ) )
14 8 13 orbi12i 
 |-  ( ( -. ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) \/ -. ( Y =/= (/) /\ Z =/= (/) ) ) <-> ( ( X = (/) \/ ( Y .+ Z ) = (/) ) \/ ( Y = (/) \/ Z = (/) ) ) )
15 3 14 bitri 
 |-  ( -. ( ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) <-> ( ( X = (/) \/ ( Y .+ Z ) = (/) ) \/ ( Y = (/) \/ Z = (/) ) ) )
16 1 2 paddssat 
 |-  ( ( K e. HL /\ Y C_ A /\ Z C_ A ) -> ( Y .+ Z ) C_ A )
17 16 3adant3r1 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( Y .+ Z ) C_ A )
18 1 2 padd02 
 |-  ( ( K e. HL /\ ( Y .+ Z ) C_ A ) -> ( (/) .+ ( Y .+ Z ) ) = ( Y .+ Z ) )
19 17 18 syldan 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( (/) .+ ( Y .+ Z ) ) = ( Y .+ Z ) )
20 1 2 padd02 
 |-  ( ( K e. HL /\ Y C_ A ) -> ( (/) .+ Y ) = Y )
21 20 3ad2antr2 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( (/) .+ Y ) = Y )
22 21 oveq1d 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( ( (/) .+ Y ) .+ Z ) = ( Y .+ Z ) )
23 19 22 eqtr4d 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( (/) .+ ( Y .+ Z ) ) = ( ( (/) .+ Y ) .+ Z ) )
24 oveq1 
 |-  ( X = (/) -> ( X .+ ( Y .+ Z ) ) = ( (/) .+ ( Y .+ Z ) ) )
25 oveq1 
 |-  ( X = (/) -> ( X .+ Y ) = ( (/) .+ Y ) )
26 25 oveq1d 
 |-  ( X = (/) -> ( ( X .+ Y ) .+ Z ) = ( ( (/) .+ Y ) .+ Z ) )
27 24 26 eqeq12d 
 |-  ( X = (/) -> ( ( X .+ ( Y .+ Z ) ) = ( ( X .+ Y ) .+ Z ) <-> ( (/) .+ ( Y .+ Z ) ) = ( ( (/) .+ Y ) .+ Z ) ) )
28 23 27 syl5ibrcom 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( X = (/) -> ( X .+ ( Y .+ Z ) ) = ( ( X .+ Y ) .+ Z ) ) )
29 eqimss 
 |-  ( ( X .+ ( Y .+ Z ) ) = ( ( X .+ Y ) .+ Z ) -> ( X .+ ( Y .+ Z ) ) C_ ( ( X .+ Y ) .+ Z ) )
30 28 29 syl6 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( X = (/) -> ( X .+ ( Y .+ Z ) ) C_ ( ( X .+ Y ) .+ Z ) ) )
31 1 2 padd01 
 |-  ( ( K e. HL /\ X C_ A ) -> ( X .+ (/) ) = X )
32 31 3ad2antr1 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( X .+ (/) ) = X )
33 1 2 sspadd1 
 |-  ( ( K e. HL /\ X C_ A /\ Y C_ A ) -> X C_ ( X .+ Y ) )
34 33 3adant3r3 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> X C_ ( X .+ Y ) )
35 simpl 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> K e. HL )
36 1 2 paddssat 
 |-  ( ( K e. HL /\ X C_ A /\ Y C_ A ) -> ( X .+ Y ) C_ A )
37 36 3adant3r3 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( X .+ Y ) C_ A )
38 simpr3 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> Z C_ A )
39 1 2 sspadd1 
 |-  ( ( K e. HL /\ ( X .+ Y ) C_ A /\ Z C_ A ) -> ( X .+ Y ) C_ ( ( X .+ Y ) .+ Z ) )
40 35 37 38 39 syl3anc 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( X .+ Y ) C_ ( ( X .+ Y ) .+ Z ) )
41 34 40 sstrd 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> X C_ ( ( X .+ Y ) .+ Z ) )
42 32 41 eqsstrd 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( X .+ (/) ) C_ ( ( X .+ Y ) .+ Z ) )
43 oveq2 
 |-  ( ( Y .+ Z ) = (/) -> ( X .+ ( Y .+ Z ) ) = ( X .+ (/) ) )
44 43 sseq1d 
 |-  ( ( Y .+ Z ) = (/) -> ( ( X .+ ( Y .+ Z ) ) C_ ( ( X .+ Y ) .+ Z ) <-> ( X .+ (/) ) C_ ( ( X .+ Y ) .+ Z ) ) )
45 42 44 syl5ibrcom 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( ( Y .+ Z ) = (/) -> ( X .+ ( Y .+ Z ) ) C_ ( ( X .+ Y ) .+ Z ) ) )
46 30 45 jaod 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( ( X = (/) \/ ( Y .+ Z ) = (/) ) -> ( X .+ ( Y .+ Z ) ) C_ ( ( X .+ Y ) .+ Z ) ) )
47 1 2 padd02 
 |-  ( ( K e. HL /\ Z C_ A ) -> ( (/) .+ Z ) = Z )
48 47 3ad2antr3 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( (/) .+ Z ) = Z )
49 48 oveq2d 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( X .+ ( (/) .+ Z ) ) = ( X .+ Z ) )
50 32 oveq1d 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( ( X .+ (/) ) .+ Z ) = ( X .+ Z ) )
51 49 50 eqtr4d 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( X .+ ( (/) .+ Z ) ) = ( ( X .+ (/) ) .+ Z ) )
52 oveq1 
 |-  ( Y = (/) -> ( Y .+ Z ) = ( (/) .+ Z ) )
53 52 oveq2d 
 |-  ( Y = (/) -> ( X .+ ( Y .+ Z ) ) = ( X .+ ( (/) .+ Z ) ) )
54 oveq2 
 |-  ( Y = (/) -> ( X .+ Y ) = ( X .+ (/) ) )
55 54 oveq1d 
 |-  ( Y = (/) -> ( ( X .+ Y ) .+ Z ) = ( ( X .+ (/) ) .+ Z ) )
56 53 55 eqeq12d 
 |-  ( Y = (/) -> ( ( X .+ ( Y .+ Z ) ) = ( ( X .+ Y ) .+ Z ) <-> ( X .+ ( (/) .+ Z ) ) = ( ( X .+ (/) ) .+ Z ) ) )
57 51 56 syl5ibrcom 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( Y = (/) -> ( X .+ ( Y .+ Z ) ) = ( ( X .+ Y ) .+ Z ) ) )
58 1 2 padd01 
 |-  ( ( K e. HL /\ Y C_ A ) -> ( Y .+ (/) ) = Y )
59 58 3ad2antr2 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( Y .+ (/) ) = Y )
60 59 oveq2d 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( X .+ ( Y .+ (/) ) ) = ( X .+ Y ) )
61 1 2 padd01 
 |-  ( ( K e. HL /\ ( X .+ Y ) C_ A ) -> ( ( X .+ Y ) .+ (/) ) = ( X .+ Y ) )
62 37 61 syldan 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( ( X .+ Y ) .+ (/) ) = ( X .+ Y ) )
63 60 62 eqtr4d 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( X .+ ( Y .+ (/) ) ) = ( ( X .+ Y ) .+ (/) ) )
64 oveq2 
 |-  ( Z = (/) -> ( Y .+ Z ) = ( Y .+ (/) ) )
65 64 oveq2d 
 |-  ( Z = (/) -> ( X .+ ( Y .+ Z ) ) = ( X .+ ( Y .+ (/) ) ) )
66 oveq2 
 |-  ( Z = (/) -> ( ( X .+ Y ) .+ Z ) = ( ( X .+ Y ) .+ (/) ) )
67 65 66 eqeq12d 
 |-  ( Z = (/) -> ( ( X .+ ( Y .+ Z ) ) = ( ( X .+ Y ) .+ Z ) <-> ( X .+ ( Y .+ (/) ) ) = ( ( X .+ Y ) .+ (/) ) ) )
68 63 67 syl5ibrcom 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( Z = (/) -> ( X .+ ( Y .+ Z ) ) = ( ( X .+ Y ) .+ Z ) ) )
69 57 68 jaod 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( ( Y = (/) \/ Z = (/) ) -> ( X .+ ( Y .+ Z ) ) = ( ( X .+ Y ) .+ Z ) ) )
70 69 29 syl6 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( ( Y = (/) \/ Z = (/) ) -> ( X .+ ( Y .+ Z ) ) C_ ( ( X .+ Y ) .+ Z ) ) )
71 46 70 jaod 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( ( ( X = (/) \/ ( Y .+ Z ) = (/) ) \/ ( Y = (/) \/ Z = (/) ) ) -> ( X .+ ( Y .+ Z ) ) C_ ( ( X .+ Y ) .+ Z ) ) )
72 15 71 syl5bi 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) -> ( -. ( ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) -> ( X .+ ( Y .+ Z ) ) C_ ( ( X .+ Y ) .+ Z ) ) )
73 72 3impia 
 |-  ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) /\ -. ( ( X =/= (/) /\ ( Y .+ Z ) =/= (/) ) /\ ( Y =/= (/) /\ Z =/= (/) ) ) ) -> ( X .+ ( Y .+ Z ) ) C_ ( ( X .+ Y ) .+ Z ) )