lhp2at0nle

Description: Inequality for 2 different atoms (or an atom and zero) under co-atom W . (Contributed by NM, 28-Jul-2013)

	Ref	Expression
Hypotheses	lhp2at0nle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lhp2at0nle.j	$⊢ \underset{˙}{\lor} = join (K)$
	lhp2at0nle.z	$⊢ \underset{˙}{0} = 0. (K)$
	lhp2at0nle.a	$⊢ A = Atoms (K)$
	lhp2at0nle.h	$⊢ H = LHyp (K)$
Assertion	lhp2at0nle	$⊢ (((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 \lor U = \underset{˙}{0}) \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		lhp2at0nle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		lhp2at0nle.j	$⊢ \underset{˙}{\lor} = join (K)$
3		lhp2at0nle.z	$⊢ \underset{˙}{0} = 0. (K)$
4		lhp2at0nle.a	$⊢ A = Atoms (K)$
5		lhp2at0nle.h	$⊢ H = LHyp (K)$
6		simpl1	$⊢ ((((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 \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land U \in A) \to ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land U \neq V)$
7		simpr	$⊢ ((((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 \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land U \in A) \to U \in A$
8		simpl2r	$⊢ ((((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 \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land U \in A) \to U \underset{˙}{\leq} W$
9		simpl3	$⊢ ((((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 \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land U \in A) \to (V \in A \land V \underset{˙}{\leq} W)$
10	1 2 4 5	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)$
11	6 7 8 9 10	syl121anc	$⊢ ((((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 \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land U \in A) \to \neg V \underset{˙}{\leq} (P \underset{˙}{\lor} U)$
12		simp3r	$⊢ (((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 \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to V \underset{˙}{\leq} W$
13		simp12r	$⊢ (((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 \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to \neg P \underset{˙}{\leq} W$
14		nbrne2	$⊢ (V \underset{˙}{\leq} W \land \neg P \underset{˙}{\leq} W) \to V \neq P$
15	12 13 14	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 \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to V \neq P$
16	15	neneqd	$⊢ (((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 \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to \neg V = P$
17		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 \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to K \in HL$
18		hlatl	$⊢ K \in HL \to K \in AtLat$
19	17 18	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 \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to K \in AtLat$
20		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 \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to V \in A$
21		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 \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to P \in A$
22	1 4	atcmp	$⊢ (K \in AtLat \land V \in A \land P \in A) \to (V \underset{˙}{\leq} P \leftrightarrow V = P)$
23	19 20 21 22	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 \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to (V \underset{˙}{\leq} P \leftrightarrow V = P)$
24	16 23	mtbird	$⊢ (((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 \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to \neg V \underset{˙}{\leq} P$
25	24	adantr	$⊢ ((((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 \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land U = \underset{˙}{0}) \to \neg V \underset{˙}{\leq} P$
26		oveq2	$⊢ U = \underset{˙}{0} \to P \underset{˙}{\lor} U = P \underset{˙}{\lor} \underset{˙}{0}$
27		hlol	$⊢ K \in HL \to K \in OL$
28	17 27	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 \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to K \in OL$
29		eqid	$⊢ {Base}_{K} = {Base}_{K}$
30	29 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
31	21 30	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 \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to P \in {Base}_{K}$
32	29 2 3	olj01	$⊢ (K \in OL \land P \in {Base}_{K}) \to P \underset{˙}{\lor} \underset{˙}{0} = P$
33	28 31 32	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 \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to P \underset{˙}{\lor} \underset{˙}{0} = P$
34	26 33	sylan9eqr	$⊢ ((((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 \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land U = \underset{˙}{0}) \to P \underset{˙}{\lor} U = P$
35	34	breq2d	$⊢ ((((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 \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land U = \underset{˙}{0}) \to (V \underset{˙}{\leq} (P \underset{˙}{\lor} U) \leftrightarrow V \underset{˙}{\leq} P)$
36	25 35	mtbird	$⊢ ((((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 \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land U = \underset{˙}{0}) \to \neg V \underset{˙}{\leq} (P \underset{˙}{\lor} U)$
37		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 \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \to (U \in A \lor U = \underset{˙}{0})$
38	11 36 37	mpjaodan	$⊢ (((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 \lor U = \underset{˙}{0}) \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 lhp2at0nle

Proof