| Step |
Hyp |
Ref |
Expression |
| 1 |
|
polat.o |
|- ._|_ = ( oc ` K ) |
| 2 |
|
polat.a |
|- A = ( Atoms ` K ) |
| 3 |
|
polat.m |
|- M = ( pmap ` K ) |
| 4 |
|
polat.p |
|- P = ( _|_P ` K ) |
| 5 |
|
snssi |
|- ( Q e. A -> { Q } C_ A ) |
| 6 |
1 2 3 4
|
polvalN |
|- ( ( K e. OL /\ { Q } C_ A ) -> ( P ` { Q } ) = ( A i^i |^|_ p e. { Q } ( M ` ( ._|_ ` p ) ) ) ) |
| 7 |
5 6
|
sylan2 |
|- ( ( K e. OL /\ Q e. A ) -> ( P ` { Q } ) = ( A i^i |^|_ p e. { Q } ( M ` ( ._|_ ` p ) ) ) ) |
| 8 |
|
2fveq3 |
|- ( p = Q -> ( M ` ( ._|_ ` p ) ) = ( M ` ( ._|_ ` Q ) ) ) |
| 9 |
8
|
iinxsng |
|- ( Q e. A -> |^|_ p e. { Q } ( M ` ( ._|_ ` p ) ) = ( M ` ( ._|_ ` Q ) ) ) |
| 10 |
9
|
adantl |
|- ( ( K e. OL /\ Q e. A ) -> |^|_ p e. { Q } ( M ` ( ._|_ ` p ) ) = ( M ` ( ._|_ ` Q ) ) ) |
| 11 |
10
|
ineq2d |
|- ( ( K e. OL /\ Q e. A ) -> ( A i^i |^|_ p e. { Q } ( M ` ( ._|_ ` p ) ) ) = ( A i^i ( M ` ( ._|_ ` Q ) ) ) ) |
| 12 |
|
olop |
|- ( K e. OL -> K e. OP ) |
| 13 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
| 14 |
13 2
|
atbase |
|- ( Q e. A -> Q e. ( Base ` K ) ) |
| 15 |
13 1
|
opoccl |
|- ( ( K e. OP /\ Q e. ( Base ` K ) ) -> ( ._|_ ` Q ) e. ( Base ` K ) ) |
| 16 |
12 14 15
|
syl2an |
|- ( ( K e. OL /\ Q e. A ) -> ( ._|_ ` Q ) e. ( Base ` K ) ) |
| 17 |
13 2 3
|
pmapssat |
|- ( ( K e. OL /\ ( ._|_ ` Q ) e. ( Base ` K ) ) -> ( M ` ( ._|_ ` Q ) ) C_ A ) |
| 18 |
16 17
|
syldan |
|- ( ( K e. OL /\ Q e. A ) -> ( M ` ( ._|_ ` Q ) ) C_ A ) |
| 19 |
|
sseqin2 |
|- ( ( M ` ( ._|_ ` Q ) ) C_ A <-> ( A i^i ( M ` ( ._|_ ` Q ) ) ) = ( M ` ( ._|_ ` Q ) ) ) |
| 20 |
18 19
|
sylib |
|- ( ( K e. OL /\ Q e. A ) -> ( A i^i ( M ` ( ._|_ ` Q ) ) ) = ( M ` ( ._|_ ` Q ) ) ) |
| 21 |
7 11 20
|
3eqtrd |
|- ( ( K e. OL /\ Q e. A ) -> ( P ` { Q } ) = ( M ` ( ._|_ ` Q ) ) ) |