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 ⊢ φ → K ∈ HL ∧ W ∈ H
Assertion dihat ⊢ φ → I ⁡ P ∈ 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 ⊢ φ → K ∈ HL ∧ W ∈ H
7 eqid ⊢ oc ⁡ K = oc ⁡ K
8 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
9 7 8 1 lhpocat ⊢ K ∈ HL ∧ W ∈ H → oc ⁡ K ⁡ W ∈ Atoms ⁡ K
10 6 9 syl ⊢ φ → oc ⁡ K ⁡ W ∈ Atoms ⁡ K
11 2 10 eqeltrid ⊢ φ → P ∈ Atoms ⁡ K
12 8 1 4 3 5 dihatlat ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ Atoms ⁡ K → I ⁡ P ∈ A
13 6 11 12 syl2anc ⊢ φ → I ⁡ P ∈ A