Metamath Proof Explorer


Theorem 2llnjN

Description: The join of two different lattice lines in a lattice plane equals the plane. (Contributed by NM, 4-Jul-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 2llnj.l ˙ = K
2llnj.j ˙ = join K
2llnj.n N = LLines K
2llnj.p P = LPlanes K
Assertion 2llnjN K HL X N Y N W P X ˙ W Y ˙ W X Y X ˙ Y = W

Proof

Step Hyp Ref Expression
1 2llnj.l ˙ = K
2 2llnj.j ˙ = join K
3 2llnj.n N = LLines K
4 2llnj.p P = LPlanes K
5 eqid Base K = Base K
6 eqid Atoms K = Atoms K
7 5 2 6 3 islln2 K HL X N X Base K q Atoms K r Atoms K q r X = q ˙ r
8 simpr X Base K q Atoms K r Atoms K q r X = q ˙ r q Atoms K r Atoms K q r X = q ˙ r
9 7 8 syl6bi K HL X N q Atoms K r Atoms K q r X = q ˙ r
10 5 2 6 3 islln2 K HL Y N Y Base K s Atoms K t Atoms K s t Y = s ˙ t
11 simpr Y Base K s Atoms K t Atoms K s t Y = s ˙ t s Atoms K t Atoms K s t Y = s ˙ t
12 10 11 syl6bi K HL Y N s Atoms K t Atoms K s t Y = s ˙ t
13 9 12 anim12d K HL X N Y N q Atoms K r Atoms K q r X = q ˙ r s Atoms K t Atoms K s t Y = s ˙ t
14 13 imp K HL X N Y N q Atoms K r Atoms K q r X = q ˙ r s Atoms K t Atoms K s t Y = s ˙ t
15 14 3adantr3 K HL X N Y N W P q Atoms K r Atoms K q r X = q ˙ r s Atoms K t Atoms K s t Y = s ˙ t
16 15 3adant3 K HL X N Y N W P X ˙ W Y ˙ W X Y q Atoms K r Atoms K q r X = q ˙ r s Atoms K t Atoms K s t Y = s ˙ t
17 simp2rr K HL X N Y N W P X ˙ W Y ˙ W X Y q Atoms K r Atoms K q r X = q ˙ r s Atoms K t Atoms K s t Y = s ˙ t X = q ˙ r
18 simp3rr K HL X N Y N W P X ˙ W Y ˙ W X Y q Atoms K r Atoms K q r X = q ˙ r s Atoms K t Atoms K s t Y = s ˙ t Y = s ˙ t
19 17 18 oveq12d K HL X N Y N W P X ˙ W Y ˙ W X Y q Atoms K r Atoms K q r X = q ˙ r s Atoms K t Atoms K s t Y = s ˙ t X ˙ Y = q ˙ r ˙ s ˙ t
20 simp13 K HL X N Y N W P X ˙ W Y ˙ W X Y q Atoms K r Atoms K q r X = q ˙ r s Atoms K t Atoms K s t Y = s ˙ t X ˙ W Y ˙ W X Y
21 breq1 X = q ˙ r X ˙ W q ˙ r ˙ W
22 neeq1 X = q ˙ r X Y q ˙ r Y
23 21 22 3anbi13d X = q ˙ r X ˙ W Y ˙ W X Y q ˙ r ˙ W Y ˙ W q ˙ r Y
24 breq1 Y = s ˙ t Y ˙ W s ˙ t ˙ W
25 neeq2 Y = s ˙ t q ˙ r Y q ˙ r s ˙ t
26 24 25 3anbi23d Y = s ˙ t q ˙ r ˙ W Y ˙ W q ˙ r Y q ˙ r ˙ W s ˙ t ˙ W q ˙ r s ˙ t
27 23 26 sylan9bb X = q ˙ r Y = s ˙ t X ˙ W Y ˙ W X Y q ˙ r ˙ W s ˙ t ˙ W q ˙ r s ˙ t
28 17 18 27 syl2anc K HL X N Y N W P X ˙ W Y ˙ W X Y q Atoms K r Atoms K q r X = q ˙ r s Atoms K t Atoms K s t Y = s ˙ t X ˙ W Y ˙ W X Y q ˙ r ˙ W s ˙ t ˙ W q ˙ r s ˙ t
29 20 28 mpbid K HL X N Y N W P X ˙ W Y ˙ W X Y q Atoms K r Atoms K q r X = q ˙ r s Atoms K t Atoms K s t Y = s ˙ t q ˙ r ˙ W s ˙ t ˙ W q ˙ r s ˙ t
30 simp11 K HL X N Y N W P X ˙ W Y ˙ W X Y q Atoms K r Atoms K q r X = q ˙ r s Atoms K t Atoms K s t Y = s ˙ t K HL
31 simp123 K HL X N Y N W P X ˙ W Y ˙ W X Y q Atoms K r Atoms K q r X = q ˙ r s Atoms K t Atoms K s t Y = s ˙ t W P
32 simp2ll K HL X N Y N W P X ˙ W Y ˙ W X Y q Atoms K r Atoms K q r X = q ˙ r s Atoms K t Atoms K s t Y = s ˙ t q Atoms K
33 simp2lr K HL X N Y N W P X ˙ W Y ˙ W X Y q Atoms K r Atoms K q r X = q ˙ r s Atoms K t Atoms K s t Y = s ˙ t r Atoms K
34 simp2rl K HL X N Y N W P X ˙ W Y ˙ W X Y q Atoms K r Atoms K q r X = q ˙ r s Atoms K t Atoms K s t Y = s ˙ t q r
35 simp3ll K HL X N Y N W P X ˙ W Y ˙ W X Y q Atoms K r Atoms K q r X = q ˙ r s Atoms K t Atoms K s t Y = s ˙ t s Atoms K
36 simp3lr K HL X N Y N W P X ˙ W Y ˙ W X Y q Atoms K r Atoms K q r X = q ˙ r s Atoms K t Atoms K s t Y = s ˙ t t Atoms K
37 simp3rl K HL X N Y N W P X ˙ W Y ˙ W X Y q Atoms K r Atoms K q r X = q ˙ r s Atoms K t Atoms K s t Y = s ˙ t s t
38 1 2 6 3 4 2llnjaN K HL W P q Atoms K r Atoms K q r s Atoms K t Atoms K s t q ˙ r ˙ W s ˙ t ˙ W q ˙ r s ˙ t q ˙ r ˙ s ˙ t = W
39 38 ex K HL W P q Atoms K r Atoms K q r s Atoms K t Atoms K s t q ˙ r ˙ W s ˙ t ˙ W q ˙ r s ˙ t q ˙ r ˙ s ˙ t = W
40 30 31 32 33 34 35 36 37 39 syl233anc K HL X N Y N W P X ˙ W Y ˙ W X Y q Atoms K r Atoms K q r X = q ˙ r s Atoms K t Atoms K s t Y = s ˙ t q ˙ r ˙ W s ˙ t ˙ W q ˙ r s ˙ t q ˙ r ˙ s ˙ t = W
41 29 40 mpd K HL X N Y N W P X ˙ W Y ˙ W X Y q Atoms K r Atoms K q r X = q ˙ r s Atoms K t Atoms K s t Y = s ˙ t q ˙ r ˙ s ˙ t = W
42 19 41 eqtrd K HL X N Y N W P X ˙ W Y ˙ W X Y q Atoms K r Atoms K q r X = q ˙ r s Atoms K t Atoms K s t Y = s ˙ t X ˙ Y = W
43 42 3exp K HL X N Y N W P X ˙ W Y ˙ W X Y q Atoms K r Atoms K q r X = q ˙ r s Atoms K t Atoms K s t Y = s ˙ t X ˙ Y = W
44 43 3impib K HL X N Y N W P X ˙ W Y ˙ W X Y q Atoms K r Atoms K q r X = q ˙ r s Atoms K t Atoms K s t Y = s ˙ t X ˙ Y = W
45 44 expd K HL X N Y N W P X ˙ W Y ˙ W X Y q Atoms K r Atoms K q r X = q ˙ r s Atoms K t Atoms K s t Y = s ˙ t X ˙ Y = W
46 45 rexlimdvv K HL X N Y N W P X ˙ W Y ˙ W X Y q Atoms K r Atoms K q r X = q ˙ r s Atoms K t Atoms K s t Y = s ˙ t X ˙ Y = W
47 46 3exp K HL X N Y N W P X ˙ W Y ˙ W X Y q Atoms K r Atoms K q r X = q ˙ r s Atoms K t Atoms K s t Y = s ˙ t X ˙ Y = W
48 47 rexlimdvv K HL X N Y N W P X ˙ W Y ˙ W X Y q Atoms K r Atoms K q r X = q ˙ r s Atoms K t Atoms K s t Y = s ˙ t X ˙ Y = W
49 48 impd K HL X N Y N W P X ˙ W Y ˙ W X Y q Atoms K r Atoms K q r X = q ˙ r s Atoms K t Atoms K s t Y = s ˙ t X ˙ Y = W
50 16 49 mpd K HL X N Y N W P X ˙ W Y ˙ W X Y X ˙ Y = W