pexmidN

Description: Excluded middle law for closed projective subspaces, which can be shown to be equivalent to (and derivable from) the orthomodular law poml4N . Lemma 3.3(2) in Holland95 p. 215, which we prove as a special case of osumclN . (Contributed by NM, 25-Mar-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pexmid.a	$⊢ A = Atoms (K)$
	pexmid.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
	pexmid.o	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
Assertion	pexmidN	$⊢ ((K \in HL \land X \subseteq A) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X) \to X \underset{˙}{+} \underset{˙}{⊥} (X) = A$

Proof

Step	Hyp	Ref	Expression
1		pexmid.a	$⊢ A = Atoms (K)$
2		pexmid.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
3		pexmid.o	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
4		simpll	$⊢ ((K \in HL \land X \subseteq A) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X) \to K \in HL$
5		simplr	$⊢ ((K \in HL \land X \subseteq A) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X) \to X \subseteq A$
6	1 3	polssatN	$⊢ (K \in HL \land X \subseteq A) \to \underset{˙}{⊥} (X) \subseteq A$
7	6	adantr	$⊢ ((K \in HL \land X \subseteq A) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X) \to \underset{˙}{⊥} (X) \subseteq A$
8	1 2 3	poldmj1N	$⊢ (K \in HL \land X \subseteq A \land \underset{˙}{⊥} (X) \subseteq A) \to \underset{˙}{⊥} (X \underset{˙}{+} \underset{˙}{⊥} (X)) = \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (\underset{˙}{⊥} (X))$
9	4 5 7 8	syl3anc	$⊢ ((K \in HL \land X \subseteq A) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X) \to \underset{˙}{⊥} (X \underset{˙}{+} \underset{˙}{⊥} (X)) = \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (\underset{˙}{⊥} (X))$
10	1 3	pnonsingN	$⊢ (K \in HL \land \underset{˙}{⊥} (X) \subseteq A) \to \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = \emptyset$
11	4 7 10	syl2anc	$⊢ ((K \in HL \land X \subseteq A) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X) \to \underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = \emptyset$
12	9 11	eqtrd	$⊢ ((K \in HL \land X \subseteq A) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X) \to \underset{˙}{⊥} (X \underset{˙}{+} \underset{˙}{⊥} (X)) = \emptyset$
13	12	fveq2d	$⊢ ((K \in HL \land X \subseteq A) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} \underset{˙}{⊥} (X))) = \underset{˙}{⊥} (\emptyset)$
14		simpr	$⊢ ((K \in HL \land X \subseteq A) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X$
15		eqid	$⊢ PSubCl (K) = PSubCl (K)$
16	1 3 15	ispsubclN	$⊢ K \in HL \to (X \in PSubCl (K) \leftrightarrow (X \subseteq A \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X))$
17	16	ad2antrr	$⊢ ((K \in HL \land X \subseteq A) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X) \to (X \in PSubCl (K) \leftrightarrow (X \subseteq A \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X))$
18	5 14 17	mpbir2and	$⊢ ((K \in HL \land X \subseteq A) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X) \to X \in PSubCl (K)$
19	1 3 15	polsubclN	$⊢ (K \in HL \land X \subseteq A) \to \underset{˙}{⊥} (X) \in PSubCl (K)$
20	19	adantr	$⊢ ((K \in HL \land X \subseteq A) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X) \to \underset{˙}{⊥} (X) \in PSubCl (K)$
21	1 3	2polssN	$⊢ (K \in HL \land X \subseteq A) \to X \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X))$
22	21	adantr	$⊢ ((K \in HL \land X \subseteq A) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X) \to X \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X))$
23	2 3 15	osumclN	$⊢ ((K \in HL \land X \in PSubCl (K) \land \underset{˙}{⊥} (X) \in PSubCl (K)) \land X \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X))) \to X \underset{˙}{+} \underset{˙}{⊥} (X) \in PSubCl (K)$
24	4 18 20 22 23	syl31anc	$⊢ ((K \in HL \land X \subseteq A) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X) \to X \underset{˙}{+} \underset{˙}{⊥} (X) \in PSubCl (K)$
25	3 15	psubcli2N	$⊢ (K \in HL \land X \underset{˙}{+} \underset{˙}{⊥} (X) \in PSubCl (K)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} \underset{˙}{⊥} (X))) = X \underset{˙}{+} \underset{˙}{⊥} (X)$
26	4 24 25	syl2anc	$⊢ ((K \in HL \land X \subseteq A) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} \underset{˙}{⊥} (X))) = X \underset{˙}{+} \underset{˙}{⊥} (X)$
27	1 3	pol0N	$⊢ K \in HL \to \underset{˙}{⊥} (\emptyset) = A$
28	27	ad2antrr	$⊢ ((K \in HL \land X \subseteq A) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X) \to \underset{˙}{⊥} (\emptyset) = A$
29	13 26 28	3eqtr3d	$⊢ ((K \in HL \land X \subseteq A) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X) \to X \underset{˙}{+} \underset{˙}{⊥} (X) = A$

Metamath Proof Explorer

Theorem pexmidN

Proof