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	⊢ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) )