Theorem ocvfval

Description: The orthocomplement operation. (Contributed by NM, 7-Oct-2011) (Revised 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	ocvfval	⊢ ( 𝑊 ∈ 𝑋 → ⊥ = ( 𝑠 ∈ 𝒫 𝑉 ↦ { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 , 𝑦 ) = 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		elex	⊢ ( 𝑊 ∈ 𝑋 → 𝑊 ∈ V )
7		fveq2	⊢ ( ℎ = 𝑊 → ( Base ‘ ℎ ) = ( Base ‘ 𝑊 ) )
8	7 1	eqtr4di	⊢ ( ℎ = 𝑊 → ( Base ‘ ℎ ) = 𝑉 )
9	8	pweqd	⊢ ( ℎ = 𝑊 → 𝒫 ( Base ‘ ℎ ) = 𝒫 𝑉 )
10		fveq2	⊢ ( ℎ = 𝑊 → ( ·𝑖 ‘ ℎ ) = ( ·𝑖 ‘ 𝑊 ) )
11	10 2	eqtr4di	⊢ ( ℎ = 𝑊 → ( ·𝑖 ‘ ℎ ) = , )
12	11	oveqd	⊢ ( ℎ = 𝑊 → ( 𝑥 ( ·𝑖 ‘ ℎ ) 𝑦 ) = ( 𝑥 , 𝑦 ) )
13		fveq2	⊢ ( ℎ = 𝑊 → ( Scalar ‘ ℎ ) = ( Scalar ‘ 𝑊 ) )
14	13 3	eqtr4di	⊢ ( ℎ = 𝑊 → ( Scalar ‘ ℎ ) = 𝐹 )
15	14	fveq2d	⊢ ( ℎ = 𝑊 → ( 0g ‘ ( Scalar ‘ ℎ ) ) = ( 0g ‘ 𝐹 ) )
16	15 4	eqtr4di	⊢ ( ℎ = 𝑊 → ( 0g ‘ ( Scalar ‘ ℎ ) ) = 0 )
17	12 16	eqeq12d	⊢ ( ℎ = 𝑊 → ( ( 𝑥 ( ·𝑖 ‘ ℎ ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ ℎ ) ) ↔ ( 𝑥 , 𝑦 ) = 0 ) )
18	17	ralbidv	⊢ ( ℎ = 𝑊 → ( ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( ·𝑖 ‘ ℎ ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ ℎ ) ) ↔ ∀ 𝑦 ∈ 𝑠 ( 𝑥 , 𝑦 ) = 0 ) )
19	8 18	rabeqbidv	⊢ ( ℎ = 𝑊 → { 𝑥 ∈ ( Base ‘ ℎ ) ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( ·𝑖 ‘ ℎ ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ ℎ ) ) } = { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 , 𝑦 ) = 0 } )
20	9 19	mpteq12dv	⊢ ( ℎ = 𝑊 → ( 𝑠 ∈ 𝒫 ( Base ‘ ℎ ) ↦ { 𝑥 ∈ ( Base ‘ ℎ ) ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( ·𝑖 ‘ ℎ ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ ℎ ) ) } ) = ( 𝑠 ∈ 𝒫 𝑉 ↦ { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 , 𝑦 ) = 0 } ) )
21		df-ocv	⊢ ocv = ( ℎ ∈ V ↦ ( 𝑠 ∈ 𝒫 ( Base ‘ ℎ ) ↦ { 𝑥 ∈ ( Base ‘ ℎ ) ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( ·𝑖 ‘ ℎ ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ ℎ ) ) } ) )
22		eqid	⊢ ( 𝑠 ∈ 𝒫 𝑉 ↦ { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 , 𝑦 ) = 0 } ) = ( 𝑠 ∈ 𝒫 𝑉 ↦ { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 , 𝑦 ) = 0 } )
23	1	fvexi	⊢ 𝑉 ∈ V
24		ssrab2	⊢ { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 , 𝑦 ) = 0 } ⊆ 𝑉
25	23 24	elpwi2	⊢ { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 , 𝑦 ) = 0 } ∈ 𝒫 𝑉
26	25	a1i	⊢ ( 𝑠 ∈ 𝒫 𝑉 → { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 , 𝑦 ) = 0 } ∈ 𝒫 𝑉 )
27	22 26	fmpti	⊢ ( 𝑠 ∈ 𝒫 𝑉 ↦ { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 , 𝑦 ) = 0 } ) : 𝒫 𝑉 ⟶ 𝒫 𝑉
28	23	pwex	⊢ 𝒫 𝑉 ∈ V
29		fex2	⊢ ( ( ( 𝑠 ∈ 𝒫 𝑉 ↦ { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 , 𝑦 ) = 0 } ) : 𝒫 𝑉 ⟶ 𝒫 𝑉 ∧ 𝒫 𝑉 ∈ V ∧ 𝒫 𝑉 ∈ V ) → ( 𝑠 ∈ 𝒫 𝑉 ↦ { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 , 𝑦 ) = 0 } ) ∈ V )
30	27 28 28 29	mp3an	⊢ ( 𝑠 ∈ 𝒫 𝑉 ↦ { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 , 𝑦 ) = 0 } ) ∈ V
31	20 21 30	fvmpt	⊢ ( 𝑊 ∈ V → ( ocv ‘ 𝑊 ) = ( 𝑠 ∈ 𝒫 𝑉 ↦ { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 , 𝑦 ) = 0 } ) )
32	6 31	syl	⊢ ( 𝑊 ∈ 𝑋 → ( ocv ‘ 𝑊 ) = ( 𝑠 ∈ 𝒫 𝑉 ↦ { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 , 𝑦 ) = 0 } ) )
33	5 32	eqtrid	⊢ ( 𝑊 ∈ 𝑋 → ⊥ = ( 𝑠 ∈ 𝒫 𝑉 ↦ { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 , 𝑦 ) = 0 } ) )