ocvlss

Description: The orthocomplement of a subset is a linear subspace of the pre-Hilbert space. (Contributed by Mario Carneiro, 13-Oct-2015)

	Ref	Expression
Hypotheses	ocvss.v	$⊢ V = {Base}_{W}$
	ocvss.o	$⊢ \underset{˙}{⊥} = ocv (W)$
	ocvlss.l	$⊢ L = LSubSp (W)$
Assertion	ocvlss	$⊢ (W \in PreHil \land S \subseteq V) \to \underset{˙}{⊥} (S) \in L$

Proof

Step	Hyp	Ref	Expression
1		ocvss.v	$⊢ V = {Base}_{W}$
2		ocvss.o	$⊢ \underset{˙}{⊥} = ocv (W)$
3		ocvlss.l	$⊢ L = LSubSp (W)$
4	1 2	ocvss	$⊢ \underset{˙}{⊥} (S) \subseteq V$
5	4	a1i	$⊢ (W \in PreHil \land S \subseteq V) \to \underset{˙}{⊥} (S) \subseteq V$
6		simpr	$⊢ (W \in PreHil \land S \subseteq V) \to S \subseteq V$
7		phllmod	$⊢ W \in PreHil \to W \in LMod$
8	7	adantr	$⊢ (W \in PreHil \land S \subseteq V) \to W \in LMod$
9		eqid	$⊢ 0_{W} = 0_{W}$
10	1 9	lmod0vcl	$⊢ W \in LMod \to 0_{W} \in V$
11	8 10	syl	$⊢ (W \in PreHil \land S \subseteq V) \to 0_{W} \in V$
12		simpll	$⊢ ((W \in PreHil \land S \subseteq V) \land x \in S) \to W \in PreHil$
13	6	sselda	$⊢ ((W \in PreHil \land S \subseteq V) \land x \in S) \to x \in V$
14		eqid	$⊢ Scalar (W) = Scalar (W)$
15		eqid	$⊢ \cdot_{𝑖} (W) = \cdot_{𝑖} (W)$
16		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
17	14 15 1 16 9	ip0l	$⊢ (W \in PreHil \land x \in V) \to 0_{W} \cdot_{𝑖} (W) x = 0_{Scalar (W)}$
18	12 13 17	syl2anc	$⊢ ((W \in PreHil \land S \subseteq V) \land x \in S) \to 0_{W} \cdot_{𝑖} (W) x = 0_{Scalar (W)}$
19	18	ralrimiva	$⊢ (W \in PreHil \land S \subseteq V) \to \forall x \in S 0_{W} \cdot_{𝑖} (W) x = 0_{Scalar (W)}$
20	1 15 14 16 2	elocv	$⊢ 0_{W} \in \underset{˙}{⊥} (S) \leftrightarrow (S \subseteq V \land 0_{W} \in V \land \forall x \in S 0_{W} \cdot_{𝑖} (W) x = 0_{Scalar (W)})$
21	6 11 19 20	syl3anbrc	$⊢ (W \in PreHil \land S \subseteq V) \to 0_{W} \in \underset{˙}{⊥} (S)$
22	21	ne0d	$⊢ (W \in PreHil \land S \subseteq V) \to \underset{˙}{⊥} (S) \neq \emptyset$
23	6	adantr	$⊢ ((W \in PreHil \land S \subseteq V) \land (r \in {Base}_{Scalar (W)} \land y \in \underset{˙}{⊥} (S) \land z \in \underset{˙}{⊥} (S))) \to S \subseteq V$
24	8	adantr	$⊢ ((W \in PreHil \land S \subseteq V) \land (r \in {Base}_{Scalar (W)} \land y \in \underset{˙}{⊥} (S) \land z \in \underset{˙}{⊥} (S))) \to W \in LMod$
25		simpr1	$⊢ ((W \in PreHil \land S \subseteq V) \land (r \in {Base}_{Scalar (W)} \land y \in \underset{˙}{⊥} (S) \land z \in \underset{˙}{⊥} (S))) \to r \in {Base}_{Scalar (W)}$
26		simpr2	$⊢ ((W \in PreHil \land S \subseteq V) \land (r \in {Base}_{Scalar (W)} \land y \in \underset{˙}{⊥} (S) \land z \in \underset{˙}{⊥} (S))) \to y \in \underset{˙}{⊥} (S)$
27	4 26	sseldi	$⊢ ((W \in PreHil \land S \subseteq V) \land (r \in {Base}_{Scalar (W)} \land y \in \underset{˙}{⊥} (S) \land z \in \underset{˙}{⊥} (S))) \to y \in V$
28		eqid	$⊢ \cdot_{W} = \cdot_{W}$
29		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
30	1 14 28 29	lmodvscl	$⊢ (W \in LMod \land r \in {Base}_{Scalar (W)} \land y \in V) \to r \cdot_{W} y \in V$
31	24 25 27 30	syl3anc	$⊢ ((W \in PreHil \land S \subseteq V) \land (r \in {Base}_{Scalar (W)} \land y \in \underset{˙}{⊥} (S) \land z \in \underset{˙}{⊥} (S))) \to r \cdot_{W} y \in V$
32		simpr3	$⊢ ((W \in PreHil \land S \subseteq V) \land (r \in {Base}_{Scalar (W)} \land y \in \underset{˙}{⊥} (S) \land z \in \underset{˙}{⊥} (S))) \to z \in \underset{˙}{⊥} (S)$
33	4 32	sseldi	$⊢ ((W \in PreHil \land S \subseteq V) \land (r \in {Base}_{Scalar (W)} \land y \in \underset{˙}{⊥} (S) \land z \in \underset{˙}{⊥} (S))) \to z \in V$
34		eqid	$⊢ +_{W} = +_{W}$
35	1 34	lmodvacl	$⊢ (W \in LMod \land r \cdot_{W} y \in V \land z \in V) \to (r \cdot_{W} y) +_{W} z \in V$
36	24 31 33 35	syl3anc	$⊢ ((W \in PreHil \land S \subseteq V) \land (r \in {Base}_{Scalar (W)} \land y \in \underset{˙}{⊥} (S) \land z \in \underset{˙}{⊥} (S))) \to (r \cdot_{W} y) +_{W} z \in V$
37	12	adantlr	$⊢ (((W \in PreHil \land S \subseteq V) \land (r \in {Base}_{Scalar (W)} \land y \in \underset{˙}{⊥} (S) \land z \in \underset{˙}{⊥} (S))) \land x \in S) \to W \in PreHil$
38	31	adantr	$⊢ (((W \in PreHil \land S \subseteq V) \land (r \in {Base}_{Scalar (W)} \land y \in \underset{˙}{⊥} (S) \land z \in \underset{˙}{⊥} (S))) \land x \in S) \to r \cdot_{W} y \in V$
39	33	adantr	$⊢ (((W \in PreHil \land S \subseteq V) \land (r \in {Base}_{Scalar (W)} \land y \in \underset{˙}{⊥} (S) \land z \in \underset{˙}{⊥} (S))) \land x \in S) \to z \in V$
40	13	adantlr	$⊢ (((W \in PreHil \land S \subseteq V) \land (r \in {Base}_{Scalar (W)} \land y \in \underset{˙}{⊥} (S) \land z \in \underset{˙}{⊥} (S))) \land x \in S) \to x \in V$
41		eqid	$⊢ +_{Scalar (W)} = +_{Scalar (W)}$
42	14 15 1 34 41	ipdir	$⊢ (W \in PreHil \land (r \cdot_{W} y \in V \land z \in V \land x \in V)) \to ((r \cdot_{W} y) +_{W} z) \cdot_{𝑖} (W) x = ((r \cdot_{W} y) \cdot_{𝑖} (W) x) +_{Scalar (W)} (z \cdot_{𝑖} (W) x)$
43	37 38 39 40 42	syl13anc	$⊢ (((W \in PreHil \land S \subseteq V) \land (r \in {Base}_{Scalar (W)} \land y \in \underset{˙}{⊥} (S) \land z \in \underset{˙}{⊥} (S))) \land x \in S) \to ((r \cdot_{W} y) +_{W} z) \cdot_{𝑖} (W) x = ((r \cdot_{W} y) \cdot_{𝑖} (W) x) +_{Scalar (W)} (z \cdot_{𝑖} (W) x)$
44	25	adantr	$⊢ (((W \in PreHil \land S \subseteq V) \land (r \in {Base}_{Scalar (W)} \land y \in \underset{˙}{⊥} (S) \land z \in \underset{˙}{⊥} (S))) \land x \in S) \to r \in {Base}_{Scalar (W)}$
45	27	adantr	$⊢ (((W \in PreHil \land S \subseteq V) \land (r \in {Base}_{Scalar (W)} \land y \in \underset{˙}{⊥} (S) \land z \in \underset{˙}{⊥} (S))) \land x \in S) \to y \in V$
46		eqid	$⊢ \cdot_{Scalar (W)} = \cdot_{Scalar (W)}$
47	14 15 1 29 28 46	ipass	$⊢ (W \in PreHil \land (r \in {Base}_{Scalar (W)} \land y \in V \land x \in V)) \to (r \cdot_{W} y) \cdot_{𝑖} (W) x = r \cdot_{Scalar (W)} (y \cdot_{𝑖} (W) x)$
48	37 44 45 40 47	syl13anc	$⊢ (((W \in PreHil \land S \subseteq V) \land (r \in {Base}_{Scalar (W)} \land y \in \underset{˙}{⊥} (S) \land z \in \underset{˙}{⊥} (S))) \land x \in S) \to (r \cdot_{W} y) \cdot_{𝑖} (W) x = r \cdot_{Scalar (W)} (y \cdot_{𝑖} (W) x)$
49	1 15 14 16 2	ocvi	$⊢ (y \in \underset{˙}{⊥} (S) \land x \in S) \to y \cdot_{𝑖} (W) x = 0_{Scalar (W)}$
50	26 49	sylan	$⊢ (((W \in PreHil \land S \subseteq V) \land (r \in {Base}_{Scalar (W)} \land y \in \underset{˙}{⊥} (S) \land z \in \underset{˙}{⊥} (S))) \land x \in S) \to y \cdot_{𝑖} (W) x = 0_{Scalar (W)}$
51	50	oveq2d	$⊢ (((W \in PreHil \land S \subseteq V) \land (r \in {Base}_{Scalar (W)} \land y \in \underset{˙}{⊥} (S) \land z \in \underset{˙}{⊥} (S))) \land x \in S) \to r \cdot_{Scalar (W)} (y \cdot_{𝑖} (W) x) = r \cdot_{Scalar (W)} 0_{Scalar (W)}$
52	24	adantr	$⊢ (((W \in PreHil \land S \subseteq V) \land (r \in {Base}_{Scalar (W)} \land y \in \underset{˙}{⊥} (S) \land z \in \underset{˙}{⊥} (S))) \land x \in S) \to W \in LMod$
53	14	lmodring	$⊢ W \in LMod \to Scalar (W) \in Ring$
54	52 53	syl	$⊢ (((W \in PreHil \land S \subseteq V) \land (r \in {Base}_{Scalar (W)} \land y \in \underset{˙}{⊥} (S) \land z \in \underset{˙}{⊥} (S))) \land x \in S) \to Scalar (W) \in Ring$
55	29 46 16	ringrz	$⊢ (Scalar (W) \in Ring \land r \in {Base}_{Scalar (W)}) \to r \cdot_{Scalar (W)} 0_{Scalar (W)} = 0_{Scalar (W)}$
56	54 44 55	syl2anc	$⊢ (((W \in PreHil \land S \subseteq V) \land (r \in {Base}_{Scalar (W)} \land y \in \underset{˙}{⊥} (S) \land z \in \underset{˙}{⊥} (S))) \land x \in S) \to r \cdot_{Scalar (W)} 0_{Scalar (W)} = 0_{Scalar (W)}$
57	48 51 56	3eqtrd	$⊢ (((W \in PreHil \land S \subseteq V) \land (r \in {Base}_{Scalar (W)} \land y \in \underset{˙}{⊥} (S) \land z \in \underset{˙}{⊥} (S))) \land x \in S) \to (r \cdot_{W} y) \cdot_{𝑖} (W) x = 0_{Scalar (W)}$
58	1 15 14 16 2	ocvi	$⊢ (z \in \underset{˙}{⊥} (S) \land x \in S) \to z \cdot_{𝑖} (W) x = 0_{Scalar (W)}$
59	32 58	sylan	$⊢ (((W \in PreHil \land S \subseteq V) \land (r \in {Base}_{Scalar (W)} \land y \in \underset{˙}{⊥} (S) \land z \in \underset{˙}{⊥} (S))) \land x \in S) \to z \cdot_{𝑖} (W) x = 0_{Scalar (W)}$
60	57 59	oveq12d	$⊢ (((W \in PreHil \land S \subseteq V) \land (r \in {Base}_{Scalar (W)} \land y \in \underset{˙}{⊥} (S) \land z \in \underset{˙}{⊥} (S))) \land x \in S) \to ((r \cdot_{W} y) \cdot_{𝑖} (W) x) +_{Scalar (W)} (z \cdot_{𝑖} (W) x) = 0_{Scalar (W)} +_{Scalar (W)} 0_{Scalar (W)}$
61	14	lmodfgrp	$⊢ W \in LMod \to Scalar (W) \in Grp$
62	29 16	grpidcl	$⊢ Scalar (W) \in Grp \to 0_{Scalar (W)} \in {Base}_{Scalar (W)}$
63	29 41 16	grplid	$⊢ (Scalar (W) \in Grp \land 0_{Scalar (W)} \in {Base}_{Scalar (W)}) \to 0_{Scalar (W)} +_{Scalar (W)} 0_{Scalar (W)} = 0_{Scalar (W)}$
64	62 63	mpdan	$⊢ Scalar (W) \in Grp \to 0_{Scalar (W)} +_{Scalar (W)} 0_{Scalar (W)} = 0_{Scalar (W)}$
65	52 61 64	3syl	$⊢ (((W \in PreHil \land S \subseteq V) \land (r \in {Base}_{Scalar (W)} \land y \in \underset{˙}{⊥} (S) \land z \in \underset{˙}{⊥} (S))) \land x \in S) \to 0_{Scalar (W)} +_{Scalar (W)} 0_{Scalar (W)} = 0_{Scalar (W)}$
66	43 60 65	3eqtrd	$⊢ (((W \in PreHil \land S \subseteq V) \land (r \in {Base}_{Scalar (W)} \land y \in \underset{˙}{⊥} (S) \land z \in \underset{˙}{⊥} (S))) \land x \in S) \to ((r \cdot_{W} y) +_{W} z) \cdot_{𝑖} (W) x = 0_{Scalar (W)}$
67	66	ralrimiva	$⊢ ((W \in PreHil \land S \subseteq V) \land (r \in {Base}_{Scalar (W)} \land y \in \underset{˙}{⊥} (S) \land z \in \underset{˙}{⊥} (S))) \to \forall x \in S ((r \cdot_{W} y) +_{W} z) \cdot_{𝑖} (W) x = 0_{Scalar (W)}$
68	1 15 14 16 2	elocv	$⊢ (r \cdot_{W} y) +_{W} z \in \underset{˙}{⊥} (S) \leftrightarrow (S \subseteq V \land (r \cdot_{W} y) +_{W} z \in V \land \forall x \in S ((r \cdot_{W} y) +_{W} z) \cdot_{𝑖} (W) x = 0_{Scalar (W)})$
69	23 36 67 68	syl3anbrc	$⊢ ((W \in PreHil \land S \subseteq V) \land (r \in {Base}_{Scalar (W)} \land y \in \underset{˙}{⊥} (S) \land z \in \underset{˙}{⊥} (S))) \to (r \cdot_{W} y) +_{W} z \in \underset{˙}{⊥} (S)$
70	69	ralrimivvva	$⊢ (W \in PreHil \land S \subseteq V) \to \forall r \in {Base}_{Scalar (W)} \forall y \in \underset{˙}{⊥} (S) \forall z \in \underset{˙}{⊥} (S) (r \cdot_{W} y) +_{W} z \in \underset{˙}{⊥} (S)$
71	14 29 1 34 28 3	islss	$⊢ \underset{˙}{⊥} (S) \in L \leftrightarrow (\underset{˙}{⊥} (S) \subseteq V \land \underset{˙}{⊥} (S) \neq \emptyset \land \forall r \in {Base}_{Scalar (W)} \forall y \in \underset{˙}{⊥} (S) \forall z \in \underset{˙}{⊥} (S) (r \cdot_{W} y) +_{W} z \in \underset{˙}{⊥} (S))$
72	5 22 70 71	syl3anbrc	$⊢ (W \in PreHil \land S \subseteq V) \to \underset{˙}{⊥} (S) \in L$

Metamath Proof Explorer

Theorem ocvlss

Proof