Metamath Proof Explorer


Theorem cdleme35h2

Description: Part of proof of Lemma E in Crawley p. 113. Show that f(x) is one-to-one outside of P .\/ Q line. TODO: FIX COMMENT. (Contributed by NM, 18-Mar-2013)

Ref Expression
Hypotheses cdleme35.l ˙ = K
cdleme35.j ˙ = join K
cdleme35.m ˙ = meet K
cdleme35.a A = Atoms K
cdleme35.h H = LHyp K
cdleme35.u U = P ˙ Q ˙ W
cdleme35.f F = R ˙ U ˙ Q ˙ P ˙ R ˙ W
cdleme35.g G = S ˙ U ˙ Q ˙ P ˙ S ˙ W
Assertion cdleme35h2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q R S F G

Proof

Step Hyp Ref Expression
1 cdleme35.l ˙ = K
2 cdleme35.j ˙ = join K
3 cdleme35.m ˙ = meet K
4 cdleme35.a A = Atoms K
5 cdleme35.h H = LHyp K
6 cdleme35.u U = P ˙ Q ˙ W
7 cdleme35.f F = R ˙ U ˙ Q ˙ P ˙ R ˙ W
8 cdleme35.g G = S ˙ U ˙ Q ˙ P ˙ S ˙ W
9 simp33 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q R S R S
10 simpl1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q R S F = G K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
11 simpl2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q R S F = G P Q R A ¬ R ˙ W S A ¬ S ˙ W
12 simpl31 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q R S F = G ¬ R ˙ P ˙ Q
13 simpl32 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q R S F = G ¬ S ˙ P ˙ Q
14 simpr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q R S F = G F = G
15 1 2 3 4 5 6 7 8 cdleme35h K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q F = G R = S
16 10 11 12 13 14 15 syl113anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q R S F = G R = S
17 16 ex K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q R S F = G R = S
18 17 necon3d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q R S R S F G
19 9 18 mpd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q R S F G