Step |
Hyp |
Ref |
Expression |
1 |
|
2polss.a |
|- A = ( Atoms ` K ) |
2 |
|
2polss.p |
|- ._|_ = ( _|_P ` K ) |
3 |
|
simp3 |
|- ( ( K e. HL /\ Y C_ A /\ X C_ Y ) -> X C_ Y ) |
4 |
|
iinss1 |
|- ( X C_ Y -> |^|_ p e. Y ( ( pmap ` K ) ` ( ( oc ` K ) ` p ) ) C_ |^|_ p e. X ( ( pmap ` K ) ` ( ( oc ` K ) ` p ) ) ) |
5 |
|
sslin |
|- ( |^|_ p e. Y ( ( pmap ` K ) ` ( ( oc ` K ) ` p ) ) C_ |^|_ p e. X ( ( pmap ` K ) ` ( ( oc ` K ) ` p ) ) -> ( A i^i |^|_ p e. Y ( ( pmap ` K ) ` ( ( oc ` K ) ` p ) ) ) C_ ( A i^i |^|_ p e. X ( ( pmap ` K ) ` ( ( oc ` K ) ` p ) ) ) ) |
6 |
3 4 5
|
3syl |
|- ( ( K e. HL /\ Y C_ A /\ X C_ Y ) -> ( A i^i |^|_ p e. Y ( ( pmap ` K ) ` ( ( oc ` K ) ` p ) ) ) C_ ( A i^i |^|_ p e. X ( ( pmap ` K ) ` ( ( oc ` K ) ` p ) ) ) ) |
7 |
|
eqid |
|- ( oc ` K ) = ( oc ` K ) |
8 |
|
eqid |
|- ( pmap ` K ) = ( pmap ` K ) |
9 |
7 1 8 2
|
polvalN |
|- ( ( K e. HL /\ Y C_ A ) -> ( ._|_ ` Y ) = ( A i^i |^|_ p e. Y ( ( pmap ` K ) ` ( ( oc ` K ) ` p ) ) ) ) |
10 |
9
|
3adant3 |
|- ( ( K e. HL /\ Y C_ A /\ X C_ Y ) -> ( ._|_ ` Y ) = ( A i^i |^|_ p e. Y ( ( pmap ` K ) ` ( ( oc ` K ) ` p ) ) ) ) |
11 |
|
simp1 |
|- ( ( K e. HL /\ Y C_ A /\ X C_ Y ) -> K e. HL ) |
12 |
|
simp2 |
|- ( ( K e. HL /\ Y C_ A /\ X C_ Y ) -> Y C_ A ) |
13 |
3 12
|
sstrd |
|- ( ( K e. HL /\ Y C_ A /\ X C_ Y ) -> X C_ A ) |
14 |
7 1 8 2
|
polvalN |
|- ( ( K e. HL /\ X C_ A ) -> ( ._|_ ` X ) = ( A i^i |^|_ p e. X ( ( pmap ` K ) ` ( ( oc ` K ) ` p ) ) ) ) |
15 |
11 13 14
|
syl2anc |
|- ( ( K e. HL /\ Y C_ A /\ X C_ Y ) -> ( ._|_ ` X ) = ( A i^i |^|_ p e. X ( ( pmap ` K ) ` ( ( oc ` K ) ` p ) ) ) ) |
16 |
6 10 15
|
3sstr4d |
|- ( ( K e. HL /\ Y C_ A /\ X C_ Y ) -> ( ._|_ ` Y ) C_ ( ._|_ ` X ) ) |