Metamath Proof Explorer

Theorem unocv

Description: The orthocomplement of a union. (Contributed by Mario Carneiro, 23-Oct-2015)

Ref Expression
Hypothesis inocv.o 
|- ._|_ = ( ocv ` W )
Assertion unocv 
|- ( ._|_ ` ( A u. B ) ) = ( ( ._|_ ` A ) i^i ( ._|_ ` B ) )

Proof

Step Hyp Ref Expression
1 inocv.o 
 |-  ._|_ = ( ocv ` W )
2 unss 
 |-  ( ( A C_ ( Base ` W ) /\ B C_ ( Base ` W ) ) <-> ( A u. B ) C_ ( Base ` W ) )
3 2 bicomi 
 |-  ( ( A u. B ) C_ ( Base ` W ) <-> ( A C_ ( Base ` W ) /\ B C_ ( Base ` W ) ) )
4 ralunb 
 |-  ( A. y e. ( A u. B ) ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) <-> ( A. y e. A ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) /\ A. y e. B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) )
5 3 4 anbi12i 
 |-  ( ( ( A u. B ) C_ ( Base ` W ) /\ A. y e. ( A u. B ) ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) <-> ( ( A C_ ( Base ` W ) /\ B C_ ( Base ` W ) ) /\ ( A. y e. A ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) /\ A. y e. B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) ) )
6 an4 
 |-  ( ( ( A C_ ( Base ` W ) /\ B C_ ( Base ` W ) ) /\ ( A. y e. A ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) /\ A. y e. B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) ) <-> ( ( A C_ ( Base ` W ) /\ A. y e. A ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) /\ ( B C_ ( Base ` W ) /\ A. y e. B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) ) )
7 5 6 bitri 
 |-  ( ( ( A u. B ) C_ ( Base ` W ) /\ A. y e. ( A u. B ) ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) <-> ( ( A C_ ( Base ` W ) /\ A. y e. A ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) /\ ( B C_ ( Base ` W ) /\ A. y e. B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) ) )
8 7 anbi2i 
 |-  ( ( z e. ( Base ` W ) /\ ( ( A u. B ) C_ ( Base ` W ) /\ A. y e. ( A u. B ) ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) ) <-> ( z e. ( Base ` W ) /\ ( ( A C_ ( Base ` W ) /\ A. y e. A ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) /\ ( B C_ ( Base ` W ) /\ A. y e. B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) ) ) )
9 eqid 
 |-  ( Base ` W ) = ( Base ` W )
10 eqid 
 |-  ( .i ` W ) = ( .i ` W )
11 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
12 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
13 9 10 11 12 1 elocv 
 |-  ( z e. ( ._|_ ` ( A u. B ) ) <-> ( ( A u. B ) C_ ( Base ` W ) /\ z e. ( Base ` W ) /\ A. y e. ( A u. B ) ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) )
14 3anan12 
 |-  ( ( ( A u. B ) C_ ( Base ` W ) /\ z e. ( Base ` W ) /\ A. y e. ( A u. B ) ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) <-> ( z e. ( Base ` W ) /\ ( ( A u. B ) C_ ( Base ` W ) /\ A. y e. ( A u. B ) ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) ) )
15 13 14 bitri 
 |-  ( z e. ( ._|_ ` ( A u. B ) ) <-> ( z e. ( Base ` W ) /\ ( ( A u. B ) C_ ( Base ` W ) /\ A. y e. ( A u. B ) ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) ) )
16 9 10 11 12 1 elocv 
 |-  ( z e. ( ._|_ ` A ) <-> ( A C_ ( Base ` W ) /\ z e. ( Base ` W ) /\ A. y e. A ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) )
17 3anan12 
 |-  ( ( A C_ ( Base ` W ) /\ z e. ( Base ` W ) /\ A. y e. A ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) <-> ( z e. ( Base ` W ) /\ ( A C_ ( Base ` W ) /\ A. y e. A ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) ) )
18 16 17 bitri 
 |-  ( z e. ( ._|_ ` A ) <-> ( z e. ( Base ` W ) /\ ( A C_ ( Base ` W ) /\ A. y e. A ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) ) )
19 9 10 11 12 1 elocv 
 |-  ( z e. ( ._|_ ` B ) <-> ( B C_ ( Base ` W ) /\ z e. ( Base ` W ) /\ A. y e. B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) )
20 3anan12 
 |-  ( ( B C_ ( Base ` W ) /\ z e. ( Base ` W ) /\ A. y e. B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) <-> ( z e. ( Base ` W ) /\ ( B C_ ( Base ` W ) /\ A. y e. B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) ) )
21 19 20 bitri 
 |-  ( z e. ( ._|_ ` B ) <-> ( z e. ( Base ` W ) /\ ( B C_ ( Base ` W ) /\ A. y e. B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) ) )
22 18 21 anbi12i 
 |-  ( ( z e. ( ._|_ ` A ) /\ z e. ( ._|_ ` B ) ) <-> ( ( z e. ( Base ` W ) /\ ( A C_ ( Base ` W ) /\ A. y e. A ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) ) /\ ( z e. ( Base ` W ) /\ ( B C_ ( Base ` W ) /\ A. y e. B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) ) ) )
23 elin 
 |-  ( z e. ( ( ._|_ ` A ) i^i ( ._|_ ` B ) ) <-> ( z e. ( ._|_ ` A ) /\ z e. ( ._|_ ` B ) ) )
24 anandi 
 |-  ( ( z e. ( Base ` W ) /\ ( ( A C_ ( Base ` W ) /\ A. y e. A ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) /\ ( B C_ ( Base ` W ) /\ A. y e. B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) ) ) <-> ( ( z e. ( Base ` W ) /\ ( A C_ ( Base ` W ) /\ A. y e. A ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) ) /\ ( z e. ( Base ` W ) /\ ( B C_ ( Base ` W ) /\ A. y e. B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) ) ) )
25 22 23 24 3bitr4i 
 |-  ( z e. ( ( ._|_ ` A ) i^i ( ._|_ ` B ) ) <-> ( z e. ( Base ` W ) /\ ( ( A C_ ( Base ` W ) /\ A. y e. A ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) /\ ( B C_ ( Base ` W ) /\ A. y e. B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) ) ) )
26 8 15 25 3bitr4i 
 |-  ( z e. ( ._|_ ` ( A u. B ) ) <-> z e. ( ( ._|_ ` A ) i^i ( ._|_ ` B ) ) )
27 26 eqriv 
 |-  ( ._|_ ` ( A u. B ) ) = ( ( ._|_ ` A ) i^i ( ._|_ ` B ) )