Theorem lvecpsslmod

Description: The class of all (left) vector spaces is a proper subclass of the class of all (left) modules. Although it is obvious (and proven by lveclmod ) that every left vector space is a left module, there is (at least) one left module which is no left vector space, for example the zero module over the zero ring, see lmod1zrnlvec . (Contributed by AV, 29-Apr-2019)

	Ref	Expression
Assertion	lvecpsslmod	⊢ LVec ⊊ LMod

Proof

Step	Hyp	Ref	Expression
1		lveclmod	⊢ ( 𝑣 ∈ LVec → 𝑣 ∈ LMod )
2	1	ssriv	⊢ LVec ⊆ LMod
3		vex	⊢ 𝑖 ∈ V
4		vex	⊢ 𝑧 ∈ V
5	3 4	pm3.2i	⊢ ( 𝑖 ∈ V ∧ 𝑧 ∈ V )
6		eqid	⊢ { ⟨ ( Base ‘ ndx ) , { 𝑧 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ } = { ⟨ ( Base ‘ ndx ) , { 𝑧 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ }
7		eqid	⊢ ( { ⟨ ( Base ‘ ndx ) , { 𝑖 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑖 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , { ⟨ ( Base ‘ ndx ) , { 𝑧 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ } ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , { 𝑖 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑖 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , { ⟨ ( Base ‘ ndx ) , { 𝑧 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ } ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ } )
8	6 7	lmod1zr	⊢ ( ( 𝑖 ∈ V ∧ 𝑧 ∈ V ) → ( { ⟨ ( Base ‘ ndx ) , { 𝑖 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑖 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , { ⟨ ( Base ‘ ndx ) , { 𝑧 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ } ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ } ) ∈ LMod )
9	6 7	lmod1zrnlvec	⊢ ( ( 𝑖 ∈ V ∧ 𝑧 ∈ V ) → ( { ⟨ ( Base ‘ ndx ) , { 𝑖 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑖 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , { ⟨ ( Base ‘ ndx ) , { 𝑧 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ } ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ } ) ∉ LVec )
10		df-nel	⊢ ( ( { ⟨ ( Base ‘ ndx ) , { 𝑖 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑖 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , { ⟨ ( Base ‘ ndx ) , { 𝑧 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ } ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ } ) ∉ LVec ↔ ¬ ( { ⟨ ( Base ‘ ndx ) , { 𝑖 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑖 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , { ⟨ ( Base ‘ ndx ) , { 𝑧 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ } ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ } ) ∈ LVec )
11	9 10	sylib	⊢ ( ( 𝑖 ∈ V ∧ 𝑧 ∈ V ) → ¬ ( { ⟨ ( Base ‘ ndx ) , { 𝑖 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑖 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , { ⟨ ( Base ‘ ndx ) , { 𝑧 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ } ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ } ) ∈ LVec )
12	8 11	jca	⊢ ( ( 𝑖 ∈ V ∧ 𝑧 ∈ V ) → ( ( { ⟨ ( Base ‘ ndx ) , { 𝑖 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑖 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , { ⟨ ( Base ‘ ndx ) , { 𝑧 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ } ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ } ) ∈ LMod ∧ ¬ ( { ⟨ ( Base ‘ ndx ) , { 𝑖 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑖 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , { ⟨ ( Base ‘ ndx ) , { 𝑧 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ } ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ } ) ∈ LVec ) )
13		nelne1	⊢ ( ( ( { ⟨ ( Base ‘ ndx ) , { 𝑖 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑖 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , { ⟨ ( Base ‘ ndx ) , { 𝑧 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ } ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ } ) ∈ LMod ∧ ¬ ( { ⟨ ( Base ‘ ndx ) , { 𝑖 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑖 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , { ⟨ ( Base ‘ ndx ) , { 𝑧 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ } ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ } ) ∈ LVec ) → LMod ≠ LVec )
14	13	necomd	⊢ ( ( ( { ⟨ ( Base ‘ ndx ) , { 𝑖 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑖 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , { ⟨ ( Base ‘ ndx ) , { 𝑧 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ } ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ } ) ∈ LMod ∧ ¬ ( { ⟨ ( Base ‘ ndx ) , { 𝑖 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑖 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , { ⟨ ( Base ‘ ndx ) , { 𝑧 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ } ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ } ) ∈ LVec ) → LVec ≠ LMod )
15	5 12 14	mp2b	⊢ LVec ≠ LMod
16		df-pss	⊢ ( LVec ⊊ LMod ↔ ( LVec ⊆ LMod ∧ LVec ≠ LMod ) )
17	2 15 16	mpbir2an	⊢ LVec ⊊ LMod