cdleme20zN

Description: Part of proof of Lemma E in Crawley p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012) (New usage is discouraged.)

	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	cdleme20zN	$⊢ (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 = 0. (K)$

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		hllat	$⊢ K \in HL \to K \in Lat$
6	5	3ad2ant1	$⊢ (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 Lat$
7		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$
8		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$
9		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$
10		eqid	$⊢ {Base}_{K} = {Base}_{K}$
11	10 2 4	hlatjcl	$⊢ (K \in HL \land S \in A \land R \in A) \to S \underset{˙}{\lor} R \in {Base}_{K}$
12	7 8 9 11	syl3anc	$⊢ (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 \in {Base}_{K}$
13		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$
14	10 4	atbase	$⊢ T \in A \to T \in {Base}_{K}$
15	13 14	syl	$⊢ (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 {Base}_{K}$
16	10 3	latmcom	$⊢ (K \in Lat \land S \underset{˙}{\lor} R \in {Base}_{K} \land T \in {Base}_{K}) \to (S \underset{˙}{\lor} R) \underset{˙}{\land} T = T \underset{˙}{\land} (S \underset{˙}{\lor} R)$
17	6 12 15 16	syl3anc	$⊢ (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 = T \underset{˙}{\land} (S \underset{˙}{\lor} R)$
18		simp3r	$⊢ (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 \neg R \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
19		hlcvl	$⊢ K \in HL \to K \in CvLat$
20	19	3ad2ant1	$⊢ (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 CvLat$
21		simp3l	$⊢ (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$
22	21	necomd	$⊢ (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 \neq S$
23	1 2 4	cvlatexch1	$⊢ (K \in CvLat \land (T \in A \land R \in A \land S \in A) \land T \neq S) \to (T \underset{˙}{\leq} (S \underset{˙}{\lor} R) \to R \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
24	20 13 9 8 22 23	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 (T \underset{˙}{\leq} (S \underset{˙}{\lor} R) \to R \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
25	18 24	mtod	$⊢ (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 \neg T \underset{˙}{\leq} (S \underset{˙}{\lor} R)$
26		hlatl	$⊢ K \in HL \to K \in AtLat$
27	26	3ad2ant1	$⊢ (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 AtLat$
28		eqid	$⊢ 0. (K) = 0. (K)$
29	10 1 3 28 4	atnle	$⊢ (K \in AtLat \land T \in A \land S \underset{˙}{\lor} R \in {Base}_{K}) \to (\neg T \underset{˙}{\leq} (S \underset{˙}{\lor} R) \leftrightarrow T \underset{˙}{\land} (S \underset{˙}{\lor} R) = 0. (K))$
30	27 13 12 29	syl3anc	$⊢ (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 (\neg T \underset{˙}{\leq} (S \underset{˙}{\lor} R) \leftrightarrow T \underset{˙}{\land} (S \underset{˙}{\lor} R) = 0. (K))$
31	25 30	mpbid	$⊢ (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 \underset{˙}{\land} (S \underset{˙}{\lor} R) = 0. (K)$
32	17 31	eqtrd	$⊢ (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 = 0. (K)$

Metamath Proof Explorer

Theorem cdleme20zN

Proof