unocv

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

		Ref	Expression
	Hypothesis	inocv.o	$⊢ \underset{˙}{⊥} = ocv (W)$
	Assertion	unocv	$⊢ \underset{˙}{⊥} (A \cup B) = \underset{˙}{⊥} (A) \cap \underset{˙}{⊥} (B)$

Proof

Step	Hyp	Ref	Expression
1		inocv.o	$⊢ \underset{˙}{⊥} = ocv (W)$
2		unss	$⊢ (A \subseteq {Base}_{W} \land B \subseteq {Base}_{W}) \leftrightarrow A \cup B \subseteq {Base}_{W}$
3	2	bicomi	$⊢ A \cup B \subseteq {Base}_{W} \leftrightarrow (A \subseteq {Base}_{W} \land B \subseteq {Base}_{W})$
4		ralunb	$⊢ \forall y \in (A \cup B) z \cdot_{𝑖} (W) y = 0_{Scalar (W)} \leftrightarrow (\forall y \in A z \cdot_{𝑖} (W) y = 0_{Scalar (W)} \land \forall y \in B z \cdot_{𝑖} (W) y = 0_{Scalar (W)})$
5	3 4	anbi12i	$⊢ (A \cup B \subseteq {Base}_{W} \land \forall y \in (A \cup B) z \cdot_{𝑖} (W) y = 0_{Scalar (W)}) \leftrightarrow ((A \subseteq {Base}_{W} \land B \subseteq {Base}_{W}) \land (\forall y \in A z \cdot_{𝑖} (W) y = 0_{Scalar (W)} \land \forall y \in B z \cdot_{𝑖} (W) y = 0_{Scalar (W)}))$
6		an4	$⊢ ((A \subseteq {Base}_{W} \land B \subseteq {Base}_{W}) \land (\forall y \in A z \cdot_{𝑖} (W) y = 0_{Scalar (W)} \land \forall y \in B z \cdot_{𝑖} (W) y = 0_{Scalar (W)})) \leftrightarrow ((A \subseteq {Base}_{W} \land \forall y \in A z \cdot_{𝑖} (W) y = 0_{Scalar (W)}) \land (B \subseteq {Base}_{W} \land \forall y \in B z \cdot_{𝑖} (W) y = 0_{Scalar (W)}))$
7	5 6	bitri	$⊢ (A \cup B \subseteq {Base}_{W} \land \forall y \in (A \cup B) z \cdot_{𝑖} (W) y = 0_{Scalar (W)}) \leftrightarrow ((A \subseteq {Base}_{W} \land \forall y \in A z \cdot_{𝑖} (W) y = 0_{Scalar (W)}) \land (B \subseteq {Base}_{W} \land \forall y \in B z \cdot_{𝑖} (W) y = 0_{Scalar (W)}))$
8	7	anbi2i	$⊢ (z \in {Base}_{W} \land (A \cup B \subseteq {Base}_{W} \land \forall y \in (A \cup B) z \cdot_{𝑖} (W) y = 0_{Scalar (W)})) \leftrightarrow (z \in {Base}_{W} \land ((A \subseteq {Base}_{W} \land \forall y \in A z \cdot_{𝑖} (W) y = 0_{Scalar (W)}) \land (B \subseteq {Base}_{W} \land \forall y \in B z \cdot_{𝑖} (W) y = 0_{Scalar (W)})))$
9		eqid	$⊢ {Base}_{W} = {Base}_{W}$
10		eqid	$⊢ \cdot_{𝑖} (W) = \cdot_{𝑖} (W)$
11		eqid	$⊢ Scalar (W) = Scalar (W)$
12		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
13	9 10 11 12 1	elocv	$⊢ z \in \underset{˙}{⊥} (A \cup B) \leftrightarrow (A \cup B \subseteq {Base}_{W} \land z \in {Base}_{W} \land \forall y \in (A \cup B) z \cdot_{𝑖} (W) y = 0_{Scalar (W)})$
14		3anan12	$⊢ (A \cup B \subseteq {Base}_{W} \land z \in {Base}_{W} \land \forall y \in (A \cup B) z \cdot_{𝑖} (W) y = 0_{Scalar (W)}) \leftrightarrow (z \in {Base}_{W} \land (A \cup B \subseteq {Base}_{W} \land \forall y \in (A \cup B) z \cdot_{𝑖} (W) y = 0_{Scalar (W)}))$
15	13 14	bitri	$⊢ z \in \underset{˙}{⊥} (A \cup B) \leftrightarrow (z \in {Base}_{W} \land (A \cup B \subseteq {Base}_{W} \land \forall y \in (A \cup B) z \cdot_{𝑖} (W) y = 0_{Scalar (W)}))$
16	9 10 11 12 1	elocv	$⊢ z \in \underset{˙}{⊥} (A) \leftrightarrow (A \subseteq {Base}_{W} \land z \in {Base}_{W} \land \forall y \in A z \cdot_{𝑖} (W) y = 0_{Scalar (W)})$
17		3anan12	$⊢ (A \subseteq {Base}_{W} \land z \in {Base}_{W} \land \forall y \in A z \cdot_{𝑖} (W) y = 0_{Scalar (W)}) \leftrightarrow (z \in {Base}_{W} \land (A \subseteq {Base}_{W} \land \forall y \in A z \cdot_{𝑖} (W) y = 0_{Scalar (W)}))$
18	16 17	bitri	$⊢ z \in \underset{˙}{⊥} (A) \leftrightarrow (z \in {Base}_{W} \land (A \subseteq {Base}_{W} \land \forall y \in A z \cdot_{𝑖} (W) y = 0_{Scalar (W)}))$
19	9 10 11 12 1	elocv	$⊢ z \in \underset{˙}{⊥} (B) \leftrightarrow (B \subseteq {Base}_{W} \land z \in {Base}_{W} \land \forall y \in B z \cdot_{𝑖} (W) y = 0_{Scalar (W)})$
20		3anan12	$⊢ (B \subseteq {Base}_{W} \land z \in {Base}_{W} \land \forall y \in B z \cdot_{𝑖} (W) y = 0_{Scalar (W)}) \leftrightarrow (z \in {Base}_{W} \land (B \subseteq {Base}_{W} \land \forall y \in B z \cdot_{𝑖} (W) y = 0_{Scalar (W)}))$
21	19 20	bitri	$⊢ z \in \underset{˙}{⊥} (B) \leftrightarrow (z \in {Base}_{W} \land (B \subseteq {Base}_{W} \land \forall y \in B z \cdot_{𝑖} (W) y = 0_{Scalar (W)}))$
22	18 21	anbi12i	$⊢ (z \in \underset{˙}{⊥} (A) \land z \in \underset{˙}{⊥} (B)) \leftrightarrow ((z \in {Base}_{W} \land (A \subseteq {Base}_{W} \land \forall y \in A z \cdot_{𝑖} (W) y = 0_{Scalar (W)})) \land (z \in {Base}_{W} \land (B \subseteq {Base}_{W} \land \forall y \in B z \cdot_{𝑖} (W) y = 0_{Scalar (W)})))$
23		elin	$⊢ z \in (\underset{˙}{⊥} (A) \cap \underset{˙}{⊥} (B)) \leftrightarrow (z \in \underset{˙}{⊥} (A) \land z \in \underset{˙}{⊥} (B))$
24		anandi	$⊢ (z \in {Base}_{W} \land ((A \subseteq {Base}_{W} \land \forall y \in A z \cdot_{𝑖} (W) y = 0_{Scalar (W)}) \land (B \subseteq {Base}_{W} \land \forall y \in B z \cdot_{𝑖} (W) y = 0_{Scalar (W)}))) \leftrightarrow ((z \in {Base}_{W} \land (A \subseteq {Base}_{W} \land \forall y \in A z \cdot_{𝑖} (W) y = 0_{Scalar (W)})) \land (z \in {Base}_{W} \land (B \subseteq {Base}_{W} \land \forall y \in B z \cdot_{𝑖} (W) y = 0_{Scalar (W)})))$
25	22 23 24	3bitr4i	$⊢ z \in (\underset{˙}{⊥} (A) \cap \underset{˙}{⊥} (B)) \leftrightarrow (z \in {Base}_{W} \land ((A \subseteq {Base}_{W} \land \forall y \in A z \cdot_{𝑖} (W) y = 0_{Scalar (W)}) \land (B \subseteq {Base}_{W} \land \forall y \in B z \cdot_{𝑖} (W) y = 0_{Scalar (W)})))$
26	8 15 25	3bitr4i	$⊢ z \in \underset{˙}{⊥} (A \cup B) \leftrightarrow z \in (\underset{˙}{⊥} (A) \cap \underset{˙}{⊥} (B))$
27	26	eqriv	$⊢ \underset{˙}{⊥} (A \cup B) = \underset{˙}{⊥} (A) \cap \underset{˙}{⊥} (B)$

Metamath Proof Explorer

Theorem unocv

Proof