| Step |
Hyp |
Ref |
Expression |
| 1 |
|
dvh4dimat.h |
|- H = ( LHyp ` K ) |
| 2 |
|
dvh4dimat.u |
|- U = ( ( DVecH ` K ) ` W ) |
| 3 |
|
dvh3dimat.s |
|- .(+) = ( LSSum ` U ) |
| 4 |
|
dvh3dimat.a |
|- A = ( LSAtoms ` U ) |
| 5 |
|
dvh3dimat.k |
|- ( ph -> ( K e. HL /\ W e. H ) ) |
| 6 |
|
dvh3dimat.p |
|- ( ph -> P e. A ) |
| 7 |
|
dvh3dimat.q |
|- ( ph -> Q e. A ) |
| 8 |
1 2 3 4 5 6 6 7
|
dvh4dimat |
|- ( ph -> E. s e. A -. s C_ ( ( P .(+) P ) .(+) Q ) ) |
| 9 |
1 2 5
|
dvhlmod |
|- ( ph -> U e. LMod ) |
| 10 |
|
eqid |
|- ( LSubSp ` U ) = ( LSubSp ` U ) |
| 11 |
10 4 9 6
|
lsatlssel |
|- ( ph -> P e. ( LSubSp ` U ) ) |
| 12 |
10
|
lsssubg |
|- ( ( U e. LMod /\ P e. ( LSubSp ` U ) ) -> P e. ( SubGrp ` U ) ) |
| 13 |
9 11 12
|
syl2anc |
|- ( ph -> P e. ( SubGrp ` U ) ) |
| 14 |
3
|
lsmidm |
|- ( P e. ( SubGrp ` U ) -> ( P .(+) P ) = P ) |
| 15 |
13 14
|
syl |
|- ( ph -> ( P .(+) P ) = P ) |
| 16 |
15
|
oveq1d |
|- ( ph -> ( ( P .(+) P ) .(+) Q ) = ( P .(+) Q ) ) |
| 17 |
16
|
sseq2d |
|- ( ph -> ( s C_ ( ( P .(+) P ) .(+) Q ) <-> s C_ ( P .(+) Q ) ) ) |
| 18 |
17
|
notbid |
|- ( ph -> ( -. s C_ ( ( P .(+) P ) .(+) Q ) <-> -. s C_ ( P .(+) Q ) ) ) |
| 19 |
18
|
rexbidv |
|- ( ph -> ( E. s e. A -. s C_ ( ( P .(+) P ) .(+) Q ) <-> E. s e. A -. s C_ ( P .(+) Q ) ) ) |
| 20 |
8 19
|
mpbid |
|- ( ph -> E. s e. A -. s C_ ( P .(+) Q ) ) |