Metamath Proof Explorer


Theorem ltrnatlw

Description: If the value of an atom equals the atom in a non-identity translation, the atom is under the fiducial hyperplane. (Contributed by NM, 15-May-2013)

Ref Expression
Hypotheses ltrn2eq.l ˙ = K
ltrn2eq.a A = Atoms K
ltrn2eq.h H = LHyp K
ltrn2eq.t T = LTrn K W
Assertion ltrnatlw K HL W H F T P A ¬ P ˙ W Q A F P P F Q = Q Q ˙ W

Proof

Step Hyp Ref Expression
1 ltrn2eq.l ˙ = K
2 ltrn2eq.a A = Atoms K
3 ltrn2eq.h H = LHyp K
4 ltrn2eq.t T = LTrn K W
5 simp3r K HL W H F T P A ¬ P ˙ W Q A F P P F Q = Q F Q = Q
6 simpl1 K HL W H F T P A ¬ P ˙ W Q A F P P F Q = Q ¬ Q ˙ W K HL W H
7 simpl21 K HL W H F T P A ¬ P ˙ W Q A F P P F Q = Q ¬ Q ˙ W F T
8 simpl22 K HL W H F T P A ¬ P ˙ W Q A F P P F Q = Q ¬ Q ˙ W P A ¬ P ˙ W
9 simpl23 K HL W H F T P A ¬ P ˙ W Q A F P P F Q = Q ¬ Q ˙ W Q A
10 simpr K HL W H F T P A ¬ P ˙ W Q A F P P F Q = Q ¬ Q ˙ W ¬ Q ˙ W
11 9 10 jca K HL W H F T P A ¬ P ˙ W Q A F P P F Q = Q ¬ Q ˙ W Q A ¬ Q ˙ W
12 simpl3l K HL W H F T P A ¬ P ˙ W Q A F P P F Q = Q ¬ Q ˙ W F P P
13 1 2 3 4 ltrnatneq K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W F P P F Q Q
14 6 7 8 11 12 13 syl131anc K HL W H F T P A ¬ P ˙ W Q A F P P F Q = Q ¬ Q ˙ W F Q Q
15 14 ex K HL W H F T P A ¬ P ˙ W Q A F P P F Q = Q ¬ Q ˙ W F Q Q
16 15 necon4bd K HL W H F T P A ¬ P ˙ W Q A F P P F Q = Q F Q = Q Q ˙ W
17 5 16 mpd K HL W H F T P A ¬ P ˙ W Q A F P P F Q = Q Q ˙ W