This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ≤ = ( le ‘ 𝐾 )
psubspset.j ⊢ ∨ = ( join ‘ 𝐾 )
psubspset.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
psubspset.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
Assertion psubspset ( 𝐾 ∈ 𝐵 → 𝑆 = { 𝑠 ∣ ( 𝑠 ⊆ 𝐴 ∧ ∀ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑠 ) ) } )

Proof

Step Hyp Ref Expression
1 psubspset.l ⊢ ≤ = ( le ‘ 𝐾 )
2 psubspset.j ⊢ ∨ = ( join ‘ 𝐾 )
3 psubspset.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 psubspset.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
5 elex ⊢ ( 𝐾 ∈ 𝐵 → 𝐾 ∈ V )
6 fveq2 ⊢ ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = ( Atoms ‘ 𝐾 ) )
7 6 3 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = 𝐴 )
8 7 sseq2d ⊢ ( 𝑘 = 𝐾 → ( 𝑠 ⊆ ( Atoms ‘ 𝑘 ) ↔ 𝑠 ⊆ 𝐴 ) )
9 fveq2 ⊢ ( 𝑘 = 𝐾 → ( join ‘ 𝑘 ) = ( join ‘ 𝐾 ) )
10 9 2 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( join ‘ 𝑘 ) = ∨ )
11 10 oveqd ⊢ ( 𝑘 = 𝐾 → ( 𝑝 ( join ‘ 𝑘 ) 𝑞 ) = ( 𝑝 ∨ 𝑞 ) )
12 11 breq2d ⊢ ( 𝑘 = 𝐾 → ( 𝑟 ( le ‘ 𝑘 ) ( 𝑝 ( join ‘ 𝑘 ) 𝑞 ) ↔ 𝑟 ( le ‘ 𝑘 ) ( 𝑝 ∨ 𝑞 ) ) )
13 fveq2 ⊢ ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = ( le ‘ 𝐾 ) )
14 13 1 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = ≤ )
15 14 breqd ⊢ ( 𝑘 = 𝐾 → ( 𝑟 ( le ‘ 𝑘 ) ( 𝑝 ∨ 𝑞 ) ↔ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) )
16 12 15 bitrd ⊢ ( 𝑘 = 𝐾 → ( 𝑟 ( le ‘ 𝑘 ) ( 𝑝 ( join ‘ 𝑘 ) 𝑞 ) ↔ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ) )
17 16 imbi1d ⊢ ( 𝑘 = 𝐾 → ( ( 𝑟 ( le ‘ 𝑘 ) ( 𝑝 ( join ‘ 𝑘 ) 𝑞 ) → 𝑟 ∈ 𝑠 ) ↔ ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑠 ) ) )
18 7 17 raleqbidv ⊢ ( 𝑘 = 𝐾 → ( ∀ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑟 ( le ‘ 𝑘 ) ( 𝑝 ( join ‘ 𝑘 ) 𝑞 ) → 𝑟 ∈ 𝑠 ) ↔ ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑠 ) ) )
19 18 2ralbidv ⊢ ( 𝑘 = 𝐾 → ( ∀ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ∀ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑟 ( le ‘ 𝑘 ) ( 𝑝 ( join ‘ 𝑘 ) 𝑞 ) → 𝑟 ∈ 𝑠 ) ↔ ∀ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑠 ) ) )
20 8 19 anbi12d ⊢ ( 𝑘 = 𝐾 → ( ( 𝑠 ⊆ ( Atoms ‘ 𝑘 ) ∧ ∀ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ∀ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑟 ( le ‘ 𝑘 ) ( 𝑝 ( join ‘ 𝑘 ) 𝑞 ) → 𝑟 ∈ 𝑠 ) ) ↔ ( 𝑠 ⊆ 𝐴 ∧ ∀ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑠 ) ) ) )
21 20 abbidv ⊢ ( 𝑘 = 𝐾 → { 𝑠 ∣ ( 𝑠 ⊆ ( Atoms ‘ 𝑘 ) ∧ ∀ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ∀ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑟 ( le ‘ 𝑘 ) ( 𝑝 ( join ‘ 𝑘 ) 𝑞 ) → 𝑟 ∈ 𝑠 ) ) } = { 𝑠 ∣ ( 𝑠 ⊆ 𝐴 ∧ ∀ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑠 ) ) } )
22 df-psubsp ⊢ PSubSp = ( 𝑘 ∈ V ↦ { 𝑠 ∣ ( 𝑠 ⊆ ( Atoms ‘ 𝑘 ) ∧ ∀ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ∀ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑟 ( le ‘ 𝑘 ) ( 𝑝 ( join ‘ 𝑘 ) 𝑞 ) → 𝑟 ∈ 𝑠 ) ) } )
23 3 fvexi ⊢ 𝐴 ∈ V
24 23 pwex ⊢ 𝒫 𝐴 ∈ V
25 velpw ⊢ ( 𝑠 ∈ 𝒫 𝐴 ↔ 𝑠 ⊆ 𝐴 )
26 25 anbi1i ⊢ ( ( 𝑠 ∈ 𝒫 𝐴 ∧ ∀ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑠 ) ) ↔ ( 𝑠 ⊆ 𝐴 ∧ ∀ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑠 ) ) )
27 26 abbii ⊢ { 𝑠 ∣ ( 𝑠 ∈ 𝒫 𝐴 ∧ ∀ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑠 ) ) } = { 𝑠 ∣ ( 𝑠 ⊆ 𝐴 ∧ ∀ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑠 ) ) }
28 ssab2 ⊢ { 𝑠 ∣ ( 𝑠 ∈ 𝒫 𝐴 ∧ ∀ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑠 ) ) } ⊆ 𝒫 𝐴
29 27 28 eqsstrri ⊢ { 𝑠 ∣ ( 𝑠 ⊆ 𝐴 ∧ ∀ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑠 ) ) } ⊆ 𝒫 𝐴
30 24 29 ssexi ⊢ { 𝑠 ∣ ( 𝑠 ⊆ 𝐴 ∧ ∀ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑠 ) ) } ∈ V
31 21 22 30 fvmpt ⊢ ( 𝐾 ∈ V → ( PSubSp ‘ 𝐾 ) = { 𝑠 ∣ ( 𝑠 ⊆ 𝐴 ∧ ∀ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑠 ) ) } )
32 4 31 eqtrid ⊢ ( 𝐾 ∈ V → 𝑆 = { 𝑠 ∣ ( 𝑠 ⊆ 𝐴 ∧ ∀ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑠 ) ) } )
33 5 32 syl ⊢ ( 𝐾 ∈ 𝐵 → 𝑆 = { 𝑠 ∣ ( 𝑠 ⊆ 𝐴 ∧ ∀ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑠 ) ) } )