Step |
Hyp |
Ref |
Expression |
1 |
|
paddass.a |
|- A = ( Atoms ` K ) |
2 |
|
paddass.p |
|- .+ = ( +P ` K ) |
3 |
|
simp1 |
|- ( ( K e. HL /\ ( X C_ A /\ Y C_ A ) /\ ( Z C_ A /\ W C_ A ) ) -> K e. HL ) |
4 |
|
simp2r |
|- ( ( K e. HL /\ ( X C_ A /\ Y C_ A ) /\ ( Z C_ A /\ W C_ A ) ) -> Y C_ A ) |
5 |
|
simp3l |
|- ( ( K e. HL /\ ( X C_ A /\ Y C_ A ) /\ ( Z C_ A /\ W C_ A ) ) -> Z C_ A ) |
6 |
|
simp3r |
|- ( ( K e. HL /\ ( X C_ A /\ Y C_ A ) /\ ( Z C_ A /\ W C_ A ) ) -> W C_ A ) |
7 |
1 2
|
padd12N |
|- ( ( K e. HL /\ ( Y C_ A /\ Z C_ A /\ W C_ A ) ) -> ( Y .+ ( Z .+ W ) ) = ( Z .+ ( Y .+ W ) ) ) |
8 |
3 4 5 6 7
|
syl13anc |
|- ( ( K e. HL /\ ( X C_ A /\ Y C_ A ) /\ ( Z C_ A /\ W C_ A ) ) -> ( Y .+ ( Z .+ W ) ) = ( Z .+ ( Y .+ W ) ) ) |
9 |
8
|
oveq2d |
|- ( ( K e. HL /\ ( X C_ A /\ Y C_ A ) /\ ( Z C_ A /\ W C_ A ) ) -> ( X .+ ( Y .+ ( Z .+ W ) ) ) = ( X .+ ( Z .+ ( Y .+ W ) ) ) ) |
10 |
|
simp2l |
|- ( ( K e. HL /\ ( X C_ A /\ Y C_ A ) /\ ( Z C_ A /\ W C_ A ) ) -> X C_ A ) |
11 |
1 2
|
paddssat |
|- ( ( K e. HL /\ Z C_ A /\ W C_ A ) -> ( Z .+ W ) C_ A ) |
12 |
3 5 6 11
|
syl3anc |
|- ( ( K e. HL /\ ( X C_ A /\ Y C_ A ) /\ ( Z C_ A /\ W C_ A ) ) -> ( Z .+ W ) C_ A ) |
13 |
1 2
|
paddass |
|- ( ( K e. HL /\ ( X C_ A /\ Y C_ A /\ ( Z .+ W ) C_ A ) ) -> ( ( X .+ Y ) .+ ( Z .+ W ) ) = ( X .+ ( Y .+ ( Z .+ W ) ) ) ) |
14 |
3 10 4 12 13
|
syl13anc |
|- ( ( K e. HL /\ ( X C_ A /\ Y C_ A ) /\ ( Z C_ A /\ W C_ A ) ) -> ( ( X .+ Y ) .+ ( Z .+ W ) ) = ( X .+ ( Y .+ ( Z .+ W ) ) ) ) |
15 |
1 2
|
paddssat |
|- ( ( K e. HL /\ Y C_ A /\ W C_ A ) -> ( Y .+ W ) C_ A ) |
16 |
3 4 6 15
|
syl3anc |
|- ( ( K e. HL /\ ( X C_ A /\ Y C_ A ) /\ ( Z C_ A /\ W C_ A ) ) -> ( Y .+ W ) C_ A ) |
17 |
1 2
|
paddass |
|- ( ( K e. HL /\ ( X C_ A /\ Z C_ A /\ ( Y .+ W ) C_ A ) ) -> ( ( X .+ Z ) .+ ( Y .+ W ) ) = ( X .+ ( Z .+ ( Y .+ W ) ) ) ) |
18 |
3 10 5 16 17
|
syl13anc |
|- ( ( K e. HL /\ ( X C_ A /\ Y C_ A ) /\ ( Z C_ A /\ W C_ A ) ) -> ( ( X .+ Z ) .+ ( Y .+ W ) ) = ( X .+ ( Z .+ ( Y .+ W ) ) ) ) |
19 |
9 14 18
|
3eqtr4d |
|- ( ( K e. HL /\ ( X C_ A /\ Y C_ A ) /\ ( Z C_ A /\ W C_ A ) ) -> ( ( X .+ Y ) .+ ( Z .+ W ) ) = ( ( X .+ Z ) .+ ( Y .+ W ) ) ) |