dochsat

Description: The double orthocomplement of an atom is an atom. (Contributed by NM, 29-Oct-2014)

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

Proof

Step	Hyp	Ref	Expression
1		dochsat.h	$⊢ H = LHyp (K)$
2		dochsat.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		dochsat.u	$⊢ U = DVecH (K) (W)$
4		dochsat.s	$⊢ S = LSubSp (U)$
5		dochsat.a	$⊢ A = LSAtoms (U)$
6		dochsat.k	$⊢ φ \to (K \in HL \land W \in H)$
7		dochsat.q	$⊢ φ \to Q \in S$
8	1 3 6	dvhlmod	$⊢ φ \to U \in LMod$
9	8	adantr	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A) \to U \in LMod$
10	7	adantr	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A) \to Q \in S$
11		eqid	$⊢ 0_{U} = 0_{U}$
12	11 4	lss0ss	$⊢ (U \in LMod \land Q \in S) \to \{0_{U}\} \subseteq Q$
13	9 10 12	syl2anc	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A) \to \{0_{U}\} \subseteq Q$
14		simpr	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A$
15	11 5 9 14	lsatn0	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \neq \{0_{U}\}$
16		simpr	$⊢ ((φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A) \land Q = \{0_{U}\}) \to Q = \{0_{U}\}$
17	16	fveq2d	$⊢ ((φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A) \land Q = \{0_{U}\}) \to \underset{˙}{⊥} (Q) = \underset{˙}{⊥} (\{0_{U}\})$
18	17	fveq2d	$⊢ ((φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A) \land Q = \{0_{U}\}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) = \underset{˙}{⊥} (\underset{˙}{⊥} (\{0_{U}\}))$
19	1 3 2 11 6	dochoc0	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (\{0_{U}\})) = \{0_{U}\}$
20	19	adantr	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\{0_{U}\})) = \{0_{U}\}$
21	20	adantr	$⊢ ((φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A) \land Q = \{0_{U}\}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\{0_{U}\})) = \{0_{U}\}$
22	18 21	eqtrd	$⊢ ((φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A) \land Q = \{0_{U}\}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) = \{0_{U}\}$
23	22	ex	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A) \to (Q = \{0_{U}\} \to \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) = \{0_{U}\})$
24	23	necon3d	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A) \to (\underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \neq \{0_{U}\} \to Q \neq \{0_{U}\})$
25	15 24	mpd	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A) \to Q \neq \{0_{U}\}$
26	25	necomd	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A) \to \{0_{U}\} \neq Q$
27		df-pss	$⊢ \{0_{U}\} \subset Q \leftrightarrow (\{0_{U}\} \subseteq Q \land \{0_{U}\} \neq Q)$
28	13 26 27	sylanbrc	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A) \to \{0_{U}\} \subset Q$
29	6	adantr	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A) \to (K \in HL \land W \in H)$
30		eqid	$⊢ {Base}_{U} = {Base}_{U}$
31	30 4	lssss	$⊢ Q \in S \to Q \subseteq {Base}_{U}$
32	7 31	syl	$⊢ φ \to Q \subseteq {Base}_{U}$
33	32	adantr	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A) \to Q \subseteq {Base}_{U}$
34	1 3 30 2	dochocss	$⊢ ((K \in HL \land W \in H) \land Q \subseteq {Base}_{U}) \to Q \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (Q))$
35	29 33 34	syl2anc	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A) \to Q \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (Q))$
36	4 5 9 14	lsatlssel	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in S$
37	4	lsssubg	$⊢ (U \in LMod \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in S) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in SubGrp (U)$
38	9 36 37	syl2anc	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in SubGrp (U)$
39		eqid	$⊢ LSSum (U) = LSSum (U)$
40	11 39	lsm02	$⊢ \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in SubGrp (U) \to \{0_{U}\} LSSum (U) \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) = \underset{˙}{⊥} (\underset{˙}{⊥} (Q))$
41	38 40	syl	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A) \to \{0_{U}\} LSSum (U) \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) = \underset{˙}{⊥} (\underset{˙}{⊥} (Q))$
42	35 41	sseqtrrd	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A) \to Q \subseteq \{0_{U}\} LSSum (U) \underset{˙}{⊥} (\underset{˙}{⊥} (Q))$
43	1 3 6	dvhlvec	$⊢ φ \to U \in LVec$
44	43	adantr	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A) \to U \in LVec$
45	11 4	lsssn0	$⊢ U \in LMod \to \{0_{U}\} \in S$
46	9 45	syl	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A) \to \{0_{U}\} \in S$
47	4 39 5 44 46 10 14	lsmsatcv	$⊢ ((φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A) \land \{0_{U}\} \subset Q \land Q \subseteq \{0_{U}\} LSSum (U) \underset{˙}{⊥} (\underset{˙}{⊥} (Q))) \to Q = \{0_{U}\} LSSum (U) \underset{˙}{⊥} (\underset{˙}{⊥} (Q))$
48	28 42 47	mpd3an23	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A) \to Q = \{0_{U}\} LSSum (U) \underset{˙}{⊥} (\underset{˙}{⊥} (Q))$
49	48 41	eqtr2d	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) = Q$
50	49 14	eqeltrrd	$⊢ (φ \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A) \to Q \in A$
51	6	adantr	$⊢ (φ \land Q \in A) \to (K \in HL \land W \in H)$
52		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
53	1 3 52 5	dih1dimat	$⊢ ((K \in HL \land W \in H) \land Q \in A) \to Q \in ran DIsoH (K) (W)$
54	6 53	sylan	$⊢ (φ \land Q \in A) \to Q \in ran DIsoH (K) (W)$
55	1 52 2	dochoc	$⊢ ((K \in HL \land W \in H) \land Q \in ran DIsoH (K) (W)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) = Q$
56	51 54 55	syl2anc	$⊢ (φ \land Q \in A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) = Q$
57		simpr	$⊢ (φ \land Q \in A) \to Q \in A$
58	56 57	eqeltrd	$⊢ (φ \land Q \in A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A$
59	50 58	impbida	$⊢ φ \to (\underset{˙}{⊥} (\underset{˙}{⊥} (Q)) \in A \leftrightarrow Q \in A)$

Metamath Proof Explorer

Theorem dochsat

Proof