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

Metamath Proof Explorer

Theorem ocv0

Description: The orthocomplement of the empty set. (Contributed by Mario Carneiro, 23-Oct-2015)

Ref Expression
Hypotheses ocvz.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
ocvz.o ⊢ ⊥ = ( ocv ‘ 𝑊 )
Assertion ocv0 ( ⊥ ‘ ∅ ) = 𝑉

Proof

Step Hyp Ref Expression
1 ocvz.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 ocvz.o ⊢ ⊥ = ( ocv ‘ 𝑊 )
3 0ss ⊢ ∅ ⊆ 𝑉
4 eqid ⊢ ( ·𝑖 ‘ 𝑊 ) = ( ·𝑖 ‘ 𝑊 )
5 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
6 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
7 1 4 5 6 2 ocvval ⊢ ( ∅ ⊆ 𝑉 → ( ⊥ ‘ ∅ ) = { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ ∅ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } )
8 3 7 ax-mp ⊢ ( ⊥ ‘ ∅ ) = { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ ∅ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) }
9 ral0 ⊢ ∀ 𝑦 ∈ ∅ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
10 9 rgenw ⊢ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ ∅ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
11 rabid2 ⊢ ( 𝑉 = { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ ∅ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ ∅ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
12 10 11 mpbir ⊢ 𝑉 = { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ∈ ∅ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) }
13 8 12 eqtr4i ⊢ ( ⊥ ‘ ∅ ) = 𝑉