Theorem hdmapeveclem

Description: Lemma for hdmapevec . TODO: combine with hdmapevec if it shortens overall. (Contributed by NM, 16-May-2015)

	Ref	Expression
Hypotheses	hdmapevec.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hdmapevec.e	⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
	hdmapevec.j	⊢ 𝐽 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
	hdmapevec.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
	hdmapevec.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	hdmapevec.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hdmapevec.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	hdmapevec.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
	hdmapevec.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	hdmapevec.d	⊢ 𝐷 = ( Base ‘ 𝐶 )
	hdmapevec.i	⊢ 𝐼 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
	hdmapevec.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	hdmapevec.ne	⊢ ( 𝜑 → ¬ 𝑋 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝐸 } ) ) )
Assertion	hdmapeveclem	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐸 ) = ( 𝐽 ‘ 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		hdmapevec.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hdmapevec.e	⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
3		hdmapevec.j	⊢ 𝐽 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
4		hdmapevec.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
5		hdmapevec.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6		hdmapevec.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
7		hdmapevec.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
8		hdmapevec.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
9		hdmapevec.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
10		hdmapevec.d	⊢ 𝐷 = ( Base ‘ 𝐶 )
11		hdmapevec.i	⊢ 𝐼 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
12		hdmapevec.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
13		hdmapevec.ne	⊢ ( 𝜑 → ¬ 𝑋 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝐸 } ) ) )
14		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
15		eqid	⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
16		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
17	1 14 15 6 7 16 2 5	dvheveccl	⊢ ( 𝜑 → 𝐸 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) )
18	17	eldifad	⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
19	1 2 6 7 8 9 10 3 11 4 5 18 12 13	hdmapval2	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐸 ) = ( 𝐼 ‘ ⟨ 𝑋 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑋 ⟩ ) , 𝐸 ⟩ ) )
20		eqid	⊢ ( LSpan ‘ 𝐶 ) = ( LSpan ‘ 𝐶 )
21		eqid	⊢ ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
22		eqid	⊢ ( 0g ‘ 𝐶 ) = ( 0g ‘ 𝐶 )
23	1 6 7 16 9 10 22 3 5 17	hvmapcl2	⊢ ( 𝜑 → ( 𝐽 ‘ 𝐸 ) ∈ ( 𝐷 ∖ { ( 0g ‘ 𝐶 ) } ) )
24	23	eldifad	⊢ ( 𝜑 → ( 𝐽 ‘ 𝐸 ) ∈ 𝐷 )
25	1 6 7 16 8 9 20 21 3 5 17	mapdhvmap	⊢ ( 𝜑 → ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑁 ‘ { 𝐸 } ) ) = ( ( LSpan ‘ 𝐶 ) ‘ { ( 𝐽 ‘ 𝐸 ) } ) )
26	1 6 5	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
27	7 8 26 12 13 18	hdmaplem1	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝐸 } ) )
28	27	necomd	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝐸 } ) ≠ ( 𝑁 ‘ { 𝑋 } ) )
29	7 8 26 12 13 18 16	hdmaplem3	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) )
30		eqidd	⊢ ( 𝜑 → ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑋 ⟩ ) = ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑋 ⟩ ) )
31	1 6 7 16 8 9 10 20 21 11 5 24 25 28 17 29 30	hdmap1eq2	⊢ ( 𝜑 → ( 𝐼 ‘ ⟨ 𝑋 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑋 ⟩ ) , 𝐸 ⟩ ) = ( 𝐽 ‘ 𝐸 ) )
32	19 31	eqtrd	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐸 ) = ( 𝐽 ‘ 𝐸 ) )