Metamath Proof Explorer


Theorem 2lplnmj

Description: The meet of two lattice planes is a lattice line iff their join is a lattice volume. (Contributed by NM, 13-Jul-2012)

Ref Expression
Hypotheses 2lplnmj.j ˙ = join K
2lplnmj.m ˙ = meet K
2lplnmj.n N = LLines K
2lplnmj.p P = LPlanes K
2lplnmj.v V = LVols K
Assertion 2lplnmj K HL X P Y P X ˙ Y N X ˙ Y V

Proof

Step Hyp Ref Expression
1 2lplnmj.j ˙ = join K
2 2lplnmj.m ˙ = meet K
3 2lplnmj.n N = LLines K
4 2lplnmj.p P = LPlanes K
5 2lplnmj.v V = LVols K
6 simp1 K HL X P Y P K HL
7 eqid Base K = Base K
8 7 4 lplnbase X P X Base K
9 8 3ad2ant2 K HL X P Y P X Base K
10 7 4 lplnbase Y P Y Base K
11 10 3ad2ant3 K HL X P Y P Y Base K
12 eqid K = K
13 7 1 2 12 cvrexch K HL X Base K Y Base K X ˙ Y K Y X K X ˙ Y
14 6 9 11 13 syl3anc K HL X P Y P X ˙ Y K Y X K X ˙ Y
15 simpl1 K HL X P Y P X ˙ Y N K HL
16 simpr K HL X P Y P X ˙ Y N X ˙ Y N
17 simpl3 K HL X P Y P X ˙ Y N Y P
18 hllat K HL K Lat
19 eqid K = K
20 7 19 2 latmle2 K Lat X Base K Y Base K X ˙ Y K Y
21 18 8 10 20 syl3an K HL X P Y P X ˙ Y K Y
22 21 adantr K HL X P Y P X ˙ Y N X ˙ Y K Y
23 19 12 3 4 llncvrlpln2 K HL X ˙ Y N Y P X ˙ Y K Y X ˙ Y K Y
24 15 16 17 22 23 syl31anc K HL X P Y P X ˙ Y N X ˙ Y K Y
25 simpl3 K HL X P Y P X ˙ Y K Y Y P
26 7 2 latmcl K Lat X Base K Y Base K X ˙ Y Base K
27 18 8 10 26 syl3an K HL X P Y P X ˙ Y Base K
28 6 27 11 3jca K HL X P Y P K HL X ˙ Y Base K Y Base K
29 7 12 3 4 llncvrlpln K HL X ˙ Y Base K Y Base K X ˙ Y K Y X ˙ Y N Y P
30 28 29 sylan K HL X P Y P X ˙ Y K Y X ˙ Y N Y P
31 25 30 mpbird K HL X P Y P X ˙ Y K Y X ˙ Y N
32 24 31 impbida K HL X P Y P X ˙ Y N X ˙ Y K Y
33 simpl1 K HL X P Y P X ˙ Y V K HL
34 simpl2 K HL X P Y P X ˙ Y V X P
35 simpr K HL X P Y P X ˙ Y V X ˙ Y V
36 7 19 1 latlej1 K Lat X Base K Y Base K X K X ˙ Y
37 18 8 10 36 syl3an K HL X P Y P X K X ˙ Y
38 37 adantr K HL X P Y P X ˙ Y V X K X ˙ Y
39 19 12 4 5 lplncvrlvol2 K HL X P X ˙ Y V X K X ˙ Y X K X ˙ Y
40 33 34 35 38 39 syl31anc K HL X P Y P X ˙ Y V X K X ˙ Y
41 simpl2 K HL X P Y P X K X ˙ Y X P
42 7 1 latjcl K Lat X Base K Y Base K X ˙ Y Base K
43 18 8 10 42 syl3an K HL X P Y P X ˙ Y Base K
44 6 9 43 3jca K HL X P Y P K HL X Base K X ˙ Y Base K
45 7 12 4 5 lplncvrlvol K HL X Base K X ˙ Y Base K X K X ˙ Y X P X ˙ Y V
46 44 45 sylan K HL X P Y P X K X ˙ Y X P X ˙ Y V
47 41 46 mpbid K HL X P Y P X K X ˙ Y X ˙ Y V
48 40 47 impbida K HL X P Y P X ˙ Y V X K X ˙ Y
49 14 32 48 3bitr4d K HL X P Y P X ˙ Y N X ˙ Y V