Theorem hdmapval2

Description: Value of map from vectors to functionals with a specific auxiliary vector. TODO: Would shorter proofs result if the .ne hypothesis were changed to two =/= hypothesis? Consider hdmaplem1 through hdmaplem4 , which would become obsolete. (Contributed by NM, 15-May-2015)

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

Proof

Step	Hyp	Ref	Expression
1		hdmapval2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hdmapval2.e	⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
3		hdmapval2.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		hdmapval2.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		hdmapval2.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
6		hdmapval2.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
7		hdmapval2.d	⊢ 𝐷 = ( Base ‘ 𝐶 )
8		hdmapval2.j	⊢ 𝐽 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
9		hdmapval2.i	⊢ 𝐼 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
10		hdmapval2.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
11		hdmapval2.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12		hdmapval2.t	⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
13		hdmapval2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
14		hdmapval2.ne	⊢ ( 𝜑 → ¬ 𝑋 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) )
15		eqidd	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑇 ) = ( 𝑆 ‘ 𝑇 ) )
16	1 3 4 6 7 10 11 12	hdmapcl	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑇 ) ∈ 𝐷 )
17	1 2 3 4 5 6 7 8 9 10 11 12 16	hdmapval2lem	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑇 ) = ( 𝑆 ‘ 𝑇 ) ↔ ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) → ( 𝑆 ‘ 𝑇 ) = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑇 ⟩ ) ) ) )
18	15 17	mpbid	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) → ( 𝑆 ‘ 𝑇 ) = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑇 ⟩ ) ) )
19		eleq1	⊢ ( 𝑧 = 𝑋 → ( 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) ↔ 𝑋 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) ) )
20	19	notbid	⊢ ( 𝑧 = 𝑋 → ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) ↔ ¬ 𝑋 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) ) )
21		oteq1	⊢ ( 𝑧 = 𝑋 → ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑇 ⟩ = ⟨ 𝑋 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑇 ⟩ )
22		oteq3	⊢ ( 𝑧 = 𝑋 → ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ = ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑋 ⟩ )
23	22	fveq2d	⊢ ( 𝑧 = 𝑋 → ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) = ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑋 ⟩ ) )
24	23	oteq2d	⊢ ( 𝑧 = 𝑋 → ⟨ 𝑋 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑇 ⟩ = ⟨ 𝑋 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑋 ⟩ ) , 𝑇 ⟩ )
25	21 24	eqtrd	⊢ ( 𝑧 = 𝑋 → ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑇 ⟩ = ⟨ 𝑋 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑋 ⟩ ) , 𝑇 ⟩ )
26	25	fveq2d	⊢ ( 𝑧 = 𝑋 → ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑇 ⟩ ) = ( 𝐼 ‘ ⟨ 𝑋 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑋 ⟩ ) , 𝑇 ⟩ ) )
27	26	eqeq2d	⊢ ( 𝑧 = 𝑋 → ( ( 𝑆 ‘ 𝑇 ) = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑇 ⟩ ) ↔ ( 𝑆 ‘ 𝑇 ) = ( 𝐼 ‘ ⟨ 𝑋 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑋 ⟩ ) , 𝑇 ⟩ ) ) )
28	20 27	imbi12d	⊢ ( 𝑧 = 𝑋 → ( ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) → ( 𝑆 ‘ 𝑇 ) = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑇 ⟩ ) ) ↔ ( ¬ 𝑋 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) → ( 𝑆 ‘ 𝑇 ) = ( 𝐼 ‘ ⟨ 𝑋 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑋 ⟩ ) , 𝑇 ⟩ ) ) ) )
29	28	rspccv	⊢ ( ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) → ( 𝑆 ‘ 𝑇 ) = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑇 ⟩ ) ) → ( 𝑋 ∈ 𝑉 → ( ¬ 𝑋 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) → ( 𝑆 ‘ 𝑇 ) = ( 𝐼 ‘ ⟨ 𝑋 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑋 ⟩ ) , 𝑇 ⟩ ) ) ) )
30	18 13 14 29	syl3c	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑇 ) = ( 𝐼 ‘ ⟨ 𝑋 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑋 ⟩ ) , 𝑇 ⟩ ) )