Metamath Proof Explorer


Theorem islpln5

Description: The predicate "is a lattice plane" in terms of atoms. (Contributed by NM, 24-Jun-2012)

Ref Expression
Hypotheses islpln5.b B = Base K
islpln5.l ˙ = K
islpln5.j ˙ = join K
islpln5.a A = Atoms K
islpln5.p P = LPlanes K
Assertion islpln5 K HL X B X P p A q A r A p q ¬ r ˙ p ˙ q X = p ˙ q ˙ r

Proof

Step Hyp Ref Expression
1 islpln5.b B = Base K
2 islpln5.l ˙ = K
3 islpln5.j ˙ = join K
4 islpln5.a A = Atoms K
5 islpln5.p P = LPlanes K
6 eqid LLines K = LLines K
7 1 2 3 4 6 5 islpln3 K HL X B X P y LLines K r A ¬ r ˙ y X = y ˙ r
8 df-rex y LLines K r A ¬ r ˙ y X = y ˙ r y y LLines K r A ¬ r ˙ y X = y ˙ r
9 r19.41v r A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q r A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q
10 an13 r A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q y = p ˙ q p q r A y B ¬ r ˙ y X = y ˙ r
11 9 10 bitri r A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q y = p ˙ q p q r A y B ¬ r ˙ y X = y ˙ r
12 11 exbii y r A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q y y = p ˙ q p q r A y B ¬ r ˙ y X = y ˙ r
13 ovex p ˙ q V
14 an12 p q y B ¬ r ˙ y X = y ˙ r y B p q ¬ r ˙ y X = y ˙ r
15 eleq1 y = p ˙ q y B p ˙ q B
16 breq2 y = p ˙ q r ˙ y r ˙ p ˙ q
17 16 notbid y = p ˙ q ¬ r ˙ y ¬ r ˙ p ˙ q
18 oveq1 y = p ˙ q y ˙ r = p ˙ q ˙ r
19 18 eqeq2d y = p ˙ q X = y ˙ r X = p ˙ q ˙ r
20 17 19 anbi12d y = p ˙ q ¬ r ˙ y X = y ˙ r ¬ r ˙ p ˙ q X = p ˙ q ˙ r
21 20 anbi2d y = p ˙ q p q ¬ r ˙ y X = y ˙ r p q ¬ r ˙ p ˙ q X = p ˙ q ˙ r
22 3anass p q ¬ r ˙ p ˙ q X = p ˙ q ˙ r p q ¬ r ˙ p ˙ q X = p ˙ q ˙ r
23 21 22 bitr4di y = p ˙ q p q ¬ r ˙ y X = y ˙ r p q ¬ r ˙ p ˙ q X = p ˙ q ˙ r
24 15 23 anbi12d y = p ˙ q y B p q ¬ r ˙ y X = y ˙ r p ˙ q B p q ¬ r ˙ p ˙ q X = p ˙ q ˙ r
25 14 24 syl5bb y = p ˙ q p q y B ¬ r ˙ y X = y ˙ r p ˙ q B p q ¬ r ˙ p ˙ q X = p ˙ q ˙ r
26 25 rexbidv y = p ˙ q r A p q y B ¬ r ˙ y X = y ˙ r r A p ˙ q B p q ¬ r ˙ p ˙ q X = p ˙ q ˙ r
27 r19.42v r A p q y B ¬ r ˙ y X = y ˙ r p q r A y B ¬ r ˙ y X = y ˙ r
28 r19.42v r A p ˙ q B p q ¬ r ˙ p ˙ q X = p ˙ q ˙ r p ˙ q B r A p q ¬ r ˙ p ˙ q X = p ˙ q ˙ r
29 26 27 28 3bitr3g y = p ˙ q p q r A y B ¬ r ˙ y X = y ˙ r p ˙ q B r A p q ¬ r ˙ p ˙ q X = p ˙ q ˙ r
30 13 29 ceqsexv y y = p ˙ q p q r A y B ¬ r ˙ y X = y ˙ r p ˙ q B r A p q ¬ r ˙ p ˙ q X = p ˙ q ˙ r
31 12 30 bitri y r A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q p ˙ q B r A p q ¬ r ˙ p ˙ q X = p ˙ q ˙ r
32 simpll K HL X B p A q A K HL
33 simprl K HL X B p A q A p A
34 simprr K HL X B p A q A q A
35 1 3 4 hlatjcl K HL p A q A p ˙ q B
36 32 33 34 35 syl3anc K HL X B p A q A p ˙ q B
37 36 biantrurd K HL X B p A q A r A p q ¬ r ˙ p ˙ q X = p ˙ q ˙ r p ˙ q B r A p q ¬ r ˙ p ˙ q X = p ˙ q ˙ r
38 31 37 bitr4id K HL X B p A q A y r A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q r A p q ¬ r ˙ p ˙ q X = p ˙ q ˙ r
39 38 2rexbidva K HL X B p A q A y r A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q p A q A r A p q ¬ r ˙ p ˙ q X = p ˙ q ˙ r
40 rexcom4 q A y r A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q y q A r A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q
41 40 rexbii p A q A y r A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q p A y q A r A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q
42 rexcom4 p A y q A r A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q y p A q A r A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q
43 41 42 bitri p A q A y r A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q y p A q A r A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q
44 39 43 bitr3di K HL X B p A q A r A p q ¬ r ˙ p ˙ q X = p ˙ q ˙ r y p A q A r A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q
45 rexcom q A r A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q r A q A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q
46 45 rexbii p A q A r A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q p A r A q A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q
47 rexcom p A r A q A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q r A p A q A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q
48 46 47 bitri p A q A r A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q r A p A q A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q
49 1 3 4 6 islln2 K HL y LLines K y B p A q A p q y = p ˙ q
50 49 adantr K HL X B y LLines K y B p A q A p q y = p ˙ q
51 50 anbi1d K HL X B y LLines K ¬ r ˙ y X = y ˙ r y B p A q A p q y = p ˙ q ¬ r ˙ y X = y ˙ r
52 r19.42v p A y B ¬ r ˙ y X = y ˙ r q A p q y = p ˙ q y B ¬ r ˙ y X = y ˙ r p A q A p q y = p ˙ q
53 r19.42v q A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q y B ¬ r ˙ y X = y ˙ r q A p q y = p ˙ q
54 53 rexbii p A q A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q p A y B ¬ r ˙ y X = y ˙ r q A p q y = p ˙ q
55 an32 y B p A q A p q y = p ˙ q ¬ r ˙ y X = y ˙ r y B ¬ r ˙ y X = y ˙ r p A q A p q y = p ˙ q
56 52 54 55 3bitr4ri y B p A q A p q y = p ˙ q ¬ r ˙ y X = y ˙ r p A q A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q
57 51 56 bitrdi K HL X B y LLines K ¬ r ˙ y X = y ˙ r p A q A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q
58 57 rexbidv K HL X B r A y LLines K ¬ r ˙ y X = y ˙ r r A p A q A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q
59 48 58 bitr4id K HL X B p A q A r A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q r A y LLines K ¬ r ˙ y X = y ˙ r
60 r19.42v r A y LLines K ¬ r ˙ y X = y ˙ r y LLines K r A ¬ r ˙ y X = y ˙ r
61 59 60 bitrdi K HL X B p A q A r A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q y LLines K r A ¬ r ˙ y X = y ˙ r
62 61 exbidv K HL X B y p A q A r A y B ¬ r ˙ y X = y ˙ r p q y = p ˙ q y y LLines K r A ¬ r ˙ y X = y ˙ r
63 44 62 bitrd K HL X B p A q A r A p q ¬ r ˙ p ˙ q X = p ˙ q ˙ r y y LLines K r A ¬ r ˙ y X = y ˙ r
64 8 63 bitr4id K HL X B y LLines K r A ¬ r ˙ y X = y ˙ r p A q A r A p q ¬ r ˙ p ˙ q X = p ˙ q ˙ r
65 7 64 bitrd K HL X B X P p A q A r A p q ¬ r ˙ p ˙ q X = p ˙ q ˙ r