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 
|- Z = ( ringLMod ` ZZring )
Assertion zclmncvs 
|- ( Z e. CMod /\ Z e/ CVec )

Proof

Step Hyp Ref Expression
1 zclmncvs.z 
 |-  Z = ( ringLMod ` ZZring )
2 zringring 
 |-  ZZring e. Ring
3 rlmlmod 
 |-  ( ZZring e. Ring -> ( ringLMod ` ZZring ) e. LMod )
4 2 3 ax-mp 
 |-  ( ringLMod ` ZZring ) e. LMod
5 rlmsca 
 |-  ( ZZring e. Ring -> ZZring = ( Scalar ` ( ringLMod ` ZZring ) ) )
6 2 5 ax-mp 
 |-  ZZring = ( Scalar ` ( ringLMod ` ZZring ) )
7 df-zring 
 |-  ZZring = ( CCfld |`s ZZ )
8 6 7 eqtr3i 
 |-  ( Scalar ` ( ringLMod ` ZZring ) ) = ( CCfld |`s ZZ )
9 zsubrg 
 |-  ZZ e. ( SubRing ` CCfld )
10 eqid 
 |-  ( Scalar ` ( ringLMod ` ZZring ) ) = ( Scalar ` ( ringLMod ` ZZring ) )
11 10 isclmi 
 |-  ( ( ( ringLMod ` ZZring ) e. LMod /\ ( Scalar ` ( ringLMod ` ZZring ) ) = ( CCfld |`s ZZ ) /\ ZZ e. ( SubRing ` CCfld ) ) -> ( ringLMod ` ZZring ) e. CMod )
12 4 8 9 11 mp3an 
 |-  ( ringLMod ` ZZring ) e. CMod
13 1 eleq1i 
 |-  ( Z e. CMod <-> ( ringLMod ` ZZring ) e. CMod )
14 12 13 mpbir 
 |-  Z e. CMod
15 zringndrg 
 |-  ZZring e/ DivRing
16 15 neli 
 |-  -. ZZring e. DivRing
17 5 eqcomd 
 |-  ( ZZring e. Ring -> ( Scalar ` ( ringLMod ` ZZring ) ) = ZZring )
18 2 17 ax-mp 
 |-  ( Scalar ` ( ringLMod ` ZZring ) ) = ZZring
19 18 eleq1i 
 |-  ( ( Scalar ` ( ringLMod ` ZZring ) ) e. DivRing <-> ZZring e. DivRing )
20 16 19 mtbir 
 |-  -. ( Scalar ` ( ringLMod ` ZZring ) ) e. DivRing
21 20 intnan 
 |-  -. ( ( ringLMod ` ZZring ) e. LMod /\ ( Scalar ` ( ringLMod ` ZZring ) ) e. DivRing )
22 10 islvec 
 |-  ( ( ringLMod ` ZZring ) e. LVec <-> ( ( ringLMod ` ZZring ) e. LMod /\ ( Scalar ` ( ringLMod ` ZZring ) ) e. DivRing ) )
23 21 22 mtbir 
 |-  -. ( ringLMod ` ZZring ) e. LVec
24 23 olci 
 |-  ( -. ( ringLMod ` ZZring ) e. CMod \/ -. ( ringLMod ` ZZring ) e. LVec )
25 df-nel 
 |-  ( Z e/ CVec <-> -. Z e. CVec )
26 ianor 
 |-  ( -. ( ( ringLMod ` ZZring ) e. CMod /\ ( ringLMod ` ZZring ) e. LVec ) <-> ( -. ( ringLMod ` ZZring ) e. CMod \/ -. ( ringLMod ` ZZring ) e. LVec ) )
27 elin 
 |-  ( ( ringLMod ` ZZring ) e. ( CMod i^i LVec ) <-> ( ( ringLMod ` ZZring ) e. CMod /\ ( ringLMod ` ZZring ) e. LVec ) )
28 26 27 xchnxbir 
 |-  ( -. ( ringLMod ` ZZring ) e. ( CMod i^i LVec ) <-> ( -. ( ringLMod ` ZZring ) e. CMod \/ -. ( ringLMod ` ZZring ) e. LVec ) )
29 df-cvs 
 |-  CVec = ( CMod i^i LVec )
30 1 29 eleq12i 
 |-  ( Z e. CVec <-> ( ringLMod ` ZZring ) e. ( CMod i^i LVec ) )
31 28 30 xchnxbir 
 |-  ( -. Z e. CVec <-> ( -. ( ringLMod ` ZZring ) e. CMod \/ -. ( ringLMod ` ZZring ) e. LVec ) )
32 25 31 bitri 
 |-  ( Z e/ CVec <-> ( -. ( ringLMod ` ZZring ) e. CMod \/ -. ( ringLMod ` ZZring ) e. LVec ) )
33 24 32 mpbir 
 |-  Z e/ CVec
34 14 33 pm3.2i 
 |-  ( Z e. CMod /\ Z e/ CVec )