Theorem lclkrlem2p

Description: Lemma for lclkr . When B is zero, X and Y must colinear, so their orthocomplements must be comparable. (Contributed by NM, 17-Jan-2015)

	Ref	Expression
Hypotheses	lclkrlem2m.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	lclkrlem2m.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
	lclkrlem2m.s	⊢ 𝑆 = ( Scalar ‘ 𝑈 )
	lclkrlem2m.q	⊢ × = ( .r ‘ 𝑆 )
	lclkrlem2m.z	⊢ 0 = ( 0g ‘ 𝑆 )
	lclkrlem2m.i	⊢ 𝐼 = ( invr ‘ 𝑆 )
	lclkrlem2m.m	⊢ − = ( -g ‘ 𝑈 )
	lclkrlem2m.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	lclkrlem2m.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
	lclkrlem2m.p	⊢ + = ( +g ‘ 𝐷 )
	lclkrlem2m.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	lclkrlem2m.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
	lclkrlem2m.e	⊢ ( 𝜑 → 𝐸 ∈ 𝐹 )
	lclkrlem2m.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
	lclkrlem2n.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
	lclkrlem2n.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	lclkrlem2o.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lclkrlem2o.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	lclkrlem2o.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lclkrlem2o.a	⊢ ⊕ = ( LSSum ‘ 𝑈 )
	lclkrlem2o.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	lclkrlem2o.b	⊢ 𝐵 = ( 𝑋 − ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) )
	lclkrlem2o.n	⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ 0 )
	lclkrlem2p.bn	⊢ ( 𝜑 → 𝐵 = ( 0g ‘ 𝑈 ) )
Assertion	lclkrlem2p	⊢ ( 𝜑 → ( ⊥ ‘ { 𝑌 } ) ⊆ ( ⊥ ‘ { 𝑋 } ) )

Proof

Step	Hyp	Ref	Expression
1		lclkrlem2m.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
2		lclkrlem2m.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
3		lclkrlem2m.s	⊢ 𝑆 = ( Scalar ‘ 𝑈 )
4		lclkrlem2m.q	⊢ × = ( .r ‘ 𝑆 )
5		lclkrlem2m.z	⊢ 0 = ( 0g ‘ 𝑆 )
6		lclkrlem2m.i	⊢ 𝐼 = ( invr ‘ 𝑆 )
7		lclkrlem2m.m	⊢ − = ( -g ‘ 𝑈 )
8		lclkrlem2m.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
9		lclkrlem2m.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
10		lclkrlem2m.p	⊢ + = ( +g ‘ 𝐷 )
11		lclkrlem2m.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
12		lclkrlem2m.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
13		lclkrlem2m.e	⊢ ( 𝜑 → 𝐸 ∈ 𝐹 )
14		lclkrlem2m.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
15		lclkrlem2n.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
16		lclkrlem2n.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
17		lclkrlem2o.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
18		lclkrlem2o.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
19		lclkrlem2o.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
20		lclkrlem2o.a	⊢ ⊕ = ( LSSum ‘ 𝑈 )
21		lclkrlem2o.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
22		lclkrlem2o.b	⊢ 𝐵 = ( 𝑋 − ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) )
23		lclkrlem2o.n	⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ 0 )
24		lclkrlem2p.bn	⊢ ( 𝜑 → 𝐵 = ( 0g ‘ 𝑈 ) )
25	17 19 21	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
26		eqid	⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
27	1 26 15	lspsncl	⊢ ( ( 𝑈 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) )
28	25 12 27	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) )
29	1 26	lssss	⊢ ( ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) → ( 𝑁 ‘ { 𝑌 } ) ⊆ 𝑉 )
30	28 29	syl	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ⊆ 𝑉 )
31	22 24	eqtr3id	⊢ ( 𝜑 → ( 𝑋 − ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) = ( 0g ‘ 𝑈 ) )
32	3	lmodring	⊢ ( 𝑈 ∈ LMod → 𝑆 ∈ Ring )
33	25 32	syl	⊢ ( 𝜑 → 𝑆 ∈ Ring )
34	8 9 10 25 13 14	ldualvaddcl	⊢ ( 𝜑 → ( 𝐸 + 𝐺 ) ∈ 𝐹 )
35		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
36	3 35 1 8	lflcl	⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝐸 + 𝐺 ) ∈ 𝐹 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
37	25 34 11 36	syl3anc	⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
38	17 19 21	dvhlvec	⊢ ( 𝜑 → 𝑈 ∈ LVec )
39	3	lvecdrng	⊢ ( 𝑈 ∈ LVec → 𝑆 ∈ DivRing )
40	38 39	syl	⊢ ( 𝜑 → 𝑆 ∈ DivRing )
41	3 35 1 8	lflcl	⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝐸 + 𝐺 ) ∈ 𝐹 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝑆 ) )
42	25 34 12 41	syl3anc	⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝑆 ) )
43	35 5 6	drnginvrcl	⊢ ( ( 𝑆 ∈ DivRing ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝑆 ) ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ 0 ) → ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ∈ ( Base ‘ 𝑆 ) )
44	40 42 23 43	syl3anc	⊢ ( 𝜑 → ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ∈ ( Base ‘ 𝑆 ) )
45	35 4	ringcl	⊢ ( ( 𝑆 ∈ Ring ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ∈ ( Base ‘ 𝑆 ) ) → ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) ∈ ( Base ‘ 𝑆 ) )
46	33 37 44 45	syl3anc	⊢ ( 𝜑 → ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) ∈ ( Base ‘ 𝑆 ) )
47	1 3 2 35	lmodvscl	⊢ ( ( 𝑈 ∈ LMod ∧ ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) ∈ ( Base ‘ 𝑆 ) ∧ 𝑌 ∈ 𝑉 ) → ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ∈ 𝑉 )
48	25 46 12 47	syl3anc	⊢ ( 𝜑 → ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ∈ 𝑉 )
49		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
50	1 49 7	lmodsubeq0	⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ∈ 𝑉 ) → ( ( 𝑋 − ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) = ( 0g ‘ 𝑈 ) ↔ 𝑋 = ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) )
51	25 11 48 50	syl3anc	⊢ ( 𝜑 → ( ( 𝑋 − ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) = ( 0g ‘ 𝑈 ) ↔ 𝑋 = ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) )
52	31 51	mpbid	⊢ ( 𝜑 → 𝑋 = ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) )
53	52	sneqd	⊢ ( 𝜑 → { 𝑋 } = { ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) } )
54	53	fveq2d	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) } ) )
55	3 35 1 2 15	lspsnvsi	⊢ ( ( 𝑈 ∈ LMod ∧ ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) ∈ ( Base ‘ 𝑆 ) ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) )
56	25 46 12 55	syl3anc	⊢ ( 𝜑 → ( 𝑁 ‘ { ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) )
57	54 56	eqsstrd	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) )
58	17 19 1 18	dochss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑁 ‘ { 𝑌 } ) ⊆ 𝑉 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑌 } ) ) → ( ⊥ ‘ ( 𝑁 ‘ { 𝑌 } ) ) ⊆ ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 } ) ) )
59	21 30 57 58	syl3anc	⊢ ( 𝜑 → ( ⊥ ‘ ( 𝑁 ‘ { 𝑌 } ) ) ⊆ ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 } ) ) )
60	12	snssd	⊢ ( 𝜑 → { 𝑌 } ⊆ 𝑉 )
61	17 19 18 1 15 21 60	dochocsp	⊢ ( 𝜑 → ( ⊥ ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( ⊥ ‘ { 𝑌 } ) )
62	11	snssd	⊢ ( 𝜑 → { 𝑋 } ⊆ 𝑉 )
63	17 19 18 1 15 21 62	dochocsp	⊢ ( 𝜑 → ( ⊥ ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( ⊥ ‘ { 𝑋 } ) )
64	59 61 63	3sstr3d	⊢ ( 𝜑 → ( ⊥ ‘ { 𝑌 } ) ⊆ ( ⊥ ‘ { 𝑋 } ) )