# 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}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{{Z}\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨{Z},{Z}⟩,{Z}⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨{Z},{Z}⟩,{Z}⟩\right\}⟩\right\}$
lmod1zr.m ${⊢}{M}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{{I}\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨{I},{I}⟩,{I}⟩\right\}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{R}⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left\{⟨⟨{Z},{I}⟩,{I}⟩\right\}⟩\right\}$
Assertion lmod1zr ${⊢}\left({I}\in {V}\wedge {Z}\in {W}\right)\to {M}\in \mathrm{LMod}$

### Proof

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