This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cdlemeiota

Description: A translation is uniquely determined by one of its values. (Contributed by NM, 18-Apr-2013)

Ref Expression
Hypotheses cdlemg1c.l ⊢ ≤ ˙ = ≤ K
cdlemg1c.a ⊢ A = Atoms ⁡ K
cdlemg1c.h ⊢ H = LHyp ⁡ K
cdlemg1c.t ⊢ T = LTrn ⁡ K ⁡ W
Assertion cdlemeiota ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ F ∈ T → F = ι f ∈ T | f ⁡ P = F ⁡ P

Proof

Step Hyp Ref Expression
1 cdlemg1c.l ⊢ ≤ ˙ = ≤ K
2 cdlemg1c.a ⊢ A = Atoms ⁡ K
3 cdlemg1c.h ⊢ H = LHyp ⁡ K
4 cdlemg1c.t ⊢ T = LTrn ⁡ K ⁡ W
5 eqidd ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ F ∈ T → F ⁡ P = F ⁡ P
6 simp3 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ F ∈ T → F ∈ T
7 1 2 3 4 ltrnel ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → F ⁡ P ∈ A ∧ ¬ F ⁡ P ≤ ˙ W
8 7 3com23 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ F ∈ T → F ⁡ P ∈ A ∧ ¬ F ⁡ P ≤ ˙ W
9 1 2 3 4 cdleme ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ F ⁡ P ∈ A ∧ ¬ F ⁡ P ≤ ˙ W → ∃! f ∈ T f ⁡ P = F ⁡ P
10 8 9 syld3an3 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ F ∈ T → ∃! f ∈ T f ⁡ P = F ⁡ P
11 fveq1 ⊢ f = F → f ⁡ P = F ⁡ P
12 11 eqeq1d ⊢ f = F → f ⁡ P = F ⁡ P ↔ F ⁡ P = F ⁡ P
13 12 riota2 ⊢ F ∈ T ∧ ∃! f ∈ T f ⁡ P = F ⁡ P → F ⁡ P = F ⁡ P ↔ ι f ∈ T | f ⁡ P = F ⁡ P = F
14 6 10 13 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ F ∈ T → F ⁡ P = F ⁡ P ↔ ι f ∈ T | f ⁡ P = F ⁡ P = F
15 5 14 mpbid ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ F ∈ T → ι f ∈ T | f ⁡ P = F ⁡ P = F
16 15 eqcomd ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ F ∈ T → F = ι f ∈ T | f ⁡ P = F ⁡ P