Metamath Proof Explorer

Theorem lhpat4N

Description: Property of an atom under a co-atom. (Contributed by NM, 24-Nov-2013) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	lhpat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		lhpat.j	$⊢ \underset{˙}{\lor} = join (K)$
		lhpat.m	$⊢ \underset{˙}{\land} = meet (K)$
		lhpat.a	$⊢ A = Atoms (K)$
		lhpat.h	$⊢ H = LHyp (K)$
	Assertion	lhpat4N	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (U \in A \land U \underset{˙}{\leq} W)) \to (P \underset{˙}{\lor} U) \underset{˙}{\land} W = U$

Proof

Step	Hyp	Ref	Expression
1		lhpat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		lhpat.j	$⊢ \underset{˙}{\lor} = join (K)$
3		lhpat.m	$⊢ \underset{˙}{\land} = meet (K)$
4		lhpat.a	$⊢ A = Atoms (K)$
5		lhpat.h	$⊢ H = LHyp (K)$
6		simp1	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (U \in A \land U \underset{˙}{\leq} W)) \to (K \in HL \land W \in H)$
7		simp2	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (U \in A \land U \underset{˙}{\leq} W)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
8		simp3l	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (U \in A \land U \underset{˙}{\leq} W)) \to U \in A$
9		eqid	$⊢ {Base}_{K} = {Base}_{K}$
10	9 4	atbase	$⊢ U \in A \to U \in {Base}_{K}$
11	8 10	syl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (U \in A \land U \underset{˙}{\leq} W)) \to U \in {Base}_{K}$
12		simp3r	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (U \in A \land U \underset{˙}{\leq} W)) \to U \underset{˙}{\leq} W$
13	9 1 2 3 4 5	lhple	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (U \in {Base}_{K} \land U \underset{˙}{\leq} W)) \to (P \underset{˙}{\lor} U) \underset{˙}{\land} W = U$
14	6 7 11 12 13	syl112anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (U \in A \land U \underset{˙}{\leq} W)) \to (P \underset{˙}{\lor} U) \underset{˙}{\land} W = U$