Metamath Proof Explorer

Theorem cdlemd

Description: If two translations agree at any atom not under the fiducial co-atom W , then they are equal. Lemma D in Crawley p. 113. (Contributed by NM, 2-Jun-2012)

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

Proof

Step	Hyp	Ref	Expression
1		cdlemd.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemd.a	$⊢ A = Atoms (K)$
3		cdlemd.h	$⊢ H = LHyp (K)$
4		cdlemd.t	$⊢ T = LTrn (K) (W)$
5		simpl11	$⊢ ((((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \land q \in A) \to (K \in HL \land W \in H)$
6		simpl12	$⊢ ((((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \land q \in A) \to F \in T$
7		simpl13	$⊢ ((((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \land q \in A) \to G \in T$
8	6 7	jca	$⊢ ((((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \land q \in A) \to (F \in T \land G \in T)$
9		simpr	$⊢ ((((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \land q \in A) \to q \in A$
10		simpl2	$⊢ ((((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \land q \in A) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
11		simpl3	$⊢ ((((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \land q \in A) \to F (P) = G (P)$
12		eqid	$⊢ join (K) = join (K)$
13	1 12 2 3 4	cdlemd9	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land q \in A) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \to F (q) = G (q)$
14	5 8 9 10 11 13	syl311anc	$⊢ ((((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \land q \in A) \to F (q) = G (q)$
15	14	ralrimiva	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \to \forall q \in A F (q) = G (q)$
16	2 3 4	ltrneq2	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to (\forall q \in A F (q) = G (q) \leftrightarrow F = G)$
17	16	3ad2ant1	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \to (\forall q \in A F (q) = G (q) \leftrightarrow F = G)$
18	15 17	mpbid	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) = G (P)) \to F = G$