lmod0rng

Description: If the scalar ring of a module is the zero ring, the module is the zero module, i.e. the base set of the module is the singleton consisting of the identity element only. (Contributed by AV, 17-Apr-2019)

		Ref	Expression
	Assertion	lmod0rng	$⊢ (M \in LMod \land \neg Scalar (M) \in NzRing) \to {Base}_{M} = \{0_{M}\}$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ Scalar (M) = Scalar (M)$
2	1	lmodring	$⊢ M \in LMod \to Scalar (M) \in Ring$
3		0ringnnzr	$⊢ Scalar (M) \in Ring \to (\|{Base}_{Scalar (M)}\| = 1 \leftrightarrow \neg Scalar (M) \in NzRing)$
4		eqid	$⊢ {Base}_{Scalar (M)} = {Base}_{Scalar (M)}$
5		eqid	$⊢ 0_{Scalar (M)} = 0_{Scalar (M)}$
6		eqid	$⊢ 1_{Scalar (M)} = 1_{Scalar (M)}$
7	4 5 6	0ring01eq	$⊢ (Scalar (M) \in Ring \land \|{Base}_{Scalar (M)}\| = 1) \to 0_{Scalar (M)} = 1_{Scalar (M)}$
8		eqid	$⊢ {Base}_{M} = {Base}_{M}$
9		eqid	$⊢ \cdot_{M} = \cdot_{M}$
10	8 1 9 6	lmodvs1	$⊢ (M \in LMod \land v \in {Base}_{M}) \to 1_{Scalar (M)} \cdot_{M} v = v$
11		eqcom	$⊢ 1_{Scalar (M)} \cdot_{M} v = v \leftrightarrow v = 1_{Scalar (M)} \cdot_{M} v$
12	11	biimpi	$⊢ 1_{Scalar (M)} \cdot_{M} v = v \to v = 1_{Scalar (M)} \cdot_{M} v$
13		oveq1	$⊢ 1_{Scalar (M)} = 0_{Scalar (M)} \to 1_{Scalar (M)} \cdot_{M} v = 0_{Scalar (M)} \cdot_{M} v$
14	13	eqcoms	$⊢ 0_{Scalar (M)} = 1_{Scalar (M)} \to 1_{Scalar (M)} \cdot_{M} v = 0_{Scalar (M)} \cdot_{M} v$
15		eqid	$⊢ 0_{M} = 0_{M}$
16	8 1 9 5 15	lmod0vs	$⊢ (M \in LMod \land v \in {Base}_{M}) \to 0_{Scalar (M)} \cdot_{M} v = 0_{M}$
17	14 16	sylan9eqr	$⊢ ((M \in LMod \land v \in {Base}_{M}) \land 0_{Scalar (M)} = 1_{Scalar (M)}) \to 1_{Scalar (M)} \cdot_{M} v = 0_{M}$
18	12 17	sylan9eq	$⊢ (1_{Scalar (M)} \cdot_{M} v = v \land ((M \in LMod \land v \in {Base}_{M}) \land 0_{Scalar (M)} = 1_{Scalar (M)})) \to v = 0_{M}$
19	18	exp32	$⊢ 1_{Scalar (M)} \cdot_{M} v = v \to ((M \in LMod \land v \in {Base}_{M}) \to (0_{Scalar (M)} = 1_{Scalar (M)} \to v = 0_{M}))$
20	10 19	mpcom	$⊢ (M \in LMod \land v \in {Base}_{M}) \to (0_{Scalar (M)} = 1_{Scalar (M)} \to v = 0_{M})$
21	20	com12	$⊢ 0_{Scalar (M)} = 1_{Scalar (M)} \to ((M \in LMod \land v \in {Base}_{M}) \to v = 0_{M})$
22	21	impl	$⊢ ((0_{Scalar (M)} = 1_{Scalar (M)} \land M \in LMod) \land v \in {Base}_{M}) \to v = 0_{M}$
23	22	ralrimiva	$⊢ (0_{Scalar (M)} = 1_{Scalar (M)} \land M \in LMod) \to \forall v \in {Base}_{M} v = 0_{M}$
24	8	lmodbn0	$⊢ M \in LMod \to {Base}_{M} \neq \emptyset$
25		eqsn	$⊢ {Base}_{M} \neq \emptyset \to ({Base}_{M} = \{0_{M}\} \leftrightarrow \forall v \in {Base}_{M} v = 0_{M})$
26	24 25	syl	$⊢ M \in LMod \to ({Base}_{M} = \{0_{M}\} \leftrightarrow \forall v \in {Base}_{M} v = 0_{M})$
27	26	adantl	$⊢ (0_{Scalar (M)} = 1_{Scalar (M)} \land M \in LMod) \to ({Base}_{M} = \{0_{M}\} \leftrightarrow \forall v \in {Base}_{M} v = 0_{M})$
28	23 27	mpbird	$⊢ (0_{Scalar (M)} = 1_{Scalar (M)} \land M \in LMod) \to {Base}_{M} = \{0_{M}\}$
29	28	ex	$⊢ 0_{Scalar (M)} = 1_{Scalar (M)} \to (M \in LMod \to {Base}_{M} = \{0_{M}\})$
30	7 29	syl	$⊢ (Scalar (M) \in Ring \land \|{Base}_{Scalar (M)}\| = 1) \to (M \in LMod \to {Base}_{M} = \{0_{M}\})$
31	30	ex	$⊢ Scalar (M) \in Ring \to (\|{Base}_{Scalar (M)}\| = 1 \to (M \in LMod \to {Base}_{M} = \{0_{M}\}))$
32	3 31	sylbird	$⊢ Scalar (M) \in Ring \to (\neg Scalar (M) \in NzRing \to (M \in LMod \to {Base}_{M} = \{0_{M}\}))$
33	32	com23	$⊢ Scalar (M) \in Ring \to (M \in LMod \to (\neg Scalar (M) \in NzRing \to {Base}_{M} = \{0_{M}\}))$
34	2 33	mpcom	$⊢ M \in LMod \to (\neg Scalar (M) \in NzRing \to {Base}_{M} = \{0_{M}\})$
35	34	imp	$⊢ (M \in LMod \land \neg Scalar (M) \in NzRing) \to {Base}_{M} = \{0_{M}\}$

Metamath Proof Explorer

Theorem lmod0rng

Proof