This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dihat

Description: There exists at least one atom in the subspaces of vector space H. (Contributed by NM, 12-Aug-2014)

Ref Expression
Hypotheses dihat.h 
|- H = ( LHyp ` K )
dihat.p 
|- P = ( ( oc ` K ) ` W )
dihat.i 
|- I = ( ( DIsoH ` K ) ` W )
dihat.u 
|- U = ( ( DVecH ` K ) ` W )
dihat.a 
|- A = ( LSAtoms ` U )
dihat.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion dihat 
|- ( ph -> ( I ` P ) e. A )

Proof

Step Hyp Ref Expression
1 dihat.h 
 |-  H = ( LHyp ` K )
2 dihat.p 
 |-  P = ( ( oc ` K ) ` W )
3 dihat.i 
 |-  I = ( ( DIsoH ` K ) ` W )
4 dihat.u 
 |-  U = ( ( DVecH ` K ) ` W )
5 dihat.a 
 |-  A = ( LSAtoms ` U )
6 dihat.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
7 eqid 
 |-  ( oc ` K ) = ( oc ` K )
8 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
9 7 8 1 lhpocat 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( oc ` K ) ` W ) e. ( Atoms ` K ) )
10 6 9 syl 
 |-  ( ph -> ( ( oc ` K ) ` W ) e. ( Atoms ` K ) )
11 2 10 eqeltrid 
 |-  ( ph -> P e. ( Atoms ` K ) )
12 8 1 4 3 5 dihatlat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ P e. ( Atoms ` K ) ) -> ( I ` P ) e. A )
13 6 11 12 syl2anc 
 |-  ( ph -> ( I ` P ) e. A )