Metamath Proof Explorer

Theorem unocv

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

Ref Expression
Hypothesis inocv.o ⊢ ⊥ = ( ocv ‘ 𝑊 )
Assertion unocv ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 inocv.o ⊢ ⊥ = ( ocv ‘ 𝑊 )
2 unss ⊢ ( ( 𝐴 ⊆ ( Base ‘ 𝑊 ) ∧ 𝐵 ⊆ ( Base ‘ 𝑊 ) ) ↔ ( 𝐴 ∪ 𝐵 ) ⊆ ( Base ‘ 𝑊 ) )
3 2 bicomi ⊢ ( ( 𝐴 ∪ 𝐵 ) ⊆ ( Base ‘ 𝑊 ) ↔ ( 𝐴 ⊆ ( Base ‘ 𝑊 ) ∧ 𝐵 ⊆ ( Base ‘ 𝑊 ) ) )
4 ralunb ⊢ ( ∀ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ↔ ( ∀ 𝑦 ∈ 𝐴 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
5 3 4 anbi12i ⊢ ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ↔ ( ( 𝐴 ⊆ ( Base ‘ 𝑊 ) ∧ 𝐵 ⊆ ( Base ‘ 𝑊 ) ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) )
6 an4 ⊢ ( ( ( 𝐴 ⊆ ( Base ‘ 𝑊 ) ∧ 𝐵 ⊆ ( Base ‘ 𝑊 ) ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) ↔ ( ( 𝐴 ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) )
7 5 6 bitri ⊢ ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ↔ ( ( 𝐴 ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) )
8 7 anbi2i ⊢ ( ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ ( ( 𝐴 ∪ 𝐵 ) ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) ↔ ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ ( ( 𝐴 ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) ) )
9 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
10 eqid ⊢ ( ·𝑖 ‘ 𝑊 ) = ( ·𝑖 ‘ 𝑊 )
11 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
12 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
13 9 10 11 12 1 elocv ⊢ ( 𝑧 ∈ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) ↔ ( ( 𝐴 ∪ 𝐵 ) ⊆ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
14 3anan12 ⊢ ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ↔ ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ ( ( 𝐴 ∪ 𝐵 ) ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) )
15 13 14 bitri ⊢ ( 𝑧 ∈ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) ↔ ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ ( ( 𝐴 ∪ 𝐵 ) ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) )
16 9 10 11 12 1 elocv ⊢ ( 𝑧 ∈ ( ⊥ ‘ 𝐴 ) ↔ ( 𝐴 ⊆ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
17 3anan12 ⊢ ( ( 𝐴 ⊆ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ↔ ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ ( 𝐴 ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) )
18 16 17 bitri ⊢ ( 𝑧 ∈ ( ⊥ ‘ 𝐴 ) ↔ ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ ( 𝐴 ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) )
19 9 10 11 12 1 elocv ⊢ ( 𝑧 ∈ ( ⊥ ‘ 𝐵 ) ↔ ( 𝐵 ⊆ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
20 3anan12 ⊢ ( ( 𝐵 ⊆ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ↔ ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) )
21 19 20 bitri ⊢ ( 𝑧 ∈ ( ⊥ ‘ 𝐵 ) ↔ ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) )
22 18 21 anbi12i ⊢ ( ( 𝑧 ∈ ( ⊥ ‘ 𝐴 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝐵 ) ) ↔ ( ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ ( 𝐴 ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) ) )
23 elin ⊢ ( 𝑧 ∈ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ↔ ( 𝑧 ∈ ( ⊥ ‘ 𝐴 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝐵 ) ) )
24 anandi ⊢ ( ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ ( ( 𝐴 ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) ) ↔ ( ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ ( 𝐴 ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) ) )
25 22 23 24 3bitr4i ⊢ ( 𝑧 ∈ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ↔ ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ ( ( 𝐴 ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) ) )
26 8 15 25 3bitr4i ⊢ ( 𝑧 ∈ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) ↔ 𝑧 ∈ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) )
27 26 eqriv ⊢ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) )