This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zclmncvs

Description: The ring of integers as left module over itself is a subcomplex module, but not a subcomplex vector space. The vector operation is + , and the scalar product is x. . (Contributed by AV, 22-Oct-2021)

Ref Expression
Hypothesis zclmncvs.z ⊢ 𝑍 = ( ringLMod ‘ ℤring )
Assertion zclmncvs ( 𝑍 ∈ ℂMod ∧ 𝑍 ∉ ℂVec )

Proof

Step Hyp Ref Expression
1 zclmncvs.z ⊢ 𝑍 = ( ringLMod ‘ ℤring )
2 zringring ⊢ ℤring ∈ Ring
3 rlmlmod ⊢ ( ℤring ∈ Ring → ( ringLMod ‘ ℤring ) ∈ LMod )
4 2 3 ax-mp ⊢ ( ringLMod ‘ ℤring ) ∈ LMod
5 rlmsca ⊢ ( ℤring ∈ Ring → ℤring = ( Scalar ‘ ( ringLMod ‘ ℤring ) ) )
6 2 5 ax-mp ⊢ ℤring = ( Scalar ‘ ( ringLMod ‘ ℤring ) )
7 df-zring ⊢ ℤring = ( ℂfld ↾s ℤ )
8 6 7 eqtr3i ⊢ ( Scalar ‘ ( ringLMod ‘ ℤring ) ) = ( ℂfld ↾s ℤ )
9 zsubrg ⊢ ℤ ∈ ( SubRing ‘ ℂfld )
10 eqid ⊢ ( Scalar ‘ ( ringLMod ‘ ℤring ) ) = ( Scalar ‘ ( ringLMod ‘ ℤring ) )
11 10 isclmi ⊢ ( ( ( ringLMod ‘ ℤring ) ∈ LMod ∧ ( Scalar ‘ ( ringLMod ‘ ℤring ) ) = ( ℂfld ↾s ℤ ) ∧ ℤ ∈ ( SubRing ‘ ℂfld ) ) → ( ringLMod ‘ ℤring ) ∈ ℂMod )
12 4 8 9 11 mp3an ⊢ ( ringLMod ‘ ℤring ) ∈ ℂMod
13 1 eleq1i ⊢ ( 𝑍 ∈ ℂMod ↔ ( ringLMod ‘ ℤring ) ∈ ℂMod )
14 12 13 mpbir ⊢ 𝑍 ∈ ℂMod
15 zringndrg ⊢ ℤring ∉ DivRing
16 15 neli ⊢ ¬ ℤring ∈ DivRing
17 5 eqcomd ⊢ ( ℤring ∈ Ring → ( Scalar ‘ ( ringLMod ‘ ℤring ) ) = ℤring )
18 2 17 ax-mp ⊢ ( Scalar ‘ ( ringLMod ‘ ℤring ) ) = ℤring
19 18 eleq1i ⊢ ( ( Scalar ‘ ( ringLMod ‘ ℤring ) ) ∈ DivRing ↔ ℤring ∈ DivRing )
20 16 19 mtbir ⊢ ¬ ( Scalar ‘ ( ringLMod ‘ ℤring ) ) ∈ DivRing
21 20 intnan ⊢ ¬ ( ( ringLMod ‘ ℤring ) ∈ LMod ∧ ( Scalar ‘ ( ringLMod ‘ ℤring ) ) ∈ DivRing )
22 10 islvec ⊢ ( ( ringLMod ‘ ℤring ) ∈ LVec ↔ ( ( ringLMod ‘ ℤring ) ∈ LMod ∧ ( Scalar ‘ ( ringLMod ‘ ℤring ) ) ∈ DivRing ) )
23 21 22 mtbir ⊢ ¬ ( ringLMod ‘ ℤring ) ∈ LVec
24 23 olci ⊢ ( ¬ ( ringLMod ‘ ℤring ) ∈ ℂMod ∨ ¬ ( ringLMod ‘ ℤring ) ∈ LVec )
25 df-nel ⊢ ( 𝑍 ∉ ℂVec ↔ ¬ 𝑍 ∈ ℂVec )
26 ianor ⊢ ( ¬ ( ( ringLMod ‘ ℤring ) ∈ ℂMod ∧ ( ringLMod ‘ ℤring ) ∈ LVec ) ↔ ( ¬ ( ringLMod ‘ ℤring ) ∈ ℂMod ∨ ¬ ( ringLMod ‘ ℤring ) ∈ LVec ) )
27 elin ⊢ ( ( ringLMod ‘ ℤring ) ∈ ( ℂMod ∩ LVec ) ↔ ( ( ringLMod ‘ ℤring ) ∈ ℂMod ∧ ( ringLMod ‘ ℤring ) ∈ LVec ) )
28 26 27 xchnxbir ⊢ ( ¬ ( ringLMod ‘ ℤring ) ∈ ( ℂMod ∩ LVec ) ↔ ( ¬ ( ringLMod ‘ ℤring ) ∈ ℂMod ∨ ¬ ( ringLMod ‘ ℤring ) ∈ LVec ) )
29 df-cvs ⊢ ℂVec = ( ℂMod ∩ LVec )
30 1 29 eleq12i ⊢ ( 𝑍 ∈ ℂVec ↔ ( ringLMod ‘ ℤring ) ∈ ( ℂMod ∩ LVec ) )
31 28 30 xchnxbir ⊢ ( ¬ 𝑍 ∈ ℂVec ↔ ( ¬ ( ringLMod ‘ ℤring ) ∈ ℂMod ∨ ¬ ( ringLMod ‘ ℤring ) ∈ LVec ) )
32 25 31 bitri ⊢ ( 𝑍 ∉ ℂVec ↔ ( ¬ ( ringLMod ‘ ℤring ) ∈ ℂMod ∨ ¬ ( ringLMod ‘ ℤring ) ∈ LVec ) )
33 24 32 mpbir ⊢ 𝑍 ∉ ℂVec
34 14 33 pm3.2i ⊢ ( 𝑍 ∈ ℂMod ∧ 𝑍 ∉ ℂVec )