Metamath Proof Explorer


Theorem islvol5

Description: The predicate "is a 3-dim lattice volume" in terms of atoms. (Contributed by NM, 1-Jul-2012)

Ref Expression
Hypotheses islvol5.b B = Base K
islvol5.l ˙ = K
islvol5.j ˙ = join K
islvol5.a A = Atoms K
islvol5.v V = LVols K
Assertion islvol5 K HL X B X V p A q A r A s A p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s

Proof

Step Hyp Ref Expression
1 islvol5.b B = Base K
2 islvol5.l ˙ = K
3 islvol5.j ˙ = join K
4 islvol5.a A = Atoms K
5 islvol5.v V = LVols K
6 eqid LPlanes K = LPlanes K
7 1 2 3 4 6 5 islvol3 K HL X B X V y LPlanes K s A ¬ s ˙ y X = y ˙ s
8 df-rex y LPlanes K s A ¬ s ˙ y X = y ˙ s y y LPlanes K s A ¬ s ˙ y X = y ˙ s
9 r19.41v s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r
10 df-3an p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r
11 10 anbi2i s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r
12 an13 s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r y = p ˙ q ˙ r p q ¬ r ˙ p ˙ q s A y B ¬ s ˙ y X = y ˙ s
13 11 12 bitri s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r y = p ˙ q ˙ r p q ¬ r ˙ p ˙ q s A y B ¬ s ˙ y X = y ˙ s
14 9 13 bitri s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r y = p ˙ q ˙ r p q ¬ r ˙ p ˙ q s A y B ¬ s ˙ y X = y ˙ s
15 14 exbii y s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r y y = p ˙ q ˙ r p q ¬ r ˙ p ˙ q s A y B ¬ s ˙ y X = y ˙ s
16 ovex p ˙ q ˙ r V
17 an12 p q ¬ r ˙ p ˙ q y B ¬ s ˙ y X = y ˙ s y B p q ¬ r ˙ p ˙ q ¬ s ˙ y X = y ˙ s
18 eleq1 y = p ˙ q ˙ r y B p ˙ q ˙ r B
19 breq2 y = p ˙ q ˙ r s ˙ y s ˙ p ˙ q ˙ r
20 19 notbid y = p ˙ q ˙ r ¬ s ˙ y ¬ s ˙ p ˙ q ˙ r
21 oveq1 y = p ˙ q ˙ r y ˙ s = p ˙ q ˙ r ˙ s
22 21 eqeq2d y = p ˙ q ˙ r X = y ˙ s X = p ˙ q ˙ r ˙ s
23 20 22 anbi12d y = p ˙ q ˙ r ¬ s ˙ y X = y ˙ s ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s
24 23 anbi2d y = p ˙ q ˙ r p q ¬ r ˙ p ˙ q ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s
25 anass p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s
26 df-3an p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r
27 26 bicomi p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r
28 27 anbi1i p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s
29 25 28 bitr3i p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s
30 24 29 bitrdi y = p ˙ q ˙ r p q ¬ r ˙ p ˙ q ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s
31 18 30 anbi12d y = p ˙ q ˙ r y B p q ¬ r ˙ p ˙ q ¬ s ˙ y X = y ˙ s p ˙ q ˙ r B p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s
32 17 31 syl5bb y = p ˙ q ˙ r p q ¬ r ˙ p ˙ q y B ¬ s ˙ y X = y ˙ s p ˙ q ˙ r B p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s
33 32 rexbidv y = p ˙ q ˙ r s A p q ¬ r ˙ p ˙ q y B ¬ s ˙ y X = y ˙ s s A p ˙ q ˙ r B p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s
34 r19.42v s A p q ¬ r ˙ p ˙ q y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q s A y B ¬ s ˙ y X = y ˙ s
35 r19.42v s A p ˙ q ˙ r B p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s p ˙ q ˙ r B s A p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s
36 33 34 35 3bitr3g y = p ˙ q ˙ r p q ¬ r ˙ p ˙ q s A y B ¬ s ˙ y X = y ˙ s p ˙ q ˙ r B s A p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s
37 16 36 ceqsexv y y = p ˙ q ˙ r p q ¬ r ˙ p ˙ q s A y B ¬ s ˙ y X = y ˙ s p ˙ q ˙ r B s A p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s
38 15 37 bitri y s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r p ˙ q ˙ r B s A p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s
39 hllat K HL K Lat
40 39 ad3antrrr K HL X B p A q A r A K Lat
41 simplll K HL X B p A q A r A K HL
42 simplrl K HL X B p A q A r A p A
43 simplrr K HL X B p A q A r A q A
44 1 3 4 hlatjcl K HL p A q A p ˙ q B
45 41 42 43 44 syl3anc K HL X B p A q A r A p ˙ q B
46 1 4 atbase r A r B
47 46 adantl K HL X B p A q A r A r B
48 1 3 latjcl K Lat p ˙ q B r B p ˙ q ˙ r B
49 40 45 47 48 syl3anc K HL X B p A q A r A p ˙ q ˙ r B
50 49 biantrurd K HL X B p A q A r A s A p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s p ˙ q ˙ r B s A p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s
51 38 50 bitr4id K HL X B p A q A r A y s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r s A p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s
52 51 rexbidva K HL X B p A q A r A y s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r r A s A p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s
53 52 2rexbidva K HL X B p A q A r A y s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r p A q A r A s A p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s
54 rexcom4 r A y s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r y r A s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r
55 54 rexbii q A r A y s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r q A y r A s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r
56 rexcom4 q A y r A s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r y q A r A s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r
57 55 56 bitri q A r A y s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r y q A r A s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r
58 57 rexbii p A q A r A y s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r p A y q A r A s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r
59 rexcom4 p A y q A r A s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r y p A q A r A s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r
60 58 59 bitri p A q A r A y s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r y p A q A r A s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r
61 53 60 bitr3di K HL X B p A q A r A s A p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s y p A q A r A s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r
62 rexcom r A s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r s A r A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r
63 62 rexbii q A r A s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r q A s A r A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r
64 rexcom q A s A r A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r s A q A r A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r
65 63 64 bitri q A r A s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r s A q A r A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r
66 65 rexbii p A q A r A s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r p A s A q A r A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r
67 rexcom p A s A q A r A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r s A p A q A r A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r
68 66 67 bitri p A q A r A s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r s A p A q A r A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r
69 1 2 3 4 6 islpln2 K HL y LPlanes K y B p A q A r A p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r
70 69 adantr K HL X B y LPlanes K y B p A q A r A p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r
71 70 anbi1d K HL X B y LPlanes K ¬ s ˙ y X = y ˙ s y B p A q A r A p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r ¬ s ˙ y X = y ˙ s
72 r19.42v p A y B ¬ s ˙ y X = y ˙ s q A r A p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r y B ¬ s ˙ y X = y ˙ s p A q A r A p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r
73 r19.42v r A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r y B ¬ s ˙ y X = y ˙ s r A p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r
74 73 rexbii q A r A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r q A y B ¬ s ˙ y X = y ˙ s r A p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r
75 r19.42v q A y B ¬ s ˙ y X = y ˙ s r A p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r y B ¬ s ˙ y X = y ˙ s q A r A p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r
76 74 75 bitri q A r A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r y B ¬ s ˙ y X = y ˙ s q A r A p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r
77 76 rexbii p A q A r A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r p A y B ¬ s ˙ y X = y ˙ s q A r A p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r
78 an32 y B p A q A r A p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r ¬ s ˙ y X = y ˙ s y B ¬ s ˙ y X = y ˙ s p A q A r A p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r
79 72 77 78 3bitr4ri y B p A q A r A p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r ¬ s ˙ y X = y ˙ s p A q A r A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r
80 71 79 bitrdi K HL X B y LPlanes K ¬ s ˙ y X = y ˙ s p A q A r A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r
81 80 rexbidv K HL X B s A y LPlanes K ¬ s ˙ y X = y ˙ s s A p A q A r A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r
82 68 81 bitr4id K HL X B p A q A r A s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r s A y LPlanes K ¬ s ˙ y X = y ˙ s
83 r19.42v s A y LPlanes K ¬ s ˙ y X = y ˙ s y LPlanes K s A ¬ s ˙ y X = y ˙ s
84 82 83 bitrdi K HL X B p A q A r A s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r y LPlanes K s A ¬ s ˙ y X = y ˙ s
85 84 exbidv K HL X B y p A q A r A s A y B ¬ s ˙ y X = y ˙ s p q ¬ r ˙ p ˙ q y = p ˙ q ˙ r y y LPlanes K s A ¬ s ˙ y X = y ˙ s
86 61 85 bitrd K HL X B p A q A r A s A p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s y y LPlanes K s A ¬ s ˙ y X = y ˙ s
87 8 86 bitr4id K HL X B y LPlanes K s A ¬ s ˙ y X = y ˙ s p A q A r A s A p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s
88 7 87 bitrd K HL X B X V p A q A r A s A p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r X = p ˙ q ˙ r ˙ s