Theorem elocv

Description: Elementhood in the orthocomplement of a subset (normally a subspace) of a pre-Hilbert space. (Contributed by Mario Carneiro, 13-Oct-2015)

	Ref	Expression
Hypotheses	ocvfval.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	ocvfval.i	⊢ , = ( ·𝑖 ‘ 𝑊 )
	ocvfval.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	ocvfval.z	⊢ 0 = ( 0g ‘ 𝐹 )
	ocvfval.o	⊢ ⊥ = ( ocv ‘ 𝑊 )
Assertion	elocv	⊢ ( 𝐴 ∈ ( ⊥ ‘ 𝑆 ) ↔ ( 𝑆 ⊆ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐴 , 𝑥 ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		ocvfval.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		ocvfval.i	⊢ , = ( ·𝑖 ‘ 𝑊 )
3		ocvfval.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4		ocvfval.z	⊢ 0 = ( 0g ‘ 𝐹 )
5		ocvfval.o	⊢ ⊥ = ( ocv ‘ 𝑊 )
6		elfvdm	⊢ ( 𝐴 ∈ ( ⊥ ‘ 𝑆 ) → 𝑆 ∈ dom ⊥ )
7		n0i	⊢ ( 𝐴 ∈ ( ⊥ ‘ 𝑆 ) → ¬ ( ⊥ ‘ 𝑆 ) = ∅ )
8		fvprc	⊢ ( ¬ 𝑊 ∈ V → ( ocv ‘ 𝑊 ) = ∅ )
9	5 8	syl5eq	⊢ ( ¬ 𝑊 ∈ V → ⊥ = ∅ )
10	9	fveq1d	⊢ ( ¬ 𝑊 ∈ V → ( ⊥ ‘ 𝑆 ) = ( ∅ ‘ 𝑆 ) )
11		0fv	⊢ ( ∅ ‘ 𝑆 ) = ∅
12	10 11	eqtrdi	⊢ ( ¬ 𝑊 ∈ V → ( ⊥ ‘ 𝑆 ) = ∅ )
13	7 12	nsyl2	⊢ ( 𝐴 ∈ ( ⊥ ‘ 𝑆 ) → 𝑊 ∈ V )
14	1 2 3 4 5	ocvfval	⊢ ( 𝑊 ∈ V → ⊥ = ( 𝑠 ∈ 𝒫 𝑉 ↦ { 𝑦 ∈ 𝑉 ∣ ∀ 𝑥 ∈ 𝑠 ( 𝑦 , 𝑥 ) = 0 } ) )
15	13 14	syl	⊢ ( 𝐴 ∈ ( ⊥ ‘ 𝑆 ) → ⊥ = ( 𝑠 ∈ 𝒫 𝑉 ↦ { 𝑦 ∈ 𝑉 ∣ ∀ 𝑥 ∈ 𝑠 ( 𝑦 , 𝑥 ) = 0 } ) )
16	15	dmeqd	⊢ ( 𝐴 ∈ ( ⊥ ‘ 𝑆 ) → dom ⊥ = dom ( 𝑠 ∈ 𝒫 𝑉 ↦ { 𝑦 ∈ 𝑉 ∣ ∀ 𝑥 ∈ 𝑠 ( 𝑦 , 𝑥 ) = 0 } ) )
17	1	fvexi	⊢ 𝑉 ∈ V
18	17	rabex	⊢ { 𝑦 ∈ 𝑉 ∣ ∀ 𝑥 ∈ 𝑠 ( 𝑦 , 𝑥 ) = 0 } ∈ V
19		eqid	⊢ ( 𝑠 ∈ 𝒫 𝑉 ↦ { 𝑦 ∈ 𝑉 ∣ ∀ 𝑥 ∈ 𝑠 ( 𝑦 , 𝑥 ) = 0 } ) = ( 𝑠 ∈ 𝒫 𝑉 ↦ { 𝑦 ∈ 𝑉 ∣ ∀ 𝑥 ∈ 𝑠 ( 𝑦 , 𝑥 ) = 0 } )
20	18 19	dmmpti	⊢ dom ( 𝑠 ∈ 𝒫 𝑉 ↦ { 𝑦 ∈ 𝑉 ∣ ∀ 𝑥 ∈ 𝑠 ( 𝑦 , 𝑥 ) = 0 } ) = 𝒫 𝑉
21	16 20	eqtrdi	⊢ ( 𝐴 ∈ ( ⊥ ‘ 𝑆 ) → dom ⊥ = 𝒫 𝑉 )
22	6 21	eleqtrd	⊢ ( 𝐴 ∈ ( ⊥ ‘ 𝑆 ) → 𝑆 ∈ 𝒫 𝑉 )
23	22	elpwid	⊢ ( 𝐴 ∈ ( ⊥ ‘ 𝑆 ) → 𝑆 ⊆ 𝑉 )
24	1 2 3 4 5	ocvval	⊢ ( 𝑆 ⊆ 𝑉 → ( ⊥ ‘ 𝑆 ) = { 𝑦 ∈ 𝑉 ∣ ∀ 𝑥 ∈ 𝑆 ( 𝑦 , 𝑥 ) = 0 } )
25	24	eleq2d	⊢ ( 𝑆 ⊆ 𝑉 → ( 𝐴 ∈ ( ⊥ ‘ 𝑆 ) ↔ 𝐴 ∈ { 𝑦 ∈ 𝑉 ∣ ∀ 𝑥 ∈ 𝑆 ( 𝑦 , 𝑥 ) = 0 } ) )
26		oveq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 , 𝑥 ) = ( 𝐴 , 𝑥 ) )
27	26	eqeq1d	⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 , 𝑥 ) = 0 ↔ ( 𝐴 , 𝑥 ) = 0 ) )
28	27	ralbidv	⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑥 ∈ 𝑆 ( 𝑦 , 𝑥 ) = 0 ↔ ∀ 𝑥 ∈ 𝑆 ( 𝐴 , 𝑥 ) = 0 ) )
29	28	elrab	⊢ ( 𝐴 ∈ { 𝑦 ∈ 𝑉 ∣ ∀ 𝑥 ∈ 𝑆 ( 𝑦 , 𝑥 ) = 0 } ↔ ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐴 , 𝑥 ) = 0 ) )
30	25 29	bitrdi	⊢ ( 𝑆 ⊆ 𝑉 → ( 𝐴 ∈ ( ⊥ ‘ 𝑆 ) ↔ ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐴 , 𝑥 ) = 0 ) ) )
31	23 30	biadanii	⊢ ( 𝐴 ∈ ( ⊥ ‘ 𝑆 ) ↔ ( 𝑆 ⊆ 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐴 , 𝑥 ) = 0 ) ) )
32		3anass	⊢ ( ( 𝑆 ⊆ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐴 , 𝑥 ) = 0 ) ↔ ( 𝑆 ⊆ 𝑉 ∧ ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐴 , 𝑥 ) = 0 ) ) )
33	31 32	bitr4i	⊢ ( 𝐴 ∈ ( ⊥ ‘ 𝑆 ) ↔ ( 𝑆 ⊆ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐴 , 𝑥 ) = 0 ) )