Metamath Proof Explorer

Theorem cdleme

Description: Lemma E in Crawley p. 113. If p,q are atoms not under hyperplane w, then there is a unique translation f such that f(p) = q. (Contributed by NM, 11-Apr-2013)

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

Proof

Step	Hyp	Ref	Expression
1		cdleme.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme.a	$⊢ A = Atoms (K)$
3		cdleme.h	$⊢ H = LHyp (K)$
4		cdleme.t	$⊢ T = LTrn (K) (W)$
5	1 2 3 4	cdleme50ex	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to \exists f \in T f (P) = Q$
6		simp11	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f \in T \land z \in T) \land (f (P) = Q \land z (P) = Q)) \to (K \in HL \land W \in H)$
7		simp2l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f \in T \land z \in T) \land (f (P) = Q \land z (P) = Q)) \to f \in T$
8		simp2r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f \in T \land z \in T) \land (f (P) = Q \land z (P) = Q)) \to z \in T$
9		simp12	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f \in T \land z \in T) \land (f (P) = Q \land z (P) = Q)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
10		eqtr3	$⊢ (f (P) = Q \land z (P) = Q) \to f (P) = z (P)$
11	10	3ad2ant3	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f \in T \land z \in T) \land (f (P) = Q \land z (P) = Q)) \to f (P) = z (P)$
12	1 2 3 4	cdlemd	$⊢ (((K \in HL \land W \in H) \land f \in T \land z \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land f (P) = z (P)) \to f = z$
13	6 7 8 9 11 12	syl311anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (f \in T \land z \in T) \land (f (P) = Q \land z (P) = Q)) \to f = z$
14	13	3exp	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to ((f \in T \land z \in T) \to ((f (P) = Q \land z (P) = Q) \to f = z))$
15	14	ralrimivv	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to \forall f \in T \forall z \in T ((f (P) = Q \land z (P) = Q) \to f = z)$
16		fveq1	$⊢ f = z \to f (P) = z (P)$
17	16	eqeq1d	$⊢ f = z \to (f (P) = Q \leftrightarrow z (P) = Q)$
18	17	reu4	$⊢ \exists! f \in T f (P) = Q \leftrightarrow (\exists f \in T f (P) = Q \land \forall f \in T \forall z \in T ((f (P) = Q \land z (P) = Q) \to f = z))$
19	5 15 18	sylanbrc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to \exists! f \in T f (P) = Q$