This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cdleme20y

Description: Part of proof of Lemma E in Crawley p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012) (Proof shortened by OpenAI, 25-Mar-2020)

		Ref	Expression
	Hypotheses	cdleme20z.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		cdleme20z.j	$⊢ \underset{˙}{\lor} = join (K)$
		cdleme20z.m	$⊢ \underset{˙}{\land} = meet (K)$
		cdleme20z.a	$⊢ A = Atoms (K)$
	Assertion	cdleme20y	$⊢ (K \in HL \land (R \in A \land S \in A \land T \in A) \land (S \neq T \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (S \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} R) = R$

Proof

Step	Hyp	Ref	Expression
1		cdleme20z.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme20z.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme20z.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme20z.a	$⊢ A = Atoms (K)$
5		simp1	$⊢ (K \in HL \land (R \in A \land S \in A \land T \in A) \land (S \neq T \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to K \in HL$
6		simp22	$⊢ (K \in HL \land (R \in A \land S \in A \land T \in A) \land (S \neq T \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to S \in A$
7		simp23	$⊢ (K \in HL \land (R \in A \land S \in A \land T \in A) \land (S \neq T \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to T \in A$
8		simp21	$⊢ (K \in HL \land (R \in A \land S \in A \land T \in A) \land (S \neq T \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to R \in A$
9		simp3	$⊢ (K \in HL \land (R \in A \land S \in A \land T \in A) \land (S \neq T \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (S \neq T \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
10	1 2 3 4	2llnma2rN	$⊢ (K \in HL \land (S \in A \land T \in A \land R \in A) \land (S \neq T \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (S \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} R) = R$
11	5 6 7 8 9 10	syl131anc	$⊢ (K \in HL \land (R \in A \land S \in A \land T \in A) \land (S \neq T \land \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (S \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} R) = R$