Theorem lmodfopne

Description: The (functionalized) operations of a left module (over a nonzero ring) cannot be identical. (Contributed by NM, 31-May-2008) (Revised by AV, 2-Oct-2021)

	Ref	Expression
Hypotheses	lmodfopne.t	$$⊢\underset{\dot{}}{·}={\cdot }_{\mathrm{𝑠𝑓}}\left(W\right)$$
	lmodfopne.a	$$⊢\underset{\dot{}}{+}={+}_{𝑓}\left(W\right)$$
	lmodfopne.v	$$⊢V={\mathrm{Base}}_W$$
	lmodfopne.s	$$⊢S=\mathrm{Scalar}\left(W\right)$$
	lmodfopne.k	$$⊢K={\mathrm{Base}}_S$$
	lmodfopne.0	$$⊢\underset{\dot{}}{0}=0_S$$
	lmodfopne.1	$$⊢\underset{\dot{}}{1}=1_S$$
Assertion	lmodfopne	$$⊢\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\to \underset{\dot{}}{+}\ne \underset{\dot{}}{·}$$

Proof

Step	Hyp	Ref	Expression
1		lmodfopne.t	$$⊢\underset{\dot{}}{·}={\cdot }_{\mathrm{𝑠𝑓}}\left(W\right)$$
2		lmodfopne.a	$$⊢\underset{\dot{}}{+}={+}_{𝑓}\left(W\right)$$
3		lmodfopne.v	$$⊢V={\mathrm{Base}}_W$$
4		lmodfopne.s	$$⊢S=\mathrm{Scalar}\left(W\right)$$
5		lmodfopne.k	$$⊢K={\mathrm{Base}}_S$$
6		lmodfopne.0	$$⊢\underset{\dot{}}{0}=0_S$$
7		lmodfopne.1	$$⊢\underset{\dot{}}{1}=1_S$$
8	1 2 3 4 5 6 7	lmodfopnelem2	$$⊢\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\to \left(\underset{\dot{}}{0}\in V\wedge \underset{\dot{}}{1}\in V\right)$$
9		simpl	$$⊢\left(\underset{\dot{}}{0}\in V\wedge \underset{\dot{}}{1}\in V\right)\to \underset{\dot{}}{0}\in V$$
10		eqid	$$⊢0_W=0_W$$
11	3 10	lmod0vcl	$$⊢W\in \mathrm{LMod}\to 0_W\in V$$
12	11	adantr	$$⊢\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\to 0_W\in V$$
13		eqid	$$⊢{+}_W={+}_W$$
14	3 13 2	plusfval	$$⊢\left(\underset{\dot{}}{0}\in V\wedge 0_W\in V\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}{0}_W=\underset{\dot{}}{0}{+}_W{0}_W$$
15	14	eqcomd	$$⊢\left(\underset{\dot{}}{0}\in V\wedge 0_W\in V\right)\to \underset{\dot{}}{0}{+}_W{0}_W=\underset{\dot{}}{0}\underset{\dot{}}{+}{0}_W$$
16	9 12 15	syl2anr	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\wedge \left(\underset{\dot{}}{0}\in V\wedge \underset{\dot{}}{1}\in V\right)\right)\to \underset{\dot{}}{0}{+}_W{0}_W=\underset{\dot{}}{0}\underset{\dot{}}{+}{0}_W$$
17		oveq	$$⊢\underset{\dot{}}{+}=\underset{\dot{}}{·}\to \underset{\dot{}}{0}\underset{\dot{}}{+}{0}_W=\underset{\dot{}}{0}\underset{\dot{}}{·}{0}_W$$
18	17	ad2antlr	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\wedge \left(\underset{\dot{}}{0}\in V\wedge \underset{\dot{}}{1}\in V\right)\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}{0}_W=\underset{\dot{}}{0}\underset{\dot{}}{·}{0}_W$$
19	16 18	eqtrd	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\wedge \left(\underset{\dot{}}{0}\in V\wedge \underset{\dot{}}{1}\in V\right)\right)\to \underset{\dot{}}{0}{+}_W{0}_W=\underset{\dot{}}{0}\underset{\dot{}}{·}{0}_W$$
20		lmodgrp	$$⊢W\in \mathrm{LMod}\to W\in \mathrm{Grp}$$
21	20	adantr	$$⊢\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\to W\in \mathrm{Grp}$$
22	3 13 10	grprid	$$⊢\left(W\in \mathrm{Grp}\wedge \underset{\dot{}}{0}\in V\right)\to \underset{\dot{}}{0}{+}_W{0}_W=\underset{\dot{}}{0}$$
23	21 9 22	syl2an	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\wedge \left(\underset{\dot{}}{0}\in V\wedge \underset{\dot{}}{1}\in V\right)\right)\to \underset{\dot{}}{0}{+}_W{0}_W=\underset{\dot{}}{0}$$
24	4 5 6	lmod0cl	$$⊢W\in \mathrm{LMod}\to \underset{\dot{}}{0}\in K$$
25	24 11	jca	$$⊢W\in \mathrm{LMod}\to \left(\underset{\dot{}}{0}\in K\wedge 0_W\in V\right)$$
26	25	adantr	$$⊢\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\to \left(\underset{\dot{}}{0}\in K\wedge 0_W\in V\right)$$
27	26	adantr	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\wedge \left(\underset{\dot{}}{0}\in V\wedge \underset{\dot{}}{1}\in V\right)\right)\to \left(\underset{\dot{}}{0}\in K\wedge 0_W\in V\right)$$
28		eqid	$$⊢{\cdot }_W={\cdot }_W$$
29	3 4 5 1 28	scafval	$$⊢\left(\underset{\dot{}}{0}\in K\wedge 0_W\in V\right)\to \underset{\dot{}}{0}\underset{\dot{}}{·}{0}_W=\underset{\dot{}}{0}{\cdot }_W{0}_W$$
30	27 29	syl	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\wedge \left(\underset{\dot{}}{0}\in V\wedge \underset{\dot{}}{1}\in V\right)\right)\to \underset{\dot{}}{0}\underset{\dot{}}{·}{0}_W=\underset{\dot{}}{0}{\cdot }_W{0}_W$$
31	24	ancli	$$⊢W\in \mathrm{LMod}\to \left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{0}\in K\right)$$
32	31	adantr	$$⊢\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\to \left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{0}\in K\right)$$
33	32	adantr	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\wedge \left(\underset{\dot{}}{0}\in V\wedge \underset{\dot{}}{1}\in V\right)\right)\to \left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{0}\in K\right)$$
34	4 28 5 10	lmodvs0	$$⊢\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{0}\in K\right)\to \underset{\dot{}}{0}{\cdot }_W{0}_W=0_W$$
35	33 34	syl	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\wedge \left(\underset{\dot{}}{0}\in V\wedge \underset{\dot{}}{1}\in V\right)\right)\to \underset{\dot{}}{0}{\cdot }_W{0}_W=0_W$$
36		simpr	$$⊢\left(\underset{\dot{}}{0}\in V\wedge \underset{\dot{}}{1}\in V\right)\to \underset{\dot{}}{1}\in V$$
37	3 13 10	grprid	$$⊢\left(W\in \mathrm{Grp}\wedge \underset{\dot{}}{1}\in V\right)\to \underset{\dot{}}{1}{+}_W{0}_W=\underset{\dot{}}{1}$$
38	21 36 37	syl2an	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\wedge \left(\underset{\dot{}}{0}\in V\wedge \underset{\dot{}}{1}\in V\right)\right)\to \underset{\dot{}}{1}{+}_W{0}_W=\underset{\dot{}}{1}$$
39	4 5 7	lmod1cl	$$⊢W\in \mathrm{LMod}\to \underset{\dot{}}{1}\in K$$
40	39	adantr	$$⊢\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\to \underset{\dot{}}{1}\in K$$
41	3 4 5 1 28	scafval	$$⊢\left(\underset{\dot{}}{1}\in K\wedge \underset{\dot{}}{1}\in V\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}\underset{\dot{}}{1}=\underset{\dot{}}{1}{\cdot }_W\underset{\dot{}}{1}$$
42	40 36 41	syl2an	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\wedge \left(\underset{\dot{}}{0}\in V\wedge \underset{\dot{}}{1}\in V\right)\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}\underset{\dot{}}{1}=\underset{\dot{}}{1}{\cdot }_W\underset{\dot{}}{1}$$
43	3 4 28 7	lmodvs1	$$⊢\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{1}\in V\right)\to \underset{\dot{}}{1}{\cdot }_W\underset{\dot{}}{1}=\underset{\dot{}}{1}$$
44	43	ad2ant2rl	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\wedge \left(\underset{\dot{}}{0}\in V\wedge \underset{\dot{}}{1}\in V\right)\right)\to \underset{\dot{}}{1}{\cdot }_W\underset{\dot{}}{1}=\underset{\dot{}}{1}$$
45	42 44	eqtrd	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\wedge \left(\underset{\dot{}}{0}\in V\wedge \underset{\dot{}}{1}\in V\right)\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}\underset{\dot{}}{1}=\underset{\dot{}}{1}$$
46		oveq	$$⊢\underset{\dot{}}{+}=\underset{\dot{}}{·}\to \underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}=\underset{\dot{}}{1}\underset{\dot{}}{·}\underset{\dot{}}{1}$$
47	46	eqcomd	$$⊢\underset{\dot{}}{+}=\underset{\dot{}}{·}\to \underset{\dot{}}{1}\underset{\dot{}}{·}\underset{\dot{}}{1}=\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}$$
48	47	ad2antlr	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\wedge \left(\underset{\dot{}}{0}\in V\wedge \underset{\dot{}}{1}\in V\right)\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}\underset{\dot{}}{1}=\underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}$$
49	36 36	jca	$$⊢\left(\underset{\dot{}}{0}\in V\wedge \underset{\dot{}}{1}\in V\right)\to \left(\underset{\dot{}}{1}\in V\wedge \underset{\dot{}}{1}\in V\right)$$
50	49	adantl	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\wedge \left(\underset{\dot{}}{0}\in V\wedge \underset{\dot{}}{1}\in V\right)\right)\to \left(\underset{\dot{}}{1}\in V\wedge \underset{\dot{}}{1}\in V\right)$$
51	3 13 2	plusfval	$$⊢\left(\underset{\dot{}}{1}\in V\wedge \underset{\dot{}}{1}\in V\right)\to \underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}=\underset{\dot{}}{1}{+}_W\underset{\dot{}}{1}$$
52	50 51	syl	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\wedge \left(\underset{\dot{}}{0}\in V\wedge \underset{\dot{}}{1}\in V\right)\right)\to \underset{\dot{}}{1}\underset{\dot{}}{+}\underset{\dot{}}{1}=\underset{\dot{}}{1}{+}_W\underset{\dot{}}{1}$$
53	48 52	eqtrd	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\wedge \left(\underset{\dot{}}{0}\in V\wedge \underset{\dot{}}{1}\in V\right)\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}\underset{\dot{}}{1}=\underset{\dot{}}{1}{+}_W\underset{\dot{}}{1}$$
54	38 45 53	3eqtr2d	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\wedge \left(\underset{\dot{}}{0}\in V\wedge \underset{\dot{}}{1}\in V\right)\right)\to \underset{\dot{}}{1}{+}_W{0}_W=\underset{\dot{}}{1}{+}_W\underset{\dot{}}{1}$$
55	21	adantr	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\wedge \left(\underset{\dot{}}{0}\in V\wedge \underset{\dot{}}{1}\in V\right)\right)\to W\in \mathrm{Grp}$$
56	12	adantr	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\wedge \left(\underset{\dot{}}{0}\in V\wedge \underset{\dot{}}{1}\in V\right)\right)\to 0_W\in V$$
57	36	adantl	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\wedge \left(\underset{\dot{}}{0}\in V\wedge \underset{\dot{}}{1}\in V\right)\right)\to \underset{\dot{}}{1}\in V$$
58	3 13	grplcan	$$⊢\left(W\in \mathrm{Grp}\wedge \left(0_W\in V\wedge \underset{\dot{}}{1}\in V\wedge \underset{\dot{}}{1}\in V\right)\right)\to \left(\underset{\dot{}}{1}{+}_W{0}_W=\underset{\dot{}}{1}{+}_W\underset{\dot{}}{1}\leftrightarrow 0_W=\underset{\dot{}}{1}\right)$$
59	55 56 57 57 58	syl13anc	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\wedge \left(\underset{\dot{}}{0}\in V\wedge \underset{\dot{}}{1}\in V\right)\right)\to \left(\underset{\dot{}}{1}{+}_W{0}_W=\underset{\dot{}}{1}{+}_W\underset{\dot{}}{1}\leftrightarrow 0_W=\underset{\dot{}}{1}\right)$$
60	54 59	mpbid	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\wedge \left(\underset{\dot{}}{0}\in V\wedge \underset{\dot{}}{1}\in V\right)\right)\to 0_W=\underset{\dot{}}{1}$$
61	30 35 60	3eqtrd	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\wedge \left(\underset{\dot{}}{0}\in V\wedge \underset{\dot{}}{1}\in V\right)\right)\to \underset{\dot{}}{0}\underset{\dot{}}{·}{0}_W=\underset{\dot{}}{1}$$
62	19 23 61	3eqtr3rd	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\wedge \left(\underset{\dot{}}{0}\in V\wedge \underset{\dot{}}{1}\in V\right)\right)\to \underset{\dot{}}{1}=\underset{\dot{}}{0}$$
63	8 62	mpdan	$$⊢\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\to \underset{\dot{}}{1}=\underset{\dot{}}{0}$$
64	63	ex	$$⊢W\in \mathrm{LMod}\to \left(\underset{\dot{}}{+}=\underset{\dot{}}{·}\to \underset{\dot{}}{1}=\underset{\dot{}}{0}\right)$$
65	64	necon3d	$$⊢W\in \mathrm{LMod}\to \left(\underset{\dot{}}{1}\ne \underset{\dot{}}{0}\to \underset{\dot{}}{+}\ne \underset{\dot{}}{·}\right)$$
66	65	imp	$$⊢\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\to \underset{\dot{}}{+}\ne \underset{\dot{}}{·}$$