Theorem hdmap10

Description: Part 10 in Baer p. 48 line 33, (Ft)* = G(tS) in their notation (S = sigma). (Contributed by NM, 17-May-2015)

	Ref	Expression
Hypotheses	hdmap10.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hdmap10.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hdmap10.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	hdmap10.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
	hdmap10.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	hdmap10.l	⊢ 𝐿 = ( LSpan ‘ 𝐶 )
	hdmap10.m	⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
	hdmap10.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
	hdmap10.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	hdmap10.t	⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
Assertion	hdmap10	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑇 } ) ) = ( 𝐿 ‘ { ( 𝑆 ‘ 𝑇 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		hdmap10.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hdmap10.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		hdmap10.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
4		hdmap10.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
5		hdmap10.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
6		hdmap10.l	⊢ 𝐿 = ( LSpan ‘ 𝐶 )
7		hdmap10.m	⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
8		hdmap10.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
9		hdmap10.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10		hdmap10.t	⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
11		sneq	⊢ ( 𝑇 = ( 0g ‘ 𝑈 ) → { 𝑇 } = { ( 0g ‘ 𝑈 ) } )
12	11	fveq2d	⊢ ( 𝑇 = ( 0g ‘ 𝑈 ) → ( 𝑁 ‘ { 𝑇 } ) = ( 𝑁 ‘ { ( 0g ‘ 𝑈 ) } ) )
13	12	fveq2d	⊢ ( 𝑇 = ( 0g ‘ 𝑈 ) → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑇 } ) ) = ( 𝑀 ‘ ( 𝑁 ‘ { ( 0g ‘ 𝑈 ) } ) ) )
14		fveq2	⊢ ( 𝑇 = ( 0g ‘ 𝑈 ) → ( 𝑆 ‘ 𝑇 ) = ( 𝑆 ‘ ( 0g ‘ 𝑈 ) ) )
15	14	sneqd	⊢ ( 𝑇 = ( 0g ‘ 𝑈 ) → { ( 𝑆 ‘ 𝑇 ) } = { ( 𝑆 ‘ ( 0g ‘ 𝑈 ) ) } )
16	15	fveq2d	⊢ ( 𝑇 = ( 0g ‘ 𝑈 ) → ( 𝐿 ‘ { ( 𝑆 ‘ 𝑇 ) } ) = ( 𝐿 ‘ { ( 𝑆 ‘ ( 0g ‘ 𝑈 ) ) } ) )
17	13 16	eqeq12d	⊢ ( 𝑇 = ( 0g ‘ 𝑈 ) → ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑇 } ) ) = ( 𝐿 ‘ { ( 𝑆 ‘ 𝑇 ) } ) ↔ ( 𝑀 ‘ ( 𝑁 ‘ { ( 0g ‘ 𝑈 ) } ) ) = ( 𝐿 ‘ { ( 𝑆 ‘ ( 0g ‘ 𝑈 ) ) } ) ) )
18	9	adantr	⊢ ( ( 𝜑 ∧ 𝑇 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
19		eqid	⊢ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
20		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
21		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
22		eqid	⊢ ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
23		eqid	⊢ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
24	10	anim1i	⊢ ( ( 𝜑 ∧ 𝑇 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝑇 ∈ 𝑉 ∧ 𝑇 ≠ ( 0g ‘ 𝑈 ) ) )
25		eldifsn	⊢ ( 𝑇 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) ↔ ( 𝑇 ∈ 𝑉 ∧ 𝑇 ≠ ( 0g ‘ 𝑈 ) ) )
26	24 25	sylibr	⊢ ( ( 𝜑 ∧ 𝑇 ≠ ( 0g ‘ 𝑈 ) ) → 𝑇 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) )
27	1 2 3 4 5 6 7 8 18 19 20 21 22 23 26	hdmap10lem	⊢ ( ( 𝜑 ∧ 𝑇 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑇 } ) ) = ( 𝐿 ‘ { ( 𝑆 ‘ 𝑇 ) } ) )
28	1 2 9	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
29	20 4	lspsn0	⊢ ( 𝑈 ∈ LMod → ( 𝑁 ‘ { ( 0g ‘ 𝑈 ) } ) = { ( 0g ‘ 𝑈 ) } )
30	28 29	syl	⊢ ( 𝜑 → ( 𝑁 ‘ { ( 0g ‘ 𝑈 ) } ) = { ( 0g ‘ 𝑈 ) } )
31	30	fveq2d	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { ( 0g ‘ 𝑈 ) } ) ) = ( 𝑀 ‘ { ( 0g ‘ 𝑈 ) } ) )
32		eqid	⊢ ( 0g ‘ 𝐶 ) = ( 0g ‘ 𝐶 )
33	1 7 2 20 5 32 9	mapd0	⊢ ( 𝜑 → ( 𝑀 ‘ { ( 0g ‘ 𝑈 ) } ) = { ( 0g ‘ 𝐶 ) } )
34	1 2 20 5 32 8 9	hdmapval0	⊢ ( 𝜑 → ( 𝑆 ‘ ( 0g ‘ 𝑈 ) ) = ( 0g ‘ 𝐶 ) )
35	34	sneqd	⊢ ( 𝜑 → { ( 𝑆 ‘ ( 0g ‘ 𝑈 ) ) } = { ( 0g ‘ 𝐶 ) } )
36	35	fveq2d	⊢ ( 𝜑 → ( 𝐿 ‘ { ( 𝑆 ‘ ( 0g ‘ 𝑈 ) ) } ) = ( 𝐿 ‘ { ( 0g ‘ 𝐶 ) } ) )
37	1 5 9	lcdlmod	⊢ ( 𝜑 → 𝐶 ∈ LMod )
38	32 6	lspsn0	⊢ ( 𝐶 ∈ LMod → ( 𝐿 ‘ { ( 0g ‘ 𝐶 ) } ) = { ( 0g ‘ 𝐶 ) } )
39	37 38	syl	⊢ ( 𝜑 → ( 𝐿 ‘ { ( 0g ‘ 𝐶 ) } ) = { ( 0g ‘ 𝐶 ) } )
40	36 39	eqtr2d	⊢ ( 𝜑 → { ( 0g ‘ 𝐶 ) } = ( 𝐿 ‘ { ( 𝑆 ‘ ( 0g ‘ 𝑈 ) ) } ) )
41	31 33 40	3eqtrd	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { ( 0g ‘ 𝑈 ) } ) ) = ( 𝐿 ‘ { ( 𝑆 ‘ ( 0g ‘ 𝑈 ) ) } ) )
42	17 27 41	pm2.61ne	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑇 } ) ) = ( 𝐿 ‘ { ( 𝑆 ‘ 𝑇 ) } ) )