lsatspn0

Description: The span of a vector is an atom iff the vector is nonzero. (Contributed by NM, 4-Feb-2015)

	Ref	Expression
Hypotheses	lsatspn0.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lsatspn0.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lsatspn0.o	⊢ 0 = ( 0_g ‘ 𝑊 )
	lsatspn0.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
	isateln0.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	isateln0.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion	lsatspn0	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 ↔ 𝑋 ≠ 0 ) )

Proof

Step	Hyp	Ref	Expression
1		lsatspn0.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lsatspn0.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3		lsatspn0.o	⊢ 0 = ( 0_g ‘ 𝑊 )
4		lsatspn0.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
5		isateln0.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
6		isateln0.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
7	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 ) → 𝑊 ∈ LMod )
8		simpr	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 )
9	3 4 7 8	lsatn0	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 ) → ( 𝑁 ‘ { 𝑋 } ) ≠ { 0 } )
10		sneq	⊢ ( 𝑋 = 0 → { 𝑋 } = { 0 } )
11	10	fveq2d	⊢ ( 𝑋 = 0 → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 0 } ) )
12	11	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 ) ∧ 𝑋 = 0 ) → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 0 } ) )
13	7	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 ) ∧ 𝑋 = 0 ) → 𝑊 ∈ LMod )
14	3 2	lspsn0	⊢ ( 𝑊 ∈ LMod → ( 𝑁 ‘ { 0 } ) = { 0 } )
15	13 14	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 ) ∧ 𝑋 = 0 ) → ( 𝑁 ‘ { 0 } ) = { 0 } )
16	12 15	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 ) ∧ 𝑋 = 0 ) → ( 𝑁 ‘ { 𝑋 } ) = { 0 } )
17	16	ex	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 ) → ( 𝑋 = 0 → ( 𝑁 ‘ { 𝑋 } ) = { 0 } ) )
18	17	necon3d	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 ) → ( ( 𝑁 ‘ { 𝑋 } ) ≠ { 0 } → 𝑋 ≠ 0 ) )
19	9 18	mpd	⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 ) → 𝑋 ≠ 0 )
20	5	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 0 ) → 𝑊 ∈ LMod )
21	6	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ 𝑉 )
22		simpr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 0 ) → 𝑋 ≠ 0 )
23		eldifsn	⊢ ( 𝑋 ∈ ( 𝑉 ∖ { 0 } ) ↔ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) )
24	21 22 23	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
25	1 2 3 4 20 24	lsatlspsn	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 0 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 )
26	19 25	impbida	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ∈ 𝐴 ↔ 𝑋 ≠ 0 ) )

Metamath Proof Explorer

Theorem lsatspn0

Proof