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

Metamath Proof Explorer

Theorem dvh3dimatN

Description: There is an atom that is outside the subspace sum of 2 others. (Contributed by NM, 25-Apr-2015) (New usage is discouraged.)

Ref Expression
Hypotheses dvh4dimat.h ⊢ H = LHyp ⁡ K
dvh4dimat.u ⊢ U = DVecH ⁡ K ⁡ W
dvh3dimat.s ⊢ ⊕ ˙ = LSSum ⁡ U
dvh3dimat.a ⊢ A = LSAtoms ⁡ U
dvh3dimat.k ⊢ φ → K ∈ HL ∧ W ∈ H
dvh3dimat.p ⊢ φ → P ∈ A
dvh3dimat.q ⊢ φ → Q ∈ A
Assertion dvh3dimatN ⊢ φ → ∃ s ∈ A ¬ s ⊆ P ⊕ ˙ Q

Proof

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 ⊢ φ → K ∈ HL ∧ W ∈ H
6 dvh3dimat.p ⊢ φ → P ∈ A
7 dvh3dimat.q ⊢ φ → Q ∈ A
8 1 2 3 4 5 6 6 7 dvh4dimat ⊢ φ → ∃ s ∈ A ¬ s ⊆ P ⊕ ˙ P ⊕ ˙ Q
9 1 2 5 dvhlmod ⊢ φ → U ∈ LMod
10 eqid ⊢ LSubSp ⁡ U = LSubSp ⁡ U
11 10 4 9 6 lsatlssel ⊢ φ → P ∈ LSubSp ⁡ U
12 10 lsssubg ⊢ U ∈ LMod ∧ P ∈ LSubSp ⁡ U → P ∈ SubGrp ⁡ U
13 9 11 12 syl2anc ⊢ φ → P ∈ SubGrp ⁡ U
14 3 lsmidm ⊢ P ∈ SubGrp ⁡ U → P ⊕ ˙ P = P
15 13 14 syl ⊢ φ → P ⊕ ˙ P = P
16 15 oveq1d ⊢ φ → P ⊕ ˙ P ⊕ ˙ Q = P ⊕ ˙ Q
17 16 sseq2d ⊢ φ → s ⊆ P ⊕ ˙ P ⊕ ˙ Q ↔ s ⊆ P ⊕ ˙ Q
18 17 notbid ⊢ φ → ¬ s ⊆ P ⊕ ˙ P ⊕ ˙ Q ↔ ¬ s ⊆ P ⊕ ˙ Q
19 18 rexbidv ⊢ φ → ∃ s ∈ A ¬ s ⊆ P ⊕ ˙ P ⊕ ˙ Q ↔ ∃ s ∈ A ¬ s ⊆ P ⊕ ˙ Q
20 8 19 mpbid ⊢ φ → ∃ s ∈ A ¬ s ⊆ P ⊕ ˙ Q