dvh2dimatN

Description: Given an atom, there exists another. (Contributed by NM, 25-Apr-2015) (New usage is discouraged.)

Step	Hyp	Ref	Expression
1		dvh4dimat.h	$⊢ H = LHyp (K)$
2		dvh4dimat.u	$⊢ U = DVecH (K) (W)$
3		dvh2dimat.a	$⊢ A = LSAtoms (U)$
4		dvh2dimat.k	$⊢ φ \to (K \in HL \land W \in H)$
5		dvh2dimat.p	$⊢ φ \to P \in A$
6		eqid	$⊢ LSSum (U) = LSSum (U)$
7	1 2 6 3 4 5 5	dvh3dimatN	$⊢ φ \to \exists s \in A \neg s \subseteq P LSSum (U) P$
8	1 2 4	dvhlmod	$⊢ φ \to U \in LMod$
9		eqid	$⊢ LSubSp (U) = LSubSp (U)$
10	9 3 8 5	lsatlssel	$⊢ φ \to P \in LSubSp (U)$
11	9	lsssubg	$⊢ (U \in LMod \land P \in LSubSp (U)) \to P \in SubGrp (U)$
12	8 10 11	syl2anc	$⊢ φ \to P \in SubGrp (U)$
13	6	lsmidm	$⊢ P \in SubGrp (U) \to P LSSum (U) P = P$
14	12 13	syl	$⊢ φ \to P LSSum (U) P = P$
15	14	sseq2d	$⊢ φ \to (s \subseteq P LSSum (U) P \leftrightarrow s \subseteq P)$
16	15	adantr	$⊢ (φ \land s \in A) \to (s \subseteq P LSSum (U) P \leftrightarrow s \subseteq P)$
17	1 2 4	dvhlvec	$⊢ φ \to U \in LVec$
18	17	adantr	$⊢ (φ \land s \in A) \to U \in LVec$
19		simpr	$⊢ (φ \land s \in A) \to s \in A$
20	5	adantr	$⊢ (φ \land s \in A) \to P \in A$
21	3 18 19 20	lsatcmp	$⊢ (φ \land s \in A) \to (s \subseteq P \leftrightarrow s = P)$
22	16 21	bitrd	$⊢ (φ \land s \in A) \to (s \subseteq P LSSum (U) P \leftrightarrow s = P)$
23	22	necon3bbid	$⊢ (φ \land s \in A) \to (\neg s \subseteq P LSSum (U) P \leftrightarrow s \neq P)$
24	23	rexbidva	$⊢ φ \to (\exists s \in A \neg s \subseteq P LSSum (U) P \leftrightarrow \exists s \in A s \neq P)$
25	7 24	mpbid	$⊢ φ \to \exists s \in A s \neq P$

Metamath Proof Explorer