Metamath Proof Explorer


Theorem cdleme40n

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

Ref Expression
Hypotheses cdleme40.b B = Base K
cdleme40.l ˙ = K
cdleme40.j ˙ = join K
cdleme40.m ˙ = meet K
cdleme40.a A = Atoms K
cdleme40.h H = LHyp K
cdleme40.u U = P ˙ Q ˙ W
cdleme40.e E = t ˙ U ˙ Q ˙ P ˙ t ˙ W
cdleme40.g G = P ˙ Q ˙ E ˙ s ˙ t ˙ W
cdleme40.i I = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = G
cdleme40.n N = if s ˙ P ˙ Q I D
cdleme40a1.y Y = P ˙ Q ˙ E ˙ R ˙ t ˙ W
cdleme40a1.c C = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = Y
cdleme40.t T = v ˙ U ˙ Q ˙ P ˙ v ˙ W
cdleme40.f F = P ˙ Q ˙ T ˙ S ˙ v ˙ W
cdleme40a1.x X = P ˙ Q ˙ T ˙ u ˙ v ˙ W
cdleme40.o O = ι z B | v A ¬ v ˙ W ¬ v ˙ P ˙ Q z = X
cdleme40.v V = if u ˙ P ˙ Q O < ˙
cdleme40a1.z Z = ι z B | v A ¬ v ˙ W ¬ v ˙ P ˙ Q z = F
Assertion cdleme40n 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 N S / u V

Proof

Step Hyp Ref Expression
1 cdleme40.b B = Base K
2 cdleme40.l ˙ = K
3 cdleme40.j ˙ = join K
4 cdleme40.m ˙ = meet K
5 cdleme40.a A = Atoms K
6 cdleme40.h H = LHyp K
7 cdleme40.u U = P ˙ Q ˙ W
8 cdleme40.e E = t ˙ U ˙ Q ˙ P ˙ t ˙ W
9 cdleme40.g G = P ˙ Q ˙ E ˙ s ˙ t ˙ W
10 cdleme40.i I = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = G
11 cdleme40.n N = if s ˙ P ˙ Q I D
12 cdleme40a1.y Y = P ˙ Q ˙ E ˙ R ˙ t ˙ W
13 cdleme40a1.c C = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = Y
14 cdleme40.t T = v ˙ U ˙ Q ˙ P ˙ v ˙ W
15 cdleme40.f F = P ˙ Q ˙ T ˙ S ˙ v ˙ W
16 cdleme40a1.x X = P ˙ Q ˙ T ˙ u ˙ v ˙ W
17 cdleme40.o O = ι z B | v A ¬ v ˙ W ¬ v ˙ P ˙ Q z = X
18 cdleme40.v V = if u ˙ P ˙ Q O < ˙
19 cdleme40a1.z Z = ι z B | v A ¬ v ˙ W ¬ v ˙ P ˙ Q z = F
20 1 fvexi B V
21 nfv v 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
22 nfcv _ v R / s N
23 nfra1 v v A ¬ v ˙ W ¬ v ˙ P ˙ Q z = F
24 nfcv _ v B
25 23 24 nfriota _ v ι z B | v A ¬ v ˙ W ¬ v ˙ P ˙ Q z = F
26 19 25 nfcxfr _ v Z
27 22 26 nfne v R / s N Z
28 27 a1i 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 v R / s N Z
29 19 a1i 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 Z = ι z B | v A ¬ v ˙ W ¬ v ˙ P ˙ Q z = F
30 neeq2 F = Z R / s N F R / s N Z
31 30 adantl 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 = Z R / s N F R / s N Z
32 simpl11 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 v A ¬ v ˙ W ¬ v ˙ P ˙ Q K HL W H
33 simpl12 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 v A ¬ v ˙ W ¬ v ˙ P ˙ Q P A ¬ P ˙ W
34 simpl13 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 v A ¬ v ˙ W ¬ v ˙ P ˙ Q Q A ¬ Q ˙ W
35 simpl21 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 v A ¬ v ˙ W ¬ v ˙ P ˙ Q P Q
36 simpl22 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 v A ¬ v ˙ W ¬ v ˙ P ˙ Q R A ¬ R ˙ W
37 simpl23 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 v A ¬ v ˙ W ¬ v ˙ P ˙ Q S A ¬ S ˙ W
38 simpl3 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 v A ¬ v ˙ W ¬ v ˙ P ˙ Q R ˙ P ˙ Q S ˙ P ˙ Q R S
39 simprl 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 v A ¬ v ˙ W ¬ v ˙ P ˙ Q v A
40 simprrl 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 v A ¬ v ˙ W ¬ v ˙ P ˙ Q ¬ v ˙ W
41 simprrr 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 v A ¬ v ˙ W ¬ v ˙ P ˙ Q ¬ v ˙ P ˙ Q
42 39 40 41 3jca 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 v A ¬ v ˙ W ¬ v ˙ P ˙ Q v A ¬ v ˙ W ¬ v ˙ P ˙ Q
43 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 cdleme40m 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 v A ¬ v ˙ W ¬ v ˙ P ˙ Q R / s N F
44 32 33 34 35 36 37 38 42 43 syl332anc 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 v A ¬ v ˙ W ¬ v ˙ P ˙ Q R / s N F
45 44 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 v A ¬ v ˙ W ¬ v ˙ P ˙ Q R / s N F
46 simp1 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 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
47 simp23l 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 S A
48 simp23r 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 ¬ S ˙ W
49 simp21 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 P Q
50 simp32 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 S ˙ P ˙ Q
51 1 2 3 4 5 6 7 14 15 19 cdleme25cl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W P Q S ˙ P ˙ Q Z B
52 46 47 48 49 50 51 syl122anc 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 Z B
53 simp11 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 K HL W H
54 simp12 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 P A ¬ P ˙ W
55 simp13 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 Q A ¬ Q ˙ W
56 2 3 5 6 cdlemb2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q v A ¬ v ˙ W ¬ v ˙ P ˙ Q
57 53 54 55 49 56 syl121anc 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 v A ¬ v ˙ W ¬ v ˙ P ˙ Q
58 21 28 29 31 45 52 57 riotasv3d 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 B V R / s N Z
59 20 58 mpan2 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 N Z
60 16 17 18 15 19 cdleme31sn1c S A S ˙ P ˙ Q S / u V = Z
61 47 50 60 syl2anc 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 S / u V = Z
62 59 61 neeqtrrd 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 N S / u V