islshpcv

Description: Hyperplane properties expressed with covers relation. (Contributed by NM, 11-Jan-2015)

	Ref	Expression
Hypotheses	islshpcv.v	$⊢ V = {Base}_{W}$
	islshpcv.s	$⊢ S = LSubSp (W)$
	islshpcv.h	$⊢ H = LSHyp (W)$
	islshpcv.c	$⊢ C = ⋖_{L} (W)$
	islshpcv.w	$⊢ φ \to W \in LVec$
Assertion	islshpcv	$⊢ φ \to (U \in H \leftrightarrow (U \in S \land U C V))$

Proof

Step	Hyp	Ref	Expression
1		islshpcv.v	$⊢ V = {Base}_{W}$
2		islshpcv.s	$⊢ S = LSubSp (W)$
3		islshpcv.h	$⊢ H = LSHyp (W)$
4		islshpcv.c	$⊢ C = ⋖_{L} (W)$
5		islshpcv.w	$⊢ φ \to W \in LVec$
6		eqid	$⊢ LSSum (W) = LSSum (W)$
7		eqid	$⊢ LSAtoms (W) = LSAtoms (W)$
8		lveclmod	$⊢ W \in LVec \to W \in LMod$
9	5 8	syl	$⊢ φ \to W \in LMod$
10	1 2 6 3 7 9	islshpat	$⊢ φ \to (U \in H \leftrightarrow (U \in S \land U \neq V \land \exists q \in LSAtoms (W) U LSSum (W) q = V))$
11		simp12	$⊢ ((φ \land U \in S \land U \neq V) \land q \in LSAtoms (W) \land U LSSum (W) q = V) \to U \in S$
12	1 2	lssss	$⊢ U \in S \to U \subseteq V$
13	11 12	syl	$⊢ ((φ \land U \in S \land U \neq V) \land q \in LSAtoms (W) \land U LSSum (W) q = V) \to U \subseteq V$
14		simp13	$⊢ ((φ \land U \in S \land U \neq V) \land q \in LSAtoms (W) \land U LSSum (W) q = V) \to U \neq V$
15		df-pss	$⊢ U \subset V \leftrightarrow (U \subseteq V \land U \neq V)$
16	13 14 15	sylanbrc	$⊢ ((φ \land U \in S \land U \neq V) \land q \in LSAtoms (W) \land U LSSum (W) q = V) \to U \subset V$
17		psseq2	$⊢ U LSSum (W) q = V \to (U \subset U LSSum (W) q \leftrightarrow U \subset V)$
18	17	3ad2ant3	$⊢ ((φ \land U \in S \land U \neq V) \land q \in LSAtoms (W) \land U LSSum (W) q = V) \to (U \subset U LSSum (W) q \leftrightarrow U \subset V)$
19	16 18	mpbird	$⊢ ((φ \land U \in S \land U \neq V) \land q \in LSAtoms (W) \land U LSSum (W) q = V) \to U \subset U LSSum (W) q$
20	5	3ad2ant1	$⊢ (φ \land U \in S \land U \neq V) \to W \in LVec$
21	20	3ad2ant1	$⊢ ((φ \land U \in S \land U \neq V) \land q \in LSAtoms (W) \land U LSSum (W) q = V) \to W \in LVec$
22		simp2	$⊢ ((φ \land U \in S \land U \neq V) \land q \in LSAtoms (W) \land U LSSum (W) q = V) \to q \in LSAtoms (W)$
23	2 6 7 4 21 11 22	lcv2	$⊢ ((φ \land U \in S \land U \neq V) \land q \in LSAtoms (W) \land U LSSum (W) q = V) \to (U \subset U LSSum (W) q \leftrightarrow U C (U LSSum (W) q))$
24	19 23	mpbid	$⊢ ((φ \land U \in S \land U \neq V) \land q \in LSAtoms (W) \land U LSSum (W) q = V) \to U C (U LSSum (W) q)$
25		simp3	$⊢ ((φ \land U \in S \land U \neq V) \land q \in LSAtoms (W) \land U LSSum (W) q = V) \to U LSSum (W) q = V$
26	24 25	breqtrd	$⊢ ((φ \land U \in S \land U \neq V) \land q \in LSAtoms (W) \land U LSSum (W) q = V) \to U C V$
27	11 26	jca	$⊢ ((φ \land U \in S \land U \neq V) \land q \in LSAtoms (W) \land U LSSum (W) q = V) \to (U \in S \land U C V)$
28	27	rexlimdv3a	$⊢ (φ \land U \in S \land U \neq V) \to (\exists q \in LSAtoms (W) U LSSum (W) q = V \to (U \in S \land U C V))$
29	28	3exp	$⊢ φ \to (U \in S \to (U \neq V \to (\exists q \in LSAtoms (W) U LSSum (W) q = V \to (U \in S \land U C V))))$
30	29	3impd	$⊢ φ \to ((U \in S \land U \neq V \land \exists q \in LSAtoms (W) U LSSum (W) q = V) \to (U \in S \land U C V))$
31		simprl	$⊢ (φ \land (U \in S \land U C V)) \to U \in S$
32	5	adantr	$⊢ (φ \land (U \in S \land U C V)) \to W \in LVec$
33	9	adantr	$⊢ (φ \land (U \in S \land U C V)) \to W \in LMod$
34	1 2	lss1	$⊢ W \in LMod \to V \in S$
35	33 34	syl	$⊢ (φ \land (U \in S \land U C V)) \to V \in S$
36		simprr	$⊢ (φ \land (U \in S \land U C V)) \to U C V$
37	2 4 32 31 35 36	lcvpss	$⊢ (φ \land (U \in S \land U C V)) \to U \subset V$
38	37	pssned	$⊢ (φ \land (U \in S \land U C V)) \to U \neq V$
39	2 6 7 4 33 31 35 36	lcvat	$⊢ (φ \land (U \in S \land U C V)) \to \exists q \in LSAtoms (W) U LSSum (W) q = V$
40	31 38 39	3jca	$⊢ (φ \land (U \in S \land U C V)) \to (U \in S \land U \neq V \land \exists q \in LSAtoms (W) U LSSum (W) q = V)$
41	40	ex	$⊢ φ \to ((U \in S \land U C V) \to (U \in S \land U \neq V \land \exists q \in LSAtoms (W) U LSSum (W) q = V))$
42	30 41	impbid	$⊢ φ \to ((U \in S \land U \neq V \land \exists q \in LSAtoms (W) U LSSum (W) q = V) \leftrightarrow (U \in S \land U C V))$
43	10 42	bitrd	$⊢ φ \to (U \in H \leftrightarrow (U \in S \land U C V))$

Metamath Proof Explorer

Theorem islshpcv

Proof