lhp2at0ne

Description: Inequality for joins with 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	lhp2at0ne	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (((U \in A \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land U \neq V) \to P \underset{˙}{\lor} U \neq Q \underset{˙}{\lor} V$

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		simp11	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (((U \in A \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land U \neq V) \to (K \in HL \land W \in H)$
7		simp12	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (((U \in A \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land U \neq V) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
8		simp3	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (((U \in A \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land U \neq V) \to U \neq V$
9		simp2l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (((U \in A \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land U \neq V) \to ((U \in A \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W)$
10		simp2r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (((U \in A \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land U \neq V) \to (V \in A \land V \underset{˙}{\leq} W)$
11	1 2 3 4 5	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)$
12	6 7 8 9 10 11	syl311anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (((U \in A \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land U \neq V) \to \neg V \underset{˙}{\leq} (P \underset{˙}{\lor} U)$
13		simp11l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (((U \in A \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land U \neq V) \to K \in HL$
14		simp13	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (((U \in A \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land U \neq V) \to Q \in A$
15		simp2rl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (((U \in A \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land U \neq V) \to V \in A$
16	1 2 4	hlatlej2	$⊢ (K \in HL \land Q \in A \land V \in A) \to V \underset{˙}{\leq} (Q \underset{˙}{\lor} V)$
17	13 14 15 16	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (((U \in A \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land U \neq V) \to V \underset{˙}{\leq} (Q \underset{˙}{\lor} V)$
18	17	adantr	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (((U \in A \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land U \neq V) \land P \underset{˙}{\lor} U = Q \underset{˙}{\lor} V) \to V \underset{˙}{\leq} (Q \underset{˙}{\lor} V)$
19		simpr	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (((U \in A \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land U \neq V) \land P \underset{˙}{\lor} U = Q \underset{˙}{\lor} V) \to P \underset{˙}{\lor} U = Q \underset{˙}{\lor} V$
20	18 19	breqtrrd	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (((U \in A \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land U \neq V) \land P \underset{˙}{\lor} U = Q \underset{˙}{\lor} V) \to V \underset{˙}{\leq} (P \underset{˙}{\lor} U)$
21	20	ex	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (((U \in A \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land U \neq V) \to (P \underset{˙}{\lor} U = Q \underset{˙}{\lor} V \to V \underset{˙}{\leq} (P \underset{˙}{\lor} U))$
22	21	necon3bd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (((U \in A \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land U \neq V) \to (\neg V \underset{˙}{\leq} (P \underset{˙}{\lor} U) \to P \underset{˙}{\lor} U \neq Q \underset{˙}{\lor} V)$
23	12 22	mpd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (((U \in A \lor U = \underset{˙}{0}) \land U \underset{˙}{\leq} W) \land (V \in A \land V \underset{˙}{\leq} W)) \land U \neq V) \to P \underset{˙}{\lor} U \neq Q \underset{˙}{\lor} V$

Metamath Proof Explorer

Theorem lhp2at0ne

Proof