Theorem hdmaprnlem4N

Description: Part of proof of part 12 in Baer p. 49 line 19. (T* =) (Ft)* = Gs. (Contributed by NM, 27-May-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hdmaprnlem1.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hdmaprnlem1.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hdmaprnlem1.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	hdmaprnlem1.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
	hdmaprnlem1.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	hdmaprnlem1.l	⊢ 𝐿 = ( LSpan ‘ 𝐶 )
	hdmaprnlem1.m	⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
	hdmaprnlem1.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
	hdmaprnlem1.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	hdmaprnlem1.se	⊢ ( 𝜑 → 𝑠 ∈ ( 𝐷 ∖ { 𝑄 } ) )
	hdmaprnlem1.ve	⊢ ( 𝜑 → 𝑣 ∈ 𝑉 )
	hdmaprnlem1.e	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑣 } ) ) = ( 𝐿 ‘ { 𝑠 } ) )
	hdmaprnlem1.ue	⊢ ( 𝜑 → 𝑢 ∈ 𝑉 )
	hdmaprnlem1.un	⊢ ( 𝜑 → ¬ 𝑢 ∈ ( 𝑁 ‘ { 𝑣 } ) )
	hdmaprnlem1.d	⊢ 𝐷 = ( Base ‘ 𝐶 )
	hdmaprnlem1.q	⊢ 𝑄 = ( 0g ‘ 𝐶 )
	hdmaprnlem1.o	⊢ 0 = ( 0g ‘ 𝑈 )
	hdmaprnlem1.a	⊢ ✚ = ( +g ‘ 𝐶 )
	hdmaprnlem1.t2	⊢ ( 𝜑 → 𝑡 ∈ ( ( 𝑁 ‘ { 𝑣 } ) ∖ { 0 } ) )
Assertion	hdmaprnlem4N	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑡 } ) ) = ( 𝐿 ‘ { 𝑠 } ) )

Proof

Step	Hyp	Ref	Expression
1		hdmaprnlem1.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hdmaprnlem1.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		hdmaprnlem1.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
4		hdmaprnlem1.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
5		hdmaprnlem1.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
6		hdmaprnlem1.l	⊢ 𝐿 = ( LSpan ‘ 𝐶 )
7		hdmaprnlem1.m	⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
8		hdmaprnlem1.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
9		hdmaprnlem1.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10		hdmaprnlem1.se	⊢ ( 𝜑 → 𝑠 ∈ ( 𝐷 ∖ { 𝑄 } ) )
11		hdmaprnlem1.ve	⊢ ( 𝜑 → 𝑣 ∈ 𝑉 )
12		hdmaprnlem1.e	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑣 } ) ) = ( 𝐿 ‘ { 𝑠 } ) )
13		hdmaprnlem1.ue	⊢ ( 𝜑 → 𝑢 ∈ 𝑉 )
14		hdmaprnlem1.un	⊢ ( 𝜑 → ¬ 𝑢 ∈ ( 𝑁 ‘ { 𝑣 } ) )
15		hdmaprnlem1.d	⊢ 𝐷 = ( Base ‘ 𝐶 )
16		hdmaprnlem1.q	⊢ 𝑄 = ( 0g ‘ 𝐶 )
17		hdmaprnlem1.o	⊢ 0 = ( 0g ‘ 𝑈 )
18		hdmaprnlem1.a	⊢ ✚ = ( +g ‘ 𝐶 )
19		hdmaprnlem1.t2	⊢ ( 𝜑 → 𝑡 ∈ ( ( 𝑁 ‘ { 𝑣 } ) ∖ { 0 } ) )
20		eqid	⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
21	1 2 9	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
22	3 20 4	lspsncl	⊢ ( ( 𝑈 ∈ LMod ∧ 𝑣 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑣 } ) ∈ ( LSubSp ‘ 𝑈 ) )
23	21 11 22	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑣 } ) ∈ ( LSubSp ‘ 𝑈 ) )
24	19	eldifad	⊢ ( 𝜑 → 𝑡 ∈ ( 𝑁 ‘ { 𝑣 } ) )
25	20 4 21 23 24	ellspsn5	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑡 } ) ⊆ ( 𝑁 ‘ { 𝑣 } ) )
26	1 2 9	dvhlvec	⊢ ( 𝜑 → 𝑈 ∈ LVec )
27	3 20	lss1	⊢ ( 𝑈 ∈ LMod → 𝑉 ∈ ( LSubSp ‘ 𝑈 ) )
28	21 27	syl	⊢ ( 𝜑 → 𝑉 ∈ ( LSubSp ‘ 𝑈 ) )
29	20 4 21 28 11	ellspsn5	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑣 } ) ⊆ 𝑉 )
30	29	ssdifd	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑣 } ) ∖ { 0 } ) ⊆ ( 𝑉 ∖ { 0 } ) )
31	30 19	sseldd	⊢ ( 𝜑 → 𝑡 ∈ ( 𝑉 ∖ { 0 } ) )
32	3 17 4 26 31 11	lspsncmp	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑡 } ) ⊆ ( 𝑁 ‘ { 𝑣 } ) ↔ ( 𝑁 ‘ { 𝑡 } ) = ( 𝑁 ‘ { 𝑣 } ) ) )
33	25 32	mpbid	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑡 } ) = ( 𝑁 ‘ { 𝑣 } ) )
34	33	fveq2d	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑡 } ) ) = ( 𝑀 ‘ ( 𝑁 ‘ { 𝑣 } ) ) )
35	34 12	eqtrd	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑡 } ) ) = ( 𝐿 ‘ { 𝑠 } ) )