Step |
Hyp |
Ref |
Expression |
1 |
|
pexmidALT.a |
|- A = ( Atoms ` K ) |
2 |
|
pexmidALT.p |
|- .+ = ( +P ` K ) |
3 |
|
pexmidALT.o |
|- ._|_ = ( _|_P ` K ) |
4 |
|
id |
|- ( X = (/) -> X = (/) ) |
5 |
|
fveq2 |
|- ( X = (/) -> ( ._|_ ` X ) = ( ._|_ ` (/) ) ) |
6 |
4 5
|
oveq12d |
|- ( X = (/) -> ( X .+ ( ._|_ ` X ) ) = ( (/) .+ ( ._|_ ` (/) ) ) ) |
7 |
1 3
|
pol0N |
|- ( K e. HL -> ( ._|_ ` (/) ) = A ) |
8 |
|
eqimss |
|- ( ( ._|_ ` (/) ) = A -> ( ._|_ ` (/) ) C_ A ) |
9 |
7 8
|
syl |
|- ( K e. HL -> ( ._|_ ` (/) ) C_ A ) |
10 |
1 2
|
padd02 |
|- ( ( K e. HL /\ ( ._|_ ` (/) ) C_ A ) -> ( (/) .+ ( ._|_ ` (/) ) ) = ( ._|_ ` (/) ) ) |
11 |
9 10
|
mpdan |
|- ( K e. HL -> ( (/) .+ ( ._|_ ` (/) ) ) = ( ._|_ ` (/) ) ) |
12 |
11 7
|
eqtrd |
|- ( K e. HL -> ( (/) .+ ( ._|_ ` (/) ) ) = A ) |
13 |
12
|
ad2antrr |
|- ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> ( (/) .+ ( ._|_ ` (/) ) ) = A ) |
14 |
6 13
|
sylan9eqr |
|- ( ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) /\ X = (/) ) -> ( X .+ ( ._|_ ` X ) ) = A ) |
15 |
1 2 3
|
pexmidlem8N |
|- ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) -> ( X .+ ( ._|_ ` X ) ) = A ) |
16 |
15
|
anassrs |
|- ( ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) /\ X =/= (/) ) -> ( X .+ ( ._|_ ` X ) ) = A ) |
17 |
14 16
|
pm2.61dane |
|- ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> ( X .+ ( ._|_ ` X ) ) = A ) |