Metamath Proof Explorer

Theorem ltrnatlw

Description: If the value of an atom equals the atom in a non-identity translation, the atom is under the fiducial hyperplane. (Contributed by NM, 15-May-2013)

		Ref	Expression
	Hypotheses	ltrn2eq.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		ltrn2eq.a	$⊢ A = Atoms (K)$
		ltrn2eq.h	$⊢ H = LHyp (K)$
		ltrn2eq.t	$⊢ T = LTrn (K) (W)$
	Assertion	ltrnatlw	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (F (P) \neq P \land F (Q) = Q)) \to Q \underset{˙}{\leq} W$

Proof

Step	Hyp	Ref	Expression
1		ltrn2eq.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		ltrn2eq.a	$⊢ A = Atoms (K)$
3		ltrn2eq.h	$⊢ H = LHyp (K)$
4		ltrn2eq.t	$⊢ T = LTrn (K) (W)$
5		simp3r	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (F (P) \neq P \land F (Q) = Q)) \to F (Q) = Q$
6		simpl1	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (F (P) \neq P \land F (Q) = Q)) \land \neg Q \underset{˙}{\leq} W) \to (K \in HL \land W \in H)$
7		simpl21	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (F (P) \neq P \land F (Q) = Q)) \land \neg Q \underset{˙}{\leq} W) \to F \in T$
8		simpl22	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (F (P) \neq P \land F (Q) = Q)) \land \neg Q \underset{˙}{\leq} W) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
9		simpl23	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (F (P) \neq P \land F (Q) = Q)) \land \neg Q \underset{˙}{\leq} W) \to Q \in A$
10		simpr	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (F (P) \neq P \land F (Q) = Q)) \land \neg Q \underset{˙}{\leq} W) \to \neg Q \underset{˙}{\leq} W$
11	9 10	jca	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (F (P) \neq P \land F (Q) = Q)) \land \neg Q \underset{˙}{\leq} W) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
12		simpl3l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (F (P) \neq P \land F (Q) = Q)) \land \neg Q \underset{˙}{\leq} W) \to F (P) \neq P$
13	1 2 3 4	ltrnatneq	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F (P) \neq P) \to F (Q) \neq Q$
14	6 7 8 11 12 13	syl131anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (F (P) \neq P \land F (Q) = Q)) \land \neg Q \underset{˙}{\leq} W) \to F (Q) \neq Q$
15	14	ex	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (F (P) \neq P \land F (Q) = Q)) \to (\neg Q \underset{˙}{\leq} W \to F (Q) \neq Q)$
16	15	necon4bd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (F (P) \neq P \land F (Q) = Q)) \to (F (Q) = Q \to Q \underset{˙}{\leq} W)$
17	5 16	mpd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (F (P) \neq P \land F (Q) = Q)) \to Q \underset{˙}{\leq} W$