iunocv

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

	Ref	Expression
Hypotheses	inocv.o	$⊢ \underset{˙}{⊥} = ocv (W)$
	iunocv.v	$⊢ V = {Base}_{W}$
Assertion	iunocv	$⊢ \underset{˙}{⊥} (⋃_{x \in A} B) = V \cap ⋂_{x \in A} \underset{˙}{⊥} (B)$

Proof

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

Metamath Proof Explorer

Theorem iunocv

Proof