| Step |
Hyp |
Ref |
Expression |
| 1 |
|
dvh4dimat.h |
|- H = ( LHyp ` K ) |
| 2 |
|
dvh4dimat.u |
|- U = ( ( DVecH ` K ) ` W ) |
| 3 |
|
dvh2dimat.a |
|- A = ( LSAtoms ` U ) |
| 4 |
|
dvh2dimat.k |
|- ( ph -> ( K e. HL /\ W e. H ) ) |
| 5 |
|
dvh2dimat.p |
|- ( ph -> P e. A ) |
| 6 |
|
eqid |
|- ( LSSum ` U ) = ( LSSum ` U ) |
| 7 |
1 2 6 3 4 5 5
|
dvh3dimatN |
|- ( ph -> E. s e. A -. s C_ ( P ( LSSum ` U ) P ) ) |
| 8 |
1 2 4
|
dvhlmod |
|- ( ph -> U e. LMod ) |
| 9 |
|
eqid |
|- ( LSubSp ` U ) = ( LSubSp ` U ) |
| 10 |
9 3 8 5
|
lsatlssel |
|- ( ph -> P e. ( LSubSp ` U ) ) |
| 11 |
9
|
lsssubg |
|- ( ( U e. LMod /\ P e. ( LSubSp ` U ) ) -> P e. ( SubGrp ` U ) ) |
| 12 |
8 10 11
|
syl2anc |
|- ( ph -> P e. ( SubGrp ` U ) ) |
| 13 |
6
|
lsmidm |
|- ( P e. ( SubGrp ` U ) -> ( P ( LSSum ` U ) P ) = P ) |
| 14 |
12 13
|
syl |
|- ( ph -> ( P ( LSSum ` U ) P ) = P ) |
| 15 |
14
|
sseq2d |
|- ( ph -> ( s C_ ( P ( LSSum ` U ) P ) <-> s C_ P ) ) |
| 16 |
15
|
adantr |
|- ( ( ph /\ s e. A ) -> ( s C_ ( P ( LSSum ` U ) P ) <-> s C_ P ) ) |
| 17 |
1 2 4
|
dvhlvec |
|- ( ph -> U e. LVec ) |
| 18 |
17
|
adantr |
|- ( ( ph /\ s e. A ) -> U e. LVec ) |
| 19 |
|
simpr |
|- ( ( ph /\ s e. A ) -> s e. A ) |
| 20 |
5
|
adantr |
|- ( ( ph /\ s e. A ) -> P e. A ) |
| 21 |
3 18 19 20
|
lsatcmp |
|- ( ( ph /\ s e. A ) -> ( s C_ P <-> s = P ) ) |
| 22 |
16 21
|
bitrd |
|- ( ( ph /\ s e. A ) -> ( s C_ ( P ( LSSum ` U ) P ) <-> s = P ) ) |
| 23 |
22
|
necon3bbid |
|- ( ( ph /\ s e. A ) -> ( -. s C_ ( P ( LSSum ` U ) P ) <-> s =/= P ) ) |
| 24 |
23
|
rexbidva |
|- ( ph -> ( E. s e. A -. s C_ ( P ( LSSum ` U ) P ) <-> E. s e. A s =/= P ) ) |
| 25 |
7 24
|
mpbid |
|- ( ph -> E. s e. A s =/= P ) |