Theorem lmodn0

Description: Left modules exist. (Contributed by AV, 29-Apr-2019)

	Ref	Expression
Assertion	lmodn0	⊢ LMod ≠ ∅

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑖 ∈ V
2		vex	⊢ 𝑧 ∈ V
3	1 2	pm3.2i	⊢ ( 𝑖 ∈ V ∧ 𝑧 ∈ V )
4		eqid	⊢ { ⟨ ( Base ‘ ndx ) , { 𝑧 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ } = { ⟨ ( Base ‘ ndx ) , { 𝑧 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ }
5		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 ) , { ⟨ ⟨ 𝑧 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ } )
6	4 5	lmod1zr	⊢ ( ( 𝑖 ∈ V ∧ 𝑧 ∈ V ) → ( { ⟨ ( Base ‘ ndx ) , { 𝑖 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑖 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , { ⟨ ( Base ‘ ndx ) , { 𝑧 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ } ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ } ) ∈ LMod )
7		ne0i	⊢ ( ( { ⟨ ( Base ‘ ndx ) , { 𝑖 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑖 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , { ⟨ ( Base ‘ ndx ) , { 𝑧 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ } ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ } ) ∈ LMod → LMod ≠ ∅ )
8	3 6 7	mp2b	⊢ LMod ≠ ∅