Theorem dvh2dimatN

Description: Given an atom, there exists another. (Contributed by NM, 25-Apr-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dvh4dimat.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dvh4dimat.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dvh2dimat.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
	dvh2dimat.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	dvh2dimat.p	⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
Assertion	dvh2dimatN	⊢ ( 𝜑 → ∃ 𝑠 ∈ 𝐴 𝑠 ≠ 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		dvh4dimat.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dvh4dimat.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		dvh2dimat.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
4		dvh2dimat.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
5		dvh2dimat.p	⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
6		eqid	⊢ ( LSSum ‘ 𝑈 ) = ( LSSum ‘ 𝑈 )
7	1 2 6 3 4 5 5	dvh3dimatN	⊢ ( 𝜑 → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ⊆ ( 𝑃 ( LSSum ‘ 𝑈 ) 𝑃 ) )
8	1 2 4	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
9		eqid	⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
10	9 3 8 5	lsatlssel	⊢ ( 𝜑 → 𝑃 ∈ ( LSubSp ‘ 𝑈 ) )
11	9	lsssubg	⊢ ( ( 𝑈 ∈ LMod ∧ 𝑃 ∈ ( LSubSp ‘ 𝑈 ) ) → 𝑃 ∈ ( SubGrp ‘ 𝑈 ) )
12	8 10 11	syl2anc	⊢ ( 𝜑 → 𝑃 ∈ ( SubGrp ‘ 𝑈 ) )
13	6	lsmidm	⊢ ( 𝑃 ∈ ( SubGrp ‘ 𝑈 ) → ( 𝑃 ( LSSum ‘ 𝑈 ) 𝑃 ) = 𝑃 )
14	12 13	syl	⊢ ( 𝜑 → ( 𝑃 ( LSSum ‘ 𝑈 ) 𝑃 ) = 𝑃 )
15	14	sseq2d	⊢ ( 𝜑 → ( 𝑠 ⊆ ( 𝑃 ( LSSum ‘ 𝑈 ) 𝑃 ) ↔ 𝑠 ⊆ 𝑃 ) )
16	15	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝑠 ⊆ ( 𝑃 ( LSSum ‘ 𝑈 ) 𝑃 ) ↔ 𝑠 ⊆ 𝑃 ) )
17	1 2 4	dvhlvec	⊢ ( 𝜑 → 𝑈 ∈ LVec )
18	17	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑈 ∈ LVec )
19		simpr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ 𝐴 )
20	5	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑃 ∈ 𝐴 )
21	3 18 19 20	lsatcmp	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝑠 ⊆ 𝑃 ↔ 𝑠 = 𝑃 ) )
22	16 21	bitrd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝑠 ⊆ ( 𝑃 ( LSSum ‘ 𝑈 ) 𝑃 ) ↔ 𝑠 = 𝑃 ) )
23	22	necon3bbid	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( ¬ 𝑠 ⊆ ( 𝑃 ( LSSum ‘ 𝑈 ) 𝑃 ) ↔ 𝑠 ≠ 𝑃 ) )
24	23	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ⊆ ( 𝑃 ( LSSum ‘ 𝑈 ) 𝑃 ) ↔ ∃ 𝑠 ∈ 𝐴 𝑠 ≠ 𝑃 ) )
25	7 24	mpbid	⊢ ( 𝜑 → ∃ 𝑠 ∈ 𝐴 𝑠 ≠ 𝑃 )