zlmodzxznm

Description: Example of a linearly dependent set whose elements are not linear combinations of the others, see note in Roman p. 112). (Contributed by AV, 23-May-2019) (Revised by AV, 10-Jun-2019)

	Ref	Expression
Hypotheses	zlmodzxzequa.z	$⊢ Z = ℤ_{ring} freeLMod \{0, 1\}$
	zlmodzxzequa.o	$⊢ \underset{˙}{0} = \{⟨0, 0⟩, ⟨1, 0⟩\}$
	zlmodzxzequa.t	$⊢ \underset{˙}{∙} = \cdot_{Z}$
	zlmodzxzequa.m	$⊢ \underset{˙}{-} = -_{Z}$
	zlmodzxzequa.a	$⊢ A = \{⟨0, 3⟩, ⟨1, 6⟩\}$
	zlmodzxzequa.b	$⊢ B = \{⟨0, 2⟩, ⟨1, 4⟩\}$
Assertion	zlmodzxznm	$⊢ \forall i \in ℤ (i \underset{˙}{∙} A \neq B \land i \underset{˙}{∙} B \neq A)$

Proof

Step	Hyp	Ref	Expression
1		zlmodzxzequa.z	$⊢ Z = ℤ_{ring} freeLMod \{0, 1\}$
2		zlmodzxzequa.o	$⊢ \underset{˙}{0} = \{⟨0, 0⟩, ⟨1, 0⟩\}$
3		zlmodzxzequa.t	$⊢ \underset{˙}{∙} = \cdot_{Z}$
4		zlmodzxzequa.m	$⊢ \underset{˙}{-} = -_{Z}$
5		zlmodzxzequa.a	$⊢ A = \{⟨0, 3⟩, ⟨1, 6⟩\}$
6		zlmodzxzequa.b	$⊢ B = \{⟨0, 2⟩, ⟨1, 4⟩\}$
7		3prm	$⊢ 3 \in ℙ$
8		2prm	$⊢ 2 \in ℙ$
9		ztprmneprm	$⊢ (i \in ℤ \land 3 \in ℙ \land 2 \in ℙ) \to (i \cdot 3 = 2 \to 3 = 2)$
10	7 8 9	mp3an23	$⊢ i \in ℤ \to (i \cdot 3 = 2 \to 3 = 2)$
11		2re	$⊢ 2 \in ℝ$
12		2lt3	$⊢ 2 < 3$
13	11 12	ltneii	$⊢ 2 \neq 3$
14		eqneqall	$⊢ 2 = 3 \to (2 \neq 3 \to i \cdot 3 \neq 2)$
15	13 14	mpi	$⊢ 2 = 3 \to i \cdot 3 \neq 2$
16	15	eqcoms	$⊢ 3 = 2 \to i \cdot 3 \neq 2$
17	10 16	syl6com	$⊢ i \cdot 3 = 2 \to (i \in ℤ \to i \cdot 3 \neq 2)$
18		ax-1	$⊢ i \cdot 3 \neq 2 \to (i \in ℤ \to i \cdot 3 \neq 2)$
19	17 18	pm2.61ine	$⊢ i \in ℤ \to i \cdot 3 \neq 2$
20	19	olcd	$⊢ i \in ℤ \to (0 \neq 0 \lor i \cdot 3 \neq 2)$
21		c0ex	$⊢ 0 \in V$
22		ovex	$⊢ i \cdot 3 \in V$
23	21 22	pm3.2i	$⊢ (0 \in V \land i \cdot 3 \in V)$
24		opthneg	$⊢ (0 \in V \land i \cdot 3 \in V) \to (⟨0, i \cdot 3⟩ \neq ⟨0, 2⟩ \leftrightarrow (0 \neq 0 \lor i \cdot 3 \neq 2))$
25	23 24	mp1i	$⊢ i \in ℤ \to (⟨0, i \cdot 3⟩ \neq ⟨0, 2⟩ \leftrightarrow (0 \neq 0 \lor i \cdot 3 \neq 2))$
26	20 25	mpbird	$⊢ i \in ℤ \to ⟨0, i \cdot 3⟩ \neq ⟨0, 2⟩$
27		0ne1	$⊢ 0 \neq 1$
28	27	a1i	$⊢ i \in ℤ \to 0 \neq 1$
29	28	orcd	$⊢ i \in ℤ \to (0 \neq 1 \lor i \cdot 3 \neq 4)$
30		opthneg	$⊢ (0 \in V \land i \cdot 3 \in V) \to (⟨0, i \cdot 3⟩ \neq ⟨1, 4⟩ \leftrightarrow (0 \neq 1 \lor i \cdot 3 \neq 4))$
31	23 30	mp1i	$⊢ i \in ℤ \to (⟨0, i \cdot 3⟩ \neq ⟨1, 4⟩ \leftrightarrow (0 \neq 1 \lor i \cdot 3 \neq 4))$
32	29 31	mpbird	$⊢ i \in ℤ \to ⟨0, i \cdot 3⟩ \neq ⟨1, 4⟩$
33	26 32	jca	$⊢ i \in ℤ \to (⟨0, i \cdot 3⟩ \neq ⟨0, 2⟩ \land ⟨0, i \cdot 3⟩ \neq ⟨1, 4⟩)$
34	33	orcd	$⊢ i \in ℤ \to ((⟨0, i \cdot 3⟩ \neq ⟨0, 2⟩ \land ⟨0, i \cdot 3⟩ \neq ⟨1, 4⟩) \lor (⟨1, i \cdot 6⟩ \neq ⟨0, 2⟩ \land ⟨1, i \cdot 6⟩ \neq ⟨1, 4⟩))$
35		opex	$⊢ ⟨0, i \cdot 3⟩ \in V$
36		opex	$⊢ ⟨1, i \cdot 6⟩ \in V$
37	35 36	pm3.2i	$⊢ (⟨0, i \cdot 3⟩ \in V \land ⟨1, i \cdot 6⟩ \in V)$
38	37	a1i	$⊢ i \in ℤ \to (⟨0, i \cdot 3⟩ \in V \land ⟨1, i \cdot 6⟩ \in V)$
39		opex	$⊢ ⟨0, 2⟩ \in V$
40		opex	$⊢ ⟨1, 4⟩ \in V$
41	39 40	pm3.2i	$⊢ (⟨0, 2⟩ \in V \land ⟨1, 4⟩ \in V)$
42	41	a1i	$⊢ i \in ℤ \to (⟨0, 2⟩ \in V \land ⟨1, 4⟩ \in V)$
43	28	orcd	$⊢ i \in ℤ \to (0 \neq 1 \lor i \cdot 3 \neq i \cdot 6)$
44		opthneg	$⊢ (0 \in V \land i \cdot 3 \in V) \to (⟨0, i \cdot 3⟩ \neq ⟨1, i \cdot 6⟩ \leftrightarrow (0 \neq 1 \lor i \cdot 3 \neq i \cdot 6))$
45	23 44	mp1i	$⊢ i \in ℤ \to (⟨0, i \cdot 3⟩ \neq ⟨1, i \cdot 6⟩ \leftrightarrow (0 \neq 1 \lor i \cdot 3 \neq i \cdot 6))$
46	43 45	mpbird	$⊢ i \in ℤ \to ⟨0, i \cdot 3⟩ \neq ⟨1, i \cdot 6⟩$
47		prnebg	$⊢ ((⟨0, i \cdot 3⟩ \in V \land ⟨1, i \cdot 6⟩ \in V) \land (⟨0, 2⟩ \in V \land ⟨1, 4⟩ \in V) \land ⟨0, i \cdot 3⟩ \neq ⟨1, i \cdot 6⟩) \to (((⟨0, i \cdot 3⟩ \neq ⟨0, 2⟩ \land ⟨0, i \cdot 3⟩ \neq ⟨1, 4⟩) \lor (⟨1, i \cdot 6⟩ \neq ⟨0, 2⟩ \land ⟨1, i \cdot 6⟩ \neq ⟨1, 4⟩)) \leftrightarrow \{⟨0, i \cdot 3⟩, ⟨1, i \cdot 6⟩\} \neq \{⟨0, 2⟩, ⟨1, 4⟩\})$
48	47	bicomd	$⊢ ((⟨0, i \cdot 3⟩ \in V \land ⟨1, i \cdot 6⟩ \in V) \land (⟨0, 2⟩ \in V \land ⟨1, 4⟩ \in V) \land ⟨0, i \cdot 3⟩ \neq ⟨1, i \cdot 6⟩) \to (\{⟨0, i \cdot 3⟩, ⟨1, i \cdot 6⟩\} \neq \{⟨0, 2⟩, ⟨1, 4⟩\} \leftrightarrow ((⟨0, i \cdot 3⟩ \neq ⟨0, 2⟩ \land ⟨0, i \cdot 3⟩ \neq ⟨1, 4⟩) \lor (⟨1, i \cdot 6⟩ \neq ⟨0, 2⟩ \land ⟨1, i \cdot 6⟩ \neq ⟨1, 4⟩)))$
49	38 42 46 48	syl3anc	$⊢ i \in ℤ \to (\{⟨0, i \cdot 3⟩, ⟨1, i \cdot 6⟩\} \neq \{⟨0, 2⟩, ⟨1, 4⟩\} \leftrightarrow ((⟨0, i \cdot 3⟩ \neq ⟨0, 2⟩ \land ⟨0, i \cdot 3⟩ \neq ⟨1, 4⟩) \lor (⟨1, i \cdot 6⟩ \neq ⟨0, 2⟩ \land ⟨1, i \cdot 6⟩ \neq ⟨1, 4⟩)))$
50	34 49	mpbird	$⊢ i \in ℤ \to \{⟨0, i \cdot 3⟩, ⟨1, i \cdot 6⟩\} \neq \{⟨0, 2⟩, ⟨1, 4⟩\}$
51	5	oveq2i	$⊢ i \underset{˙}{∙} A = i \underset{˙}{∙} \{⟨0, 3⟩, ⟨1, 6⟩\}$
52		3z	$⊢ 3 \in ℤ$
53		6nn	$⊢ 6 \in ℕ$
54	53	nnzi	$⊢ 6 \in ℤ$
55	1 3	zlmodzxzscm	$⊢ (i \in ℤ \land 3 \in ℤ \land 6 \in ℤ) \to i \underset{˙}{∙} \{⟨0, 3⟩, ⟨1, 6⟩\} = \{⟨0, i \cdot 3⟩, ⟨1, i \cdot 6⟩\}$
56	52 54 55	mp3an23	$⊢ i \in ℤ \to i \underset{˙}{∙} \{⟨0, 3⟩, ⟨1, 6⟩\} = \{⟨0, i \cdot 3⟩, ⟨1, i \cdot 6⟩\}$
57	51 56	syl5eq	$⊢ i \in ℤ \to i \underset{˙}{∙} A = \{⟨0, i \cdot 3⟩, ⟨1, i \cdot 6⟩\}$
58	6	a1i	$⊢ i \in ℤ \to B = \{⟨0, 2⟩, ⟨1, 4⟩\}$
59	50 57 58	3netr4d	$⊢ i \in ℤ \to i \underset{˙}{∙} A \neq B$
60		ztprmneprm	$⊢ (i \in ℤ \land 2 \in ℙ \land 3 \in ℙ) \to (i \cdot 2 = 3 \to 2 = 3)$
61	8 7 60	mp3an23	$⊢ i \in ℤ \to (i \cdot 2 = 3 \to 2 = 3)$
62		eqneqall	$⊢ 2 = 3 \to (2 \neq 3 \to i \cdot 2 \neq 3)$
63	13 62	mpi	$⊢ 2 = 3 \to i \cdot 2 \neq 3$
64	61 63	syl6com	$⊢ i \cdot 2 = 3 \to (i \in ℤ \to i \cdot 2 \neq 3)$
65		ax-1	$⊢ i \cdot 2 \neq 3 \to (i \in ℤ \to i \cdot 2 \neq 3)$
66	64 65	pm2.61ine	$⊢ i \in ℤ \to i \cdot 2 \neq 3$
67	66	olcd	$⊢ i \in ℤ \to (0 \neq 0 \lor i \cdot 2 \neq 3)$
68		ovex	$⊢ i \cdot 2 \in V$
69	21 68	pm3.2i	$⊢ (0 \in V \land i \cdot 2 \in V)$
70		opthneg	$⊢ (0 \in V \land i \cdot 2 \in V) \to (⟨0, i \cdot 2⟩ \neq ⟨0, 3⟩ \leftrightarrow (0 \neq 0 \lor i \cdot 2 \neq 3))$
71	69 70	mp1i	$⊢ i \in ℤ \to (⟨0, i \cdot 2⟩ \neq ⟨0, 3⟩ \leftrightarrow (0 \neq 0 \lor i \cdot 2 \neq 3))$
72	67 71	mpbird	$⊢ i \in ℤ \to ⟨0, i \cdot 2⟩ \neq ⟨0, 3⟩$
73	28	orcd	$⊢ i \in ℤ \to (0 \neq 1 \lor i \cdot 2 \neq 6)$
74		opthneg	$⊢ (0 \in V \land i \cdot 2 \in V) \to (⟨0, i \cdot 2⟩ \neq ⟨1, 6⟩ \leftrightarrow (0 \neq 1 \lor i \cdot 2 \neq 6))$
75	69 74	mp1i	$⊢ i \in ℤ \to (⟨0, i \cdot 2⟩ \neq ⟨1, 6⟩ \leftrightarrow (0 \neq 1 \lor i \cdot 2 \neq 6))$
76	73 75	mpbird	$⊢ i \in ℤ \to ⟨0, i \cdot 2⟩ \neq ⟨1, 6⟩$
77	72 76	jca	$⊢ i \in ℤ \to (⟨0, i \cdot 2⟩ \neq ⟨0, 3⟩ \land ⟨0, i \cdot 2⟩ \neq ⟨1, 6⟩)$
78	77	orcd	$⊢ i \in ℤ \to ((⟨0, i \cdot 2⟩ \neq ⟨0, 3⟩ \land ⟨0, i \cdot 2⟩ \neq ⟨1, 6⟩) \lor (⟨1, i \cdot 4⟩ \neq ⟨0, 3⟩ \land ⟨1, i \cdot 4⟩ \neq ⟨1, 6⟩))$
79		opex	$⊢ ⟨0, i \cdot 2⟩ \in V$
80		opex	$⊢ ⟨1, i \cdot 4⟩ \in V$
81	79 80	pm3.2i	$⊢ (⟨0, i \cdot 2⟩ \in V \land ⟨1, i \cdot 4⟩ \in V)$
82	81	a1i	$⊢ i \in ℤ \to (⟨0, i \cdot 2⟩ \in V \land ⟨1, i \cdot 4⟩ \in V)$
83		opex	$⊢ ⟨0, 3⟩ \in V$
84		opex	$⊢ ⟨1, 6⟩ \in V$
85	83 84	pm3.2i	$⊢ (⟨0, 3⟩ \in V \land ⟨1, 6⟩ \in V)$
86	85	a1i	$⊢ i \in ℤ \to (⟨0, 3⟩ \in V \land ⟨1, 6⟩ \in V)$
87	28	orcd	$⊢ i \in ℤ \to (0 \neq 1 \lor i \cdot 2 \neq i \cdot 4)$
88		opthneg	$⊢ (0 \in V \land i \cdot 2 \in V) \to (⟨0, i \cdot 2⟩ \neq ⟨1, i \cdot 4⟩ \leftrightarrow (0 \neq 1 \lor i \cdot 2 \neq i \cdot 4))$
89	69 88	mp1i	$⊢ i \in ℤ \to (⟨0, i \cdot 2⟩ \neq ⟨1, i \cdot 4⟩ \leftrightarrow (0 \neq 1 \lor i \cdot 2 \neq i \cdot 4))$
90	87 89	mpbird	$⊢ i \in ℤ \to ⟨0, i \cdot 2⟩ \neq ⟨1, i \cdot 4⟩$
91		prnebg	$⊢ ((⟨0, i \cdot 2⟩ \in V \land ⟨1, i \cdot 4⟩ \in V) \land (⟨0, 3⟩ \in V \land ⟨1, 6⟩ \in V) \land ⟨0, i \cdot 2⟩ \neq ⟨1, i \cdot 4⟩) \to (((⟨0, i \cdot 2⟩ \neq ⟨0, 3⟩ \land ⟨0, i \cdot 2⟩ \neq ⟨1, 6⟩) \lor (⟨1, i \cdot 4⟩ \neq ⟨0, 3⟩ \land ⟨1, i \cdot 4⟩ \neq ⟨1, 6⟩)) \leftrightarrow \{⟨0, i \cdot 2⟩, ⟨1, i \cdot 4⟩\} \neq \{⟨0, 3⟩, ⟨1, 6⟩\})$
92	91	bicomd	$⊢ ((⟨0, i \cdot 2⟩ \in V \land ⟨1, i \cdot 4⟩ \in V) \land (⟨0, 3⟩ \in V \land ⟨1, 6⟩ \in V) \land ⟨0, i \cdot 2⟩ \neq ⟨1, i \cdot 4⟩) \to (\{⟨0, i \cdot 2⟩, ⟨1, i \cdot 4⟩\} \neq \{⟨0, 3⟩, ⟨1, 6⟩\} \leftrightarrow ((⟨0, i \cdot 2⟩ \neq ⟨0, 3⟩ \land ⟨0, i \cdot 2⟩ \neq ⟨1, 6⟩) \lor (⟨1, i \cdot 4⟩ \neq ⟨0, 3⟩ \land ⟨1, i \cdot 4⟩ \neq ⟨1, 6⟩)))$
93	82 86 90 92	syl3anc	$⊢ i \in ℤ \to (\{⟨0, i \cdot 2⟩, ⟨1, i \cdot 4⟩\} \neq \{⟨0, 3⟩, ⟨1, 6⟩\} \leftrightarrow ((⟨0, i \cdot 2⟩ \neq ⟨0, 3⟩ \land ⟨0, i \cdot 2⟩ \neq ⟨1, 6⟩) \lor (⟨1, i \cdot 4⟩ \neq ⟨0, 3⟩ \land ⟨1, i \cdot 4⟩ \neq ⟨1, 6⟩)))$
94	78 93	mpbird	$⊢ i \in ℤ \to \{⟨0, i \cdot 2⟩, ⟨1, i \cdot 4⟩\} \neq \{⟨0, 3⟩, ⟨1, 6⟩\}$
95	6	oveq2i	$⊢ i \underset{˙}{∙} B = i \underset{˙}{∙} \{⟨0, 2⟩, ⟨1, 4⟩\}$
96		2z	$⊢ 2 \in ℤ$
97		4z	$⊢ 4 \in ℤ$
98	1 3	zlmodzxzscm	$⊢ (i \in ℤ \land 2 \in ℤ \land 4 \in ℤ) \to i \underset{˙}{∙} \{⟨0, 2⟩, ⟨1, 4⟩\} = \{⟨0, i \cdot 2⟩, ⟨1, i \cdot 4⟩\}$
99	96 97 98	mp3an23	$⊢ i \in ℤ \to i \underset{˙}{∙} \{⟨0, 2⟩, ⟨1, 4⟩\} = \{⟨0, i \cdot 2⟩, ⟨1, i \cdot 4⟩\}$
100	95 99	syl5eq	$⊢ i \in ℤ \to i \underset{˙}{∙} B = \{⟨0, i \cdot 2⟩, ⟨1, i \cdot 4⟩\}$
101	5	a1i	$⊢ i \in ℤ \to A = \{⟨0, 3⟩, ⟨1, 6⟩\}$
102	94 100 101	3netr4d	$⊢ i \in ℤ \to i \underset{˙}{∙} B \neq A$
103	59 102	jca	$⊢ i \in ℤ \to (i \underset{˙}{∙} A \neq B \land i \underset{˙}{∙} B \neq A)$
104	103	rgen	$⊢ \forall i \in ℤ (i \underset{˙}{∙} A \neq B \land i \underset{˙}{∙} B \neq A)$

Metamath Proof Explorer

Theorem zlmodzxznm

Proof