dochsatshpb

Description: The orthocomplement of a subspace atom is a hyperplane. (Contributed by NM, 29-Oct-2014)

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

Proof

Step	Hyp	Ref	Expression
1		dochsatshpb.h	$⊢ H = LHyp (K)$
2		dochsatshpb.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		dochsatshpb.u	$⊢ U = DVecH (K) (W)$
4		dochsatshpb.s	$⊢ S = LSubSp (U)$
5		dochsatshpb.a	$⊢ A = LSAtoms (U)$
6		dochsatshpb.y	$⊢ Y = LSHyp (U)$
7		dochsatshpb.k	$⊢ φ \to (K \in HL \land W \in H)$
8		dochsatshpb.q	$⊢ φ \to Q \in S$
9	7	adantr	$⊢ (φ \land Q \in A) \to (K \in HL \land W \in H)$
10		simpr	$⊢ (φ \land Q \in A) \to Q \in A$
11	1 3 2 5 6 9 10	dochsatshp	$⊢ (φ \land Q \in A) \to \underset{˙}{⊥} (Q) \in Y$
12		eqid	$⊢ {Base}_{U} = {Base}_{U}$
13	12 4	lssss	$⊢ Q \in S \to Q \subseteq {Base}_{U}$
14	8 13	syl	$⊢ φ \to Q \subseteq {Base}_{U}$
15		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
16	1 15 3 12 2	dochcl	$⊢ ((K \in HL \land W \in H) \land Q \subseteq {Base}_{U}) \to \underset{˙}{⊥} (Q) \in ran DIsoH (K) (W)$
17	7 14 16	syl2anc	$⊢ φ \to \underset{˙}{⊥} (Q) \in ran DIsoH (K) (W)$
18	1 15 2	dochoc	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (Q) \in ran DIsoH (K) (W)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (Q))) = \underset{˙}{⊥} (Q)$
19	7 17 18	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (Q))) = \underset{˙}{⊥} (Q)$
20	19	adantr	$⊢ (φ \land \underset{˙}{⊥} (Q) \in Y) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (Q))) = \underset{˙}{⊥} (Q)$
21	1 3 7	dvhlmod	$⊢ φ \to U \in LMod$
22	21	adantr	$⊢ (φ \land \underset{˙}{⊥} (Q) \in Y) \to U \in LMod$
23		simpr	$⊢ (φ \land \underset{˙}{⊥} (Q) \in Y) \to \underset{˙}{⊥} (Q) \in Y$
24	12 6 22 23	lshpne	$⊢ (φ \land \underset{˙}{⊥} (Q) \in Y) \to \underset{˙}{⊥} (Q) \neq {Base}_{U}$
25	20 24	eqnetrd	$⊢ (φ \land \underset{˙}{⊥} (Q) \in Y) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (Q))) \neq {Base}_{U}$
26		eqid	$⊢ 0_{U} = 0_{U}$
27	1 3 12 2	dochssv	$⊢ ((K \in HL \land W \in H) \land Q \subseteq {Base}_{U}) \to \underset{˙}{⊥} (Q) \subseteq {Base}_{U}$
28	7 14 27	syl2anc	$⊢ φ \to \underset{˙}{⊥} (Q) \subseteq {Base}_{U}$
29	1 2 3 12 26 7 28	dochn0nv	$⊢ φ \to (\underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \neq \{0_{U}\} \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (Q))) \neq {Base}_{U})$
30	29	adantr	$⊢ (φ \land \underset{˙}{⊥} (Q) \in Y) \to (\underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \neq \{0_{U}\} \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (Q))) \neq {Base}_{U})$
31	25 30	mpbird	$⊢ (φ \land \underset{˙}{⊥} (Q) \in Y) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \neq \{0_{U}\}$
32	1 3 12 4 2	dochlss	$⊢ ((K \in HL \land W \in H) \land Q \subseteq {Base}_{U}) \to \underset{˙}{⊥} (Q) \in S$
33	7 14 32	syl2anc	$⊢ φ \to \underset{˙}{⊥} (Q) \in S$
34	12 4	lssss	$⊢ \underset{˙}{⊥} (Q) \in S \to \underset{˙}{⊥} (Q) \subseteq {Base}_{U}$
35	33 34	syl	$⊢ φ \to \underset{˙}{⊥} (Q) \subseteq {Base}_{U}$
36	1 3 12 4 2	dochlss	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (Q) \subseteq {Base}_{U}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in S$
37	7 35 36	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in S$
38	37	adantr	$⊢ (φ \land \underset{˙}{⊥} (Q) \in Y) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in S$
39	26 4	lssne0	$⊢ \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in S \to (\underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \neq \{0_{U}\} \leftrightarrow \exists v \in \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) v \neq 0_{U})$
40	38 39	syl	$⊢ (φ \land \underset{˙}{⊥} (Q) \in Y) \to (\underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \neq \{0_{U}\} \leftrightarrow \exists v \in \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) v \neq 0_{U})$
41	31 40	mpbid	$⊢ (φ \land \underset{˙}{⊥} (Q) \in Y) \to \exists v \in \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) v \neq 0_{U}$
42	7	adantr	$⊢ (φ \land \underset{˙}{⊥} (Q) \in Y) \to (K \in HL \land W \in H)$
43	42	3ad2ant1	$⊢ ((φ \land \underset{˙}{⊥} (Q) \in Y) \land v \in \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \land v \neq 0_{U}) \to (K \in HL \land W \in H)$
44	17	adantr	$⊢ (φ \land \underset{˙}{⊥} (Q) \in Y) \to \underset{˙}{⊥} (Q) \in ran DIsoH (K) (W)$
45	44	3ad2ant1	$⊢ ((φ \land \underset{˙}{⊥} (Q) \in Y) \land v \in \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \land v \neq 0_{U}) \to \underset{˙}{⊥} (Q) \in ran DIsoH (K) (W)$
46	43 45 18	syl2anc	$⊢ ((φ \land \underset{˙}{⊥} (Q) \in Y) \land v \in \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \land v \neq 0_{U}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (Q))) = \underset{˙}{⊥} (Q)$
47		eqid	$⊢ LSpan (U) = LSpan (U)$
48	22	3ad2ant1	$⊢ ((φ \land \underset{˙}{⊥} (Q) \in Y) \land v \in \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \land v \neq 0_{U}) \to U \in LMod$
49	38	3ad2ant1	$⊢ ((φ \land \underset{˙}{⊥} (Q) \in Y) \land v \in \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \land v \neq 0_{U}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in S$
50		simp2	$⊢ ((φ \land \underset{˙}{⊥} (Q) \in Y) \land v \in \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \land v \neq 0_{U}) \to v \in \underset{˙}{⊥} (\underset{˙}{⊥} (Q))$
51	4 47 48 49 50	ellspsn5	$⊢ ((φ \land \underset{˙}{⊥} (Q) \in Y) \land v \in \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \land v \neq 0_{U}) \to LSpan (U) (\{v\}) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (Q))$
52	12 4	lssel	$⊢ (\underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in S \land v \in \underset{˙}{⊥} (\underset{˙}{⊥} (Q))) \to v \in {Base}_{U}$
53	49 50 52	syl2anc	$⊢ ((φ \land \underset{˙}{⊥} (Q) \in Y) \land v \in \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \land v \neq 0_{U}) \to v \in {Base}_{U}$
54	1 3 12 47 15	dihlsprn	$⊢ ((K \in HL \land W \in H) \land v \in {Base}_{U}) \to LSpan (U) (\{v\}) \in ran DIsoH (K) (W)$
55	43 53 54	syl2anc	$⊢ ((φ \land \underset{˙}{⊥} (Q) \in Y) \land v \in \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \land v \neq 0_{U}) \to LSpan (U) (\{v\}) \in ran DIsoH (K) (W)$
56	1 15 3 12 2	dochcl	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (Q) \subseteq {Base}_{U}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in ran DIsoH (K) (W)$
57	7 35 56	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in ran DIsoH (K) (W)$
58	57	adantr	$⊢ (φ \land \underset{˙}{⊥} (Q) \in Y) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in ran DIsoH (K) (W)$
59	58	3ad2ant1	$⊢ ((φ \land \underset{˙}{⊥} (Q) \in Y) \land v \in \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \land v \neq 0_{U}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in ran DIsoH (K) (W)$
60	1 15 2 43 55 59	dochord	$⊢ ((φ \land \underset{˙}{⊥} (Q) \in Y) \land v \in \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \land v \neq 0_{U}) \to (LSpan (U) (\{v\}) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (Q))) \subseteq \underset{˙}{⊥} (LSpan (U) (\{v\})))$
61	51 60	mpbid	$⊢ ((φ \land \underset{˙}{⊥} (Q) \in Y) \land v \in \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \land v \neq 0_{U}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (Q))) \subseteq \underset{˙}{⊥} (LSpan (U) (\{v\}))$
62	46 61	eqsstrrd	$⊢ ((φ \land \underset{˙}{⊥} (Q) \in Y) \land v \in \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \land v \neq 0_{U}) \to \underset{˙}{⊥} (Q) \subseteq \underset{˙}{⊥} (LSpan (U) (\{v\}))$
63	1 3 7	dvhlvec	$⊢ φ \to U \in LVec$
64	63	adantr	$⊢ (φ \land \underset{˙}{⊥} (Q) \in Y) \to U \in LVec$
65	64	3ad2ant1	$⊢ ((φ \land \underset{˙}{⊥} (Q) \in Y) \land v \in \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \land v \neq 0_{U}) \to U \in LVec$
66		simp1r	$⊢ ((φ \land \underset{˙}{⊥} (Q) \in Y) \land v \in \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \land v \neq 0_{U}) \to \underset{˙}{⊥} (Q) \in Y$
67		simp3	$⊢ ((φ \land \underset{˙}{⊥} (Q) \in Y) \land v \in \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \land v \neq 0_{U}) \to v \neq 0_{U}$
68	12 47 26 5	lsatlspsn2	$⊢ (U \in LMod \land v \in {Base}_{U} \land v \neq 0_{U}) \to LSpan (U) (\{v\}) \in A$
69	48 53 67 68	syl3anc	$⊢ ((φ \land \underset{˙}{⊥} (Q) \in Y) \land v \in \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \land v \neq 0_{U}) \to LSpan (U) (\{v\}) \in A$
70	1 3 2 5 6 43 69	dochsatshp	$⊢ ((φ \land \underset{˙}{⊥} (Q) \in Y) \land v \in \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \land v \neq 0_{U}) \to \underset{˙}{⊥} (LSpan (U) (\{v\})) \in Y$
71	6 65 66 70	lshpcmp	$⊢ ((φ \land \underset{˙}{⊥} (Q) \in Y) \land v \in \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \land v \neq 0_{U}) \to (\underset{˙}{⊥} (Q) \subseteq \underset{˙}{⊥} (LSpan (U) (\{v\})) \leftrightarrow \underset{˙}{⊥} (Q) = \underset{˙}{⊥} (LSpan (U) (\{v\})))$
72	62 71	mpbid	$⊢ ((φ \land \underset{˙}{⊥} (Q) \in Y) \land v \in \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \land v \neq 0_{U}) \to \underset{˙}{⊥} (Q) = \underset{˙}{⊥} (LSpan (U) (\{v\}))$
73	72	fveq2d	$⊢ ((φ \land \underset{˙}{⊥} (Q) \in Y) \land v \in \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \land v \neq 0_{U}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) = \underset{˙}{⊥} (\underset{˙}{⊥} (LSpan (U) (\{v\})))$
74	1 15 2	dochoc	$⊢ ((K \in HL \land W \in H) \land LSpan (U) (\{v\}) \in ran DIsoH (K) (W)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (LSpan (U) (\{v\}))) = LSpan (U) (\{v\})$
75	43 55 74	syl2anc	$⊢ ((φ \land \underset{˙}{⊥} (Q) \in Y) \land v \in \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \land v \neq 0_{U}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (LSpan (U) (\{v\}))) = LSpan (U) (\{v\})$
76	73 75	eqtrd	$⊢ ((φ \land \underset{˙}{⊥} (Q) \in Y) \land v \in \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \land v \neq 0_{U}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) = LSpan (U) (\{v\})$
77	76 69	eqeltrd	$⊢ ((φ \land \underset{˙}{⊥} (Q) \in Y) \land v \in \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \land v \neq 0_{U}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A$
78	77	rexlimdv3a	$⊢ (φ \land \underset{˙}{⊥} (Q) \in Y) \to (\exists v \in \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) v \neq 0_{U} \to \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A)$
79	41 78	mpd	$⊢ (φ \land \underset{˙}{⊥} (Q) \in Y) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A$
80	8	adantr	$⊢ (φ \land \underset{˙}{⊥} (Q) \in Y) \to Q \in S$
81	1 2 3 4 5 42 80	dochsat	$⊢ (φ \land \underset{˙}{⊥} (Q) \in Y) \to (\underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A \leftrightarrow Q \in A)$
82	79 81	mpbid	$⊢ (φ \land \underset{˙}{⊥} (Q) \in Y) \to Q \in A$
83	11 82	impbida	$⊢ φ \to (Q \in A \leftrightarrow \underset{˙}{⊥} (Q) \in Y)$

Metamath Proof Explorer

Theorem dochsatshpb

Proof