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

Metamath Proof Explorer

Theorem dvh1dimat

Description: There exists an atom. (Contributed by NM, 25-Apr-2015)

Ref Expression
Hypotheses dvh4dimat.h ⊢ H = LHyp ⁡ K
dvh4dimat.u ⊢ U = DVecH ⁡ K ⁡ W
dvh1dimat.a ⊢ A = LSAtoms ⁡ U
dvh1dimat.k ⊢ φ → K ∈ HL ∧ W ∈ H
Assertion dvh1dimat ⊢ φ → ∃ s s ∈ A

Proof

Step Hyp Ref Expression
1 dvh4dimat.h ⊢ H = LHyp ⁡ K
2 dvh4dimat.u ⊢ U = DVecH ⁡ K ⁡ W
3 dvh1dimat.a ⊢ A = LSAtoms ⁡ U
4 dvh1dimat.k ⊢ φ → K ∈ HL ∧ W ∈ H
5 eqid ⊢ oc ⁡ K ⁡ W = oc ⁡ K ⁡ W
6 eqid ⊢ DIsoH ⁡ K ⁡ W = DIsoH ⁡ K ⁡ W
7 1 5 6 2 3 4 dihat ⊢ φ → DIsoH ⁡ K ⁡ W ⁡ oc ⁡ K ⁡ W ∈ A
8 elex2 ⊢ DIsoH ⁡ K ⁡ W ⁡ oc ⁡ K ⁡ W ∈ A → ∃ s s ∈ A
9 7 8 syl ⊢ φ → ∃ s s ∈ A