dochexmid

Description: Excluded middle law for closed subspaces, which is equivalent to (and derived from) the orthomodular law dihoml4 . Lemma 3.3(2) in Holland95 p. 215. In our proof, we use the variables X , M , p , q , r in place of Hollands' l, m, P, Q, L respectively. ( pexmidALTN analog.) (Contributed by NM, 15-Jan-2015)

	Ref	Expression
Hypotheses	dochexmid.h	$⊢ H = LHyp (K)$
	dochexmid.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	dochexmid.u	$⊢ U = DVecH (K) (W)$
	dochexmid.v	$⊢ V = {Base}_{U}$
	dochexmid.s	$⊢ S = LSubSp (U)$
	dochexmid.p	$⊢ \underset{˙}{\oplus} = LSSum (U)$
	dochexmid.k	$⊢ φ \to (K \in HL \land W \in H)$
	dochexmid.x	$⊢ φ \to X \in S$
	dochexmid.c	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X$
Assertion	dochexmid	$⊢ φ \to X \underset{˙}{\oplus} \underset{˙}{⊥} (X) = V$

Proof

Step	Hyp	Ref	Expression
1		dochexmid.h	$⊢ H = LHyp (K)$
2		dochexmid.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		dochexmid.u	$⊢ U = DVecH (K) (W)$
4		dochexmid.v	$⊢ V = {Base}_{U}$
5		dochexmid.s	$⊢ S = LSubSp (U)$
6		dochexmid.p	$⊢ \underset{˙}{\oplus} = LSSum (U)$
7		dochexmid.k	$⊢ φ \to (K \in HL \land W \in H)$
8		dochexmid.x	$⊢ φ \to X \in S$
9		dochexmid.c	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X$
10		id	$⊢ X = \{0_{U}\} \to X = \{0_{U}\}$
11		fveq2	$⊢ X = \{0_{U}\} \to \underset{˙}{⊥} (X) = \underset{˙}{⊥} (\{0_{U}\})$
12	10 11	oveq12d	$⊢ X = \{0_{U}\} \to X \underset{˙}{\oplus} \underset{˙}{⊥} (X) = \{0_{U}\} \underset{˙}{\oplus} \underset{˙}{⊥} (\{0_{U}\})$
13	1 3 7	dvhlmod	$⊢ φ \to U \in LMod$
14		eqid	$⊢ 0_{U} = 0_{U}$
15	4 14	lmod0vcl	$⊢ U \in LMod \to 0_{U} \in V$
16	13 15	syl	$⊢ φ \to 0_{U} \in V$
17	16	snssd	$⊢ φ \to \{0_{U}\} \subseteq V$
18	1 3 4 5 2	dochlss	$⊢ ((K \in HL \land W \in H) \land \{0_{U}\} \subseteq V) \to \underset{˙}{⊥} (\{0_{U}\}) \in S$
19	7 17 18	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\{0_{U}\}) \in S$
20	5	lsssubg	$⊢ (U \in LMod \land \underset{˙}{⊥} (\{0_{U}\}) \in S) \to \underset{˙}{⊥} (\{0_{U}\}) \in SubGrp (U)$
21	13 19 20	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\{0_{U}\}) \in SubGrp (U)$
22	14 6	lsm02	$⊢ \underset{˙}{⊥} (\{0_{U}\}) \in SubGrp (U) \to \{0_{U}\} \underset{˙}{\oplus} \underset{˙}{⊥} (\{0_{U}\}) = \underset{˙}{⊥} (\{0_{U}\})$
23	21 22	syl	$⊢ φ \to \{0_{U}\} \underset{˙}{\oplus} \underset{˙}{⊥} (\{0_{U}\}) = \underset{˙}{⊥} (\{0_{U}\})$
24	1 3 2 4 14	doch0	$⊢ (K \in HL \land W \in H) \to \underset{˙}{⊥} (\{0_{U}\}) = V$
25	7 24	syl	$⊢ φ \to \underset{˙}{⊥} (\{0_{U}\}) = V$
26	23 25	eqtrd	$⊢ φ \to \{0_{U}\} \underset{˙}{\oplus} \underset{˙}{⊥} (\{0_{U}\}) = V$
27	12 26	sylan9eqr	$⊢ (φ \land X = \{0_{U}\}) \to X \underset{˙}{\oplus} \underset{˙}{⊥} (X) = V$
28		eqid	$⊢ LSpan (U) = LSpan (U)$
29		eqid	$⊢ LSAtoms (U) = LSAtoms (U)$
30	7	adantr	$⊢ (φ \land X \neq \{0_{U}\}) \to (K \in HL \land W \in H)$
31	8	adantr	$⊢ (φ \land X \neq \{0_{U}\}) \to X \in S$
32		simpr	$⊢ (φ \land X \neq \{0_{U}\}) \to X \neq \{0_{U}\}$
33	9	adantr	$⊢ (φ \land X \neq \{0_{U}\}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X$
34	1 2 3 4 5 28 6 29 30 31 14 32 33	dochexmidlem8	$⊢ (φ \land X \neq \{0_{U}\}) \to X \underset{˙}{\oplus} \underset{˙}{⊥} (X) = V$
35	27 34	pm2.61dane	$⊢ φ \to X \underset{˙}{\oplus} \underset{˙}{⊥} (X) = V$

Metamath Proof Explorer

Theorem dochexmid

Proof