Metamath Proof Explorer


Theorem lmod1zr

Description: The (smallest) structure representing azero module over a zero ring. (Contributed by AV, 29-Apr-2019)

Ref Expression
Hypotheses lmod1zr.r
|- R = { <. ( Base ` ndx ) , { Z } >. , <. ( +g ` ndx ) , { <. <. Z , Z >. , Z >. } >. , <. ( .r ` ndx ) , { <. <. Z , Z >. , Z >. } >. }
lmod1zr.m
|- M = ( { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , { <. <. Z , I >. , I >. } >. } )
Assertion lmod1zr
|- ( ( I e. V /\ Z e. W ) -> M e. LMod )

Proof

Step Hyp Ref Expression
1 lmod1zr.r
 |-  R = { <. ( Base ` ndx ) , { Z } >. , <. ( +g ` ndx ) , { <. <. Z , Z >. , Z >. } >. , <. ( .r ` ndx ) , { <. <. Z , Z >. , Z >. } >. }
2 lmod1zr.m
 |-  M = ( { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , { <. <. Z , I >. , I >. } >. } )
3 elsni
 |-  ( p e. { <. Z , I >. } -> p = <. Z , I >. )
4 fveq2
 |-  ( p = <. Z , I >. -> ( 2nd ` p ) = ( 2nd ` <. Z , I >. ) )
5 4 adantl
 |-  ( ( ( I e. V /\ Z e. W ) /\ p = <. Z , I >. ) -> ( 2nd ` p ) = ( 2nd ` <. Z , I >. ) )
6 op2ndg
 |-  ( ( Z e. W /\ I e. V ) -> ( 2nd ` <. Z , I >. ) = I )
7 6 ancoms
 |-  ( ( I e. V /\ Z e. W ) -> ( 2nd ` <. Z , I >. ) = I )
8 snidg
 |-  ( I e. V -> I e. { I } )
9 8 adantr
 |-  ( ( I e. V /\ Z e. W ) -> I e. { I } )
10 7 9 eqeltrd
 |-  ( ( I e. V /\ Z e. W ) -> ( 2nd ` <. Z , I >. ) e. { I } )
11 10 adantr
 |-  ( ( ( I e. V /\ Z e. W ) /\ p = <. Z , I >. ) -> ( 2nd ` <. Z , I >. ) e. { I } )
12 5 11 eqeltrd
 |-  ( ( ( I e. V /\ Z e. W ) /\ p = <. Z , I >. ) -> ( 2nd ` p ) e. { I } )
13 3 12 sylan2
 |-  ( ( ( I e. V /\ Z e. W ) /\ p e. { <. Z , I >. } ) -> ( 2nd ` p ) e. { I } )
14 13 fmpttd
 |-  ( ( I e. V /\ Z e. W ) -> ( p e. { <. Z , I >. } |-> ( 2nd ` p ) ) : { <. Z , I >. } --> { I } )
15 opex
 |-  <. Z , I >. e. _V
16 simpl
 |-  ( ( I e. V /\ Z e. W ) -> I e. V )
17 fsng
 |-  ( ( <. Z , I >. e. _V /\ I e. V ) -> ( ( p e. { <. Z , I >. } |-> ( 2nd ` p ) ) : { <. Z , I >. } --> { I } <-> ( p e. { <. Z , I >. } |-> ( 2nd ` p ) ) = { <. <. Z , I >. , I >. } ) )
18 15 16 17 sylancr
 |-  ( ( I e. V /\ Z e. W ) -> ( ( p e. { <. Z , I >. } |-> ( 2nd ` p ) ) : { <. Z , I >. } --> { I } <-> ( p e. { <. Z , I >. } |-> ( 2nd ` p ) ) = { <. <. Z , I >. , I >. } ) )
19 14 18 mpbid
 |-  ( ( I e. V /\ Z e. W ) -> ( p e. { <. Z , I >. } |-> ( 2nd ` p ) ) = { <. <. Z , I >. , I >. } )
20 xpsng
 |-  ( ( Z e. W /\ I e. V ) -> ( { Z } X. { I } ) = { <. Z , I >. } )
21 20 ancoms
 |-  ( ( I e. V /\ Z e. W ) -> ( { Z } X. { I } ) = { <. Z , I >. } )
22 21 eqcomd
 |-  ( ( I e. V /\ Z e. W ) -> { <. Z , I >. } = ( { Z } X. { I } ) )
23 22 mpteq1d
 |-  ( ( I e. V /\ Z e. W ) -> ( p e. { <. Z , I >. } |-> ( 2nd ` p ) ) = ( p e. ( { Z } X. { I } ) |-> ( 2nd ` p ) ) )
24 19 23 eqtr3d
 |-  ( ( I e. V /\ Z e. W ) -> { <. <. Z , I >. , I >. } = ( p e. ( { Z } X. { I } ) |-> ( 2nd ` p ) ) )
25 vex
 |-  z e. _V
26 vex
 |-  i e. _V
27 25 26 op2ndd
 |-  ( p = <. z , i >. -> ( 2nd ` p ) = i )
28 27 mpompt
 |-  ( p e. ( { Z } X. { I } ) |-> ( 2nd ` p ) ) = ( z e. { Z } , i e. { I } |-> i )
29 28 a1i
 |-  ( ( I e. V /\ Z e. W ) -> ( p e. ( { Z } X. { I } ) |-> ( 2nd ` p ) ) = ( z e. { Z } , i e. { I } |-> i ) )
30 snex
 |-  { Z } e. _V
31 1 rngbase
 |-  ( { Z } e. _V -> { Z } = ( Base ` R ) )
32 30 31 mp1i
 |-  ( ( I e. V /\ Z e. W ) -> { Z } = ( Base ` R ) )
33 eqidd
 |-  ( ( I e. V /\ Z e. W ) -> { I } = { I } )
34 mpoeq12
 |-  ( ( { Z } = ( Base ` R ) /\ { I } = { I } ) -> ( z e. { Z } , i e. { I } |-> i ) = ( z e. ( Base ` R ) , i e. { I } |-> i ) )
35 32 33 34 syl2anc
 |-  ( ( I e. V /\ Z e. W ) -> ( z e. { Z } , i e. { I } |-> i ) = ( z e. ( Base ` R ) , i e. { I } |-> i ) )
36 24 29 35 3eqtrd
 |-  ( ( I e. V /\ Z e. W ) -> { <. <. Z , I >. , I >. } = ( z e. ( Base ` R ) , i e. { I } |-> i ) )
37 36 opeq2d
 |-  ( ( I e. V /\ Z e. W ) -> <. ( .s ` ndx ) , { <. <. Z , I >. , I >. } >. = <. ( .s ` ndx ) , ( z e. ( Base ` R ) , i e. { I } |-> i ) >. )
38 37 sneqd
 |-  ( ( I e. V /\ Z e. W ) -> { <. ( .s ` ndx ) , { <. <. Z , I >. , I >. } >. } = { <. ( .s ` ndx ) , ( z e. ( Base ` R ) , i e. { I } |-> i ) >. } )
39 38 uneq2d
 |-  ( ( I e. V /\ Z e. W ) -> ( { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , { <. <. Z , I >. , I >. } >. } ) = ( { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , ( z e. ( Base ` R ) , i e. { I } |-> i ) >. } ) )
40 2 39 syl5eq
 |-  ( ( I e. V /\ Z e. W ) -> M = ( { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , ( z e. ( Base ` R ) , i e. { I } |-> i ) >. } ) )
41 1 ring1
 |-  ( Z e. W -> R e. Ring )
42 eqidd
 |-  ( z = a -> i = i )
43 id
 |-  ( i = b -> i = b )
44 42 43 cbvmpov
 |-  ( z e. ( Base ` R ) , i e. { I } |-> i ) = ( a e. ( Base ` R ) , b e. { I } |-> b )
45 44 opeq2i
 |-  <. ( .s ` ndx ) , ( z e. ( Base ` R ) , i e. { I } |-> i ) >. = <. ( .s ` ndx ) , ( a e. ( Base ` R ) , b e. { I } |-> b ) >.
46 45 sneqi
 |-  { <. ( .s ` ndx ) , ( z e. ( Base ` R ) , i e. { I } |-> i ) >. } = { <. ( .s ` ndx ) , ( a e. ( Base ` R ) , b e. { I } |-> b ) >. }
47 46 uneq2i
 |-  ( { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , ( z e. ( Base ` R ) , i e. { I } |-> i ) >. } ) = ( { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , ( a e. ( Base ` R ) , b e. { I } |-> b ) >. } )
48 47 lmod1
 |-  ( ( I e. V /\ R e. Ring ) -> ( { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , ( z e. ( Base ` R ) , i e. { I } |-> i ) >. } ) e. LMod )
49 41 48 sylan2
 |-  ( ( I e. V /\ Z e. W ) -> ( { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , ( z e. ( Base ` R ) , i e. { I } |-> i ) >. } ) e. LMod )
50 40 49 eqeltrd
 |-  ( ( I e. V /\ Z e. W ) -> M e. LMod )