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

Proof

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

Metamath Proof Explorer

Theorem lmod1zr

Proof