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 ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dvh4dimat.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dvh3dimat.s ⊢ ⊕ = ( LSSum ‘ 𝑈 )
dvh3dimat.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
dvh3dimat.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dvh3dimat.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
dvh3dimat.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
Assertion dvh3dimatN ( 𝜑 → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ⊆ ( 𝑃 ⊕ 𝑄 ) )

Proof

Step Hyp Ref Expression
1 dvh4dimat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dvh4dimat.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 dvh3dimat.s ⊢ ⊕ = ( LSSum ‘ 𝑈 )
4 dvh3dimat.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
5 dvh3dimat.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6 dvh3dimat.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
7 dvh3dimat.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
8 1 2 3 4 5 6 6 7 dvh4dimat ⊢ ( 𝜑 → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ⊆ ( ( 𝑃 ⊕ 𝑃 ) ⊕ 𝑄 ) )
9 1 2 5 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
10 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
11 10 4 9 6 lsatlssel ⊢ ( 𝜑 → 𝑃 ∈ ( LSubSp ‘ 𝑈 ) )
12 10 lsssubg ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑃 ∈ ( LSubSp ‘ 𝑈 ) ) → 𝑃 ∈ ( SubGrp ‘ 𝑈 ) )
13 9 11 12 syl2anc ⊢ ( 𝜑 → 𝑃 ∈ ( SubGrp ‘ 𝑈 ) )
14 3 lsmidm ⊢ ( 𝑃 ∈ ( SubGrp ‘ 𝑈 ) → ( 𝑃 ⊕ 𝑃 ) = 𝑃 )
15 13 14 syl ⊢ ( 𝜑 → ( 𝑃 ⊕ 𝑃 ) = 𝑃 )
16 15 oveq1d ⊢ ( 𝜑 → ( ( 𝑃 ⊕ 𝑃 ) ⊕ 𝑄 ) = ( 𝑃 ⊕ 𝑄 ) )
17 16 sseq2d ⊢ ( 𝜑 → ( 𝑠 ⊆ ( ( 𝑃 ⊕ 𝑃 ) ⊕ 𝑄 ) ↔ 𝑠 ⊆ ( 𝑃 ⊕ 𝑄 ) ) )
18 17 notbid ⊢ ( 𝜑 → ( ¬ 𝑠 ⊆ ( ( 𝑃 ⊕ 𝑃 ) ⊕ 𝑄 ) ↔ ¬ 𝑠 ⊆ ( 𝑃 ⊕ 𝑄 ) ) )
19 18 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ⊆ ( ( 𝑃 ⊕ 𝑃 ) ⊕ 𝑄 ) ↔ ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ⊆ ( 𝑃 ⊕ 𝑄 ) ) )
20 8 19 mpbid ⊢ ( 𝜑 → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ⊆ ( 𝑃 ⊕ 𝑄 ) )