Metamath Proof Explorer


Theorem llncvrlpln2

Description: A lattice line under a lattice plane is covered by it. (Contributed by NM, 24-Jun-2012)

Ref Expression
Hypotheses llncvrlpln2.l ˙ = K
llncvrlpln2.c C = K
llncvrlpln2.n N = LLines K
llncvrlpln2.p P = LPlanes K
Assertion llncvrlpln2 K HL X N Y P X ˙ Y X C Y

Proof

Step Hyp Ref Expression
1 llncvrlpln2.l ˙ = K
2 llncvrlpln2.c C = K
3 llncvrlpln2.n N = LLines K
4 llncvrlpln2.p P = LPlanes K
5 simpr K HL X N Y P X ˙ Y X ˙ Y
6 simpl1 K HL X N Y P X ˙ Y K HL
7 simpl3 K HL X N Y P X ˙ Y Y P
8 3 4 lplnnelln K HL Y P ¬ Y N
9 6 7 8 syl2anc K HL X N Y P X ˙ Y ¬ Y N
10 simpl2 K HL X N Y P X ˙ Y X N
11 eleq1 X = Y X N Y N
12 10 11 syl5ibcom K HL X N Y P X ˙ Y X = Y Y N
13 12 necon3bd K HL X N Y P X ˙ Y ¬ Y N X Y
14 9 13 mpd K HL X N Y P X ˙ Y X Y
15 eqid < K = < K
16 1 15 pltval K HL X N Y P X < K Y X ˙ Y X Y
17 16 adantr K HL X N Y P X ˙ Y X < K Y X ˙ Y X Y
18 5 14 17 mpbir2and K HL X N Y P X ˙ Y X < K Y
19 simpl1 K HL X N Y P X < K Y K HL
20 simpl2 K HL X N Y P X < K Y X N
21 eqid Base K = Base K
22 21 3 llnbase X N X Base K
23 20 22 syl K HL X N Y P X < K Y X Base K
24 simpl3 K HL X N Y P X < K Y Y P
25 21 4 lplnbase Y P Y Base K
26 24 25 syl K HL X N Y P X < K Y Y Base K
27 simpr K HL X N Y P X < K Y X < K Y
28 eqid join K = join K
29 eqid Atoms K = Atoms K
30 21 1 15 28 2 29 hlrelat3 K HL X Base K Y Base K X < K Y r Atoms K X C X join K r X join K r ˙ Y
31 19 23 26 27 30 syl31anc K HL X N Y P X < K Y r Atoms K X C X join K r X join K r ˙ Y
32 21 1 28 29 4 islpln2 K HL Y P Y Base K s Atoms K t Atoms K u Atoms K s t ¬ u ˙ s join K t Y = s join K t join K u
33 32 adantr K HL X N Y P Y Base K s Atoms K t Atoms K u Atoms K s t ¬ u ˙ s join K t Y = s join K t join K u
34 simp3 s t ¬ u ˙ s join K t Y = s join K t join K u Y = s join K t join K u
35 21 28 29 3 islln2 K HL X N X Base K p Atoms K q Atoms K p q X = p join K q
36 simp3l K HL p Atoms K q Atoms K p q X = p join K q s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y X C X join K r
37 simp3r K HL p Atoms K q Atoms K p q X = p join K q s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y X join K r ˙ Y
38 simp12r K HL p Atoms K q Atoms K p q X = p join K q s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y X = p join K q
39 38 oveq1d K HL p Atoms K q Atoms K p q X = p join K q s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y X join K r = p join K q join K r
40 simp22 K HL p Atoms K q Atoms K p q X = p join K q s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y Y = s join K t join K u
41 37 39 40 3brtr3d K HL p Atoms K q Atoms K p q X = p join K q s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y p join K q join K r ˙ s join K t join K u
42 simp111 K HL p Atoms K q Atoms K p q X = p join K q s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y K HL
43 simp112 K HL p Atoms K q Atoms K p q X = p join K q s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y p Atoms K
44 simp113 K HL p Atoms K q Atoms K p q X = p join K q s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y q Atoms K
45 simp23 K HL p Atoms K q Atoms K p q X = p join K q s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y r Atoms K
46 43 44 45 3jca K HL p Atoms K q Atoms K p q X = p join K q s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y p Atoms K q Atoms K r Atoms K
47 simp13l K HL p Atoms K q Atoms K p q X = p join K q s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y s Atoms K
48 simp13r K HL p Atoms K q Atoms K p q X = p join K q s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y t Atoms K
49 simp21 K HL p Atoms K q Atoms K p q X = p join K q s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y u Atoms K
50 47 48 49 3jca K HL p Atoms K q Atoms K p q X = p join K q s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y s Atoms K t Atoms K u Atoms K
51 36 38 39 3brtr3d K HL p Atoms K q Atoms K p q X = p join K q s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y p join K q C p join K q join K r
52 21 28 29 hlatjcl K HL p Atoms K q Atoms K p join K q Base K
53 42 43 44 52 syl3anc K HL p Atoms K q Atoms K p q X = p join K q s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y p join K q Base K
54 21 1 28 2 29 cvr1 K HL p join K q Base K r Atoms K ¬ r ˙ p join K q p join K q C p join K q join K r
55 42 53 45 54 syl3anc K HL p Atoms K q Atoms K p q X = p join K q s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y ¬ r ˙ p join K q p join K q C p join K q join K r
56 51 55 mpbird K HL p Atoms K q Atoms K p q X = p join K q s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y ¬ r ˙ p join K q
57 simp12l K HL p Atoms K q Atoms K p q X = p join K q s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y p q
58 1 28 29 3at K HL p Atoms K q Atoms K r Atoms K s Atoms K t Atoms K u Atoms K ¬ r ˙ p join K q p q p join K q join K r ˙ s join K t join K u p join K q join K r = s join K t join K u
59 42 46 50 56 57 58 syl32anc K HL p Atoms K q Atoms K p q X = p join K q s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y p join K q join K r ˙ s join K t join K u p join K q join K r = s join K t join K u
60 41 59 mpbid K HL p Atoms K q Atoms K p q X = p join K q s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y p join K q join K r = s join K t join K u
61 60 39 40 3eqtr4d K HL p Atoms K q Atoms K p q X = p join K q s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y X join K r = Y
62 36 61 breqtrd K HL p Atoms K q Atoms K p q X = p join K q s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y X C Y
63 62 3exp K HL p Atoms K q Atoms K p q X = p join K q s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y X C Y
64 63 3expd K HL p Atoms K q Atoms K p q X = p join K q s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y X C Y
65 64 3exp K HL p Atoms K q Atoms K p q X = p join K q s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y X C Y
66 65 3expib K HL p Atoms K q Atoms K p q X = p join K q s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y X C Y
67 66 rexlimdvv K HL p Atoms K q Atoms K p q X = p join K q s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y X C Y
68 67 adantld K HL X Base K p Atoms K q Atoms K p q X = p join K q s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y X C Y
69 35 68 sylbid K HL X N s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y X C Y
70 69 imp31 K HL X N s Atoms K t Atoms K u Atoms K Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y X C Y
71 34 70 syl7 K HL X N s Atoms K t Atoms K u Atoms K s t ¬ u ˙ s join K t Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y X C Y
72 71 rexlimdv K HL X N s Atoms K t Atoms K u Atoms K s t ¬ u ˙ s join K t Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y X C Y
73 72 rexlimdvva K HL X N s Atoms K t Atoms K u Atoms K s t ¬ u ˙ s join K t Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y X C Y
74 73 adantld K HL X N Y Base K s Atoms K t Atoms K u Atoms K s t ¬ u ˙ s join K t Y = s join K t join K u r Atoms K X C X join K r X join K r ˙ Y X C Y
75 33 74 sylbid K HL X N Y P r Atoms K X C X join K r X join K r ˙ Y X C Y
76 75 3impia K HL X N Y P r Atoms K X C X join K r X join K r ˙ Y X C Y
77 76 rexlimdv K HL X N Y P r Atoms K X C X join K r X join K r ˙ Y X C Y
78 77 imp K HL X N Y P r Atoms K X C X join K r X join K r ˙ Y X C Y
79 31 78 syldan K HL X N Y P X < K Y X C Y
80 18 79 syldan K HL X N Y P X ˙ Y X C Y