dochsatshp

Description: The orthocomplement of a subspace atom is a hyperplane. (Contributed by NM, 27-Jul-2014) (Revised by Mario Carneiro, 1-Oct-2014)

	Ref	Expression
Hypotheses	dochsatshp.h	$⊢ H = LHyp (K)$
	dochsatshp.u	$⊢ U = DVecH (K) (W)$
	dochsatshp.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	dochsatshp.a	$⊢ A = LSAtoms (U)$
	dochsatshp.y	$⊢ Y = LSHyp (U)$
	dochsatshp.k	$⊢ φ \to (K \in HL \land W \in H)$
	dochsatshp.q	$⊢ φ \to Q \in A$
Assertion	dochsatshp	$⊢ φ \to \underset{˙}{⊥} (Q) \in Y$

Proof

Step	Hyp	Ref	Expression
1		dochsatshp.h	$⊢ H = LHyp (K)$
2		dochsatshp.u	$⊢ U = DVecH (K) (W)$
3		dochsatshp.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
4		dochsatshp.a	$⊢ A = LSAtoms (U)$
5		dochsatshp.y	$⊢ Y = LSHyp (U)$
6		dochsatshp.k	$⊢ φ \to (K \in HL \land W \in H)$
7		dochsatshp.q	$⊢ φ \to Q \in A$
8		eqid	$⊢ {Base}_{U} = {Base}_{U}$
9	1 2 6	dvhlmod	$⊢ φ \to U \in LMod$
10	8 4 9 7	lsatssv	$⊢ φ \to Q \subseteq {Base}_{U}$
11		eqid	$⊢ LSubSp (U) = LSubSp (U)$
12	1 2 8 11 3	dochlss	$⊢ ((K \in HL \land W \in H) \land Q \subseteq {Base}_{U}) \to \underset{˙}{⊥} (Q) \in LSubSp (U)$
13	6 10 12	syl2anc	$⊢ φ \to \underset{˙}{⊥} (Q) \in LSubSp (U)$
14		eqid	$⊢ 0_{U} = 0_{U}$
15	14 4 9 7	lsatn0	$⊢ φ \to Q \neq \{0_{U}\}$
16	1 2 3 8 14	doch0	$⊢ (K \in HL \land W \in H) \to \underset{˙}{⊥} (\{0_{U}\}) = {Base}_{U}$
17	6 16	syl	$⊢ φ \to \underset{˙}{⊥} (\{0_{U}\}) = {Base}_{U}$
18	17	eqeq2d	$⊢ φ \to (\underset{˙}{⊥} (Q) = \underset{˙}{⊥} (\{0_{U}\}) \leftrightarrow \underset{˙}{⊥} (Q) = {Base}_{U})$
19		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
20	1 2 19 4	dih1dimat	$⊢ ((K \in HL \land W \in H) \land Q \in A) \to Q \in ran DIsoH (K) (W)$
21	6 7 20	syl2anc	$⊢ φ \to Q \in ran DIsoH (K) (W)$
22	1 19 2 14	dih0rn	$⊢ (K \in HL \land W \in H) \to \{0_{U}\} \in ran DIsoH (K) (W)$
23	6 22	syl	$⊢ φ \to \{0_{U}\} \in ran DIsoH (K) (W)$
24	1 19 3 6 21 23	doch11	$⊢ φ \to (\underset{˙}{⊥} (Q) = \underset{˙}{⊥} (\{0_{U}\}) \leftrightarrow Q = \{0_{U}\})$
25	18 24	bitr3d	$⊢ φ \to (\underset{˙}{⊥} (Q) = {Base}_{U} \leftrightarrow Q = \{0_{U}\})$
26	25	necon3bid	$⊢ φ \to (\underset{˙}{⊥} (Q) \neq {Base}_{U} \leftrightarrow Q \neq \{0_{U}\})$
27	15 26	mpbird	$⊢ φ \to \underset{˙}{⊥} (Q) \neq {Base}_{U}$
28		eqid	$⊢ LSpan (U) = LSpan (U)$
29	8 28 14 4	islsat	$⊢ U \in LMod \to (Q \in A \leftrightarrow \exists v \in ({Base}_{U} ∖ \{0_{U}\}) Q = LSpan (U) (\{v\}))$
30	9 29	syl	$⊢ φ \to (Q \in A \leftrightarrow \exists v \in ({Base}_{U} ∖ \{0_{U}\}) Q = LSpan (U) (\{v\}))$
31	7 30	mpbid	$⊢ φ \to \exists v \in ({Base}_{U} ∖ \{0_{U}\}) Q = LSpan (U) (\{v\})$
32		eldifi	$⊢ v \in ({Base}_{U} ∖ \{0_{U}\}) \to v \in {Base}_{U}$
33	32	adantr	$⊢ (v \in ({Base}_{U} ∖ \{0_{U}\}) \land Q = LSpan (U) (\{v\})) \to v \in {Base}_{U}$
34	33	a1i	$⊢ φ \to ((v \in ({Base}_{U} ∖ \{0_{U}\}) \land Q = LSpan (U) (\{v\})) \to v \in {Base}_{U})$
35	11 28	lspid	$⊢ (U \in LMod \land \underset{˙}{⊥} (Q) \in LSubSp (U)) \to LSpan (U) (\underset{˙}{⊥} (Q)) = \underset{˙}{⊥} (Q)$
36	9 13 35	syl2anc	$⊢ φ \to LSpan (U) (\underset{˙}{⊥} (Q)) = \underset{˙}{⊥} (Q)$
37	36	uneq1d	$⊢ φ \to LSpan (U) (\underset{˙}{⊥} (Q)) \cup LSpan (U) (\{v\}) = \underset{˙}{⊥} (Q) \cup LSpan (U) (\{v\})$
38	37	fveq2d	$⊢ φ \to LSpan (U) (LSpan (U) (\underset{˙}{⊥} (Q)) \cup LSpan (U) (\{v\})) = LSpan (U) (\underset{˙}{⊥} (Q) \cup LSpan (U) (\{v\}))$
39	38	adantr	$⊢ (φ \land (v \in ({Base}_{U} ∖ \{0_{U}\}) \land Q = LSpan (U) (\{v\}))) \to LSpan (U) (LSpan (U) (\underset{˙}{⊥} (Q)) \cup LSpan (U) (\{v\})) = LSpan (U) (\underset{˙}{⊥} (Q) \cup LSpan (U) (\{v\}))$
40	9	adantr	$⊢ (φ \land (v \in ({Base}_{U} ∖ \{0_{U}\}) \land Q = LSpan (U) (\{v\}))) \to U \in LMod$
41	8 11	lssss	$⊢ \underset{˙}{⊥} (Q) \in LSubSp (U) \to \underset{˙}{⊥} (Q) \subseteq {Base}_{U}$
42	13 41	syl	$⊢ φ \to \underset{˙}{⊥} (Q) \subseteq {Base}_{U}$
43	42	adantr	$⊢ (φ \land (v \in ({Base}_{U} ∖ \{0_{U}\}) \land Q = LSpan (U) (\{v\}))) \to \underset{˙}{⊥} (Q) \subseteq {Base}_{U}$
44	32	snssd	$⊢ v \in ({Base}_{U} ∖ \{0_{U}\}) \to \{v\} \subseteq {Base}_{U}$
45	44	adantr	$⊢ (v \in ({Base}_{U} ∖ \{0_{U}\}) \land Q = LSpan (U) (\{v\})) \to \{v\} \subseteq {Base}_{U}$
46	45	adantl	$⊢ (φ \land (v \in ({Base}_{U} ∖ \{0_{U}\}) \land Q = LSpan (U) (\{v\}))) \to \{v\} \subseteq {Base}_{U}$
47	8 28	lspun	$⊢ (U \in LMod \land \underset{˙}{⊥} (Q) \subseteq {Base}_{U} \land \{v\} \subseteq {Base}_{U}) \to LSpan (U) (\underset{˙}{⊥} (Q) \cup \{v\}) = LSpan (U) (LSpan (U) (\underset{˙}{⊥} (Q)) \cup LSpan (U) (\{v\}))$
48	40 43 46 47	syl3anc	$⊢ (φ \land (v \in ({Base}_{U} ∖ \{0_{U}\}) \land Q = LSpan (U) (\{v\}))) \to LSpan (U) (\underset{˙}{⊥} (Q) \cup \{v\}) = LSpan (U) (LSpan (U) (\underset{˙}{⊥} (Q)) \cup LSpan (U) (\{v\}))$
49		uneq2	$⊢ Q = LSpan (U) (\{v\}) \to \underset{˙}{⊥} (Q) \cup Q = \underset{˙}{⊥} (Q) \cup LSpan (U) (\{v\})$
50	49	fveq2d	$⊢ Q = LSpan (U) (\{v\}) \to LSpan (U) (\underset{˙}{⊥} (Q) \cup Q) = LSpan (U) (\underset{˙}{⊥} (Q) \cup LSpan (U) (\{v\}))$
51	50	adantl	$⊢ (v \in ({Base}_{U} ∖ \{0_{U}\}) \land Q = LSpan (U) (\{v\})) \to LSpan (U) (\underset{˙}{⊥} (Q) \cup Q) = LSpan (U) (\underset{˙}{⊥} (Q) \cup LSpan (U) (\{v\}))$
52	51	adantl	$⊢ (φ \land (v \in ({Base}_{U} ∖ \{0_{U}\}) \land Q = LSpan (U) (\{v\}))) \to LSpan (U) (\underset{˙}{⊥} (Q) \cup Q) = LSpan (U) (\underset{˙}{⊥} (Q) \cup LSpan (U) (\{v\}))$
53	39 48 52	3eqtr4d	$⊢ (φ \land (v \in ({Base}_{U} ∖ \{0_{U}\}) \land Q = LSpan (U) (\{v\}))) \to LSpan (U) (\underset{˙}{⊥} (Q) \cup \{v\}) = LSpan (U) (\underset{˙}{⊥} (Q) \cup Q)$
54		eqid	$⊢ joinH (K) (W) = joinH (K) (W)$
55		eqid	$⊢ LSSum (U) = LSSum (U)$
56	1 19 2 8 3	dochcl	$⊢ ((K \in HL \land W \in H) \land Q \subseteq {Base}_{U}) \to \underset{˙}{⊥} (Q) \in ran DIsoH (K) (W)$
57	6 10 56	syl2anc	$⊢ φ \to \underset{˙}{⊥} (Q) \in ran DIsoH (K) (W)$
58	1 19 54 2 55 4 6 57 7	dihjat2	$⊢ φ \to \underset{˙}{⊥} (Q) joinH (K) (W) Q = \underset{˙}{⊥} (Q) LSSum (U) Q$
59	1 2 8 54 6 42 10	djhcom	$⊢ φ \to \underset{˙}{⊥} (Q) joinH (K) (W) Q = Q joinH (K) (W) \underset{˙}{⊥} (Q)$
60	11 4 9 7	lsatlssel	$⊢ φ \to Q \in LSubSp (U)$
61	11 28 55	lsmsp	$⊢ (U \in LMod \land \underset{˙}{⊥} (Q) \in LSubSp (U) \land Q \in LSubSp (U)) \to \underset{˙}{⊥} (Q) LSSum (U) Q = LSpan (U) (\underset{˙}{⊥} (Q) \cup Q)$
62	9 13 60 61	syl3anc	$⊢ φ \to \underset{˙}{⊥} (Q) LSSum (U) Q = LSpan (U) (\underset{˙}{⊥} (Q) \cup Q)$
63	58 59 62	3eqtr3rd	$⊢ φ \to LSpan (U) (\underset{˙}{⊥} (Q) \cup Q) = Q joinH (K) (W) \underset{˙}{⊥} (Q)$
64	1 2 8 3 54	djhexmid	$⊢ ((K \in HL \land W \in H) \land Q \subseteq {Base}_{U}) \to Q joinH (K) (W) \underset{˙}{⊥} (Q) = {Base}_{U}$
65	6 10 64	syl2anc	$⊢ φ \to Q joinH (K) (W) \underset{˙}{⊥} (Q) = {Base}_{U}$
66	63 65	eqtrd	$⊢ φ \to LSpan (U) (\underset{˙}{⊥} (Q) \cup Q) = {Base}_{U}$
67	66	adantr	$⊢ (φ \land (v \in ({Base}_{U} ∖ \{0_{U}\}) \land Q = LSpan (U) (\{v\}))) \to LSpan (U) (\underset{˙}{⊥} (Q) \cup Q) = {Base}_{U}$
68	53 67	eqtrd	$⊢ (φ \land (v \in ({Base}_{U} ∖ \{0_{U}\}) \land Q = LSpan (U) (\{v\}))) \to LSpan (U) (\underset{˙}{⊥} (Q) \cup \{v\}) = {Base}_{U}$
69	68	ex	$⊢ φ \to ((v \in ({Base}_{U} ∖ \{0_{U}\}) \land Q = LSpan (U) (\{v\})) \to LSpan (U) (\underset{˙}{⊥} (Q) \cup \{v\}) = {Base}_{U})$
70	34 69	jcad	$⊢ φ \to ((v \in ({Base}_{U} ∖ \{0_{U}\}) \land Q = LSpan (U) (\{v\})) \to (v \in {Base}_{U} \land LSpan (U) (\underset{˙}{⊥} (Q) \cup \{v\}) = {Base}_{U}))$
71	70	reximdv2	$⊢ φ \to (\exists v \in ({Base}_{U} ∖ \{0_{U}\}) Q = LSpan (U) (\{v\}) \to \exists v \in {Base}_{U} LSpan (U) (\underset{˙}{⊥} (Q) \cup \{v\}) = {Base}_{U})$
72	31 71	mpd	$⊢ φ \to \exists v \in {Base}_{U} LSpan (U) (\underset{˙}{⊥} (Q) \cup \{v\}) = {Base}_{U}$
73	1 2 6	dvhlvec	$⊢ φ \to U \in LVec$
74	8 28 11 5	islshp	$⊢ U \in LVec \to (\underset{˙}{⊥} (Q) \in Y \leftrightarrow (\underset{˙}{⊥} (Q) \in LSubSp (U) \land \underset{˙}{⊥} (Q) \neq {Base}_{U} \land \exists v \in {Base}_{U} LSpan (U) (\underset{˙}{⊥} (Q) \cup \{v\}) = {Base}_{U}))$
75	73 74	syl	$⊢ φ \to (\underset{˙}{⊥} (Q) \in Y \leftrightarrow (\underset{˙}{⊥} (Q) \in LSubSp (U) \land \underset{˙}{⊥} (Q) \neq {Base}_{U} \land \exists v \in {Base}_{U} LSpan (U) (\underset{˙}{⊥} (Q) \cup \{v\}) = {Base}_{U}))$
76	13 27 72 75	mpbir3and	$⊢ φ \to \underset{˙}{⊥} (Q) \in Y$

Metamath Proof Explorer

Theorem dochsatshp

Proof