Theorem hdmapeq0

Description: Part of proof of part 12 in Baer p. 49 line 3. (Contributed by NM, 22-May-2015)

	Ref	Expression
Hypotheses	hdmap12a.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hdmap12a.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hdmap12a.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	hdmap12a.o	⊢ 0 = ( 0g ‘ 𝑈 )
	hdmap12a.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	hdmap12a.q	⊢ 𝑄 = ( 0g ‘ 𝐶 )
	hdmap12a.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
	hdmap12a.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	hdmap12a.x	⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
Assertion	hdmapeq0	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑇 ) = 𝑄 ↔ 𝑇 = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		hdmap12a.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hdmap12a.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		hdmap12a.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
4		hdmap12a.o	⊢ 0 = ( 0g ‘ 𝑈 )
5		hdmap12a.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
6		hdmap12a.q	⊢ 𝑄 = ( 0g ‘ 𝐶 )
7		hdmap12a.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
8		hdmap12a.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9		hdmap12a.x	⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
10		eqid	⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
11		eqid	⊢ ( LSpan ‘ 𝐶 ) = ( LSpan ‘ 𝐶 )
12		eqid	⊢ ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
13	1 2 3 10 5 11 12 7 8 9	hdmap10	⊢ ( 𝜑 → ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑇 } ) ) = ( ( LSpan ‘ 𝐶 ) ‘ { ( 𝑆 ‘ 𝑇 ) } ) )
14	1 12 2 4 5 6 8	mapd0	⊢ ( 𝜑 → ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 0 } ) = { 𝑄 } )
15	13 14	eqeq12d	⊢ ( 𝜑 → ( ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑇 } ) ) = ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 0 } ) ↔ ( ( LSpan ‘ 𝐶 ) ‘ { ( 𝑆 ‘ 𝑇 ) } ) = { 𝑄 } ) )
16		eqid	⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
17	1 2 8	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
18	3 16 10	lspsncl	⊢ ( ( 𝑈 ∈ LMod ∧ 𝑇 ∈ 𝑉 ) → ( ( LSpan ‘ 𝑈 ) ‘ { 𝑇 } ) ∈ ( LSubSp ‘ 𝑈 ) )
19	17 9 18	syl2anc	⊢ ( 𝜑 → ( ( LSpan ‘ 𝑈 ) ‘ { 𝑇 } ) ∈ ( LSubSp ‘ 𝑈 ) )
20	4 16	lsssn0	⊢ ( 𝑈 ∈ LMod → { 0 } ∈ ( LSubSp ‘ 𝑈 ) )
21	17 20	syl	⊢ ( 𝜑 → { 0 } ∈ ( LSubSp ‘ 𝑈 ) )
22	1 2 16 12 8 19 21	mapd11	⊢ ( 𝜑 → ( ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑇 } ) ) = ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 0 } ) ↔ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑇 } ) = { 0 } ) )
23	1 5 8	lcdlmod	⊢ ( 𝜑 → 𝐶 ∈ LMod )
24		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
25	1 2 3 5 24 7 8 9	hdmapcl	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑇 ) ∈ ( Base ‘ 𝐶 ) )
26	24 6 11	lspsneq0	⊢ ( ( 𝐶 ∈ LMod ∧ ( 𝑆 ‘ 𝑇 ) ∈ ( Base ‘ 𝐶 ) ) → ( ( ( LSpan ‘ 𝐶 ) ‘ { ( 𝑆 ‘ 𝑇 ) } ) = { 𝑄 } ↔ ( 𝑆 ‘ 𝑇 ) = 𝑄 ) )
27	23 25 26	syl2anc	⊢ ( 𝜑 → ( ( ( LSpan ‘ 𝐶 ) ‘ { ( 𝑆 ‘ 𝑇 ) } ) = { 𝑄 } ↔ ( 𝑆 ‘ 𝑇 ) = 𝑄 ) )
28	15 22 27	3bitr3rd	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑇 ) = 𝑄 ↔ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑇 } ) = { 0 } ) )
29	3 4 10	lspsneq0	⊢ ( ( 𝑈 ∈ LMod ∧ 𝑇 ∈ 𝑉 ) → ( ( ( LSpan ‘ 𝑈 ) ‘ { 𝑇 } ) = { 0 } ↔ 𝑇 = 0 ) )
30	17 9 29	syl2anc	⊢ ( 𝜑 → ( ( ( LSpan ‘ 𝑈 ) ‘ { 𝑇 } ) = { 0 } ↔ 𝑇 = 0 ) )
31	28 30	bitrd	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑇 ) = 𝑄 ↔ 𝑇 = 0 ) )