islininds2

Description: Implication of being a linearly independent subset of a (left) module over a nonzero ring. (Contributed by AV, 29-Apr-2019) (Proof shortened by AV, 30-Jul-2019)

	Ref	Expression
Hypotheses	islindeps2.b	$⊢ B = {Base}_{M}$
	islindeps2.z	$⊢ Z = 0_{M}$
	islindeps2.r	$⊢ R = Scalar (M)$
	islindeps2.e	$⊢ E = {Base}_{R}$
	islindeps2.0	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	islininds2	$⊢ (M \in LMod \land S \in 𝒫 B \land R \in NzRing) \to (S linIndS M \to \forall s \in S \forall f \in (E^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (f) \lor f linC (M) (S ∖ \{s\}) \neq s))$

Proof

Step	Hyp	Ref	Expression
1		islindeps2.b	$⊢ B = {Base}_{M}$
2		islindeps2.z	$⊢ Z = 0_{M}$
3		islindeps2.r	$⊢ R = Scalar (M)$
4		islindeps2.e	$⊢ E = {Base}_{R}$
5		islindeps2.0	$⊢ \underset{˙}{0} = 0_{R}$
6		lindepsnlininds	$⊢ (S \in 𝒫 B \land M \in LMod) \to (S linDepS M \leftrightarrow \neg S linIndS M)$
7	6	ancoms	$⊢ (M \in LMod \land S \in 𝒫 B) \to (S linDepS M \leftrightarrow \neg S linIndS M)$
8	7	3adant3	$⊢ (M \in LMod \land S \in 𝒫 B \land R \in NzRing) \to (S linDepS M \leftrightarrow \neg S linIndS M)$
9	8	con2bid	$⊢ (M \in LMod \land S \in 𝒫 B \land R \in NzRing) \to (S linIndS M \leftrightarrow \neg S linDepS M)$
10		notnotb	$⊢ {finSupp}_{\underset{˙}{0}} (f) \leftrightarrow \neg \neg {finSupp}_{\underset{˙}{0}} (f)$
11		nne	$⊢ \neg f linC (M) (S ∖ \{s\}) \neq s \leftrightarrow f linC (M) (S ∖ \{s\}) = s$
12	11	bicomi	$⊢ f linC (M) (S ∖ \{s\}) = s \leftrightarrow \neg f linC (M) (S ∖ \{s\}) \neq s$
13	10 12	anbi12i	$⊢ ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s) \leftrightarrow (\neg \neg {finSupp}_{\underset{˙}{0}} (f) \land \neg f linC (M) (S ∖ \{s\}) \neq s)$
14		pm4.56	$⊢ (\neg \neg {finSupp}_{\underset{˙}{0}} (f) \land \neg f linC (M) (S ∖ \{s\}) \neq s) \leftrightarrow \neg (\neg {finSupp}_{\underset{˙}{0}} (f) \lor f linC (M) (S ∖ \{s\}) \neq s)$
15	13 14	bitri	$⊢ ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s) \leftrightarrow \neg (\neg {finSupp}_{\underset{˙}{0}} (f) \lor f linC (M) (S ∖ \{s\}) \neq s)$
16	15	rexbii	$⊢ \exists f \in (E^{(S ∖ \{s\})}) ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s) \leftrightarrow \exists f \in (E^{(S ∖ \{s\})}) \neg (\neg {finSupp}_{\underset{˙}{0}} (f) \lor f linC (M) (S ∖ \{s\}) \neq s)$
17		rexnal	$⊢ \exists f \in (E^{(S ∖ \{s\})}) \neg (\neg {finSupp}_{\underset{˙}{0}} (f) \lor f linC (M) (S ∖ \{s\}) \neq s) \leftrightarrow \neg \forall f \in (E^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (f) \lor f linC (M) (S ∖ \{s\}) \neq s)$
18	16 17	bitri	$⊢ \exists f \in (E^{(S ∖ \{s\})}) ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s) \leftrightarrow \neg \forall f \in (E^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (f) \lor f linC (M) (S ∖ \{s\}) \neq s)$
19	18	rexbii	$⊢ \exists s \in S \exists f \in (E^{(S ∖ \{s\})}) ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s) \leftrightarrow \exists s \in S \neg \forall f \in (E^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (f) \lor f linC (M) (S ∖ \{s\}) \neq s)$
20		rexnal	$⊢ \exists s \in S \neg \forall f \in (E^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (f) \lor f linC (M) (S ∖ \{s\}) \neq s) \leftrightarrow \neg \forall s \in S \forall f \in (E^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (f) \lor f linC (M) (S ∖ \{s\}) \neq s)$
21	19 20	bitri	$⊢ \exists s \in S \exists f \in (E^{(S ∖ \{s\})}) ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s) \leftrightarrow \neg \forall s \in S \forall f \in (E^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (f) \lor f linC (M) (S ∖ \{s\}) \neq s)$
22	1 2 3 4 5	islindeps2	$⊢ (M \in LMod \land S \in 𝒫 B \land R \in NzRing) \to (\exists s \in S \exists f \in (E^{(S ∖ \{s\})}) ({finSupp}_{\underset{˙}{0}} (f) \land f linC (M) (S ∖ \{s\}) = s) \to S linDepS M)$
23	21 22	syl5bir	$⊢ (M \in LMod \land S \in 𝒫 B \land R \in NzRing) \to (\neg \forall s \in S \forall f \in (E^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (f) \lor f linC (M) (S ∖ \{s\}) \neq s) \to S linDepS M)$
24	23	con1d	$⊢ (M \in LMod \land S \in 𝒫 B \land R \in NzRing) \to (\neg S linDepS M \to \forall s \in S \forall f \in (E^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (f) \lor f linC (M) (S ∖ \{s\}) \neq s))$
25	9 24	sylbid	$⊢ (M \in LMod \land S \in 𝒫 B \land R \in NzRing) \to (S linIndS M \to \forall s \in S \forall f \in (E^{(S ∖ \{s\})}) (\neg {finSupp}_{\underset{˙}{0}} (f) \lor f linC (M) (S ∖ \{s\}) \neq s))$

Metamath Proof Explorer

Theorem islininds2

Proof