Theorem lmod1zr 31054

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

Hypotheses

Ref	Expression
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

Ref	Expression
lmod1zr	|- ( ( I e. V /\ Z e. W ) -> M e. LMod )

Proof of Theorem lmod1zr

Dummy variables a b i p z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		lmod1zr.m	. . 3 |- M = ( { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. (Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , { <. <. Z , I >. , I >. } >. } )
2		elsni 3917	. . . . . . . . . . 11 |- ( p e. { <. Z , I >. } -> p = <. Z , I >. )
3		fveq2 5706	. . . . . . . . . . . . 13 |- ( p = <. Z , I >. -> ( 2nd ` p ) = ( 2nd ` <. Z , I >. ) )
4	3	adantl 466	. . . . . . . . . . . 12 |- ( ( ( I e. V /\ Z e. W ) /\ p = <. Z , I >. ) -> ( 2nd ` p ) = ( 2nd ` <. Z , I >. ) )
5		op2ndg 6605	. . . . . . . . . . . . . . 15 |- ( ( Z e. W /\ I e. V ) -> ( 2nd ` <. Z , I >. ) = I )
6	5	ancoms 453	. . . . . . . . . . . . . 14 |- ( ( I e. V /\ Z e. W ) -> ( 2nd ` <. Z , I >. ) = I )
7		snidg 3918	. . . . . . . . . . . . . . 15 |- ( I e. V -> I e. { I } )
8	7	adantr 465	. . . . . . . . . . . . . 14 |- ( ( I e. V /\ Z e. W ) -> I e. { I } )
9	6, 8	eqeltrd 2517	. . . . . . . . . . . . 13 |- ( ( I e. V /\ Z e. W ) -> ( 2nd ` <. Z , I >. ) e. { I } )
10	9	adantr 465	. . . . . . . . . . . 12 |- ( ( ( I e. V /\ Z e. W ) /\ p = <. Z , I >. ) -> ( 2nd ` <. Z , I >. ) e. { I } )
11	4, 10	eqeltrd 2517	. . . . . . . . . . 11 |- ( ( ( I e. V /\ Z e. W ) /\ p = <. Z , I >. ) -> ( 2nd ` p ) e. { I } )
12	2, 11	sylan2 474	. . . . . . . . . 10 |- ( ( ( I e. V /\ Z e. W ) /\ p e. { <. Z , I >. } ) -> ( 2nd ` p ) e. { I } )
13		eqid 2443	. . . . . . . . . 10 |- ( p e. { <. Z , I >. } |-> ( 2nd ` p ) ) = ( p e. { <. Z , I >. } |-> ( 2nd ` p ) )
14	12, 13	fmptd 5882	. . . . . . . . 9 |- ( ( I e. V /\ Z e. W ) -> ( p e. { <. Z , I >. } |-> ( 2nd ` p ) ) : { <. Z , I >. } --> { I } )
15		opex 4571	. . . . . . . . . 10 |- <. Z , I >. e. _V
16		simpl 457	. . . . . . . . . 10 |- ( ( I e. V /\ Z e. W ) -> I e. V )
17		fsng 5897	. . . . . . . . . 10 |- ( ( <. 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 663	. . . . . . . . 9 |- ( ( 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 210	. . . . . . . 8 |- ( ( I e. V /\ Z e. W ) -> ( p e. { <. Z , I >. } |-> ( 2nd ` p ) ) = { <. <. Z , I >. , I >. } )
20		xpsng 5899	. . . . . . . . . . 11 |- ( ( Z e. W /\ I e. V ) -> ( { Z } X. { I } ) = { <. Z , I >. } )
21	20	ancoms 453	. . . . . . . . . 10 |- ( ( I e. V /\ Z e. W ) -> ( { Z } X. { I } ) = { <. Z , I >. } )
22	21	eqcomd 2448	. . . . . . . . 9 |- ( ( I e. V /\ Z e. W ) -> { <. Z , I >. } = ( { Z } X. { I } ) )
23	22	mpteq1d 4388	. . . . . . . 8 |- ( ( I e. V /\ Z e. W ) -> ( p e. { <. Z , I >. } |-> ( 2nd ` p ) ) = ( p e. ( { Z } X. { I } ) |-> ( 2nd ` p ) ) )
24	19, 23	eqtr3d 2477	. . . . . . 7 |- ( ( I e. V /\ Z e. W ) -> { <. <. Z , I >. , I >. } = ( p e. ( { Z } X. { I } ) |-> ( 2nd ` p ) ) )
25		vex 2990	. . . . . . . . . 10 |- z e. _V
26		vex 2990	. . . . . . . . . 10 |- i e. _V
27	25, 26	op2ndd 6603	. . . . . . . . 9 |- ( p = <. z , i >. -> ( 2nd ` p ) = i )
28	27	mpt2mpt 6197	. . . . . . . 8 |- ( p e. ( { Z } X. { I } ) |-> ( 2nd ` p ) ) = ( z e. { Z } , i e. { I } |-> i )
29	28	a1i 11	. . . . . . 7 |- ( ( I e. V /\ Z e. W ) -> ( p e. ( { Z } X. { I } ) |-> ( 2nd ` p ) ) = ( z e. { Z } , i e. { I } |-> i ) )
30		snex 4548	. . . . . . . . 9 |- { Z } e. _V
31		lmod1zr.r	. . . . . . . . . 10 |- R = { <. ( Base ` ndx ) , { Z } >. , <. ( +g ` ndx ) , { <. <. Z , Z >. , Z >. } >. , <. ( .r ` ndx ) , { <. <. Z , Z >. , Z >. } >. }
32	31	rngbase 14301	. . . . . . . . 9 |- ( { Z } e. _V -> { Z } = ( Base ` R ) )
33	30, 32	mp1i 12	. . . . . . . 8 |- ( ( I e. V /\ Z e. W ) -> { Z } = ( Base ` R ) )
34		eqidd 2444	. . . . . . . 8 |- ( ( I e. V /\ Z e. W ) -> { I } = { I } )
35		mpt2eq12 6161	. . . . . . . 8 |- ( ( { Z } = ( Base ` R ) /\ { I } = { I } ) -> ( z e. { Z } , i e. { I } |-> i ) = ( z e. ( Base ` R ) , i e. { I } |-> i ) )
36	33, 34, 35	syl2anc 661	. . . . . . 7 |- ( ( I e. V /\ Z e. W ) -> ( z e. { Z } , i e. { I } |-> i ) = ( z e. ( Base ` R ) , i e. { I } |-> i ) )
37	24, 29, 36	3eqtrd 2479	. . . . . 6 |- ( ( I e. V /\ Z e. W ) -> { <. <. Z , I >. , I >. } = ( z e. ( Base ` R ) , i e. { I } |-> i ) )
38	37	opeq2d 4081	. . . . 5 |- ( ( I e. V /\ Z e. W ) -> <. ( .s ` ndx ) , { <. <. Z , I >. , I >. } >. = <. ( .s ` ndx ) , ( z e. ( Base ` R ) , i e. { I } |-> i ) >. )
39	38	sneqd 3904	. . . 4 |- ( ( I e. V /\ Z e. W ) -> { <. ( .s ` ndx ) , { <. <. Z , I >. , I >. } >. } = { <. ( .s ` ndx ) , ( z e. ( Base ` R ) , i e. { I } |-> i ) >. } )
40	39	uneq2d 3525	. . 3 |- ( ( 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 ) >. } ) )
41	1, 40	syl5eq 2487	. 2 |- ( ( 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 ) >. } ) )
42	31	rng1 31044	. . 3 |- ( Z e. W -> R e. Ring )
43		eqidd 2444	. . . . . . . 8 |- ( z = a -> i = i )
44		id 22	. . . . . . . 8 |- ( i = b -> i = b )
45	43, 44	cbvmpt2v 6181	. . . . . . 7 |- ( z e. ( Base ` R ) , i e. { I } |-> i ) = ( a e. ( Base ` R ) , b e. { I } |-> b )
46	45	opeq2i 4078	. . . . . 6 |- <. ( .s ` ndx ) , ( z e. ( Base ` R ) , i e. { I } |-> i ) >. = <. ( .s ` ndx ) , ( a e. ( Base ` R ) , b e. { I } |-> b ) >.
47	46	sneqi 3903	. . . . 5 |- { <. ( .s ` ndx ) , ( z e. ( Base ` R ) , i e. { I } |-> i ) >. } = { <. ( .s ` ndx ) , ( a e. ( Base ` R ) , b e. { I } |-> b ) >. }
48	47	uneq2i 3522	. . . 4 |- ( { <. ( 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 ) >. } )
49	48	lmod1 31053	. . 3 |- ( ( 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 )
50	42, 49	sylan2 474	. 2 |- ( ( 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 )
51	41, 50	eqeltrd 2517	1 |- ( ( I e. V /\ Z e. W ) -> M e. LMod )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1369   e. wcel 1756   _Vcvv 2987   u. cun 3341   {csn 3892   {ctp 3896   <.cop 3898   e. cmpt 4365   X. cxp 4853   -->wf 5429   ` cfv 5433   e. cmpt2 6108   2ndc2nd 6591   ndxcnx 14186   Basecbs 14189   +g cplusg 14253   .rcmulr 14254  Scalarcsca 14256   .scvsca 14257   Ringcrg 16660   LModclmod 16963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4418  ax-sep 4428  ax-nul 4436  ax-pow 4485  ax-pr 4546  ax-un 6387  ax-cnex 9353  ax-resscn 9354  ax-1cn 9355  ax-icn 9356  ax-addcl 9357  ax-addrcl 9358  ax-mulcl 9359  ax-mulrcl 9360  ax-mulcom 9361  ax-addass 9362  ax-mulass 9363  ax-distr 9364  ax-i2m1 9365  ax-1ne0 9366  ax-1rid 9367  ax-rnegex 9368  ax-rrecex 9369  ax-cnre 9370  ax-pre-lttri 9371  ax-pre-lttrn 9372  ax-pre-ltadd 9373  ax-pre-mulgt0 9374

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-nel 2623  df-ral 2735  df-rex 2736  df-reu 2737  df-rmo 2738  df-rab 2739  df-v 2989  df-sbc 3202  df-csb 3304  df-dif 3346  df-un 3348  df-in 3350  df-ss 3357  df-pss 3359  df-nul 3653  df-if 3807  df-pw 3877  df-sn 3893  df-pr 3895  df-tp 3897  df-op 3899  df-uni 4107  df-int 4144  df-iun 4188  df-br 4308  df-opab 4366  df-mpt 4367  df-tr 4401  df-eprel 4647  df-id 4651  df-po 4656  df-so 4657  df-fr 4694  df-we 4696  df-ord 4737  df-on 4738  df-lim 4739  df-suc 4740  df-xp 4861  df-rel 4862  df-cnv 4863  df-co 4864  df-dm 4865  df-rn 4866  df-res 4867  df-ima 4868  df-iota 5396  df-fun 5435  df-fn 5436  df-f 5437  df-f1 5438  df-fo 5439  df-f1o 5440  df-fv 5441  df-riota 6067  df-ov 6109  df-oprab 6110  df-mpt2 6111  df-om 6492  df-1st 6592  df-2nd 6593  df-recs 6847  df-rdg 6881  df-1o 6935  df-oadd 6939  df-er 7116  df-en 7326  df-dom 7327  df-sdom 7328  df-fin 7329  df-pnf 9435  df-mnf 9436  df-xr 9437  df-ltxr 9438  df-le 9439  df-sub 9612  df-neg 9613  df-nn 10338  df-2 10395  df-3 10396  df-4 10397  df-5 10398  df-6 10399  df-n0 10595  df-z 10662  df-uz 10877  df-fz 11453  df-struct 14191  df-ndx 14192  df-slot 14193  df-base 14194  df-sets 14195  df-plusg 14266  df-mulr 14267  df-sca 14269  df-vsca 14270  df-0g 14395  df-mnd 15430  df-grp 15560  df-mgp 16607  df-ur 16619  df-rng 16662  df-lmod 16965

This theorem is referenced by:  lmodn0  31056  lvecpsslmod  31068