pexmidALTN

Description: Excluded middle law for closed projective subspaces, which is equivalent to (and derived from) the orthomodular law poml4N . 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. TODO: should we make this obsolete? (Contributed by NM, 3-Feb-2012) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		pexmidALT.a	$⊢ A = Atoms (K)$
2		pexmidALT.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
3		pexmidALT.o	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
4		id	$⊢ X = \emptyset \to X = \emptyset$
5		fveq2	$⊢ X = \emptyset \to \underset{˙}{⊥} (X) = \underset{˙}{⊥} (\emptyset)$
6	4 5	oveq12d	$⊢ X = \emptyset \to X \underset{˙}{+} \underset{˙}{⊥} (X) = \emptyset \underset{˙}{+} \underset{˙}{⊥} (\emptyset)$
7	1 3	pol0N	$⊢ K \in HL \to \underset{˙}{⊥} (\emptyset) = A$
8		eqimss	$⊢ \underset{˙}{⊥} (\emptyset) = A \to \underset{˙}{⊥} (\emptyset) \subseteq A$
9	7 8	syl	$⊢ K \in HL \to \underset{˙}{⊥} (\emptyset) \subseteq A$
10	1 2	padd02	$⊢ (K \in HL \land \underset{˙}{⊥} (\emptyset) \subseteq A) \to \emptyset \underset{˙}{+} \underset{˙}{⊥} (\emptyset) = \underset{˙}{⊥} (\emptyset)$
11	9 10	mpdan	$⊢ K \in HL \to \emptyset \underset{˙}{+} \underset{˙}{⊥} (\emptyset) = \underset{˙}{⊥} (\emptyset)$
12	11 7	eqtrd	$⊢ K \in HL \to \emptyset \underset{˙}{+} \underset{˙}{⊥} (\emptyset) = A$
13	12	ad2antrr	$⊢ ((K \in HL \land X \subseteq A) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X) \to \emptyset \underset{˙}{+} \underset{˙}{⊥} (\emptyset) = A$
14	6 13	sylan9eqr	$⊢ (((K \in HL \land X \subseteq A) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X) \land X = \emptyset) \to X \underset{˙}{+} \underset{˙}{⊥} (X) = A$
15	1 2 3	pexmidlem8N	$⊢ ((K \in HL \land X \subseteq A) \land (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X \land X \neq \emptyset)) \to X \underset{˙}{+} \underset{˙}{⊥} (X) = A$
16	15	anassrs	$⊢ (((K \in HL \land X \subseteq A) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X) \land X \neq \emptyset) \to X \underset{˙}{+} \underset{˙}{⊥} (X) = A$
17	14 16	pm2.61dane	$⊢ ((K \in HL \land X \subseteq A) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X) \to X \underset{˙}{+} \underset{˙}{⊥} (X) = A$

Metamath Proof Explorer

Theorem pexmidALTN

Proof