Theorem lsatel

Description: A nonzero vector in an atom determines the atom. (Contributed by NM, 25-Aug-2014)

	Ref	Expression
Hypotheses	lsatel.o	⊢ 0 = ( 0g ‘ 𝑊 )
	lsatel.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lsatel.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
	lsatel.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lsatel.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
	lsatel.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
	lsatel.e	⊢ ( 𝜑 → 𝑋 ≠ 0 )
Assertion	lsatel	⊢ ( 𝜑 → 𝑈 = ( 𝑁 ‘ { 𝑋 } ) )

Proof

Step	Hyp	Ref	Expression
1		lsatel.o	⊢ 0 = ( 0g ‘ 𝑊 )
2		lsatel.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3		lsatel.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
4		lsatel.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
5		lsatel.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
6		lsatel.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
7		lsatel.e	⊢ ( 𝜑 → 𝑋 ≠ 0 )
8		eqid	⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
9		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
10	4 9	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
11	8 3 10 5	lsatlssel	⊢ ( 𝜑 → 𝑈 ∈ ( LSubSp ‘ 𝑊 ) )
12	8 2 10 11 6	ellspsn5	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )
13		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
14	13 8	lssel	⊢ ( ( 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ ( Base ‘ 𝑊 ) )
15	11 6 14	syl2anc	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑊 ) )
16	13 2 1 3	lsatlspsn2	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ∧ 𝑋 ≠ 0 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 )
17	10 15 7 16	syl3anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 )
18	3 4 17 5	lsatcmp	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ↔ ( 𝑁 ‘ { 𝑋 } ) = 𝑈 ) )
19	12 18	mpbid	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) = 𝑈 )
20	19	eqcomd	⊢ ( 𝜑 → 𝑈 = ( 𝑁 ‘ { 𝑋 } ) )