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	⊢ ( ⊥ ‘ ∅ ) = 𝑉