cdlemg18a

Description: Show two lines are different. TODO: fix comment. (Contributed by NM, 14-May-2013)

	Ref	Expression
Hypotheses	cdlemg12.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemg12.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemg12.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemg12.a	$⊢ A = Atoms (K)$
	cdlemg12.h	$⊢ H = LHyp (K)$
	cdlemg12.t	$⊢ T = LTrn (K) (W)$
	cdlemg12b.r	$⊢ R = trL (K) (W)$
Assertion	cdlemg18a	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land F \in T) \land (P \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to P \underset{˙}{\lor} F (Q) \neq Q \underset{˙}{\lor} F (P)$

Proof

Step	Hyp	Ref	Expression
1		cdlemg12.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemg12.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdlemg12.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdlemg12.a	$⊢ A = Atoms (K)$
5		cdlemg12.h	$⊢ H = LHyp (K)$
6		cdlemg12.t	$⊢ T = LTrn (K) (W)$
7		cdlemg12b.r	$⊢ R = trL (K) (W)$
8		simp3r	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land F \in T) \land (P \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q$
9		simpl1l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land Q \in A \land F \in T) \land (P \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \land P \underset{˙}{\lor} F (Q) = Q \underset{˙}{\lor} F (P)) \to K \in HL$
10		simpl21	$⊢ (((K \in HL \land W \in H) \land (P \in A \land Q \in A \land F \in T) \land (P \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \land P \underset{˙}{\lor} F (Q) = Q \underset{˙}{\lor} F (P)) \to P \in A$
11		simpl1	$⊢ (((K \in HL \land W \in H) \land (P \in A \land Q \in A \land F \in T) \land (P \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \land P \underset{˙}{\lor} F (Q) = Q \underset{˙}{\lor} F (P)) \to (K \in HL \land W \in H)$
12		simpl23	$⊢ (((K \in HL \land W \in H) \land (P \in A \land Q \in A \land F \in T) \land (P \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \land P \underset{˙}{\lor} F (Q) = Q \underset{˙}{\lor} F (P)) \to F \in T$
13		simpl22	$⊢ (((K \in HL \land W \in H) \land (P \in A \land Q \in A \land F \in T) \land (P \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \land P \underset{˙}{\lor} F (Q) = Q \underset{˙}{\lor} F (P)) \to Q \in A$
14	1 4 5 6	ltrnat	$⊢ ((K \in HL \land W \in H) \land F \in T \land Q \in A) \to F (Q) \in A$
15	11 12 13 14	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land Q \in A \land F \in T) \land (P \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \land P \underset{˙}{\lor} F (Q) = Q \underset{˙}{\lor} F (P)) \to F (Q) \in A$
16	1 4 5 6	ltrnat	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in A) \to F (P) \in A$
17	11 12 10 16	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land Q \in A \land F \in T) \land (P \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \land P \underset{˙}{\lor} F (Q) = Q \underset{˙}{\lor} F (P)) \to F (P) \in A$
18		simpl3l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land Q \in A \land F \in T) \land (P \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \land P \underset{˙}{\lor} F (Q) = Q \underset{˙}{\lor} F (P)) \to P \neq Q$
19	4 5 6	ltrn11at	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land Q \in A \land P \neq Q)) \to F (P) \neq F (Q)$
20	11 12 10 13 18 19	syl113anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land Q \in A \land F \in T) \land (P \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \land P \underset{˙}{\lor} F (Q) = Q \underset{˙}{\lor} F (P)) \to F (P) \neq F (Q)$
21	20	necomd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land Q \in A \land F \in T) \land (P \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \land P \underset{˙}{\lor} F (Q) = Q \underset{˙}{\lor} F (P)) \to F (Q) \neq F (P)$
22		simpr	$⊢ (((K \in HL \land W \in H) \land (P \in A \land Q \in A \land F \in T) \land (P \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \land P \underset{˙}{\lor} F (Q) = Q \underset{˙}{\lor} F (P)) \to P \underset{˙}{\lor} F (Q) = Q \underset{˙}{\lor} F (P)$
23	2 4	hlatexch4	$⊢ ((K \in HL \land P \in A \land F (Q) \in A) \land (Q \in A \land F (P) \in A) \land (P \neq Q \land F (Q) \neq F (P) \land P \underset{˙}{\lor} F (Q) = Q \underset{˙}{\lor} F (P))) \to P \underset{˙}{\lor} Q = F (Q) \underset{˙}{\lor} F (P)$
24	9 10 15 13 17 18 21 22 23	syl323anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land Q \in A \land F \in T) \land (P \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \land P \underset{˙}{\lor} F (Q) = Q \underset{˙}{\lor} F (P)) \to P \underset{˙}{\lor} Q = F (Q) \underset{˙}{\lor} F (P)$
25	24	eqcomd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land Q \in A \land F \in T) \land (P \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \land P \underset{˙}{\lor} F (Q) = Q \underset{˙}{\lor} F (P)) \to F (Q) \underset{˙}{\lor} F (P) = P \underset{˙}{\lor} Q$
26	25	ex	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land F \in T) \land (P \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to (P \underset{˙}{\lor} F (Q) = Q \underset{˙}{\lor} F (P) \to F (Q) \underset{˙}{\lor} F (P) = P \underset{˙}{\lor} Q)$
27	26	necon3d	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land F \in T) \land (P \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to (F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q \to P \underset{˙}{\lor} F (Q) \neq Q \underset{˙}{\lor} F (P))$
28	8 27	mpd	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land F \in T) \land (P \neq Q \land F (Q) \underset{˙}{\lor} F (P) \neq P \underset{˙}{\lor} Q)) \to P \underset{˙}{\lor} F (Q) \neq Q \underset{˙}{\lor} F (P)$

Metamath Proof Explorer

Theorem cdlemg18a

Proof