ltrneq

Description: The equality of two translations is determined by their equality at atoms not under co-atom W . (Contributed by NM, 20-Jun-2013)

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

Proof

Step	Hyp	Ref	Expression
1		ltrne.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		ltrne.a	$⊢ A = Atoms (K)$
3		ltrne.h	$⊢ H = LHyp (K)$
4		ltrne.t	$⊢ T = LTrn (K) (W)$
5		simp11	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land p \in A \land p \underset{˙}{\leq} W) \to (K \in HL \land W \in H)$
6		simp12	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land p \in A \land p \underset{˙}{\leq} W) \to F \in T$
7		eqid	$⊢ {Base}_{K} = {Base}_{K}$
8	7 2	atbase	$⊢ p \in A \to p \in {Base}_{K}$
9	8	3ad2ant2	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land p \in A \land p \underset{˙}{\leq} W) \to p \in {Base}_{K}$
10		simp3	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land p \in A \land p \underset{˙}{\leq} W) \to p \underset{˙}{\leq} W$
11	7 1 3 4	ltrnval1	$⊢ ((K \in HL \land W \in H) \land F \in T \land (p \in {Base}_{K} \land p \underset{˙}{\leq} W)) \to F (p) = p$
12	5 6 9 10 11	syl112anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land p \in A \land p \underset{˙}{\leq} W) \to F (p) = p$
13		simp13	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land p \in A \land p \underset{˙}{\leq} W) \to G \in T$
14	7 1 3 4	ltrnval1	$⊢ ((K \in HL \land W \in H) \land G \in T \land (p \in {Base}_{K} \land p \underset{˙}{\leq} W)) \to G (p) = p$
15	5 13 9 10 14	syl112anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land p \in A \land p \underset{˙}{\leq} W) \to G (p) = p$
16	12 15	eqtr4d	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land p \in A \land p \underset{˙}{\leq} W) \to F (p) = G (p)$
17	16	3expia	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land p \in A) \to (p \underset{˙}{\leq} W \to F (p) = G (p))$
18		pm2.61	$⊢ (p \underset{˙}{\leq} W \to F (p) = G (p)) \to ((\neg p \underset{˙}{\leq} W \to F (p) = G (p)) \to F (p) = G (p))$
19	17 18	syl	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land p \in A) \to ((\neg p \underset{˙}{\leq} W \to F (p) = G (p)) \to F (p) = G (p))$
20		re1tbw2	$⊢ F (p) = G (p) \to (\neg p \underset{˙}{\leq} W \to F (p) = G (p))$
21	19 20	impbid1	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land p \in A) \to ((\neg p \underset{˙}{\leq} W \to F (p) = G (p)) \leftrightarrow F (p) = G (p))$
22	21	ralbidva	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to (\forall p \in A (\neg p \underset{˙}{\leq} W \to F (p) = G (p)) \leftrightarrow \forall p \in A F (p) = G (p))$
23	2 3 4	ltrneq2	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to (\forall p \in A F (p) = G (p) \leftrightarrow F = G)$
24	22 23	bitrd	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to (\forall p \in A (\neg p \underset{˙}{\leq} W \to F (p) = G (p)) \leftrightarrow F = G)$

Metamath Proof Explorer

Theorem ltrneq

Proof