Metamath Proof Explorer

Theorem iunocv

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

Ref Expression
Hypotheses inocv.o 
|- ._|_ = ( ocv ` W )
iunocv.v 
|- V = ( Base ` W )
Assertion iunocv 
|- ( ._|_ ` U_ x e. A B ) = ( V i^i |^|_ x e. A ( ._|_ ` B ) )

Proof

Step Hyp Ref Expression
1 inocv.o 
 |-  ._|_ = ( ocv ` W )
2 iunocv.v 
 |-  V = ( Base ` W )
3 iunss 
 |-  ( U_ x e. A B C_ V <-> A. x e. A B C_ V )
4 eliun 
 |-  ( y e. U_ x e. A B <-> E. x e. A y e. B )
5 4 imbi1i 
 |-  ( ( y e. U_ x e. A B -> ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) <-> ( E. x e. A y e. B -> ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) )
6 r19.23v 
 |-  ( A. x e. A ( y e. B -> ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) <-> ( E. x e. A y e. B -> ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) )
7 5 6 bitr4i 
 |-  ( ( y e. U_ x e. A B -> ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) <-> A. x e. A ( y e. B -> ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) )
8 7 albii 
 |-  ( A. y ( y e. U_ x e. A B -> ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) <-> A. y A. x e. A ( y e. B -> ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) )
9 df-ral 
 |-  ( A. y e. U_ x e. A B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) <-> A. y ( y e. U_ x e. A B -> ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) )
10 df-ral 
 |-  ( A. y e. B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) <-> A. y ( y e. B -> ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) )
11 10 ralbii 
 |-  ( A. x e. A A. y e. B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) <-> A. x e. A A. y ( y e. B -> ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) )
12 ralcom4 
 |-  ( A. x e. A A. y ( y e. B -> ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) <-> A. y A. x e. A ( y e. B -> ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) )
13 11 12 bitri 
 |-  ( A. x e. A A. y e. B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) <-> A. y A. x e. A ( y e. B -> ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) )
14 8 9 13 3bitr4i 
 |-  ( A. y e. U_ x e. A B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) <-> A. x e. A A. y e. B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) )
15 3 14 anbi12i 
 |-  ( ( U_ x e. A B C_ V /\ A. y e. U_ x e. A B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) <-> ( A. x e. A B C_ V /\ A. x e. A A. y e. B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) )
16 r19.26 
 |-  ( A. x e. A ( B C_ V /\ A. y e. B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) <-> ( A. x e. A B C_ V /\ A. x e. A A. y e. B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) )
17 15 16 bitr4i 
 |-  ( ( U_ x e. A B C_ V /\ A. y e. U_ x e. A B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) <-> A. x e. A ( B C_ V /\ A. y e. B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) )
18 eliin 
 |-  ( z e. V -> ( z e. |^|_ x e. A ( ._|_ ` B ) <-> A. x e. A z e. ( ._|_ ` B ) ) )
19 eqid 
 |-  ( .i ` W ) = ( .i ` W )
20 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
21 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
22 2 19 20 21 1 elocv 
 |-  ( z e. ( ._|_ ` B ) <-> ( B C_ V /\ z e. V /\ A. y e. B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) )
23 3anan12 
 |-  ( ( B C_ V /\ z e. V /\ A. y e. B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) <-> ( z e. V /\ ( B C_ V /\ A. y e. B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) ) )
24 22 23 bitri 
 |-  ( z e. ( ._|_ ` B ) <-> ( z e. V /\ ( B C_ V /\ A. y e. B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) ) )
25 24 baib 
 |-  ( z e. V -> ( z e. ( ._|_ ` B ) <-> ( B C_ V /\ A. y e. B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) ) )
26 25 ralbidv 
 |-  ( z e. V -> ( A. x e. A z e. ( ._|_ ` B ) <-> A. x e. A ( B C_ V /\ A. y e. B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) ) )
27 18 26 bitr2d 
 |-  ( z e. V -> ( A. x e. A ( B C_ V /\ A. y e. B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) <-> z e. |^|_ x e. A ( ._|_ ` B ) ) )
28 17 27 syl5bb 
 |-  ( z e. V -> ( ( U_ x e. A B C_ V /\ A. y e. U_ x e. A B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) <-> z e. |^|_ x e. A ( ._|_ ` B ) ) )
29 28 pm5.32i 
 |-  ( ( z e. V /\ ( U_ x e. A B C_ V /\ A. y e. U_ x e. A B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) ) <-> ( z e. V /\ z e. |^|_ x e. A ( ._|_ ` B ) ) )
30 2 19 20 21 1 elocv 
 |-  ( z e. ( ._|_ ` U_ x e. A B ) <-> ( U_ x e. A B C_ V /\ z e. V /\ A. y e. U_ x e. A B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) )
31 3anan12 
 |-  ( ( U_ x e. A B C_ V /\ z e. V /\ A. y e. U_ x e. A B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) <-> ( z e. V /\ ( U_ x e. A B C_ V /\ A. y e. U_ x e. A B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) ) )
32 30 31 bitri 
 |-  ( z e. ( ._|_ ` U_ x e. A B ) <-> ( z e. V /\ ( U_ x e. A B C_ V /\ A. y e. U_ x e. A B ( z ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) ) ) )
33 elin 
 |-  ( z e. ( V i^i |^|_ x e. A ( ._|_ ` B ) ) <-> ( z e. V /\ z e. |^|_ x e. A ( ._|_ ` B ) ) )
34 29 32 33 3bitr4i 
 |-  ( z e. ( ._|_ ` U_ x e. A B ) <-> z e. ( V i^i |^|_ x e. A ( ._|_ ` B ) ) )
35 34 eqriv 
 |-  ( ._|_ ` U_ x e. A B ) = ( V i^i |^|_ x e. A ( ._|_ ` B ) )