lshpcmp

Description: If two hyperplanes are comparable, they are equal. (Contributed by NM, 9-Oct-2014)

	Ref	Expression
Hypotheses	lshpcmp.h	$⊢ H = LSHyp (W)$
	lshpcmp.w	$⊢ φ \to W \in LVec$
	lshpcmp.t	$⊢ φ \to T \in H$
	lshpcmp.u	$⊢ φ \to U \in H$
Assertion	lshpcmp	$⊢ φ \to (T \subseteq U \leftrightarrow T = U)$

Proof

Step	Hyp	Ref	Expression
1		lshpcmp.h	$⊢ H = LSHyp (W)$
2		lshpcmp.w	$⊢ φ \to W \in LVec$
3		lshpcmp.t	$⊢ φ \to T \in H$
4		lshpcmp.u	$⊢ φ \to U \in H$
5		eqid	$⊢ {Base}_{W} = {Base}_{W}$
6		lveclmod	$⊢ W \in LVec \to W \in LMod$
7	2 6	syl	$⊢ φ \to W \in LMod$
8	5 1 7 4	lshpne	$⊢ φ \to U \neq {Base}_{W}$
9		eqid	$⊢ LSubSp (W) = LSubSp (W)$
10	9 1 7 4	lshplss	$⊢ φ \to U \in LSubSp (W)$
11	5 9	lssss	$⊢ U \in LSubSp (W) \to U \subseteq {Base}_{W}$
12	10 11	syl	$⊢ φ \to U \subseteq {Base}_{W}$
13		eqid	$⊢ LSpan (W) = LSpan (W)$
14		eqid	$⊢ LSSum (W) = LSSum (W)$
15	5 13 9 14 1 7	islshpsm	$⊢ φ \to (T \in H \leftrightarrow (T \in LSubSp (W) \land T \neq {Base}_{W} \land \exists v \in {Base}_{W} T LSSum (W) LSpan (W) (\{v\}) = {Base}_{W}))$
16	3 15	mpbid	$⊢ φ \to (T \in LSubSp (W) \land T \neq {Base}_{W} \land \exists v \in {Base}_{W} T LSSum (W) LSpan (W) (\{v\}) = {Base}_{W})$
17	16	simp3d	$⊢ φ \to \exists v \in {Base}_{W} T LSSum (W) LSpan (W) (\{v\}) = {Base}_{W}$
18		id	$⊢ (φ \land v \in {Base}_{W}) \to (φ \land v \in {Base}_{W})$
19	18	adantrr	$⊢ (φ \land (v \in {Base}_{W} \land T LSSum (W) LSpan (W) (\{v\}) = {Base}_{W})) \to (φ \land v \in {Base}_{W})$
20	2	adantr	$⊢ (φ \land v \in {Base}_{W}) \to W \in LVec$
21	9 1 7 3	lshplss	$⊢ φ \to T \in LSubSp (W)$
22	21	adantr	$⊢ (φ \land v \in {Base}_{W}) \to T \in LSubSp (W)$
23	10	adantr	$⊢ (φ \land v \in {Base}_{W}) \to U \in LSubSp (W)$
24		simpr	$⊢ (φ \land v \in {Base}_{W}) \to v \in {Base}_{W}$
25	5 9 13 14 20 22 23 24	lsmcv	$⊢ ((φ \land v \in {Base}_{W}) \land T \subset U \land U \subseteq T LSSum (W) LSpan (W) (\{v\})) \to U = T LSSum (W) LSpan (W) (\{v\})$
26	19 25	syl3an1	$⊢ ((φ \land (v \in {Base}_{W} \land T LSSum (W) LSpan (W) (\{v\}) = {Base}_{W})) \land T \subset U \land U \subseteq T LSSum (W) LSpan (W) (\{v\})) \to U = T LSSum (W) LSpan (W) (\{v\})$
27	26	3expia	$⊢ ((φ \land (v \in {Base}_{W} \land T LSSum (W) LSpan (W) (\{v\}) = {Base}_{W})) \land T \subset U) \to (U \subseteq T LSSum (W) LSpan (W) (\{v\}) \to U = T LSSum (W) LSpan (W) (\{v\}))$
28		simplrr	$⊢ ((φ \land (v \in {Base}_{W} \land T LSSum (W) LSpan (W) (\{v\}) = {Base}_{W})) \land T \subset U) \to T LSSum (W) LSpan (W) (\{v\}) = {Base}_{W}$
29	28	sseq2d	$⊢ ((φ \land (v \in {Base}_{W} \land T LSSum (W) LSpan (W) (\{v\}) = {Base}_{W})) \land T \subset U) \to (U \subseteq T LSSum (W) LSpan (W) (\{v\}) \leftrightarrow U \subseteq {Base}_{W})$
30	28	eqeq2d	$⊢ ((φ \land (v \in {Base}_{W} \land T LSSum (W) LSpan (W) (\{v\}) = {Base}_{W})) \land T \subset U) \to (U = T LSSum (W) LSpan (W) (\{v\}) \leftrightarrow U = {Base}_{W})$
31	27 29 30	3imtr3d	$⊢ ((φ \land (v \in {Base}_{W} \land T LSSum (W) LSpan (W) (\{v\}) = {Base}_{W})) \land T \subset U) \to (U \subseteq {Base}_{W} \to U = {Base}_{W})$
32	31	exp42	$⊢ φ \to (v \in {Base}_{W} \to (T LSSum (W) LSpan (W) (\{v\}) = {Base}_{W} \to (T \subset U \to (U \subseteq {Base}_{W} \to U = {Base}_{W}))))$
33	32	rexlimdv	$⊢ φ \to (\exists v \in {Base}_{W} T LSSum (W) LSpan (W) (\{v\}) = {Base}_{W} \to (T \subset U \to (U \subseteq {Base}_{W} \to U = {Base}_{W})))$
34	17 33	mpd	$⊢ φ \to (T \subset U \to (U \subseteq {Base}_{W} \to U = {Base}_{W}))$
35	12 34	mpid	$⊢ φ \to (T \subset U \to U = {Base}_{W})$
36	35	necon3ad	$⊢ φ \to (U \neq {Base}_{W} \to \neg T \subset U)$
37	8 36	mpd	$⊢ φ \to \neg T \subset U$
38		df-pss	$⊢ T \subset U \leftrightarrow (T \subseteq U \land T \neq U)$
39	38	simplbi2	$⊢ T \subseteq U \to (T \neq U \to T \subset U)$
40	39	necon1bd	$⊢ T \subseteq U \to (\neg T \subset U \to T = U)$
41	37 40	syl5com	$⊢ φ \to (T \subseteq U \to T = U)$
42		eqimss	$⊢ T = U \to T \subseteq U$
43	41 42	impbid1	$⊢ φ \to (T \subseteq U \leftrightarrow T = U)$

Metamath Proof Explorer

Theorem lshpcmp

Proof