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 )