Metamath Proof Explorer

Theorem poml6N

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

		Ref	Expression
	Hypotheses	poml6.c	$⊢ C = PSubCl (K)$
		poml6.p	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
	Assertion	poml6N	$⊢ ((K \in HL \land X \in C \land Y \in C) \land X \subseteq Y) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap Y) \cap Y = X$

Proof

Step	Hyp	Ref	Expression
1		poml6.c	$⊢ C = PSubCl (K)$
2		poml6.p	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
3		simpl1	$⊢ ((K \in HL \land X \in C \land Y \in C) \land X \subseteq Y) \to K \in HL$
4		simpl2	$⊢ ((K \in HL \land X \in C \land Y \in C) \land X \subseteq Y) \to X \in C$
5		eqid	$⊢ Atoms (K) = Atoms (K)$
6	5 1	psubclssatN	$⊢ (K \in HL \land X \in C) \to X \subseteq Atoms (K)$
7	3 4 6	syl2anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land X \subseteq Y) \to X \subseteq Atoms (K)$
8		simpl3	$⊢ ((K \in HL \land X \in C \land Y \in C) \land X \subseteq Y) \to Y \in C$
9	5 1	psubclssatN	$⊢ (K \in HL \land Y \in C) \to Y \subseteq Atoms (K)$
10	3 8 9	syl2anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land X \subseteq Y) \to Y \subseteq Atoms (K)$
11		simpr	$⊢ ((K \in HL \land X \in C \land Y \in C) \land X \subseteq Y) \to X \subseteq Y$
12	2 1	psubcli2N	$⊢ (K \in HL \land Y \in C) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) = Y$
13	3 8 12	syl2anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land X \subseteq Y) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) = Y$
14	5 2	poml4N	$⊢ (K \in HL \land X \subseteq Atoms (K) \land Y \subseteq Atoms (K)) \to ((X \subseteq Y \land \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) = Y) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap Y) \cap Y = \underset{˙}{⊥} (\underset{˙}{⊥} (X)))$
15	14	imp	$⊢ ((K \in HL \land X \subseteq Atoms (K) \land Y \subseteq Atoms (K)) \land (X \subseteq Y \land \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) = Y)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap Y) \cap Y = \underset{˙}{⊥} (\underset{˙}{⊥} (X))$
16	3 7 10 11 13 15	syl32anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land X \subseteq Y) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap Y) \cap Y = \underset{˙}{⊥} (\underset{˙}{⊥} (X))$
17	2 1	psubcli2N	$⊢ (K \in HL \land X \in C) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X$
18	3 4 17	syl2anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land X \subseteq Y) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X$
19	16 18	eqtrd	$⊢ ((K \in HL \land X \in C \land Y \in C) \land X \subseteq Y) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X) \cap Y) \cap Y = X$