lhp2atnle

Description: Inequality for 2 different atoms under co-atom W . (Contributed by NM, 17-Jun-2013)

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

Proof

Step	Hyp	Ref	Expression
1		lhp2atnle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		lhp2atnle.j	$⊢ \underset{˙}{\lor} = join (K)$
3		lhp2atnle.a	$⊢ A = Atoms (K)$
4		lhp2atnle.h	$⊢ H = LHyp (K)$
5		simp11l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to K \in HL$
6		hlatl	$⊢ K \in HL \to K \in AtLat$
7	5 6	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to K \in AtLat$
8		simp3l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to V \in A$
9		eqid	$⊢ 0. (K) = 0. (K)$
10	9 3	atn0	$⊢ (K \in AtLat \land V \in A) \to V \neq 0. (K)$
11	7 8 10	syl2anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to V \neq 0. (K)$
12	5	hllatd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to K \in Lat$
13		eqid	$⊢ {Base}_{K} = {Base}_{K}$
14	13 3	atbase	$⊢ V \in A \to V \in {Base}_{K}$
15	8 14	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to V \in {Base}_{K}$
16		simp12l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to P \in A$
17		simp2l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to U \in A$
18	13 2 3	hlatjcl	$⊢ (K \in HL \land P \in A \land U \in A) \to P \underset{˙}{\lor} U \in {Base}_{K}$
19	5 16 17 18	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to P \underset{˙}{\lor} U \in {Base}_{K}$
20		eqid	$⊢ meet (K) = meet (K)$
21	13 1 20	latleeqm2	$⊢ (K \in Lat \land V \in {Base}_{K} \land P \underset{˙}{\lor} U \in {Base}_{K}) \to (V \underset{˙}{\leq} (P \underset{˙}{\lor} U) \leftrightarrow (P \underset{˙}{\lor} U) meet (K) V = V)$
22	12 15 19 21	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to (V \underset{˙}{\leq} (P \underset{˙}{\lor} U) \leftrightarrow (P \underset{˙}{\lor} U) meet (K) V = V)$
23	1 2 20 9 3 4	lhp2at0	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to (P \underset{˙}{\lor} U) meet (K) V = 0. (K)$
24		eqeq1	$⊢ (P \underset{˙}{\lor} U) meet (K) V = V \to ((P \underset{˙}{\lor} U) meet (K) V = 0. (K) \leftrightarrow V = 0. (K))$
25	23 24	syl5ibcom	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to ((P \underset{˙}{\lor} U) meet (K) V = V \to V = 0. (K))$
26	22 25	sylbid	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to (V \underset{˙}{\leq} (P \underset{˙}{\lor} U) \to V = 0. (K))$
27	26	necon3ad	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to (V \neq 0. (K) \to \neg V \underset{˙}{\leq} (P \underset{˙}{\lor} U))$
28	11 27	mpd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V) \land (U \in A \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to \neg V \underset{˙}{\leq} (P \underset{˙}{\lor} U)$

Metamath Proof Explorer

Theorem lhp2atnle

Proof