Theorem hdmapglem7a

Description: Lemma for hdmapg . (Contributed by NM, 14-Jun-2015)

	Ref	Expression
Hypotheses	hdmapglem7.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hdmapglem7.e	⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
	hdmapglem7.o	⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	hdmapglem7.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hdmapglem7.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	hdmapglem7.p	⊢ + = ( +g ‘ 𝑈 )
	hdmapglem7.q	⊢ · = ( ·𝑠 ‘ 𝑈 )
	hdmapglem7.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
	hdmapglem7.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	hdmapglem7.a	⊢ ⊕ = ( LSSum ‘ 𝑈 )
	hdmapglem7.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
	hdmapglem7.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	hdmapglem7.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion	hdmapglem7a	⊢ ( 𝜑 → ∃ 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∃ 𝑘 ∈ 𝐵 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) )

Proof

Step	Hyp	Ref	Expression
1		hdmapglem7.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hdmapglem7.e	⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
3		hdmapglem7.o	⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
4		hdmapglem7.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5		hdmapglem7.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
6		hdmapglem7.p	⊢ + = ( +g ‘ 𝑈 )
7		hdmapglem7.q	⊢ · = ( ·𝑠 ‘ 𝑈 )
8		hdmapglem7.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
9		hdmapglem7.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
10		hdmapglem7.a	⊢ ⊕ = ( LSSum ‘ 𝑈 )
11		hdmapglem7.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
12		hdmapglem7.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13		hdmapglem7.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
14		eqid	⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
15	1 4 12	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
16		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
17		eqid	⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
18		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
19	1 16 17 4 5 18 2 12	dvheveccl	⊢ ( 𝜑 → 𝐸 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) )
20	19	eldifad	⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
21	5 14 11	lspsncl	⊢ ( ( 𝑈 ∈ LMod ∧ 𝐸 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝐸 } ) ∈ ( LSubSp ‘ 𝑈 ) )
22	15 20 21	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝐸 } ) ∈ ( LSubSp ‘ 𝑈 ) )
23	20	snssd	⊢ ( 𝜑 → { 𝐸 } ⊆ 𝑉 )
24	1 4 3 5 11 12 23	dochocsp	⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝑁 ‘ { 𝐸 } ) ) = ( 𝑂 ‘ { 𝐸 } ) )
25	24	fveq2d	⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝑂 ‘ ( 𝑁 ‘ { 𝐸 } ) ) ) = ( 𝑂 ‘ ( 𝑂 ‘ { 𝐸 } ) ) )
26	1 4 3 5 11 12 20	dochocsn	⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝑂 ‘ { 𝐸 } ) ) = ( 𝑁 ‘ { 𝐸 } ) )
27	25 26	eqtrd	⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝑂 ‘ ( 𝑁 ‘ { 𝐸 } ) ) ) = ( 𝑁 ‘ { 𝐸 } ) )
28	1 3 4 5 14 10 12 22 27	dochexmid	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝐸 } ) ⊕ ( 𝑂 ‘ ( 𝑁 ‘ { 𝐸 } ) ) ) = 𝑉 )
29	24	oveq2d	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝐸 } ) ⊕ ( 𝑂 ‘ ( 𝑁 ‘ { 𝐸 } ) ) ) = ( ( 𝑁 ‘ { 𝐸 } ) ⊕ ( 𝑂 ‘ { 𝐸 } ) ) )
30	28 29	eqtr3d	⊢ ( 𝜑 → 𝑉 = ( ( 𝑁 ‘ { 𝐸 } ) ⊕ ( 𝑂 ‘ { 𝐸 } ) ) )
31	13 30	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ⊕ ( 𝑂 ‘ { 𝐸 } ) ) )
32	14	lsssssubg	⊢ ( 𝑈 ∈ LMod → ( LSubSp ‘ 𝑈 ) ⊆ ( SubGrp ‘ 𝑈 ) )
33	15 32	syl	⊢ ( 𝜑 → ( LSubSp ‘ 𝑈 ) ⊆ ( SubGrp ‘ 𝑈 ) )
34	33 22	sseldd	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝐸 } ) ∈ ( SubGrp ‘ 𝑈 ) )
35	1 4 5 14 3	dochlss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { 𝐸 } ⊆ 𝑉 ) → ( 𝑂 ‘ { 𝐸 } ) ∈ ( LSubSp ‘ 𝑈 ) )
36	12 23 35	syl2anc	⊢ ( 𝜑 → ( 𝑂 ‘ { 𝐸 } ) ∈ ( LSubSp ‘ 𝑈 ) )
37	33 36	sseldd	⊢ ( 𝜑 → ( 𝑂 ‘ { 𝐸 } ) ∈ ( SubGrp ‘ 𝑈 ) )
38	6 10	lsmelval	⊢ ( ( ( 𝑁 ‘ { 𝐸 } ) ∈ ( SubGrp ‘ 𝑈 ) ∧ ( 𝑂 ‘ { 𝐸 } ) ∈ ( SubGrp ‘ 𝑈 ) ) → ( 𝑋 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ⊕ ( 𝑂 ‘ { 𝐸 } ) ) ↔ ∃ 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) ∃ 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) 𝑋 = ( 𝑎 + 𝑢 ) ) )
39	34 37 38	syl2anc	⊢ ( 𝜑 → ( 𝑋 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ⊕ ( 𝑂 ‘ { 𝐸 } ) ) ↔ ∃ 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) ∃ 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) 𝑋 = ( 𝑎 + 𝑢 ) ) )
40	31 39	mpbid	⊢ ( 𝜑 → ∃ 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) ∃ 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) 𝑋 = ( 𝑎 + 𝑢 ) )
41		rexcom	⊢ ( ∃ 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) ∃ 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) 𝑋 = ( 𝑎 + 𝑢 ) ↔ ∃ 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∃ 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) 𝑋 = ( 𝑎 + 𝑢 ) )
42		df-rex	⊢ ( ∃ 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) 𝑋 = ( 𝑎 + 𝑢 ) ↔ ∃ 𝑎 ( 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) ∧ 𝑋 = ( 𝑎 + 𝑢 ) ) )
43	8 9 5 7 11	lspsnel	⊢ ( ( 𝑈 ∈ LMod ∧ 𝐸 ∈ 𝑉 ) → ( 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) ↔ ∃ 𝑘 ∈ 𝐵 𝑎 = ( 𝑘 · 𝐸 ) ) )
44	15 20 43	syl2anc	⊢ ( 𝜑 → ( 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) ↔ ∃ 𝑘 ∈ 𝐵 𝑎 = ( 𝑘 · 𝐸 ) ) )
45	44	anbi1d	⊢ ( 𝜑 → ( ( 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) ∧ 𝑋 = ( 𝑎 + 𝑢 ) ) ↔ ( ∃ 𝑘 ∈ 𝐵 𝑎 = ( 𝑘 · 𝐸 ) ∧ 𝑋 = ( 𝑎 + 𝑢 ) ) ) )
46		r19.41v	⊢ ( ∃ 𝑘 ∈ 𝐵 ( 𝑎 = ( 𝑘 · 𝐸 ) ∧ 𝑋 = ( 𝑎 + 𝑢 ) ) ↔ ( ∃ 𝑘 ∈ 𝐵 𝑎 = ( 𝑘 · 𝐸 ) ∧ 𝑋 = ( 𝑎 + 𝑢 ) ) )
47	45 46	bitr4di	⊢ ( 𝜑 → ( ( 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) ∧ 𝑋 = ( 𝑎 + 𝑢 ) ) ↔ ∃ 𝑘 ∈ 𝐵 ( 𝑎 = ( 𝑘 · 𝐸 ) ∧ 𝑋 = ( 𝑎 + 𝑢 ) ) ) )
48	47	exbidv	⊢ ( 𝜑 → ( ∃ 𝑎 ( 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) ∧ 𝑋 = ( 𝑎 + 𝑢 ) ) ↔ ∃ 𝑎 ∃ 𝑘 ∈ 𝐵 ( 𝑎 = ( 𝑘 · 𝐸 ) ∧ 𝑋 = ( 𝑎 + 𝑢 ) ) ) )
49		rexcom4	⊢ ( ∃ 𝑘 ∈ 𝐵 ∃ 𝑎 ( 𝑎 = ( 𝑘 · 𝐸 ) ∧ 𝑋 = ( 𝑎 + 𝑢 ) ) ↔ ∃ 𝑎 ∃ 𝑘 ∈ 𝐵 ( 𝑎 = ( 𝑘 · 𝐸 ) ∧ 𝑋 = ( 𝑎 + 𝑢 ) ) )
50		ovex	⊢ ( 𝑘 · 𝐸 ) ∈ V
51		oveq1	⊢ ( 𝑎 = ( 𝑘 · 𝐸 ) → ( 𝑎 + 𝑢 ) = ( ( 𝑘 · 𝐸 ) + 𝑢 ) )
52	51	eqeq2d	⊢ ( 𝑎 = ( 𝑘 · 𝐸 ) → ( 𝑋 = ( 𝑎 + 𝑢 ) ↔ 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) )
53	50 52	ceqsexv	⊢ ( ∃ 𝑎 ( 𝑎 = ( 𝑘 · 𝐸 ) ∧ 𝑋 = ( 𝑎 + 𝑢 ) ) ↔ 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) )
54	53	rexbii	⊢ ( ∃ 𝑘 ∈ 𝐵 ∃ 𝑎 ( 𝑎 = ( 𝑘 · 𝐸 ) ∧ 𝑋 = ( 𝑎 + 𝑢 ) ) ↔ ∃ 𝑘 ∈ 𝐵 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) )
55	49 54	bitr3i	⊢ ( ∃ 𝑎 ∃ 𝑘 ∈ 𝐵 ( 𝑎 = ( 𝑘 · 𝐸 ) ∧ 𝑋 = ( 𝑎 + 𝑢 ) ) ↔ ∃ 𝑘 ∈ 𝐵 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) )
56	48 55	bitrdi	⊢ ( 𝜑 → ( ∃ 𝑎 ( 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) ∧ 𝑋 = ( 𝑎 + 𝑢 ) ) ↔ ∃ 𝑘 ∈ 𝐵 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) )
57	42 56	bitrid	⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) 𝑋 = ( 𝑎 + 𝑢 ) ↔ ∃ 𝑘 ∈ 𝐵 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) )
58	57	rexbidv	⊢ ( 𝜑 → ( ∃ 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∃ 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) 𝑋 = ( 𝑎 + 𝑢 ) ↔ ∃ 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∃ 𝑘 ∈ 𝐵 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) )
59	41 58	bitrid	⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) ∃ 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) 𝑋 = ( 𝑎 + 𝑢 ) ↔ ∃ 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∃ 𝑘 ∈ 𝐵 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) )
60	40 59	mpbid	⊢ ( 𝜑 → ∃ 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∃ 𝑘 ∈ 𝐵 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) )