ldepspr

Description: If a vector is a scalar multiple of another vector, the (unordered pair containing the) two vectors are linearly dependent. (Contributed by AV, 16-Apr-2019) (Revised by AV, 27-Apr-2019) (Proof shortened by AV, 30-Jul-2019)

	Ref	Expression
Hypotheses	snlindsntor.b	$⊢ B = {Base}_{M}$
	snlindsntor.r	$⊢ R = Scalar (M)$
	snlindsntor.s	$⊢ S = {Base}_{R}$
	snlindsntor.0	$⊢ \underset{˙}{0} = 0_{R}$
	snlindsntor.z	$⊢ Z = 0_{M}$
	snlindsntor.t	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
Assertion	ldepspr	$⊢ (M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \to ((A \in S \land X = A \underset{˙}{\cdot} Y) \to \{X, Y\} linDepS M)$

Proof

Step	Hyp	Ref	Expression
1		snlindsntor.b	$⊢ B = {Base}_{M}$
2		snlindsntor.r	$⊢ R = Scalar (M)$
3		snlindsntor.s	$⊢ S = {Base}_{R}$
4		snlindsntor.0	$⊢ \underset{˙}{0} = 0_{R}$
5		snlindsntor.z	$⊢ Z = 0_{M}$
6		snlindsntor.t	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
7		3simpa	$⊢ (X \in B \land Y \in B \land X \neq Y) \to (X \in B \land Y \in B)$
8	7	ad2antlr	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to (X \in B \land Y \in B)$
9		fvex	$⊢ 1_{R} \in V$
10		fvex	$⊢ {inv}_{g} (R) (A) \in V$
11	9 10	pm3.2i	$⊢ (1_{R} \in V \land {inv}_{g} (R) (A) \in V)$
12	11	a1i	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to (1_{R} \in V \land {inv}_{g} (R) (A) \in V)$
13		simp3	$⊢ (X \in B \land Y \in B \land X \neq Y) \to X \neq Y$
14	13	ad2antlr	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to X \neq Y$
15		fprg	$⊢ ((X \in B \land Y \in B) \land (1_{R} \in V \land {inv}_{g} (R) (A) \in V) \land X \neq Y) \to \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} : \{X, Y\} ⟶ \{1_{R}, {inv}_{g} (R) (A)\}$
16	8 12 14 15	syl3anc	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} : \{X, Y\} ⟶ \{1_{R}, {inv}_{g} (R) (A)\}$
17		prfi	$⊢ \{X, Y\} \in Fin$
18	17	a1i	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to \{X, Y\} \in Fin$
19	4	fvexi	$⊢ \underset{˙}{0} \in V$
20	19	a1i	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to \underset{˙}{0} \in V$
21	16 18 20	fdmfifsupp	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to {finSupp}_{\underset{˙}{0}} (\{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\})$
22	13	anim2i	$⊢ (M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \to (M \in LMod \land X \neq Y)$
23	22	adantr	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to (M \in LMod \land X \neq Y)$
24		eqid	$⊢ 1_{R} = 1_{R}$
25	2 3 24	lmod1cl	$⊢ M \in LMod \to 1_{R} \in S$
26		simp1	$⊢ (X \in B \land Y \in B \land X \neq Y) \to X \in B$
27	25 26	anim12ci	$⊢ (M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \to (X \in B \land 1_{R} \in S)$
28	27	adantr	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to (X \in B \land 1_{R} \in S)$
29		simp2	$⊢ (X \in B \land Y \in B \land X \neq Y) \to Y \in B$
30	29	ad2antlr	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to Y \in B$
31	2	lmodfgrp	$⊢ M \in LMod \to R \in Grp$
32	31	adantr	$⊢ (M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \to R \in Grp$
33		simpl	$⊢ (A \in S \land X = A \underset{˙}{\cdot} Y) \to A \in S$
34		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
35	3 34	grpinvcl	$⊢ (R \in Grp \land A \in S) \to {inv}_{g} (R) (A) \in S$
36	32 33 35	syl2an	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to {inv}_{g} (R) (A) \in S$
37		eqid	$⊢ +_{M} = +_{M}$
38		eqid	$⊢ \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} = \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\}$
39	1 2 3 6 37 38	lincvalpr	$⊢ ((M \in LMod \land X \neq Y) \land (X \in B \land 1_{R} \in S) \land (Y \in B \land {inv}_{g} (R) (A) \in S)) \to \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} linC (M) \{X, Y\} = (1_{R} \underset{˙}{\cdot} X) +_{M} ({inv}_{g} (R) (A) \underset{˙}{\cdot} Y)$
40	23 28 30 36 39	syl112anc	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} linC (M) \{X, Y\} = (1_{R} \underset{˙}{\cdot} X) +_{M} ({inv}_{g} (R) (A) \underset{˙}{\cdot} Y)$
41		simpll	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to M \in LMod$
42	26	ad2antlr	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to X \in B$
43	33	adantl	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to A \in S$
44	42 30 43	3jca	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to (X \in B \land Y \in B \land A \in S)$
45	41 44	jca	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to (M \in LMod \land (X \in B \land Y \in B \land A \in S))$
46		simprr	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to X = A \underset{˙}{\cdot} Y$
47	1 2 3 4 5 6 24 34	ldepsprlem	$⊢ (M \in LMod \land (X \in B \land Y \in B \land A \in S)) \to (X = A \underset{˙}{\cdot} Y \to (1_{R} \underset{˙}{\cdot} X) +_{M} ({inv}_{g} (R) (A) \underset{˙}{\cdot} Y) = Z)$
48	45 46 47	sylc	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to (1_{R} \underset{˙}{\cdot} X) +_{M} ({inv}_{g} (R) (A) \underset{˙}{\cdot} Y) = Z$
49	40 48	eqtrd	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} linC (M) \{X, Y\} = Z$
50	2	lmodring	$⊢ M \in LMod \to R \in Ring$
51		eqcom	$⊢ 1_{R} = 0_{R} \leftrightarrow 0_{R} = 1_{R}$
52		eqid	$⊢ 0_{R} = 0_{R}$
53	3 52 24	01eq0ring	$⊢ (R \in Ring \land 0_{R} = 1_{R}) \to S = \{0_{R}\}$
54		sneq	$⊢ 0_{R} = 1_{R} \to \{0_{R}\} = \{1_{R}\}$
55	54	eqeq2d	$⊢ 0_{R} = 1_{R} \to (S = \{0_{R}\} \leftrightarrow S = \{1_{R}\})$
56		eleq2	$⊢ S = \{1_{R}\} \to (A \in S \leftrightarrow A \in \{1_{R}\})$
57		elsni	$⊢ A \in \{1_{R}\} \to A = 1_{R}$
58		oveq1	$⊢ A = 1_{R} \to A \underset{˙}{\cdot} Y = 1_{R} \underset{˙}{\cdot} Y$
59	58	eqeq2d	$⊢ A = 1_{R} \to (X = A \underset{˙}{\cdot} Y \leftrightarrow X = 1_{R} \underset{˙}{\cdot} Y)$
60	29	anim1i	$⊢ ((X \in B \land Y \in B \land X \neq Y) \land M \in LMod) \to (Y \in B \land M \in LMod)$
61	60	ancomd	$⊢ ((X \in B \land Y \in B \land X \neq Y) \land M \in LMod) \to (M \in LMod \land Y \in B)$
62	1 2 6 24	lmodvs1	$⊢ (M \in LMod \land Y \in B) \to 1_{R} \underset{˙}{\cdot} Y = Y$
63	61 62	syl	$⊢ ((X \in B \land Y \in B \land X \neq Y) \land M \in LMod) \to 1_{R} \underset{˙}{\cdot} Y = Y$
64	63	eqeq2d	$⊢ ((X \in B \land Y \in B \land X \neq Y) \land M \in LMod) \to (X = 1_{R} \underset{˙}{\cdot} Y \leftrightarrow X = Y)$
65		eqneqall	$⊢ X = Y \to (X \neq Y \to (\neg 1_{R} = 0_{R} \lor {inv}_{g} (R) (A) \neq \underset{˙}{0}))$
66	65	com12	$⊢ X \neq Y \to (X = Y \to (\neg 1_{R} = 0_{R} \lor {inv}_{g} (R) (A) \neq \underset{˙}{0}))$
67	66	3ad2ant3	$⊢ (X \in B \land Y \in B \land X \neq Y) \to (X = Y \to (\neg 1_{R} = 0_{R} \lor {inv}_{g} (R) (A) \neq \underset{˙}{0}))$
68	67	adantr	$⊢ ((X \in B \land Y \in B \land X \neq Y) \land M \in LMod) \to (X = Y \to (\neg 1_{R} = 0_{R} \lor {inv}_{g} (R) (A) \neq \underset{˙}{0}))$
69	64 68	sylbid	$⊢ ((X \in B \land Y \in B \land X \neq Y) \land M \in LMod) \to (X = 1_{R} \underset{˙}{\cdot} Y \to (\neg 1_{R} = 0_{R} \lor {inv}_{g} (R) (A) \neq \underset{˙}{0}))$
70	69	ex	$⊢ (X \in B \land Y \in B \land X \neq Y) \to (M \in LMod \to (X = 1_{R} \underset{˙}{\cdot} Y \to (\neg 1_{R} = 0_{R} \lor {inv}_{g} (R) (A) \neq \underset{˙}{0})))$
71	70	com3r	$⊢ X = 1_{R} \underset{˙}{\cdot} Y \to ((X \in B \land Y \in B \land X \neq Y) \to (M \in LMod \to (\neg 1_{R} = 0_{R} \lor {inv}_{g} (R) (A) \neq \underset{˙}{0})))$
72	59 71	syl6bi	$⊢ A = 1_{R} \to (X = A \underset{˙}{\cdot} Y \to ((X \in B \land Y \in B \land X \neq Y) \to (M \in LMod \to (\neg 1_{R} = 0_{R} \lor {inv}_{g} (R) (A) \neq \underset{˙}{0}))))$
73	57 72	syl	$⊢ A \in \{1_{R}\} \to (X = A \underset{˙}{\cdot} Y \to ((X \in B \land Y \in B \land X \neq Y) \to (M \in LMod \to (\neg 1_{R} = 0_{R} \lor {inv}_{g} (R) (A) \neq \underset{˙}{0}))))$
74	56 73	syl6bi	$⊢ S = \{1_{R}\} \to (A \in S \to (X = A \underset{˙}{\cdot} Y \to ((X \in B \land Y \in B \land X \neq Y) \to (M \in LMod \to (\neg 1_{R} = 0_{R} \lor {inv}_{g} (R) (A) \neq \underset{˙}{0})))))$
75	74	impd	$⊢ S = \{1_{R}\} \to ((A \in S \land X = A \underset{˙}{\cdot} Y) \to ((X \in B \land Y \in B \land X \neq Y) \to (M \in LMod \to (\neg 1_{R} = 0_{R} \lor {inv}_{g} (R) (A) \neq \underset{˙}{0}))))$
76	75	com23	$⊢ S = \{1_{R}\} \to ((X \in B \land Y \in B \land X \neq Y) \to ((A \in S \land X = A \underset{˙}{\cdot} Y) \to (M \in LMod \to (\neg 1_{R} = 0_{R} \lor {inv}_{g} (R) (A) \neq \underset{˙}{0}))))$
77	55 76	syl6bi	$⊢ 0_{R} = 1_{R} \to (S = \{0_{R}\} \to ((X \in B \land Y \in B \land X \neq Y) \to ((A \in S \land X = A \underset{˙}{\cdot} Y) \to (M \in LMod \to (\neg 1_{R} = 0_{R} \lor {inv}_{g} (R) (A) \neq \underset{˙}{0})))))$
78	77	adantl	$⊢ (R \in Ring \land 0_{R} = 1_{R}) \to (S = \{0_{R}\} \to ((X \in B \land Y \in B \land X \neq Y) \to ((A \in S \land X = A \underset{˙}{\cdot} Y) \to (M \in LMod \to (\neg 1_{R} = 0_{R} \lor {inv}_{g} (R) (A) \neq \underset{˙}{0})))))$
79	53 78	mpd	$⊢ (R \in Ring \land 0_{R} = 1_{R}) \to ((X \in B \land Y \in B \land X \neq Y) \to ((A \in S \land X = A \underset{˙}{\cdot} Y) \to (M \in LMod \to (\neg 1_{R} = 0_{R} \lor {inv}_{g} (R) (A) \neq \underset{˙}{0}))))$
80	79	ex	$⊢ R \in Ring \to (0_{R} = 1_{R} \to ((X \in B \land Y \in B \land X \neq Y) \to ((A \in S \land X = A \underset{˙}{\cdot} Y) \to (M \in LMod \to (\neg 1_{R} = 0_{R} \lor {inv}_{g} (R) (A) \neq \underset{˙}{0})))))$
81	51 80	syl5bi	$⊢ R \in Ring \to (1_{R} = 0_{R} \to ((X \in B \land Y \in B \land X \neq Y) \to ((A \in S \land X = A \underset{˙}{\cdot} Y) \to (M \in LMod \to (\neg 1_{R} = 0_{R} \lor {inv}_{g} (R) (A) \neq \underset{˙}{0})))))$
82	81	com25	$⊢ R \in Ring \to (M \in LMod \to ((X \in B \land Y \in B \land X \neq Y) \to ((A \in S \land X = A \underset{˙}{\cdot} Y) \to (1_{R} = 0_{R} \to (\neg 1_{R} = 0_{R} \lor {inv}_{g} (R) (A) \neq \underset{˙}{0})))))$
83	50 82	mpcom	$⊢ M \in LMod \to ((X \in B \land Y \in B \land X \neq Y) \to ((A \in S \land X = A \underset{˙}{\cdot} Y) \to (1_{R} = 0_{R} \to (\neg 1_{R} = 0_{R} \lor {inv}_{g} (R) (A) \neq \underset{˙}{0}))))$
84	83	imp31	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to (1_{R} = 0_{R} \to (\neg 1_{R} = 0_{R} \lor {inv}_{g} (R) (A) \neq \underset{˙}{0}))$
85		orc	$⊢ \neg 1_{R} = 0_{R} \to (\neg 1_{R} = 0_{R} \lor {inv}_{g} (R) (A) \neq \underset{˙}{0})$
86	84 85	pm2.61d1	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to (\neg 1_{R} = 0_{R} \lor {inv}_{g} (R) (A) \neq \underset{˙}{0})$
87	4	eqeq2i	$⊢ 1_{R} = \underset{˙}{0} \leftrightarrow 1_{R} = 0_{R}$
88	87	necon3abii	$⊢ 1_{R} \neq \underset{˙}{0} \leftrightarrow \neg 1_{R} = 0_{R}$
89	88	orbi1i	$⊢ (1_{R} \neq \underset{˙}{0} \lor {inv}_{g} (R) (A) \neq \underset{˙}{0}) \leftrightarrow (\neg 1_{R} = 0_{R} \lor {inv}_{g} (R) (A) \neq \underset{˙}{0})$
90	86 89	sylibr	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to (1_{R} \neq \underset{˙}{0} \lor {inv}_{g} (R) (A) \neq \underset{˙}{0})$
91		fvexd	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to 1_{R} \in V$
92		fvpr1g	$⊢ (X \in B \land 1_{R} \in V \land X \neq Y) \to \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (X) = 1_{R}$
93	42 91 14 92	syl3anc	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (X) = 1_{R}$
94	93	neeq1d	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to (\{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (X) \neq \underset{˙}{0} \leftrightarrow 1_{R} \neq \underset{˙}{0})$
95		fvexd	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to {inv}_{g} (R) (A) \in V$
96		fvpr2g	$⊢ (Y \in B \land {inv}_{g} (R) (A) \in V \land X \neq Y) \to \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (Y) = {inv}_{g} (R) (A)$
97	30 95 14 96	syl3anc	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (Y) = {inv}_{g} (R) (A)$
98	97	neeq1d	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to (\{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (Y) \neq \underset{˙}{0} \leftrightarrow {inv}_{g} (R) (A) \neq \underset{˙}{0})$
99	94 98	orbi12d	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to ((\{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (X) \neq \underset{˙}{0} \lor \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (Y) \neq \underset{˙}{0}) \leftrightarrow (1_{R} \neq \underset{˙}{0} \lor {inv}_{g} (R) (A) \neq \underset{˙}{0}))$
100	90 99	mpbird	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to (\{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (X) \neq \underset{˙}{0} \lor \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (Y) \neq \underset{˙}{0})$
101		fveq2	$⊢ v = X \to \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (v) = \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (X)$
102	101	neeq1d	$⊢ v = X \to (\{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (v) \neq \underset{˙}{0} \leftrightarrow \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (X) \neq \underset{˙}{0})$
103		fveq2	$⊢ v = Y \to \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (v) = \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (Y)$
104	103	neeq1d	$⊢ v = Y \to (\{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (v) \neq \underset{˙}{0} \leftrightarrow \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (Y) \neq \underset{˙}{0})$
105	102 104	rexprg	$⊢ (X \in B \land Y \in B) \to (\exists v \in \{X, Y\} \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (v) \neq \underset{˙}{0} \leftrightarrow (\{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (X) \neq \underset{˙}{0} \lor \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (Y) \neq \underset{˙}{0}))$
106	8 105	syl	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to (\exists v \in \{X, Y\} \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (v) \neq \underset{˙}{0} \leftrightarrow (\{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (X) \neq \underset{˙}{0} \lor \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (Y) \neq \underset{˙}{0}))$
107	100 106	mpbird	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to \exists v \in \{X, Y\} \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (v) \neq \underset{˙}{0}$
108	25	adantr	$⊢ (M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \to 1_{R} \in S$
109	108	adantr	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to 1_{R} \in S$
110	3	fvexi	$⊢ S \in V$
111	14 110	jctir	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to (X \neq Y \land S \in V)$
112	38	mapprop	$⊢ ((X \in B \land 1_{R} \in S) \land (Y \in B \land {inv}_{g} (R) (A) \in S) \land (X \neq Y \land S \in V)) \to \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} \in (S^{\{X, Y\}})$
113	42 109 30 36 111 112	syl221anc	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} \in (S^{\{X, Y\}})$
114		breq1	$⊢ f = \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} \to ({finSupp}_{\underset{˙}{0}} (f) \leftrightarrow {finSupp}_{\underset{˙}{0}} (\{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\}))$
115		oveq1	$⊢ f = \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} \to f linC (M) \{X, Y\} = \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} linC (M) \{X, Y\}$
116	115	eqeq1d	$⊢ f = \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} \to (f linC (M) \{X, Y\} = Z \leftrightarrow \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} linC (M) \{X, Y\} = Z)$
117		fveq1	$⊢ f = \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} \to f (v) = \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (v)$
118	117	neeq1d	$⊢ f = \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} \to (f (v) \neq \underset{˙}{0} \leftrightarrow \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (v) \neq \underset{˙}{0})$
119	118	rexbidv	$⊢ f = \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} \to (\exists v \in \{X, Y\} f (v) \neq \underset{˙}{0} \leftrightarrow \exists v \in \{X, Y\} \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (v) \neq \underset{˙}{0})$
120	114 116 119	3anbi123d	$⊢ f = \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} \to (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) \{X, Y\} = Z \land \exists v \in \{X, Y\} f (v) \neq \underset{˙}{0}) \leftrightarrow ({finSupp}_{\underset{˙}{0}} (\{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\}) \land \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} linC (M) \{X, Y\} = Z \land \exists v \in \{X, Y\} \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (v) \neq \underset{˙}{0}))$
121	120	adantl	$⊢ (((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \land f = \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\}) \to (({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) \{X, Y\} = Z \land \exists v \in \{X, Y\} f (v) \neq \underset{˙}{0}) \leftrightarrow ({finSupp}_{\underset{˙}{0}} (\{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\}) \land \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} linC (M) \{X, Y\} = Z \land \exists v \in \{X, Y\} \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (v) \neq \underset{˙}{0}))$
122	113 121	rspcedv	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to (({finSupp}_{\underset{˙}{0}} (\{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\}) \land \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} linC (M) \{X, Y\} = Z \land \exists v \in \{X, Y\} \{⟨X, 1_{R}⟩, ⟨Y, {inv}_{g} (R) (A)⟩\} (v) \neq \underset{˙}{0}) \to \exists f \in (S^{\{X, Y\}}) ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) \{X, Y\} = Z \land \exists v \in \{X, Y\} f (v) \neq \underset{˙}{0}))$
123	21 49 107 122	mp3and	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to \exists f \in (S^{\{X, Y\}}) ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) \{X, Y\} = Z \land \exists v \in \{X, Y\} f (v) \neq \underset{˙}{0})$
124		prelpwi	$⊢ (X \in B \land Y \in B) \to \{X, Y\} \in 𝒫 B$
125	124	3adant3	$⊢ (X \in B \land Y \in B \land X \neq Y) \to \{X, Y\} \in 𝒫 B$
126	125	ad2antlr	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to \{X, Y\} \in 𝒫 B$
127	1 5 2 3 4	islindeps	$⊢ (M \in LMod \land \{X, Y\} \in 𝒫 B) \to (\{X, Y\} linDepS M \leftrightarrow \exists f \in (S^{\{X, Y\}}) ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) \{X, Y\} = Z \land \exists v \in \{X, Y\} f (v) \neq \underset{˙}{0}))$
128	41 126 127	syl2anc	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to (\{X, Y\} linDepS M \leftrightarrow \exists f \in (S^{\{X, Y\}}) ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) \{X, Y\} = Z \land \exists v \in \{X, Y\} f (v) \neq \underset{˙}{0}))$
129	123 128	mpbird	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \land (A \in S \land X = A \underset{˙}{\cdot} Y)) \to \{X, Y\} linDepS M$
130	129	ex	$⊢ (M \in LMod \land (X \in B \land Y \in B \land X \neq Y)) \to ((A \in S \land X = A \underset{˙}{\cdot} Y) \to \{X, Y\} linDepS M)$

Metamath Proof Explorer

Theorem ldepspr

Proof