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	syl5eq	⊢ ( 𝐾 ∈ V → 𝑆 = { 𝑠 ∣ ( 𝑠 ⊆ 𝐴 ∧ ∀ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑠 ) ) } )
33	5 32	syl	⊢ ( 𝐾 ∈ 𝐵 → 𝑆 = { 𝑠 ∣ ( 𝑠 ⊆ 𝐴 ∧ ∀ 𝑝 ∈ 𝑠 ∀ 𝑞 ∈ 𝑠 ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑠 ) ) } )