Metamath Proof Explorer


Theorem lineset

Description: The set of lines in a Hilbert lattice. (Contributed by NM, 19-Sep-2011)

Ref Expression
Hypotheses lineset.l ˙ = K
lineset.j ˙ = join K
lineset.a A = Atoms K
lineset.n N = Lines K
Assertion lineset K B N = s | q A r A q r s = p A | p ˙ q ˙ r

Proof

Step Hyp Ref Expression
1 lineset.l ˙ = K
2 lineset.j ˙ = join K
3 lineset.a A = Atoms K
4 lineset.n N = Lines K
5 elex K B K V
6 fveq2 k = K Atoms k = Atoms K
7 6 3 eqtr4di k = K Atoms k = A
8 fveq2 k = K k = K
9 8 1 eqtr4di k = K k = ˙
10 9 breqd k = K p k q join k r p ˙ q join k r
11 fveq2 k = K join k = join K
12 11 2 eqtr4di k = K join k = ˙
13 12 oveqd k = K q join k r = q ˙ r
14 13 breq2d k = K p ˙ q join k r p ˙ q ˙ r
15 10 14 bitrd k = K p k q join k r p ˙ q ˙ r
16 7 15 rabeqbidv k = K p Atoms k | p k q join k r = p A | p ˙ q ˙ r
17 16 eqeq2d k = K s = p Atoms k | p k q join k r s = p A | p ˙ q ˙ r
18 17 anbi2d k = K q r s = p Atoms k | p k q join k r q r s = p A | p ˙ q ˙ r
19 7 18 rexeqbidv k = K r Atoms k q r s = p Atoms k | p k q join k r r A q r s = p A | p ˙ q ˙ r
20 7 19 rexeqbidv k = K q Atoms k r Atoms k q r s = p Atoms k | p k q join k r q A r A q r s = p A | p ˙ q ˙ r
21 20 abbidv k = K s | q Atoms k r Atoms k q r s = p Atoms k | p k q join k r = s | q A r A q r s = p A | p ˙ q ˙ r
22 df-lines Lines = k V s | q Atoms k r Atoms k q r s = p Atoms k | p k q join k r
23 3 fvexi A V
24 df-sn p A | p ˙ q ˙ r = s | s = p A | p ˙ q ˙ r
25 snex p A | p ˙ q ˙ r V
26 24 25 eqeltrri s | s = p A | p ˙ q ˙ r V
27 simpr q r s = p A | p ˙ q ˙ r s = p A | p ˙ q ˙ r
28 27 ss2abi s | q r s = p A | p ˙ q ˙ r s | s = p A | p ˙ q ˙ r
29 26 28 ssexi s | q r s = p A | p ˙ q ˙ r V
30 23 23 29 ab2rexex2 s | q A r A q r s = p A | p ˙ q ˙ r V
31 21 22 30 fvmpt K V Lines K = s | q A r A q r s = p A | p ˙ q ˙ r
32 4 31 syl5eq K V N = s | q A r A q r s = p A | p ˙ q ˙ r
33 5 32 syl K B N = s | q A r A q r s = p A | p ˙ q ˙ r