islshpsm

Description: Hyperplane properties expressed with subspace sum. (Contributed by NM, 3-Jul-2014)

	Ref	Expression
Hypotheses	islshpsm.v	$⊢ V = {Base}_{W}$
	islshpsm.n	$⊢ N = LSpan (W)$
	islshpsm.s	$⊢ S = LSubSp (W)$
	islshpsm.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
	islshpsm.h	$⊢ H = LSHyp (W)$
	islshpsm.w	$⊢ φ \to W \in LMod$
Assertion	islshpsm	$⊢ φ \to (U \in H \leftrightarrow (U \in S \land U \neq V \land \exists v \in V U \underset{˙}{\oplus} N (\{v\}) = V))$

Proof

Step	Hyp	Ref	Expression
1		islshpsm.v	$⊢ V = {Base}_{W}$
2		islshpsm.n	$⊢ N = LSpan (W)$
3		islshpsm.s	$⊢ S = LSubSp (W)$
4		islshpsm.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
5		islshpsm.h	$⊢ H = LSHyp (W)$
6		islshpsm.w	$⊢ φ \to W \in LMod$
7	1 2 3 5	islshp	$⊢ W \in LMod \to (U \in H \leftrightarrow (U \in S \land U \neq V \land \exists v \in V N (U \cup \{v\}) = V))$
8	6 7	syl	$⊢ φ \to (U \in H \leftrightarrow (U \in S \land U \neq V \land \exists v \in V N (U \cup \{v\}) = V))$
9	6	ad2antrr	$⊢ ((φ \land (U \in S \land U \neq V)) \land v \in V) \to W \in LMod$
10		simplrl	$⊢ ((φ \land (U \in S \land U \neq V)) \land v \in V) \to U \in S$
11	3 2	lspid	$⊢ (W \in LMod \land U \in S) \to N (U) = U$
12	9 10 11	syl2anc	$⊢ ((φ \land (U \in S \land U \neq V)) \land v \in V) \to N (U) = U$
13	12	uneq1d	$⊢ ((φ \land (U \in S \land U \neq V)) \land v \in V) \to N (U) \cup N (\{v\}) = U \cup N (\{v\})$
14	13	fveq2d	$⊢ ((φ \land (U \in S \land U \neq V)) \land v \in V) \to N (N (U) \cup N (\{v\})) = N (U \cup N (\{v\}))$
15	1 3	lssss	$⊢ U \in S \to U \subseteq V$
16	10 15	syl	$⊢ ((φ \land (U \in S \land U \neq V)) \land v \in V) \to U \subseteq V$
17		snssi	$⊢ v \in V \to \{v\} \subseteq V$
18	17	adantl	$⊢ ((φ \land (U \in S \land U \neq V)) \land v \in V) \to \{v\} \subseteq V$
19	1 2	lspun	$⊢ (W \in LMod \land U \subseteq V \land \{v\} \subseteq V) \to N (U \cup \{v\}) = N (N (U) \cup N (\{v\}))$
20	9 16 18 19	syl3anc	$⊢ ((φ \land (U \in S \land U \neq V)) \land v \in V) \to N (U \cup \{v\}) = N (N (U) \cup N (\{v\}))$
21	1 3 2	lspcl	$⊢ (W \in LMod \land \{v\} \subseteq V) \to N (\{v\}) \in S$
22	9 18 21	syl2anc	$⊢ ((φ \land (U \in S \land U \neq V)) \land v \in V) \to N (\{v\}) \in S$
23	3 2 4	lsmsp	$⊢ (W \in LMod \land U \in S \land N (\{v\}) \in S) \to U \underset{˙}{\oplus} N (\{v\}) = N (U \cup N (\{v\}))$
24	9 10 22 23	syl3anc	$⊢ ((φ \land (U \in S \land U \neq V)) \land v \in V) \to U \underset{˙}{\oplus} N (\{v\}) = N (U \cup N (\{v\}))$
25	14 20 24	3eqtr4rd	$⊢ ((φ \land (U \in S \land U \neq V)) \land v \in V) \to U \underset{˙}{\oplus} N (\{v\}) = N (U \cup \{v\})$
26	25	eqeq1d	$⊢ ((φ \land (U \in S \land U \neq V)) \land v \in V) \to (U \underset{˙}{\oplus} N (\{v\}) = V \leftrightarrow N (U \cup \{v\}) = V)$
27	26	rexbidva	$⊢ (φ \land (U \in S \land U \neq V)) \to (\exists v \in V U \underset{˙}{\oplus} N (\{v\}) = V \leftrightarrow \exists v \in V N (U \cup \{v\}) = V)$
28	27	pm5.32da	$⊢ φ \to (((U \in S \land U \neq V) \land \exists v \in V U \underset{˙}{\oplus} N (\{v\}) = V) \leftrightarrow ((U \in S \land U \neq V) \land \exists v \in V N (U \cup \{v\}) = V))$
29	28	bicomd	$⊢ φ \to (((U \in S \land U \neq V) \land \exists v \in V N (U \cup \{v\}) = V) \leftrightarrow ((U \in S \land U \neq V) \land \exists v \in V U \underset{˙}{\oplus} N (\{v\}) = V))$
30		df-3an	$⊢ (U \in S \land U \neq V \land \exists v \in V N (U \cup \{v\}) = V) \leftrightarrow ((U \in S \land U \neq V) \land \exists v \in V N (U \cup \{v\}) = V)$
31		df-3an	$⊢ (U \in S \land U \neq V \land \exists v \in V U \underset{˙}{\oplus} N (\{v\}) = V) \leftrightarrow ((U \in S \land U \neq V) \land \exists v \in V U \underset{˙}{\oplus} N (\{v\}) = V)$
32	29 30 31	3bitr4g	$⊢ φ \to ((U \in S \land U \neq V \land \exists v \in V N (U \cup \{v\}) = V) \leftrightarrow (U \in S \land U \neq V \land \exists v \in V U \underset{˙}{\oplus} N (\{v\}) = V))$
33	8 32	bitrd	$⊢ φ \to (U \in H \leftrightarrow (U \in S \land U \neq V \land \exists v \in V U \underset{˙}{\oplus} N (\{v\}) = V))$

Metamath Proof Explorer

Theorem islshpsm

Proof