Metamath Proof Explorer


Theorem psubspset

Description: The set of projective subspaces in a Hilbert lattice. (Contributed by NM, 2-Oct-2011)

Ref Expression
Hypotheses psubspset.l ˙ = K
psubspset.j ˙ = join K
psubspset.a A = Atoms K
psubspset.s S = PSubSp K
Assertion psubspset K B S = s | s A p s q s r A r ˙ p ˙ q r s

Proof

Step Hyp Ref Expression
1 psubspset.l ˙ = K
2 psubspset.j ˙ = join K
3 psubspset.a A = Atoms K
4 psubspset.s S = PSubSp 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 7 sseq2d k = K s Atoms k s A
9 fveq2 k = K join k = join K
10 9 2 eqtr4di k = K join k = ˙
11 10 oveqd k = K p join k q = p ˙ q
12 11 breq2d k = K r k p join k q r k p ˙ q
13 fveq2 k = K k = K
14 13 1 eqtr4di k = K k = ˙
15 14 breqd k = K r k p ˙ q r ˙ p ˙ q
16 12 15 bitrd k = K r k p join k q r ˙ p ˙ q
17 16 imbi1d k = K r k p join k q r s r ˙ p ˙ q r s
18 7 17 raleqbidv k = K r Atoms k r k p join k q r s r A r ˙ p ˙ q r s
19 18 2ralbidv k = K p s q s r Atoms k r k p join k q r s p s q s r A r ˙ p ˙ q r s
20 8 19 anbi12d k = K s Atoms k p s q s r Atoms k r k p join k q r s s A p s q s r A r ˙ p ˙ q r s
21 20 abbidv k = K s | s Atoms k p s q s r Atoms k r k p join k q r s = s | s A p s q s r A r ˙ p ˙ q r s
22 df-psubsp PSubSp = k V s | s Atoms k p s q s r Atoms k r k p join k q r s
23 3 fvexi A V
24 23 pwex 𝒫 A V
25 velpw s 𝒫 A s A
26 25 anbi1i s 𝒫 A p s q s r A r ˙ p ˙ q r s s A p s q s r A r ˙ p ˙ q r s
27 26 abbii s | s 𝒫 A p s q s r A r ˙ p ˙ q r s = s | s A p s q s r A r ˙ p ˙ q r s
28 ssab2 s | s 𝒫 A p s q s r A r ˙ p ˙ q r s 𝒫 A
29 27 28 eqsstrri s | s A p s q s r A r ˙ p ˙ q r s 𝒫 A
30 24 29 ssexi s | s A p s q s r A r ˙ p ˙ q r s V
31 21 22 30 fvmpt K V PSubSp K = s | s A p s q s r A r ˙ p ˙ q r s
32 4 31 syl5eq K V S = s | s A p s q s r A r ˙ p ˙ q r s
33 5 32 syl K B S = s | s A p s q s r A r ˙ p ˙ q r s