Theorem lmod1zrnlvec

Description: There is a (left) module (azero module) which is not a (left) vector space. (Contributed by AV, 29-Apr-2019)

	Ref	Expression
Hypotheses	lmod1zr.r	⊢ 𝑅 = { ⟨ ( Base ‘ ndx ) , { 𝑍 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ }
	lmod1zr.m	⊢ 𝑀 = ( { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } )
Assertion	lmod1zrnlvec	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → 𝑀 ∉ LVec )

Proof

Step	Hyp	Ref	Expression
1		lmod1zr.r	⊢ 𝑅 = { ⟨ ( Base ‘ ndx ) , { 𝑍 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ }
2		lmod1zr.m	⊢ 𝑀 = ( { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } )
3		tpex	⊢ { ⟨ ( Base ‘ ndx ) , { 𝑍 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ } ∈ V
4	1 3	eqeltri	⊢ 𝑅 ∈ V
5	2	lmodsca	⊢ ( 𝑅 ∈ V → 𝑅 = ( Scalar ‘ 𝑀 ) )
6	4 5	mp1i	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → 𝑅 = ( Scalar ‘ 𝑀 ) )
7	1	rng1nnzr	⊢ ( 𝑍 ∈ 𝑊 → 𝑅 ∉ NzRing )
8		df-nel	⊢ ( 𝑅 ∉ NzRing ↔ ¬ 𝑅 ∈ NzRing )
9	7 8	sylib	⊢ ( 𝑍 ∈ 𝑊 → ¬ 𝑅 ∈ NzRing )
10		drngnzr	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ NzRing )
11	9 10	nsyl	⊢ ( 𝑍 ∈ 𝑊 → ¬ 𝑅 ∈ DivRing )
12	11	adantl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ¬ 𝑅 ∈ DivRing )
13	6 12	eqneltrrd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ¬ ( Scalar ‘ 𝑀 ) ∈ DivRing )
14	13	intnand	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ¬ ( 𝑀 ∈ LMod ∧ ( Scalar ‘ 𝑀 ) ∈ DivRing ) )
15		df-nel	⊢ ( 𝑀 ∉ LVec ↔ ¬ 𝑀 ∈ LVec )
16		eqid	⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
17	16	islvec	⊢ ( 𝑀 ∈ LVec ↔ ( 𝑀 ∈ LMod ∧ ( Scalar ‘ 𝑀 ) ∈ DivRing ) )
18	15 17	xchbinx	⊢ ( 𝑀 ∉ LVec ↔ ¬ ( 𝑀 ∈ LMod ∧ ( Scalar ‘ 𝑀 ) ∈ DivRing ) )
19	14 18	sylibr	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → 𝑀 ∉ LVec )