islshpat

Description: Hyperplane properties expressed with subspace sum and an atom. TODO: can proof be shortened? Seems long for a simple variation of islshpsm . (Contributed by NM, 11-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		islshpat.v	$⊢ V = {Base}_{W}$
2		islshpat.s	$⊢ S = LSubSp (W)$
3		islshpat.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
4		islshpat.h	$⊢ H = LSHyp (W)$
5		islshpat.a	$⊢ A = LSAtoms (W)$
6		islshpat.w	$⊢ φ \to W \in LMod$
7		eqid	$⊢ LSpan (W) = LSpan (W)$
8	1 7 2 3 4 6	islshpsm	$⊢ φ \to (U \in H \leftrightarrow (U \in S \land U \neq V \land \exists v \in V U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V))$
9		df-3an	$⊢ (U \in S \land U \neq V \land \exists v \in V U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V) \leftrightarrow ((U \in S \land U \neq V) \land \exists v \in V U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V)$
10		r19.42v	$⊢ \exists v \in V ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V) \leftrightarrow ((U \in S \land U \neq V) \land \exists v \in V U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V)$
11	9 10	bitr4i	$⊢ (U \in S \land U \neq V \land \exists v \in V U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V) \leftrightarrow \exists v \in V ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V)$
12		df-rex	$⊢ \exists v \in V ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V) \leftrightarrow \exists v (v \in V \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V))$
13		simpr	$⊢ (((φ \land v \in V) \land (U \in S \land U \neq V)) \land v = 0_{W}) \to v = 0_{W}$
14	13	sneqd	$⊢ (((φ \land v \in V) \land (U \in S \land U \neq V)) \land v = 0_{W}) \to \{v\} = \{0_{W}\}$
15	14	fveq2d	$⊢ (((φ \land v \in V) \land (U \in S \land U \neq V)) \land v = 0_{W}) \to LSpan (W) (\{v\}) = LSpan (W) (\{0_{W}\})$
16	6	ad3antrrr	$⊢ (((φ \land v \in V) \land (U \in S \land U \neq V)) \land v = 0_{W}) \to W \in LMod$
17		eqid	$⊢ 0_{W} = 0_{W}$
18	17 7	lspsn0	$⊢ W \in LMod \to LSpan (W) (\{0_{W}\}) = \{0_{W}\}$
19	16 18	syl	$⊢ (((φ \land v \in V) \land (U \in S \land U \neq V)) \land v = 0_{W}) \to LSpan (W) (\{0_{W}\}) = \{0_{W}\}$
20	15 19	eqtrd	$⊢ (((φ \land v \in V) \land (U \in S \land U \neq V)) \land v = 0_{W}) \to LSpan (W) (\{v\}) = \{0_{W}\}$
21	20	oveq2d	$⊢ (((φ \land v \in V) \land (U \in S \land U \neq V)) \land v = 0_{W}) \to U \underset{˙}{\oplus} LSpan (W) (\{v\}) = U \underset{˙}{\oplus} \{0_{W}\}$
22		simplrl	$⊢ (((φ \land v \in V) \land (U \in S \land U \neq V)) \land v = 0_{W}) \to U \in S$
23	2	lsssubg	$⊢ (W \in LMod \land U \in S) \to U \in SubGrp (W)$
24	16 22 23	syl2anc	$⊢ (((φ \land v \in V) \land (U \in S \land U \neq V)) \land v = 0_{W}) \to U \in SubGrp (W)$
25	17 3	lsm01	$⊢ U \in SubGrp (W) \to U \underset{˙}{\oplus} \{0_{W}\} = U$
26	24 25	syl	$⊢ (((φ \land v \in V) \land (U \in S \land U \neq V)) \land v = 0_{W}) \to U \underset{˙}{\oplus} \{0_{W}\} = U$
27	21 26	eqtrd	$⊢ (((φ \land v \in V) \land (U \in S \land U \neq V)) \land v = 0_{W}) \to U \underset{˙}{\oplus} LSpan (W) (\{v\}) = U$
28		simplrr	$⊢ (((φ \land v \in V) \land (U \in S \land U \neq V)) \land v = 0_{W}) \to U \neq V$
29	27 28	eqnetrd	$⊢ (((φ \land v \in V) \land (U \in S \land U \neq V)) \land v = 0_{W}) \to U \underset{˙}{\oplus} LSpan (W) (\{v\}) \neq V$
30	29	ex	$⊢ ((φ \land v \in V) \land (U \in S \land U \neq V)) \to (v = 0_{W} \to U \underset{˙}{\oplus} LSpan (W) (\{v\}) \neq V)$
31	30	necon2d	$⊢ ((φ \land v \in V) \land (U \in S \land U \neq V)) \to (U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V \to v \neq 0_{W})$
32	31	pm4.71rd	$⊢ ((φ \land v \in V) \land (U \in S \land U \neq V)) \to (U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V \leftrightarrow (v \neq 0_{W} \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V))$
33	32	pm5.32da	$⊢ (φ \land v \in V) \to (((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V) \leftrightarrow ((U \in S \land U \neq V) \land (v \neq 0_{W} \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V)))$
34	33	pm5.32da	$⊢ φ \to ((v \in V \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V)) \leftrightarrow (v \in V \land ((U \in S \land U \neq V) \land (v \neq 0_{W} \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V))))$
35		eldifsn	$⊢ v \in (V ∖ \{0_{W}\}) \leftrightarrow (v \in V \land v \neq 0_{W})$
36	35	anbi1i	$⊢ (v \in (V ∖ \{0_{W}\}) \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V)) \leftrightarrow ((v \in V \land v \neq 0_{W}) \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V))$
37		anass	$⊢ ((v \in V \land v \neq 0_{W}) \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V)) \leftrightarrow (v \in V \land (v \neq 0_{W} \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V)))$
38		an12	$⊢ (v \neq 0_{W} \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V)) \leftrightarrow ((U \in S \land U \neq V) \land (v \neq 0_{W} \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V))$
39	38	anbi2i	$⊢ (v \in V \land (v \neq 0_{W} \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V))) \leftrightarrow (v \in V \land ((U \in S \land U \neq V) \land (v \neq 0_{W} \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V)))$
40	37 39	bitri	$⊢ ((v \in V \land v \neq 0_{W}) \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V)) \leftrightarrow (v \in V \land ((U \in S \land U \neq V) \land (v \neq 0_{W} \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V)))$
41	36 40	bitr2i	$⊢ (v \in V \land ((U \in S \land U \neq V) \land (v \neq 0_{W} \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V))) \leftrightarrow (v \in (V ∖ \{0_{W}\}) \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V))$
42	34 41	syl6bb	$⊢ φ \to ((v \in V \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V)) \leftrightarrow (v \in (V ∖ \{0_{W}\}) \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V)))$
43	42	exbidv	$⊢ φ \to (\exists v (v \in V \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V)) \leftrightarrow \exists v (v \in (V ∖ \{0_{W}\}) \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V)))$
44	12 43	syl5bb	$⊢ φ \to (\exists v \in V ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V) \leftrightarrow \exists v (v \in (V ∖ \{0_{W}\}) \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V)))$
45		fvex	$⊢ LSpan (W) (\{v\}) \in V$
46	45	rexcom4b	$⊢ \exists q \exists v \in (V ∖ \{0_{W}\}) (((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V) \land q = LSpan (W) (\{v\})) \leftrightarrow \exists v \in (V ∖ \{0_{W}\}) ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V)$
47		df-rex	$⊢ \exists v \in (V ∖ \{0_{W}\}) ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V) \leftrightarrow \exists v (v \in (V ∖ \{0_{W}\}) \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V))$
48	46 47	bitr2i	$⊢ \exists v (v \in (V ∖ \{0_{W}\}) \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V)) \leftrightarrow \exists q \exists v \in (V ∖ \{0_{W}\}) (((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V) \land q = LSpan (W) (\{v\}))$
49		ancom	$⊢ (((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V) \land q = LSpan (W) (\{v\})) \leftrightarrow (q = LSpan (W) (\{v\}) \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V))$
50	49	rexbii	$⊢ \exists v \in (V ∖ \{0_{W}\}) (((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V) \land q = LSpan (W) (\{v\})) \leftrightarrow \exists v \in (V ∖ \{0_{W}\}) (q = LSpan (W) (\{v\}) \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V))$
51	50	exbii	$⊢ \exists q \exists v \in (V ∖ \{0_{W}\}) (((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V) \land q = LSpan (W) (\{v\})) \leftrightarrow \exists q \exists v \in (V ∖ \{0_{W}\}) (q = LSpan (W) (\{v\}) \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V))$
52	48 51	bitri	$⊢ \exists v (v \in (V ∖ \{0_{W}\}) \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V)) \leftrightarrow \exists q \exists v \in (V ∖ \{0_{W}\}) (q = LSpan (W) (\{v\}) \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V))$
53	44 52	syl6bb	$⊢ φ \to (\exists v \in V ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V) \leftrightarrow \exists q \exists v \in (V ∖ \{0_{W}\}) (q = LSpan (W) (\{v\}) \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V)))$
54		r19.41v	$⊢ \exists v \in (V ∖ \{0_{W}\}) (q = LSpan (W) (\{v\}) \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} q = V)) \leftrightarrow (\exists v \in (V ∖ \{0_{W}\}) q = LSpan (W) (\{v\}) \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} q = V))$
55		oveq2	$⊢ q = LSpan (W) (\{v\}) \to U \underset{˙}{\oplus} q = U \underset{˙}{\oplus} LSpan (W) (\{v\})$
56	55	eqeq1d	$⊢ q = LSpan (W) (\{v\}) \to (U \underset{˙}{\oplus} q = V \leftrightarrow U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V)$
57	56	anbi2d	$⊢ q = LSpan (W) (\{v\}) \to (((U \in S \land U \neq V) \land U \underset{˙}{\oplus} q = V) \leftrightarrow ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V))$
58	57	pm5.32i	$⊢ (q = LSpan (W) (\{v\}) \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} q = V)) \leftrightarrow (q = LSpan (W) (\{v\}) \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V))$
59	58	rexbii	$⊢ \exists v \in (V ∖ \{0_{W}\}) (q = LSpan (W) (\{v\}) \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} q = V)) \leftrightarrow \exists v \in (V ∖ \{0_{W}\}) (q = LSpan (W) (\{v\}) \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V))$
60	54 59	bitr3i	$⊢ (\exists v \in (V ∖ \{0_{W}\}) q = LSpan (W) (\{v\}) \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} q = V)) \leftrightarrow \exists v \in (V ∖ \{0_{W}\}) (q = LSpan (W) (\{v\}) \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V))$
61	60	exbii	$⊢ \exists q (\exists v \in (V ∖ \{0_{W}\}) q = LSpan (W) (\{v\}) \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} q = V)) \leftrightarrow \exists q \exists v \in (V ∖ \{0_{W}\}) (q = LSpan (W) (\{v\}) \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V))$
62	53 61	syl6bbr	$⊢ φ \to (\exists v \in V ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V) \leftrightarrow \exists q (\exists v \in (V ∖ \{0_{W}\}) q = LSpan (W) (\{v\}) \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} q = V)))$
63	1 7 17 5	islsat	$⊢ W \in LMod \to (q \in A \leftrightarrow \exists v \in (V ∖ \{0_{W}\}) q = LSpan (W) (\{v\}))$
64	6 63	syl	$⊢ φ \to (q \in A \leftrightarrow \exists v \in (V ∖ \{0_{W}\}) q = LSpan (W) (\{v\}))$
65	64	anbi1d	$⊢ φ \to ((q \in A \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} q = V)) \leftrightarrow (\exists v \in (V ∖ \{0_{W}\}) q = LSpan (W) (\{v\}) \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} q = V)))$
66	65	exbidv	$⊢ φ \to (\exists q (q \in A \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} q = V)) \leftrightarrow \exists q (\exists v \in (V ∖ \{0_{W}\}) q = LSpan (W) (\{v\}) \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} q = V)))$
67	62 66	bitr4d	$⊢ φ \to (\exists v \in V ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V) \leftrightarrow \exists q (q \in A \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} q = V)))$
68	11 67	syl5bb	$⊢ φ \to ((U \in S \land U \neq V \land \exists v \in V U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V) \leftrightarrow \exists q (q \in A \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} q = V)))$
69		df-3an	$⊢ (U \in S \land U \neq V \land \exists q \in A U \underset{˙}{\oplus} q = V) \leftrightarrow ((U \in S \land U \neq V) \land \exists q \in A U \underset{˙}{\oplus} q = V)$
70		r19.42v	$⊢ \exists q \in A ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} q = V) \leftrightarrow ((U \in S \land U \neq V) \land \exists q \in A U \underset{˙}{\oplus} q = V)$
71		df-rex	$⊢ \exists q \in A ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} q = V) \leftrightarrow \exists q (q \in A \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} q = V))$
72	70 71	bitr3i	$⊢ ((U \in S \land U \neq V) \land \exists q \in A U \underset{˙}{\oplus} q = V) \leftrightarrow \exists q (q \in A \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} q = V))$
73	69 72	bitr2i	$⊢ \exists q (q \in A \land ((U \in S \land U \neq V) \land U \underset{˙}{\oplus} q = V)) \leftrightarrow (U \in S \land U \neq V \land \exists q \in A U \underset{˙}{\oplus} q = V)$
74	68 73	syl6bb	$⊢ φ \to ((U \in S \land U \neq V \land \exists v \in V U \underset{˙}{\oplus} LSpan (W) (\{v\}) = V) \leftrightarrow (U \in S \land U \neq V \land \exists q \in A U \underset{˙}{\oplus} q = V))$
75	8 74	bitrd	$⊢ φ \to (U \in H \leftrightarrow (U \in S \land U \neq V \land \exists q \in A U \underset{˙}{\oplus} q = V))$

Metamath Proof Explorer

Theorem islshpat

Proof