lsatcmp

Description: If two atoms are comparable, they are equal. ( atsseq analog.) TODO: can lspsncmp shorten this? (Contributed by NM, 25-Aug-2014)

	Ref	Expression
Hypotheses	lsatcmp.a	$⊢ A = LSAtoms (W)$
	lsatcmp.w	$⊢ φ \to W \in LVec$
	lsatcmp.t	$⊢ φ \to T \in A$
	lsatcmp.u	$⊢ φ \to U \in A$
Assertion	lsatcmp	$⊢ φ \to (T \subseteq U \leftrightarrow T = U)$

Proof

Step	Hyp	Ref	Expression
1		lsatcmp.a	$⊢ A = LSAtoms (W)$
2		lsatcmp.w	$⊢ φ \to W \in LVec$
3		lsatcmp.t	$⊢ φ \to T \in A$
4		lsatcmp.u	$⊢ φ \to U \in A$
5		lveclmod	$⊢ W \in LVec \to W \in LMod$
6	2 5	syl	$⊢ φ \to W \in LMod$
7		eqid	$⊢ {Base}_{W} = {Base}_{W}$
8		eqid	$⊢ LSpan (W) = LSpan (W)$
9		eqid	$⊢ 0_{W} = 0_{W}$
10	7 8 9 1	islsat	$⊢ W \in LMod \to (U \in A \leftrightarrow \exists v \in ({Base}_{W} ∖ \{0_{W}\}) U = LSpan (W) (\{v\}))$
11	6 10	syl	$⊢ φ \to (U \in A \leftrightarrow \exists v \in ({Base}_{W} ∖ \{0_{W}\}) U = LSpan (W) (\{v\}))$
12	4 11	mpbid	$⊢ φ \to \exists v \in ({Base}_{W} ∖ \{0_{W}\}) U = LSpan (W) (\{v\})$
13		eldifsn	$⊢ v \in ({Base}_{W} ∖ \{0_{W}\}) \leftrightarrow (v \in {Base}_{W} \land v \neq 0_{W})$
14	9 1 6 3	lsatn0	$⊢ φ \to T \neq \{0_{W}\}$
15	14	ad2antrr	$⊢ ((φ \land (v \in {Base}_{W} \land v \neq 0_{W})) \land T \subseteq LSpan (W) (\{v\})) \to T \neq \{0_{W}\}$
16	2	ad2antrr	$⊢ ((φ \land (v \in {Base}_{W} \land v \neq 0_{W})) \land T \subseteq LSpan (W) (\{v\})) \to W \in LVec$
17		eqid	$⊢ LSubSp (W) = LSubSp (W)$
18	17 1 6 3	lsatlssel	$⊢ φ \to T \in LSubSp (W)$
19	18	ad2antrr	$⊢ ((φ \land (v \in {Base}_{W} \land v \neq 0_{W})) \land T \subseteq LSpan (W) (\{v\})) \to T \in LSubSp (W)$
20		simplrl	$⊢ ((φ \land (v \in {Base}_{W} \land v \neq 0_{W})) \land T \subseteq LSpan (W) (\{v\})) \to v \in {Base}_{W}$
21		simpr	$⊢ ((φ \land (v \in {Base}_{W} \land v \neq 0_{W})) \land T \subseteq LSpan (W) (\{v\})) \to T \subseteq LSpan (W) (\{v\})$
22	7 9 17 8	lspsnat	$⊢ ((W \in LVec \land T \in LSubSp (W) \land v \in {Base}_{W}) \land T \subseteq LSpan (W) (\{v\})) \to (T = LSpan (W) (\{v\}) \lor T = \{0_{W}\})$
23	16 19 20 21 22	syl31anc	$⊢ ((φ \land (v \in {Base}_{W} \land v \neq 0_{W})) \land T \subseteq LSpan (W) (\{v\})) \to (T = LSpan (W) (\{v\}) \lor T = \{0_{W}\})$
24	23	ord	$⊢ ((φ \land (v \in {Base}_{W} \land v \neq 0_{W})) \land T \subseteq LSpan (W) (\{v\})) \to (\neg T = LSpan (W) (\{v\}) \to T = \{0_{W}\})$
25	24	necon1ad	$⊢ ((φ \land (v \in {Base}_{W} \land v \neq 0_{W})) \land T \subseteq LSpan (W) (\{v\})) \to (T \neq \{0_{W}\} \to T = LSpan (W) (\{v\}))$
26	15 25	mpd	$⊢ ((φ \land (v \in {Base}_{W} \land v \neq 0_{W})) \land T \subseteq LSpan (W) (\{v\})) \to T = LSpan (W) (\{v\})$
27	26	ex	$⊢ (φ \land (v \in {Base}_{W} \land v \neq 0_{W})) \to (T \subseteq LSpan (W) (\{v\}) \to T = LSpan (W) (\{v\}))$
28		eqimss	$⊢ T = LSpan (W) (\{v\}) \to T \subseteq LSpan (W) (\{v\})$
29	27 28	impbid1	$⊢ (φ \land (v \in {Base}_{W} \land v \neq 0_{W})) \to (T \subseteq LSpan (W) (\{v\}) \leftrightarrow T = LSpan (W) (\{v\}))$
30	29	ex	$⊢ φ \to ((v \in {Base}_{W} \land v \neq 0_{W}) \to (T \subseteq LSpan (W) (\{v\}) \leftrightarrow T = LSpan (W) (\{v\})))$
31	13 30	biimtrid	$⊢ φ \to (v \in ({Base}_{W} ∖ \{0_{W}\}) \to (T \subseteq LSpan (W) (\{v\}) \leftrightarrow T = LSpan (W) (\{v\})))$
32		sseq2	$⊢ U = LSpan (W) (\{v\}) \to (T \subseteq U \leftrightarrow T \subseteq LSpan (W) (\{v\}))$
33		eqeq2	$⊢ U = LSpan (W) (\{v\}) \to (T = U \leftrightarrow T = LSpan (W) (\{v\}))$
34	32 33	bibi12d	$⊢ U = LSpan (W) (\{v\}) \to ((T \subseteq U \leftrightarrow T = U) \leftrightarrow (T \subseteq LSpan (W) (\{v\}) \leftrightarrow T = LSpan (W) (\{v\})))$
35	34	biimprcd	$⊢ (T \subseteq LSpan (W) (\{v\}) \leftrightarrow T = LSpan (W) (\{v\})) \to (U = LSpan (W) (\{v\}) \to (T \subseteq U \leftrightarrow T = U))$
36	31 35	syl6	$⊢ φ \to (v \in ({Base}_{W} ∖ \{0_{W}\}) \to (U = LSpan (W) (\{v\}) \to (T \subseteq U \leftrightarrow T = U)))$
37	36	rexlimdv	$⊢ φ \to (\exists v \in ({Base}_{W} ∖ \{0_{W}\}) U = LSpan (W) (\{v\}) \to (T \subseteq U \leftrightarrow T = U))$
38	12 37	mpd	$⊢ φ \to (T \subseteq U \leftrightarrow T = U)$

Metamath Proof Explorer

Theorem lsatcmp

Proof