Theorem lmod1zr 49549

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

Hypotheses

Ref	Expression
lmod1zr.r	⊢ 𝑅 = {⟨(Base‘ndx), {𝑍}⟩, ⟨(+g‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩, ⟨(.r‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩}
lmod1zr.m	⊢ 𝑀 = ({⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩, ⟨(Scalar‘ndx), 𝑅⟩} ∪ {⟨( ·𝑠 ‘ndx), {⟨⟨𝑍, 𝐼⟩, 𝐼⟩}⟩})

Assertion

Ref	Expression
lmod1zr	⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → 𝑀 ∈ LMod)

Proof of Theorem lmod1zr

Dummy variables 𝑎 𝑏 𝑖 𝑝 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		lmod1zr.m	. . 3 ⊢ 𝑀 = ({⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩, ⟨(Scalar‘ndx), 𝑅⟩} ∪ {⟨( ·𝑠 ‘ndx), {⟨⟨𝑍, 𝐼⟩, 𝐼⟩}⟩})
2		elsni 4601	. . . . . . . . . . 11 ⊢ (𝑝 ∈ {⟨𝑍, 𝐼⟩} → 𝑝 = ⟨𝑍, 𝐼⟩)
3		fveq2 6877	. . . . . . . . . . . . 13 ⊢ (𝑝 = ⟨𝑍, 𝐼⟩ → (2nd ‘𝑝) = (2nd ‘⟨𝑍, 𝐼⟩))
4	3	adantl 487	. . . . . . . . . . . 12 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝑝 = ⟨𝑍, 𝐼⟩) → (2nd ‘𝑝) = (2nd ‘⟨𝑍, 𝐼⟩))
5		op2ndg 8003	. . . . . . . . . . . . . . 15 ⊢ ((𝑍 ∈ 𝑊 ∧ 𝐼 ∈ 𝑉) → (2nd ‘⟨𝑍, 𝐼⟩) = 𝐼)
6	5	ancoms 464	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (2nd ‘⟨𝑍, 𝐼⟩) = 𝐼)
7		snidg 4621	. . . . . . . . . . . . . . 15 ⊢ (𝐼 ∈ 𝑉 → 𝐼 ∈ {𝐼})
8	7	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → 𝐼 ∈ {𝐼})
9	6, 8	eqeltrd 2861	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (2nd ‘⟨𝑍, 𝐼⟩) ∈ {𝐼})
10	9	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝑝 = ⟨𝑍, 𝐼⟩) → (2nd ‘⟨𝑍, 𝐼⟩) ∈ {𝐼})
11	4, 10	eqeltrd 2861	. . . . . . . . . . 11 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝑝 = ⟨𝑍, 𝐼⟩) → (2nd ‘𝑝) ∈ {𝐼})
12	2, 11	sylan2 605	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝑝 ∈ {⟨𝑍, 𝐼⟩}) → (2nd ‘𝑝) ∈ {𝐼})
13	12	fmpttd 7107	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑝 ∈ {⟨𝑍, 𝐼⟩} ↦ (2nd ‘𝑝)):{⟨𝑍, 𝐼⟩}⟶{𝐼})
14		opex 5432	. . . . . . . . . 10 ⊢ ⟨𝑍, 𝐼⟩ ∈ V
15		simpl 488	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → 𝐼 ∈ 𝑉)
16		fsng 7130	. . . . . . . . . 10 ⊢ ((⟨𝑍, 𝐼⟩ ∈ V ∧ 𝐼 ∈ 𝑉) → ((𝑝 ∈ {⟨𝑍, 𝐼⟩} ↦ (2nd ‘𝑝)):{⟨𝑍, 𝐼⟩}⟶{𝐼} ↔ (𝑝 ∈ {⟨𝑍, 𝐼⟩} ↦ (2nd ‘𝑝)) = {⟨⟨𝑍, 𝐼⟩, 𝐼⟩}))
17	14, 15, 16	sylancr 599	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → ((𝑝 ∈ {⟨𝑍, 𝐼⟩} ↦ (2nd ‘𝑝)):{⟨𝑍, 𝐼⟩}⟶{𝐼} ↔ (𝑝 ∈ {⟨𝑍, 𝐼⟩} ↦ (2nd ‘𝑝)) = {⟨⟨𝑍, 𝐼⟩, 𝐼⟩}))
18	13, 17	mpbid 235	. . . . . . . 8 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑝 ∈ {⟨𝑍, 𝐼⟩} ↦ (2nd ‘𝑝)) = {⟨⟨𝑍, 𝐼⟩, 𝐼⟩})
19		xpsng 7132	. . . . . . . . . . 11 ⊢ ((𝑍 ∈ 𝑊 ∧ 𝐼 ∈ 𝑉) → ({𝑍} × {𝐼}) = {⟨𝑍, 𝐼⟩})
20	19	ancoms 464	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → ({𝑍} × {𝐼}) = {⟨𝑍, 𝐼⟩})
21	20	eqcomd 2767	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → {⟨𝑍, 𝐼⟩} = ({𝑍} × {𝐼}))
22	21	mpteq1d 5195	. . . . . . . 8 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑝 ∈ {⟨𝑍, 𝐼⟩} ↦ (2nd ‘𝑝)) = (𝑝 ∈ ({𝑍} × {𝐼}) ↦ (2nd ‘𝑝)))
23	18, 22	eqtr3d 2798	. . . . . . 7 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → {⟨⟨𝑍, 𝐼⟩, 𝐼⟩} = (𝑝 ∈ ({𝑍} × {𝐼}) ↦ (2nd ‘𝑝)))
24		vex 3455	. . . . . . . . . 10 ⊢ 𝑧 ∈ V
25		vex 3455	. . . . . . . . . 10 ⊢ 𝑖 ∈ V
26	24, 25	op2ndd 8001	. . . . . . . . 9 ⊢ (𝑝 = ⟨𝑧, 𝑖⟩ → (2nd ‘𝑝) = 𝑖)
27	26	mpompt 7526	. . . . . . . 8 ⊢ (𝑝 ∈ ({𝑍} × {𝐼}) ↦ (2nd ‘𝑝)) = (𝑧 ∈ {𝑍}, 𝑖 ∈ {𝐼} ↦ 𝑖)
28	27	a1i 11	. . . . . . 7 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑝 ∈ ({𝑍} × {𝐼}) ↦ (2nd ‘𝑝)) = (𝑧 ∈ {𝑍}, 𝑖 ∈ {𝐼} ↦ 𝑖))
29		snex 5397	. . . . . . . . 9 ⊢ {𝑍} ∈ V
30		lmod1zr.r	. . . . . . . . . 10 ⊢ 𝑅 = {⟨(Base‘ndx), {𝑍}⟩, ⟨(+g‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩, ⟨(.r‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩}
31	30	rngbase 17450	. . . . . . . . 9 ⊢ ({𝑍} ∈ V → {𝑍} = (Base‘𝑅))
32	29, 31	mp1i 14	. . . . . . . 8 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → {𝑍} = (Base‘𝑅))
33		eqidd 2762	. . . . . . . 8 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → {𝐼} = {𝐼})
34		mpoeq12 7485	. . . . . . . 8 ⊢ (({𝑍} = (Base‘𝑅) ∧ {𝐼} = {𝐼}) → (𝑧 ∈ {𝑍}, 𝑖 ∈ {𝐼} ↦ 𝑖) = (𝑧 ∈ (Base‘𝑅), 𝑖 ∈ {𝐼} ↦ 𝑖))
35	32, 33, 34	syl2anc 596	. . . . . . 7 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑧 ∈ {𝑍}, 𝑖 ∈ {𝐼} ↦ 𝑖) = (𝑧 ∈ (Base‘𝑅), 𝑖 ∈ {𝐼} ↦ 𝑖))
36	23, 28, 35	3eqtrd 2800	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → {⟨⟨𝑍, 𝐼⟩, 𝐼⟩} = (𝑧 ∈ (Base‘𝑅), 𝑖 ∈ {𝐼} ↦ 𝑖))
37	36	opeq2d 4840	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → ⟨( ·𝑠 ‘ndx), {⟨⟨𝑍, 𝐼⟩, 𝐼⟩}⟩ = ⟨( ·𝑠 ‘ndx), (𝑧 ∈ (Base‘𝑅), 𝑖 ∈ {𝐼} ↦ 𝑖)⟩)
38	37	sneqd 4596	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → {⟨( ·𝑠 ‘ndx), {⟨⟨𝑍, 𝐼⟩, 𝐼⟩}⟩} = {⟨( ·𝑠 ‘ndx), (𝑧 ∈ (Base‘𝑅), 𝑖 ∈ {𝐼} ↦ 𝑖)⟩})
39	38	uneq2d 4115	. . 3 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → ({⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩, ⟨(Scalar‘ndx), 𝑅⟩} ∪ {⟨( ·𝑠 ‘ndx), {⟨⟨𝑍, 𝐼⟩, 𝐼⟩}⟩}) = ({⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩, ⟨(Scalar‘ndx), 𝑅⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑧 ∈ (Base‘𝑅), 𝑖 ∈ {𝐼} ↦ 𝑖)⟩}))
40	1, 39	eqtrid 2808	. 2 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → 𝑀 = ({⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩, ⟨(Scalar‘ndx), 𝑅⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑧 ∈ (Base‘𝑅), 𝑖 ∈ {𝐼} ↦ 𝑖)⟩}))
41	30	ring1 20521	. . 3 ⊢ (𝑍 ∈ 𝑊 → 𝑅 ∈ Ring)
42		eqidd 2762	. . . . . . . 8 ⊢ (𝑧 = 𝑎 → 𝑖 = 𝑖)
43		id 23	. . . . . . . 8 ⊢ (𝑖 = 𝑏 → 𝑖 = 𝑏)
44	42, 43	cbvmpov 7507	. . . . . . 7 ⊢ (𝑧 ∈ (Base‘𝑅), 𝑖 ∈ {𝐼} ↦ 𝑖) = (𝑎 ∈ (Base‘𝑅), 𝑏 ∈ {𝐼} ↦ 𝑏)
45	44	opeq2i 4837	. . . . . 6 ⊢ ⟨( ·𝑠 ‘ndx), (𝑧 ∈ (Base‘𝑅), 𝑖 ∈ {𝐼} ↦ 𝑖)⟩ = ⟨( ·𝑠 ‘ndx), (𝑎 ∈ (Base‘𝑅), 𝑏 ∈ {𝐼} ↦ 𝑏)⟩
46	45	sneqi 4595	. . . . 5 ⊢ {⟨( ·𝑠 ‘ndx), (𝑧 ∈ (Base‘𝑅), 𝑖 ∈ {𝐼} ↦ 𝑖)⟩} = {⟨( ·𝑠 ‘ndx), (𝑎 ∈ (Base‘𝑅), 𝑏 ∈ {𝐼} ↦ 𝑏)⟩}
47	46	uneq2i 4112	. . . 4 ⊢ ({⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩, ⟨(Scalar‘ndx), 𝑅⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑧 ∈ (Base‘𝑅), 𝑖 ∈ {𝐼} ↦ 𝑖)⟩}) = ({⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩, ⟨(Scalar‘ndx), 𝑅⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑎 ∈ (Base‘𝑅), 𝑏 ∈ {𝐼} ↦ 𝑏)⟩})
48	47	lmod1 49548	. . 3 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → ({⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩, ⟨(Scalar‘ndx), 𝑅⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑧 ∈ (Base‘𝑅), 𝑖 ∈ {𝐼} ↦ 𝑖)⟩}) ∈ LMod)
49	41, 48	sylan2 605	. 2 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → ({⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩, ⟨(Scalar‘ndx), 𝑅⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑧 ∈ (Base‘𝑅), 𝑖 ∈ {𝐼} ↦ 𝑖)⟩}) ∈ LMod)
50	40, 49	eqeltrd 2861	1 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → 𝑀 ∈ LMod)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  Vcvv 3451   ∪ cun 3897  {csn 4584  {ctp 4588  ⟨cop 4590   ↦ cmpt 5186   × cxp 5649  ⟶wf 6527  ‘cfv 6531   ∈ cmpo 7414  2^nd c2nd 7989  ndxcnx 17351  Basecbs 17367  +_gcplusg 17408  ._rcmulr 17409  Scalarcsca 17411   ·_𝑠 cvsca 17412  Ringcrg 20439  LModclmod 21115

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740  ax-cnex 11237  ax-resscn 11238  ax-1cn 11239  ax-icn 11240  ax-addcl 11241  ax-addrcl 11242  ax-mulcl 11243  ax-mulrcl 11244  ax-mulcom 11245  ax-addass 11246  ax-mulass 11247  ax-distr 11248  ax-i2m1 11249  ax-1ne0 11250  ax-1rid 11251  ax-rnegex 11252  ax-rrecex 11253  ax-cnre 11254  ax-pre-lttri 11255  ax-pre-lttrn 11256  ax-pre-ltadd 11257  ax-pre-mulgt0 11258

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6297  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7867  df-1st 7990  df-2nd 7991  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-1o 8460  df-er 8701  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11524  df-neg 11525  df-nn 12317  df-2 12386  df-3 12387  df-4 12388  df-5 12389  df-6 12390  df-n0 12588  df-z 12675  df-uz 12947  df-fz 13621  df-struct 17305  df-sets 17322  df-slot 17340  df-ndx 17352  df-base 17368  df-plusg 17421  df-mulr 17422  df-sca 17424  df-vsca 17425  df-0g 17592  df-mgm 18796  df-sgrp 18888  df-mnd 18904  df-grp 19127  df-mgp 20341  df-ur 20388  df-ring 20441  df-lmod 21117

This theorem is used by:  lmodn0  49551  lvecpsslmod  49563