Theorem 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	⊢ 𝑉 = ( Base ‘ 𝑊 )
	ocvss.o	⊢ ⊥ = ( ocv ‘ 𝑊 )
	ocvlss.l	⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
Assertion	ocvlss	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑆 ) ∈ 𝐿 )

Proof

Step	Hyp	Ref	Expression
1		ocvss.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		ocvss.o	⊢ ⊥ = ( ocv ‘ 𝑊 )
3		ocvlss.l	⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
4	1 2	ocvss	⊢ ( ⊥ ‘ 𝑆 ) ⊆ 𝑉
5	4	a1i	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑆 ) ⊆ 𝑉 )
6		simpr	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → 𝑆 ⊆ 𝑉 )
7		phllmod	⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )
8	7	adantr	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → 𝑊 ∈ LMod )
9		eqid	⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
10	1 9	lmod0vcl	⊢ ( 𝑊 ∈ LMod → ( 0g ‘ 𝑊 ) ∈ 𝑉 )
11	8 10	syl	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( 0g ‘ 𝑊 ) ∈ 𝑉 )
12		simpll	⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑊 ∈ PreHil )
13	6	sselda	⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑉 )
14		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
15		eqid	⊢ ( ·𝑖 ‘ 𝑊 ) = ( ·𝑖 ‘ 𝑊 )
16		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
17	14 15 1 16 9	ip0l	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑥 ∈ 𝑉 ) → ( ( 0g ‘ 𝑊 ) ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
18	12 13 17	syl2anc	⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 0g ‘ 𝑊 ) ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
19	18	ralrimiva	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ∀ 𝑥 ∈ 𝑆 ( ( 0g ‘ 𝑊 ) ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
20	1 15 14 16 2	elocv	⊢ ( ( 0g ‘ 𝑊 ) ∈ ( ⊥ ‘ 𝑆 ) ↔ ( 𝑆 ⊆ 𝑉 ∧ ( 0g ‘ 𝑊 ) ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 0g ‘ 𝑊 ) ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
21	6 11 19 20	syl3anbrc	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( 0g ‘ 𝑊 ) ∈ ( ⊥ ‘ 𝑆 ) )
22	21	ne0d	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑆 ) ≠ ∅ )
23	6	adantr	⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) → 𝑆 ⊆ 𝑉 )
24	8	adantr	⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) → 𝑊 ∈ LMod )
25		simpr1	⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) → 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
26		simpr2	⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) → 𝑦 ∈ ( ⊥ ‘ 𝑆 ) )
27	4 26	sselid	⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) → 𝑦 ∈ 𝑉 )
28		eqid	⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
29		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
30	1 14 28 29	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ 𝑉 ) → ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑉 )
31	24 25 27 30	syl3anc	⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑉 )
32		simpr3	⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) → 𝑧 ∈ ( ⊥ ‘ 𝑆 ) )
33	4 32	sselid	⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) → 𝑧 ∈ 𝑉 )
34		eqid	⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
35	1 34	lmodvacl	⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ∈ 𝑉 )
36	24 31 33 35	syl3anc	⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ∈ 𝑉 )
37	12	adantlr	⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑊 ∈ PreHil )
38	31	adantr	⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑉 )
39	33	adantr	⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑧 ∈ 𝑉 )
40	13	adantlr	⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑉 )
41		eqid	⊢ ( +g ‘ ( Scalar ‘ 𝑊 ) ) = ( +g ‘ ( Scalar ‘ 𝑊 ) )
42	14 15 1 34 41	ipdir	⊢ ( ( 𝑊 ∈ PreHil ∧ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) ) → ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ) )
43	37 38 39 40 42	syl13anc	⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ) )
44	25	adantr	⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
45	27	adantr	⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑦 ∈ 𝑉 )
46		eqid	⊢ ( .r ‘ ( Scalar ‘ 𝑊 ) ) = ( .r ‘ ( Scalar ‘ 𝑊 ) )
47	14 15 1 29 28 46	ipass	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( 𝑦 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ) )
48	37 44 45 40 47	syl13anc	⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( 𝑦 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ) )
49	1 15 14 16 2	ocvi	⊢ ( ( 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑦 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
50	26 49	sylan	⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑦 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
51	50	oveq2d	⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( 𝑦 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ) = ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
52	24	adantr	⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑊 ∈ LMod )
53	14	lmodring	⊢ ( 𝑊 ∈ LMod → ( Scalar ‘ 𝑊 ) ∈ Ring )
54	52 53	syl	⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( Scalar ‘ 𝑊 ) ∈ Ring )
55	29 46 16	ringrz	⊢ ( ( ( Scalar ‘ 𝑊 ) ∈ Ring ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
56	54 44 55	syl2anc	⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑟 ( .r ‘ ( Scalar ‘ 𝑊 ) ) ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
57	48 51 56	3eqtrd	⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
58	1 15 14 16 2	ocvi	⊢ ( ( 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
59	32 58	sylan	⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
60	57 59	oveq12d	⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ) = ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
61	14	lmodfgrp	⊢ ( 𝑊 ∈ LMod → ( Scalar ‘ 𝑊 ) ∈ Grp )
62	29 16	grpidcl	⊢ ( ( Scalar ‘ 𝑊 ) ∈ Grp → ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
63	29 41 16	grplid	⊢ ( ( ( Scalar ‘ 𝑊 ) ∈ Grp ∧ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
64	62 63	mpdan	⊢ ( ( Scalar ‘ 𝑊 ) ∈ Grp → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
65	52 61 64	3syl	⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
66	43 60 65	3eqtrd	⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
67	66	ralrimiva	⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) → ∀ 𝑥 ∈ 𝑆 ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
68	1 15 14 16 2	elocv	⊢ ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ 𝑆 ) ↔ ( 𝑆 ⊆ 𝑉 ∧ ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝑆 ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
69	23 36 67 68	syl3anbrc	⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ 𝑆 ) )
70	69	ralrimivvva	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∀ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ 𝑆 ) )
71	14 29 1 34 28 3	islss	⊢ ( ( ⊥ ‘ 𝑆 ) ∈ 𝐿 ↔ ( ( ⊥ ‘ 𝑆 ) ⊆ 𝑉 ∧ ( ⊥ ‘ 𝑆 ) ≠ ∅ ∧ ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∀ 𝑧 ∈ ( ⊥ ‘ 𝑆 ) ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ⊥ ‘ 𝑆 ) ) )
72	5 22 70 71	syl3anbrc	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑆 ) ∈ 𝐿 )