Metamath Proof Explorer

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 syl5eq ⊢ ( 𝑊 ∈ 𝑋 → ⊥ = ( 𝑠 ∈ 𝒫 𝑉 ↦ { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 , 𝑦 ) = 0 } ) )