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	⊢ ( 𝜑 → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ⊆ ( 𝑃 ⊕ 𝑄 ) )