Theorem lsatelbN

Description: A nonzero vector in an atom determines the atom. (Contributed by NM, 3-Feb-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lsatelb.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lsatelb.o	⊢ 0 = ( 0g ‘ 𝑊 )
	lsatelb.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lsatelb.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
	lsatelb.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lsatelb.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
	lsatelb.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
Assertion	lsatelbN	⊢ ( 𝜑 → ( 𝑋 ∈ 𝑈 ↔ 𝑈 = ( 𝑁 ‘ { 𝑋 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		lsatelb.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lsatelb.o	⊢ 0 = ( 0g ‘ 𝑊 )
3		lsatelb.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4		lsatelb.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
5		lsatelb.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
6		lsatelb.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
7		lsatelb.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
8	5	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑊 ∈ LVec )
9	7	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑈 ∈ 𝐴 )
10		simpr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ 𝑈 )
11		eldifsn	⊢ ( 𝑋 ∈ ( 𝑉 ∖ { 0 } ) ↔ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) )
12	6 11	sylib	⊢ ( 𝜑 → ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) )
13	12	simprd	⊢ ( 𝜑 → 𝑋 ≠ 0 )
14	13	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ≠ 0 )
15	2 3 4 8 9 10 14	lsatel	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑈 = ( 𝑁 ‘ { 𝑋 } ) )
16		eqimss2	⊢ ( 𝑈 = ( 𝑁 ‘ { 𝑋 } ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )
17	16	adantl	⊢ ( ( 𝜑 ∧ 𝑈 = ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )
18		eqid	⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
19		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
20	5 19	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
21	18 4 20 7	lsatlssel	⊢ ( 𝜑 → 𝑈 ∈ ( LSubSp ‘ 𝑊 ) )
22	6	eldifad	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
23	1 18 3 20 21 22	ellspsn5b	⊢ ( 𝜑 → ( 𝑋 ∈ 𝑈 ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ) )
24	23	adantr	⊢ ( ( 𝜑 ∧ 𝑈 = ( 𝑁 ‘ { 𝑋 } ) ) → ( 𝑋 ∈ 𝑈 ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ) )
25	17 24	mpbird	⊢ ( ( 𝜑 ∧ 𝑈 = ( 𝑁 ‘ { 𝑋 } ) ) → 𝑋 ∈ 𝑈 )
26	15 25	impbida	⊢ ( 𝜑 → ( 𝑋 ∈ 𝑈 ↔ 𝑈 = ( 𝑁 ‘ { 𝑋 } ) ) )