# Metamath Proof Explorer

## Theorem iunocv

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

Ref Expression
Hypotheses inocv.o
iunocv.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
Assertion iunocv

### Proof

Step Hyp Ref Expression
1 inocv.o
2 iunocv.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
3 iunss ${⊢}\bigcup _{{x}\in {A}}{B}\subseteq {V}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\subseteq {V}$
4 eliun ${⊢}{y}\in \bigcup _{{x}\in {A}}{B}↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {B}$
5 4 imbi1i ${⊢}\left({y}\in \bigcup _{{x}\in {A}}{B}\to {z}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right)↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {B}\to {z}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right)$
6 r19.23v ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\to {z}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right)↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {B}\to {z}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right)$
7 5 6 bitr4i ${⊢}\left({y}\in \bigcup _{{x}\in {A}}{B}\to {z}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\to {z}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right)$
8 7 albii ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \bigcup _{{x}\in {A}}{B}\to {z}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\to {z}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right)$
9 df-ral ${⊢}\forall {y}\in \bigcup _{{x}\in {A}}{B}\phantom{\rule{.4em}{0ex}}{z}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \bigcup _{{x}\in {A}}{B}\to {z}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right)$
10 df-ral ${⊢}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\to {z}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right)$
11 10 ralbii ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\to {z}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right)$
12 ralcom4 ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\to {z}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\to {z}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right)$
13 11 12 bitri ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}↔\forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\to {z}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right)$
14 8 9 13 3bitr4i ${⊢}\forall {y}\in \bigcup _{{x}\in {A}}{B}\phantom{\rule{.4em}{0ex}}{z}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}$
15 3 14 anbi12i ${⊢}\left(\bigcup _{{x}\in {A}}{B}\subseteq {V}\wedge \forall {y}\in \bigcup _{{x}\in {A}}{B}\phantom{\rule{.4em}{0ex}}{z}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right)↔\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\subseteq {V}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right)$
16 r19.26 ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {V}\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right)↔\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\subseteq {V}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right)$
17 15 16 bitr4i ${⊢}\left(\bigcup _{{x}\in {A}}{B}\subseteq {V}\wedge \forall {y}\in \bigcup _{{x}\in {A}}{B}\phantom{\rule{.4em}{0ex}}{z}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {V}\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right)$
18 eliin
19 eqid ${⊢}{\cdot }_{𝑖}\left({W}\right)={\cdot }_{𝑖}\left({W}\right)$
20 eqid ${⊢}\mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({W}\right)$
21 eqid ${⊢}{0}_{\mathrm{Scalar}\left({W}\right)}={0}_{\mathrm{Scalar}\left({W}\right)}$
22 2 19 20 21 1 elocv
23 3anan12 ${⊢}\left({B}\subseteq {V}\wedge {z}\in {V}\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right)↔\left({z}\in {V}\wedge \left({B}\subseteq {V}\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right)\right)$
24 22 23 bitri
25 24 baib
26 25 ralbidv
27 18 26 bitr2d
28 17 27 syl5bb
29 28 pm5.32i
30 2 19 20 21 1 elocv
31 3anan12 ${⊢}\left(\bigcup _{{x}\in {A}}{B}\subseteq {V}\wedge {z}\in {V}\wedge \forall {y}\in \bigcup _{{x}\in {A}}{B}\phantom{\rule{.4em}{0ex}}{z}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right)↔\left({z}\in {V}\wedge \left(\bigcup _{{x}\in {A}}{B}\subseteq {V}\wedge \forall {y}\in \bigcup _{{x}\in {A}}{B}\phantom{\rule{.4em}{0ex}}{z}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right)\right)$
32 30 31 bitri
33 elin
34 29 32 33 3bitr4i
35 34 eqriv