Theorem hdmapval3lemN

Description: Value of map from vectors to functionals at arguments not colinear with the reference vector E . (Contributed by NM, 17-May-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hdmapval3.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hdmapval3.e	⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
	hdmapval3.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hdmapval3.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	hdmapval3.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
	hdmapval3.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	hdmapval3.d	⊢ 𝐷 = ( Base ‘ 𝐶 )
	hdmapval3.j	⊢ 𝐽 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
	hdmapval3.i	⊢ 𝐼 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
	hdmapval3.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
	hdmapval3.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	hdmapval3.te	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑇 } ) ≠ ( 𝑁 ‘ { 𝐸 } ) )
	hdmapval3lem.t	⊢ ( 𝜑 → 𝑇 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) )
	hdmapval3lem.x	⊢ ( 𝜑 → 𝑥 ∈ 𝑉 )
	hdmapval3lem.xn	⊢ ( 𝜑 → ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) )
Assertion	hdmapval3lemN	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑇 ) = ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑇 ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		hdmapval3.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hdmapval3.e	⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
3		hdmapval3.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		hdmapval3.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		hdmapval3.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
6		hdmapval3.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
7		hdmapval3.d	⊢ 𝐷 = ( Base ‘ 𝐶 )
8		hdmapval3.j	⊢ 𝐽 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
9		hdmapval3.i	⊢ 𝐼 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
10		hdmapval3.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
11		hdmapval3.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12		hdmapval3.te	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑇 } ) ≠ ( 𝑁 ‘ { 𝐸 } ) )
13		hdmapval3lem.t	⊢ ( 𝜑 → 𝑇 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) )
14		hdmapval3lem.x	⊢ ( 𝜑 → 𝑥 ∈ 𝑉 )
15		hdmapval3lem.xn	⊢ ( 𝜑 → ¬ 𝑥 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) )
16		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
17		eqid	⊢ ( LSpan ‘ 𝐶 ) = ( LSpan ‘ 𝐶 )
18		eqid	⊢ ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
19		eqid	⊢ ( 0g ‘ 𝐶 ) = ( 0g ‘ 𝐶 )
20		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
21		eqid	⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
22	1 20 21 3 4 16 2 11	dvheveccl	⊢ ( 𝜑 → 𝐸 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) )
23	1 3 4 16 6 7 19 8 11 22	hvmapcl2	⊢ ( 𝜑 → ( 𝐽 ‘ 𝐸 ) ∈ ( 𝐷 ∖ { ( 0g ‘ 𝐶 ) } ) )
24	23	eldifad	⊢ ( 𝜑 → ( 𝐽 ‘ 𝐸 ) ∈ 𝐷 )
25	1 3 4 16 5 6 17 18 8 11 22	mapdhvmap	⊢ ( 𝜑 → ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑁 ‘ { 𝐸 } ) ) = ( ( LSpan ‘ 𝐶 ) ‘ { ( 𝐽 ‘ 𝐸 ) } ) )
26	1 3 11	dvhlvec	⊢ ( 𝜑 → 𝑈 ∈ LVec )
27	22	eldifad	⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
28	13	eldifad	⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
29	4 5 26 14 27 28 15	lspindpi	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑥 } ) ≠ ( 𝑁 ‘ { 𝐸 } ) ∧ ( 𝑁 ‘ { 𝑥 } ) ≠ ( 𝑁 ‘ { 𝑇 } ) ) )
30	29	simpld	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑥 } ) ≠ ( 𝑁 ‘ { 𝐸 } ) )
31	30	necomd	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝐸 } ) ≠ ( 𝑁 ‘ { 𝑥 } ) )
32	1 3 4 16 5 6 7 17 18 9 11 24 25 31 22 14	hdmap1cl	⊢ ( 𝜑 → ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑥 ⟩ ) ∈ 𝐷 )
33		eqidd	⊢ ( 𝜑 → ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑥 ⟩ ) = ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑥 ⟩ ) )
34		eqid	⊢ ( -g ‘ 𝑈 ) = ( -g ‘ 𝑈 )
35		eqid	⊢ ( -g ‘ 𝐶 ) = ( -g ‘ 𝐶 )
36		eqid	⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
37	1 3 11	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
38	4 36 5 37 27 28	lspprcl	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝐸 , 𝑇 } ) ∈ ( LSubSp ‘ 𝑈 ) )
39	16 36 37 38 14 15	lssneln0	⊢ ( 𝜑 → 𝑥 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) )
40	1 3 4 34 16 5 6 7 35 17 18 9 11 22 24 39 32 31 25	hdmap1eq	⊢ ( 𝜑 → ( ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑥 ⟩ ) = ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑥 ⟩ ) ↔ ( ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑁 ‘ { 𝑥 } ) ) = ( ( LSpan ‘ 𝐶 ) ‘ { ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑥 ⟩ ) } ) ∧ ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑁 ‘ { ( 𝐸 ( -g ‘ 𝑈 ) 𝑥 ) } ) ) = ( ( LSpan ‘ 𝐶 ) ‘ { ( ( 𝐽 ‘ 𝐸 ) ( -g ‘ 𝐶 ) ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑥 ⟩ ) ) } ) ) ) )
41	33 40	mpbid	⊢ ( 𝜑 → ( ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑁 ‘ { 𝑥 } ) ) = ( ( LSpan ‘ 𝐶 ) ‘ { ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑥 ⟩ ) } ) ∧ ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑁 ‘ { ( 𝐸 ( -g ‘ 𝑈 ) 𝑥 ) } ) ) = ( ( LSpan ‘ 𝐶 ) ‘ { ( ( 𝐽 ‘ 𝐸 ) ( -g ‘ 𝐶 ) ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑥 ⟩ ) ) } ) ) )
42	41	simpld	⊢ ( 𝜑 → ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑁 ‘ { 𝑥 } ) ) = ( ( LSpan ‘ 𝐶 ) ‘ { ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑥 ⟩ ) } ) )
43	12	necomd	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝐸 } ) ≠ ( 𝑁 ‘ { 𝑇 } ) )
44	4 5 37 27 28	lspprid1	⊢ ( 𝜑 → 𝐸 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) )
45	36 5 37 38 44	ellspsn5	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝐸 } ) ⊆ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) )
46	45 45	unssd	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝐸 } ) ) ⊆ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) )
47	46 15	ssneldd	⊢ ( 𝜑 → ¬ 𝑥 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝐸 } ) ) )
48	1 2 3 4 5 6 7 8 9 10 11 27 14 47	hdmapval2	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐸 ) = ( 𝐼 ‘ ⟨ 𝑥 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑥 ⟩ ) , 𝐸 ⟩ ) )
49	1 2 8 10 11	hdmapevec	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐸 ) = ( 𝐽 ‘ 𝐸 ) )
50	48 49	eqtr3d	⊢ ( 𝜑 → ( 𝐼 ‘ ⟨ 𝑥 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑥 ⟩ ) , 𝐸 ⟩ ) = ( 𝐽 ‘ 𝐸 ) )
51	4 5 37 27 28	lspprid2	⊢ ( 𝜑 → 𝑇 ∈ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) )
52	36 5 37 38 51	ellspsn5	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑇 } ) ⊆ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) )
53	45 52	unssd	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) ⊆ ( 𝑁 ‘ { 𝐸 , 𝑇 } ) )
54	53 15	ssneldd	⊢ ( 𝜑 → ¬ 𝑥 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) )
55	1 2 3 4 5 6 7 8 9 10 11 28 14 54	hdmapval2	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑇 ) = ( 𝐼 ‘ ⟨ 𝑥 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑥 ⟩ ) , 𝑇 ⟩ ) )
56	55	eqcomd	⊢ ( 𝜑 → ( 𝐼 ‘ ⟨ 𝑥 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑥 ⟩ ) , 𝑇 ⟩ ) = ( 𝑆 ‘ 𝑇 ) )
57	1 3 4 16 5 6 7 17 18 9 11 32 42 39 22 13 43 15 50 56	hdmap1eq4N	⊢ ( 𝜑 → ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑇 ⟩ ) = ( 𝑆 ‘ 𝑇 ) )
58	57	eqcomd	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑇 ) = ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑇 ⟩ ) )