Theorem lcfrlem6

Description: Lemma for lcfr . Closure of vector sum with colinear vectors. TODO: Move down N definition so top hypotheses can be shared. (Contributed by NM, 10-Mar-2015)

	Ref	Expression
Hypotheses	lcfrlem6.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcfrlem6.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	lcfrlem6.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lcfrlem6.p	⊢ + = ( +g ‘ 𝑈 )
	lcfrlem6.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
	lcfrlem6.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	lcfrlem6.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
	lcfrlem6.q	⊢ 𝑄 = ( LSubSp ‘ 𝐷 )
	lcfrlem6.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	lcfrlem6.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑄 )
	lcfrlem6.e	⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) )
	lcfrlem6.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐸 )
	lcfrlem6.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐸 )
	lcfrlem6.en	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) )
Assertion	lcfrlem6	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		lcfrlem6.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcfrlem6.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		lcfrlem6.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		lcfrlem6.p	⊢ + = ( +g ‘ 𝑈 )
5		lcfrlem6.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
6		lcfrlem6.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
7		lcfrlem6.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
8		lcfrlem6.q	⊢ 𝑄 = ( LSubSp ‘ 𝐷 )
9		lcfrlem6.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10		lcfrlem6.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑄 )
11		lcfrlem6.e	⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) )
12		lcfrlem6.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐸 )
13		lcfrlem6.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐸 )
14		lcfrlem6.en	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) )
15	12 11	eleqtrdi	⊢ ( 𝜑 → 𝑋 ∈ ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) )
16		eliun	⊢ ( 𝑋 ∈ ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ↔ ∃ 𝑔 ∈ 𝐺 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) )
17	15 16	sylib	⊢ ( 𝜑 → ∃ 𝑔 ∈ 𝐺 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) )
18	1 3 9	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
19	18	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) → 𝑈 ∈ LMod )
20	19	adantr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → 𝑈 ∈ LMod )
21	9	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
22		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
23		eqid	⊢ ( LFnl ‘ 𝑈 ) = ( LFnl ‘ 𝑈 )
24		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
25	24 8	lssel	⊢ ( ( 𝐺 ∈ 𝑄 ∧ 𝑔 ∈ 𝐺 ) → 𝑔 ∈ ( Base ‘ 𝐷 ) )
26	10 25	sylan	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) → 𝑔 ∈ ( Base ‘ 𝐷 ) )
27	23 7 24 18	ldualvbase	⊢ ( 𝜑 → ( Base ‘ 𝐷 ) = ( LFnl ‘ 𝑈 ) )
28	27	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) → ( Base ‘ 𝐷 ) = ( LFnl ‘ 𝑈 ) )
29	26 28	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) → 𝑔 ∈ ( LFnl ‘ 𝑈 ) )
30	22 23 6 19 29	lkrssv	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) → ( 𝐿 ‘ 𝑔 ) ⊆ ( Base ‘ 𝑈 ) )
31		eqid	⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
32	1 3 22 31 2	dochlss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ 𝑔 ) ⊆ ( Base ‘ 𝑈 ) ) → ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
33	21 30 32	syl2anc	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) → ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
34	33	adantr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
35		simpr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) )
36	14	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) )
37	36	adantr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) )
38		simpr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) )
39	37 38	eqsstrrd	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → ( 𝑁 ‘ { 𝑌 } ) ⊆ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) )
40	39	ex	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) → ( ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) → ( 𝑁 ‘ { 𝑌 } ) ⊆ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) )
41	1 2 3 22 6 7 8 11 9 10 12	lcfrlem4	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑈 ) )
42	41	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) → 𝑋 ∈ ( Base ‘ 𝑈 ) )
43	22 31 5 19 33 42	ellspsn5b	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) → ( 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) )
44	1 2 3 22 6 7 8 11 9 10 13	lcfrlem4	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝑈 ) )
45	44	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) → 𝑌 ∈ ( Base ‘ 𝑈 ) )
46	22 31 5 19 33 45	ellspsn5b	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) → ( 𝑌 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ↔ ( 𝑁 ‘ { 𝑌 } ) ⊆ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) )
47	40 43 46	3imtr4d	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) → ( 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) → 𝑌 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) )
48	47	imp	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → 𝑌 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) )
49	4 31	lssvacl	⊢ ( ( ( 𝑈 ∈ LMod ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ∈ ( LSubSp ‘ 𝑈 ) ) ∧ ( 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ∧ 𝑌 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) ) → ( 𝑋 + 𝑌 ) ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) )
50	20 34 35 48 49	syl22anc	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → ( 𝑋 + 𝑌 ) ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) )
51	50	ex	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) → ( 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) → ( 𝑋 + 𝑌 ) ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) )
52	51	reximdva	⊢ ( 𝜑 → ( ∃ 𝑔 ∈ 𝐺 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) → ∃ 𝑔 ∈ 𝐺 ( 𝑋 + 𝑌 ) ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) )
53	17 52	mpd	⊢ ( 𝜑 → ∃ 𝑔 ∈ 𝐺 ( 𝑋 + 𝑌 ) ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) )
54		eliun	⊢ ( ( 𝑋 + 𝑌 ) ∈ ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ↔ ∃ 𝑔 ∈ 𝐺 ( 𝑋 + 𝑌 ) ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) )
55	53 54	sylibr	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) )
56	55 11	eleqtrrdi	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝐸 )