ocsh

Description: The orthogonal complement of a subspace is a subspace. Part of Remark 3.12 of Beran p. 107. (Contributed by NM, 7-Aug-2000) (New usage is discouraged.)

		Ref	Expression
	Assertion	ocsh	$⊢ A \subseteq ℋ \to ⊥ (A) \in S_{ℋ}$

Proof

Step	Hyp	Ref	Expression
1		ocval	$⊢ A \subseteq ℋ \to ⊥ (A) = \{x \in ℋ \| \forall y \in A x \cdot_{ih} y = 0\}$
2		ssrab2	$⊢ \{x \in ℋ \| \forall y \in A x \cdot_{ih} y = 0\} \subseteq ℋ$
3	1 2	eqsstrdi	$⊢ A \subseteq ℋ \to ⊥ (A) \subseteq ℋ$
4		ssel	$⊢ A \subseteq ℋ \to (y \in A \to y \in ℋ)$
5		hi01	$⊢ y \in ℋ \to 0_{ℎ} \cdot_{ih} y = 0$
6	4 5	syl6	$⊢ A \subseteq ℋ \to (y \in A \to 0_{ℎ} \cdot_{ih} y = 0)$
7	6	ralrimiv	$⊢ A \subseteq ℋ \to \forall y \in A 0_{ℎ} \cdot_{ih} y = 0$
8		ax-hv0cl	$⊢ 0_{ℎ} \in ℋ$
9	7 8	jctil	$⊢ A \subseteq ℋ \to (0_{ℎ} \in ℋ \land \forall y \in A 0_{ℎ} \cdot_{ih} y = 0)$
10		ocel	$⊢ A \subseteq ℋ \to (0_{ℎ} \in ⊥ (A) \leftrightarrow (0_{ℎ} \in ℋ \land \forall y \in A 0_{ℎ} \cdot_{ih} y = 0))$
11	9 10	mpbird	$⊢ A \subseteq ℋ \to 0_{ℎ} \in ⊥ (A)$
12	3 11	jca	$⊢ A \subseteq ℋ \to (⊥ (A) \subseteq ℋ \land 0_{ℎ} \in ⊥ (A))$
13		ssel2	$⊢ (A \subseteq ℋ \land z \in A) \to z \in ℋ$
14		ax-his2	$⊢ (x \in ℋ \land y \in ℋ \land z \in ℋ) \to (x +_{ℎ} y) \cdot_{ih} z = (x \cdot_{ih} z) + (y \cdot_{ih} z)$
15	14	3expa	$⊢ ((x \in ℋ \land y \in ℋ) \land z \in ℋ) \to (x +_{ℎ} y) \cdot_{ih} z = (x \cdot_{ih} z) + (y \cdot_{ih} z)$
16		oveq12	$⊢ (x \cdot_{ih} z = 0 \land y \cdot_{ih} z = 0) \to (x \cdot_{ih} z) + (y \cdot_{ih} z) = 0 + 0$
17		00id	$⊢ 0 + 0 = 0$
18	16 17	eqtrdi	$⊢ (x \cdot_{ih} z = 0 \land y \cdot_{ih} z = 0) \to (x \cdot_{ih} z) + (y \cdot_{ih} z) = 0$
19	15 18	sylan9eq	$⊢ (((x \in ℋ \land y \in ℋ) \land z \in ℋ) \land (x \cdot_{ih} z = 0 \land y \cdot_{ih} z = 0)) \to (x +_{ℎ} y) \cdot_{ih} z = 0$
20	19	ex	$⊢ ((x \in ℋ \land y \in ℋ) \land z \in ℋ) \to ((x \cdot_{ih} z = 0 \land y \cdot_{ih} z = 0) \to (x +_{ℎ} y) \cdot_{ih} z = 0)$
21	20	ancoms	$⊢ (z \in ℋ \land (x \in ℋ \land y \in ℋ)) \to ((x \cdot_{ih} z = 0 \land y \cdot_{ih} z = 0) \to (x +_{ℎ} y) \cdot_{ih} z = 0)$
22	13 21	sylan	$⊢ ((A \subseteq ℋ \land z \in A) \land (x \in ℋ \land y \in ℋ)) \to ((x \cdot_{ih} z = 0 \land y \cdot_{ih} z = 0) \to (x +_{ℎ} y) \cdot_{ih} z = 0)$
23	22	an32s	$⊢ ((A \subseteq ℋ \land (x \in ℋ \land y \in ℋ)) \land z \in A) \to ((x \cdot_{ih} z = 0 \land y \cdot_{ih} z = 0) \to (x +_{ℎ} y) \cdot_{ih} z = 0)$
24	23	ralimdva	$⊢ (A \subseteq ℋ \land (x \in ℋ \land y \in ℋ)) \to (\forall z \in A (x \cdot_{ih} z = 0 \land y \cdot_{ih} z = 0) \to \forall z \in A (x +_{ℎ} y) \cdot_{ih} z = 0)$
25	24	imdistanda	$⊢ A \subseteq ℋ \to (((x \in ℋ \land y \in ℋ) \land \forall z \in A (x \cdot_{ih} z = 0 \land y \cdot_{ih} z = 0)) \to ((x \in ℋ \land y \in ℋ) \land \forall z \in A (x +_{ℎ} y) \cdot_{ih} z = 0))$
26		hvaddcl	$⊢ (x \in ℋ \land y \in ℋ) \to x +_{ℎ} y \in ℋ$
27	26	anim1i	$⊢ ((x \in ℋ \land y \in ℋ) \land \forall z \in A (x +_{ℎ} y) \cdot_{ih} z = 0) \to (x +_{ℎ} y \in ℋ \land \forall z \in A (x +_{ℎ} y) \cdot_{ih} z = 0)$
28	25 27	syl6	$⊢ A \subseteq ℋ \to (((x \in ℋ \land y \in ℋ) \land \forall z \in A (x \cdot_{ih} z = 0 \land y \cdot_{ih} z = 0)) \to (x +_{ℎ} y \in ℋ \land \forall z \in A (x +_{ℎ} y) \cdot_{ih} z = 0))$
29		ocel	$⊢ A \subseteq ℋ \to (x \in ⊥ (A) \leftrightarrow (x \in ℋ \land \forall z \in A x \cdot_{ih} z = 0))$
30		ocel	$⊢ A \subseteq ℋ \to (y \in ⊥ (A) \leftrightarrow (y \in ℋ \land \forall z \in A y \cdot_{ih} z = 0))$
31	29 30	anbi12d	$⊢ A \subseteq ℋ \to ((x \in ⊥ (A) \land y \in ⊥ (A)) \leftrightarrow ((x \in ℋ \land \forall z \in A x \cdot_{ih} z = 0) \land (y \in ℋ \land \forall z \in A y \cdot_{ih} z = 0)))$
32		an4	$⊢ ((x \in ℋ \land \forall z \in A x \cdot_{ih} z = 0) \land (y \in ℋ \land \forall z \in A y \cdot_{ih} z = 0)) \leftrightarrow ((x \in ℋ \land y \in ℋ) \land (\forall z \in A x \cdot_{ih} z = 0 \land \forall z \in A y \cdot_{ih} z = 0))$
33		r19.26	$⊢ \forall z \in A (x \cdot_{ih} z = 0 \land y \cdot_{ih} z = 0) \leftrightarrow (\forall z \in A x \cdot_{ih} z = 0 \land \forall z \in A y \cdot_{ih} z = 0)$
34	33	anbi2i	$⊢ ((x \in ℋ \land y \in ℋ) \land \forall z \in A (x \cdot_{ih} z = 0 \land y \cdot_{ih} z = 0)) \leftrightarrow ((x \in ℋ \land y \in ℋ) \land (\forall z \in A x \cdot_{ih} z = 0 \land \forall z \in A y \cdot_{ih} z = 0))$
35	32 34	bitr4i	$⊢ ((x \in ℋ \land \forall z \in A x \cdot_{ih} z = 0) \land (y \in ℋ \land \forall z \in A y \cdot_{ih} z = 0)) \leftrightarrow ((x \in ℋ \land y \in ℋ) \land \forall z \in A (x \cdot_{ih} z = 0 \land y \cdot_{ih} z = 0))$
36	31 35	bitrdi	$⊢ A \subseteq ℋ \to ((x \in ⊥ (A) \land y \in ⊥ (A)) \leftrightarrow ((x \in ℋ \land y \in ℋ) \land \forall z \in A (x \cdot_{ih} z = 0 \land y \cdot_{ih} z = 0)))$
37		ocel	$⊢ A \subseteq ℋ \to (x +_{ℎ} y \in ⊥ (A) \leftrightarrow (x +_{ℎ} y \in ℋ \land \forall z \in A (x +_{ℎ} y) \cdot_{ih} z = 0))$
38	28 36 37	3imtr4d	$⊢ A \subseteq ℋ \to ((x \in ⊥ (A) \land y \in ⊥ (A)) \to x +_{ℎ} y \in ⊥ (A))$
39	38	ralrimivv	$⊢ A \subseteq ℋ \to \forall x \in ⊥ (A) \forall y \in ⊥ (A) x +_{ℎ} y \in ⊥ (A)$
40		mul01	$⊢ x \in ℂ \to x \cdot 0 = 0$
41		oveq2	$⊢ y \cdot_{ih} z = 0 \to x (y \cdot_{ih} z) = x \cdot 0$
42	41	eqeq1d	$⊢ y \cdot_{ih} z = 0 \to (x (y \cdot_{ih} z) = 0 \leftrightarrow x \cdot 0 = 0)$
43	40 42	syl5ibrcom	$⊢ x \in ℂ \to (y \cdot_{ih} z = 0 \to x (y \cdot_{ih} z) = 0)$
44	43	ad2antrl	$⊢ (z \in ℋ \land (x \in ℂ \land y \in ℋ)) \to (y \cdot_{ih} z = 0 \to x (y \cdot_{ih} z) = 0)$
45		ax-his3	$⊢ (x \in ℂ \land y \in ℋ \land z \in ℋ) \to (x \cdot_{ℎ} y) \cdot_{ih} z = x (y \cdot_{ih} z)$
46	45	eqeq1d	$⊢ (x \in ℂ \land y \in ℋ \land z \in ℋ) \to ((x \cdot_{ℎ} y) \cdot_{ih} z = 0 \leftrightarrow x (y \cdot_{ih} z) = 0)$
47	46	3expa	$⊢ ((x \in ℂ \land y \in ℋ) \land z \in ℋ) \to ((x \cdot_{ℎ} y) \cdot_{ih} z = 0 \leftrightarrow x (y \cdot_{ih} z) = 0)$
48	47	ancoms	$⊢ (z \in ℋ \land (x \in ℂ \land y \in ℋ)) \to ((x \cdot_{ℎ} y) \cdot_{ih} z = 0 \leftrightarrow x (y \cdot_{ih} z) = 0)$
49	44 48	sylibrd	$⊢ (z \in ℋ \land (x \in ℂ \land y \in ℋ)) \to (y \cdot_{ih} z = 0 \to (x \cdot_{ℎ} y) \cdot_{ih} z = 0)$
50	13 49	sylan	$⊢ ((A \subseteq ℋ \land z \in A) \land (x \in ℂ \land y \in ℋ)) \to (y \cdot_{ih} z = 0 \to (x \cdot_{ℎ} y) \cdot_{ih} z = 0)$
51	50	an32s	$⊢ ((A \subseteq ℋ \land (x \in ℂ \land y \in ℋ)) \land z \in A) \to (y \cdot_{ih} z = 0 \to (x \cdot_{ℎ} y) \cdot_{ih} z = 0)$
52	51	ralimdva	$⊢ (A \subseteq ℋ \land (x \in ℂ \land y \in ℋ)) \to (\forall z \in A y \cdot_{ih} z = 0 \to \forall z \in A (x \cdot_{ℎ} y) \cdot_{ih} z = 0)$
53	52	imdistanda	$⊢ A \subseteq ℋ \to (((x \in ℂ \land y \in ℋ) \land \forall z \in A y \cdot_{ih} z = 0) \to ((x \in ℂ \land y \in ℋ) \land \forall z \in A (x \cdot_{ℎ} y) \cdot_{ih} z = 0))$
54		hvmulcl	$⊢ (x \in ℂ \land y \in ℋ) \to x \cdot_{ℎ} y \in ℋ$
55	54	anim1i	$⊢ ((x \in ℂ \land y \in ℋ) \land \forall z \in A (x \cdot_{ℎ} y) \cdot_{ih} z = 0) \to (x \cdot_{ℎ} y \in ℋ \land \forall z \in A (x \cdot_{ℎ} y) \cdot_{ih} z = 0)$
56	53 55	syl6	$⊢ A \subseteq ℋ \to (((x \in ℂ \land y \in ℋ) \land \forall z \in A y \cdot_{ih} z = 0) \to (x \cdot_{ℎ} y \in ℋ \land \forall z \in A (x \cdot_{ℎ} y) \cdot_{ih} z = 0))$
57	30	anbi2d	$⊢ A \subseteq ℋ \to ((x \in ℂ \land y \in ⊥ (A)) \leftrightarrow (x \in ℂ \land (y \in ℋ \land \forall z \in A y \cdot_{ih} z = 0)))$
58		anass	$⊢ ((x \in ℂ \land y \in ℋ) \land \forall z \in A y \cdot_{ih} z = 0) \leftrightarrow (x \in ℂ \land (y \in ℋ \land \forall z \in A y \cdot_{ih} z = 0))$
59	57 58	bitr4di	$⊢ A \subseteq ℋ \to ((x \in ℂ \land y \in ⊥ (A)) \leftrightarrow ((x \in ℂ \land y \in ℋ) \land \forall z \in A y \cdot_{ih} z = 0))$
60		ocel	$⊢ A \subseteq ℋ \to (x \cdot_{ℎ} y \in ⊥ (A) \leftrightarrow (x \cdot_{ℎ} y \in ℋ \land \forall z \in A (x \cdot_{ℎ} y) \cdot_{ih} z = 0))$
61	56 59 60	3imtr4d	$⊢ A \subseteq ℋ \to ((x \in ℂ \land y \in ⊥ (A)) \to x \cdot_{ℎ} y \in ⊥ (A))$
62	61	ralrimivv	$⊢ A \subseteq ℋ \to \forall x \in ℂ \forall y \in ⊥ (A) x \cdot_{ℎ} y \in ⊥ (A)$
63	39 62	jca	$⊢ A \subseteq ℋ \to (\forall x \in ⊥ (A) \forall y \in ⊥ (A) x +_{ℎ} y \in ⊥ (A) \land \forall x \in ℂ \forall y \in ⊥ (A) x \cdot_{ℎ} y \in ⊥ (A))$
64		issh2	$⊢ ⊥ (A) \in S_{ℋ} \leftrightarrow ((⊥ (A) \subseteq ℋ \land 0_{ℎ} \in ⊥ (A)) \land (\forall x \in ⊥ (A) \forall y \in ⊥ (A) x +_{ℎ} y \in ⊥ (A) \land \forall x \in ℂ \forall y \in ⊥ (A) x \cdot_{ℎ} y \in ⊥ (A)))$
65	12 63 64	sylanbrc	$⊢ A \subseteq ℋ \to ⊥ (A) \in S_{ℋ}$

Metamath Proof Explorer

Theorem ocsh

Proof