lsatn0

Description: A 1-dim subspace (atom) of a left module or left vector space is nonzero. ( atne0 analog.) (Contributed by NM, 25-Aug-2014)

	Ref	Expression
Hypotheses	lsatn0.o	⊢ 0 = ( 0_g ‘ 𝑊 )
	lsatn0.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
	lsatn0.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lsatn0.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
Assertion	lsatn0	⊢ ( 𝜑 → 𝑈 ≠ { 0 } )

Proof

Step	Hyp	Ref	Expression
1		lsatn0.o	⊢ 0 = ( 0_g ‘ 𝑊 )
2		lsatn0.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
3		lsatn0.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
4		lsatn0.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
5		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
6		eqid	⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
7	5 6 1 2	islsat	⊢ ( 𝑊 ∈ LMod → ( 𝑈 ∈ 𝐴 ↔ ∃ 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) )
8	3 7	syl	⊢ ( 𝜑 → ( 𝑈 ∈ 𝐴 ↔ ∃ 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ) )
9	4 8	mpbid	⊢ ( 𝜑 → ∃ 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) )
10		eldifsn	⊢ ( 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ↔ ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ 𝑣 ≠ 0 ) )
11	5 1 6	lspsneq0	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) = { 0 } ↔ 𝑣 = 0 ) )
12	3 11	sylan	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) = { 0 } ↔ 𝑣 = 0 ) )
13	12	biimpd	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) = { 0 } → 𝑣 = 0 ) )
14	13	necon3d	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑣 ≠ 0 → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ≠ { 0 } ) )
15	14	expimpd	⊢ ( 𝜑 → ( ( 𝑣 ∈ ( Base ‘ 𝑊 ) ∧ 𝑣 ≠ 0 ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ≠ { 0 } ) )
16	10 15	biimtrid	⊢ ( 𝜑 → ( 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ≠ { 0 } ) )
17		neeq1	⊢ ( 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → ( 𝑈 ≠ { 0 } ↔ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ≠ { 0 } ) )
18	17	biimprcd	⊢ ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) ≠ { 0 } → ( 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → 𝑈 ≠ { 0 } ) )
19	16 18	syl6	⊢ ( 𝜑 → ( 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) → ( 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → 𝑈 ≠ { 0 } ) ) )
20	19	rexlimdv	⊢ ( 𝜑 → ( ∃ 𝑣 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑈 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑣 } ) → 𝑈 ≠ { 0 } ) )
21	9 20	mpd	⊢ ( 𝜑 → 𝑈 ≠ { 0 } )

Metamath Proof Explorer

Theorem lsatn0

Proof