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

Metamath Proof Explorer

Theorem cdlemksel

Description: Part of proof of Lemma K of Crawley p. 118. Conditions for the sigma(p) function to be a translation. TODO: combine cdlemki ? (Contributed by NM, 26-Jun-2013)

Ref Expression
Hypotheses cdlemk.b ⊢ B = Base K
cdlemk.l ⊢ ≤ ˙ = ≤ K
cdlemk.j ⊢ ∨ ˙ = join ⁡ K
cdlemk.a ⊢ A = Atoms ⁡ K
cdlemk.h ⊢ H = LHyp ⁡ K
cdlemk.t ⊢ T = LTrn ⁡ K ⁡ W
cdlemk.r ⊢ R = trL ⁡ K ⁡ W
cdlemk.m ⊢ ∧ ˙ = meet ⁡ K
cdlemk.s ⊢ S = f ∈ T ⟼ ι i ∈ T | i ⁡ P = P ∨ ˙ R ⁡ f ∧ ˙ N ⁡ P ∨ ˙ R ⁡ f ∘ F -1
Assertion cdlemksel ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ N ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ R ⁡ F = R ⁡ N ∧ F ≠ I ↾ B ∧ G ≠ I ↾ B ∧ R ⁡ G ≠ R ⁡ F → S ⁡ G ∈ T

Proof

Step Hyp Ref Expression
1 cdlemk.b ⊢ B = Base K
2 cdlemk.l ⊢ ≤ ˙ = ≤ K
3 cdlemk.j ⊢ ∨ ˙ = join ⁡ K
4 cdlemk.a ⊢ A = Atoms ⁡ K
5 cdlemk.h ⊢ H = LHyp ⁡ K
6 cdlemk.t ⊢ T = LTrn ⁡ K ⁡ W
7 cdlemk.r ⊢ R = trL ⁡ K ⁡ W
8 cdlemk.m ⊢ ∧ ˙ = meet ⁡ K
9 cdlemk.s ⊢ S = f ∈ T ⟼ ι i ∈ T | i ⁡ P = P ∨ ˙ R ⁡ f ∧ ˙ N ⁡ P ∨ ˙ R ⁡ f ∘ F -1
10 simp13 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ N ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ R ⁡ F = R ⁡ N ∧ F ≠ I ↾ B ∧ G ≠ I ↾ B ∧ R ⁡ G ≠ R ⁡ F → G ∈ T
11 1 2 3 4 5 6 7 8 9 cdlemksv ⊢ G ∈ T → S ⁡ G = ι i ∈ T | i ⁡ P = P ∨ ˙ R ⁡ G ∧ ˙ N ⁡ P ∨ ˙ R ⁡ G ∘ F -1
12 10 11 syl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ N ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ R ⁡ F = R ⁡ N ∧ F ≠ I ↾ B ∧ G ≠ I ↾ B ∧ R ⁡ G ≠ R ⁡ F → S ⁡ G = ι i ∈ T | i ⁡ P = P ∨ ˙ R ⁡ G ∧ ˙ N ⁡ P ∨ ˙ R ⁡ G ∘ F -1
13 eqid ⊢ ι i ∈ T | i ⁡ P = P ∨ ˙ R ⁡ G ∧ ˙ N ⁡ P ∨ ˙ R ⁡ G ∘ F -1 = ι i ∈ T | i ⁡ P = P ∨ ˙ R ⁡ G ∧ ˙ N ⁡ P ∨ ˙ R ⁡ G ∘ F -1
14 1 2 3 4 5 6 7 8 13 cdlemki ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ N ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ R ⁡ F = R ⁡ N ∧ F ≠ I ↾ B ∧ G ≠ I ↾ B ∧ R ⁡ G ≠ R ⁡ F → ι i ∈ T | i ⁡ P = P ∨ ˙ R ⁡ G ∧ ˙ N ⁡ P ∨ ˙ R ⁡ G ∘ F -1 ∈ T
15 12 14 eqeltrd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ N ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ R ⁡ F = R ⁡ N ∧ F ≠ I ↾ B ∧ G ≠ I ↾ B ∧ R ⁡ G ≠ R ⁡ F → S ⁡ G ∈ T