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 ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihat.p ⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
dihat.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihat.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dihat.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
dihat.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion dihat ( 𝜑 → ( 𝐼 ‘ 𝑃 ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 dihat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dihat.p ⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
3 dihat.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
4 dihat.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 dihat.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
6 dihat.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7 eqid ⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
8 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
9 7 8 1 lhpocat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ ( Atoms ‘ 𝐾 ) )
10 6 9 syl ⊢ ( 𝜑 → ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ ( Atoms ‘ 𝐾 ) )
11 2 10 eqeltrid ⊢ ( 𝜑 → 𝑃 ∈ ( Atoms ‘ 𝐾 ) )
12 8 1 4 3 5 dihatlat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑃 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝐼 ‘ 𝑃 ) ∈ 𝐴 )
13 6 11 12 syl2anc ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑃 ) ∈ 𝐴 )