Theorem hdmapinvlem2

Description: Line 28 in Baer p. 110, 0 = f(w,u). (Contributed by NM, 11-Jun-2015)

	Ref	Expression
Hypotheses	hdmapinvlem1.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hdmapinvlem1.e	⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
	hdmapinvlem1.o	⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	hdmapinvlem1.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hdmapinvlem1.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	hdmapinvlem1.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
	hdmapinvlem1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	hdmapinvlem1.t	⊢ · = ( .r ‘ 𝑅 )
	hdmapinvlem1.z	⊢ 0 = ( 0g ‘ 𝑅 )
	hdmapinvlem1.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
	hdmapinvlem1.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	hdmapinvlem1.c	⊢ ( 𝜑 → 𝐶 ∈ ( 𝑂 ‘ { 𝐸 } ) )
Assertion	hdmapinvlem2	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		hdmapinvlem1.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hdmapinvlem1.e	⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
3		hdmapinvlem1.o	⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
4		hdmapinvlem1.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5		hdmapinvlem1.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
6		hdmapinvlem1.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
7		hdmapinvlem1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
8		hdmapinvlem1.t	⊢ · = ( .r ‘ 𝑅 )
9		hdmapinvlem1.z	⊢ 0 = ( 0g ‘ 𝑅 )
10		hdmapinvlem1.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
11		hdmapinvlem1.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12		hdmapinvlem1.c	⊢ ( 𝜑 → 𝐶 ∈ ( 𝑂 ‘ { 𝐸 } ) )
13	1 2 3 4 5 6 7 8 9 10 11 12	hdmapinvlem1	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐶 ) = 0 )
14		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
15		eqid	⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
16		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
17	1 14 15 4 5 16 2 11	dvheveccl	⊢ ( 𝜑 → 𝐸 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) )
18	17	eldifad	⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
19	18	snssd	⊢ ( 𝜑 → { 𝐸 } ⊆ 𝑉 )
20	1 4 5 3	dochssv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { 𝐸 } ⊆ 𝑉 ) → ( 𝑂 ‘ { 𝐸 } ) ⊆ 𝑉 )
21	11 19 20	syl2anc	⊢ ( 𝜑 → ( 𝑂 ‘ { 𝐸 } ) ⊆ 𝑉 )
22	21 12	sseldd	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
23	1 4 5 6 9 10 11 18 22	hdmapip0com	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐶 ) = 0 ↔ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) = 0 ) )
24	13 23	mpbid	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) = 0 )