Metamath Proof Explorer

Theorem poml5N

Description: Orthomodular law for projective lattices. (Contributed by NM, 23-Mar-2012) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	poml4.a	$⊢ A = Atoms (K)$
		poml4.p	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
	Assertion	poml5N	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y)) \cap \underset{˙}{⊥} (Y) = \underset{˙}{⊥} (\underset{˙}{⊥} (X))$

Proof

Step	Hyp	Ref	Expression
1		poml4.a	$⊢ A = Atoms (K)$
2		poml4.p	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
3		simp1	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \to K \in HL$
4		simp3	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \to X \subseteq \underset{˙}{⊥} (Y)$
5	1 2	polssatN	$⊢ (K \in HL \land Y \subseteq A) \to \underset{˙}{⊥} (Y) \subseteq A$
6	5	3adant3	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \to \underset{˙}{⊥} (Y) \subseteq A$
7	4 6	sstrd	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \to X \subseteq A$
8	3 7 6	3jca	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \to (K \in HL \land X \subseteq A \land \underset{˙}{⊥} (Y) \subseteq A)$
9	1 2	3polN	$⊢ (K \in HL \land Y \subseteq A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (Y))) = \underset{˙}{⊥} (Y)$
10	9	3adant3	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (Y))) = \underset{˙}{⊥} (Y)$
11	4 10	jca	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \to (X \subseteq \underset{˙}{⊥} (Y) \land \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (Y))) = \underset{˙}{⊥} (Y))$
12	1 2	poml4N	$⊢ (K \in HL \land X \subseteq A \land \underset{˙}{⊥} (Y) \subseteq A) \to ((X \subseteq \underset{˙}{⊥} (Y) \land \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (Y))) = \underset{˙}{⊥} (Y)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y)) \cap \underset{˙}{⊥} (Y) = \underset{˙}{⊥} (\underset{˙}{⊥} (X)))$
13	8 11 12	sylc	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap \underset{˙}{⊥} (Y)) \cap \underset{˙}{⊥} (Y) = \underset{˙}{⊥} (\underset{˙}{⊥} (X))$