Metamath Proof Explorer

Theorem hdmapip0

Description: Zero property that will be used for inner product. (Contributed by NM, 9-Jun-2015)

Ref Expression
Hypotheses hdmapip0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hdmapip0.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hdmapip0.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
hdmapip0.o ⊢ 0 = ( 0g ‘ 𝑈 )
hdmapip0.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
hdmapip0.z ⊢ 𝑍 = ( 0g ‘ 𝑅 )
hdmapip0.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hdmapip0.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
hdmapip0.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion hdmapip0 ( 𝜑 → ( ( ( 𝑆 ‘ 𝑋 ) ‘ 𝑋 ) = 𝑍 ↔ 𝑋 = 0 ) )

Proof

Step Hyp Ref Expression
1 hdmapip0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmapip0.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hdmapip0.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 hdmapip0.o ⊢ 0 = ( 0g ‘ 𝑈 )
5 hdmapip0.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
6 hdmapip0.z ⊢ 𝑍 = ( 0g ‘ 𝑅 )
7 hdmapip0.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
8 hdmapip0.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 hdmapip0.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
10 eqid ⊢ ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
11 8 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 0 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12 9 anim1i ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 0 ) → ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) )
13 eldifsn ⊢ ( 𝑋 ∈ ( 𝑉 ∖ { 0 } ) ↔ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) )
14 12 13 sylibr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
15 1 10 2 3 4 11 14 dochnel ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 0 ) → ¬ 𝑋 ∈ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑋 } ) )
16 eqid ⊢ ( LFnl ‘ 𝑈 ) = ( LFnl ‘ 𝑈 )
17 eqid ⊢ ( LKer ‘ 𝑈 ) = ( LKer ‘ 𝑈 )
18 1 2 8 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
19 eqid ⊢ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
20 eqid ⊢ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
21 1 2 3 19 20 7 8 9 hdmapcl ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
22 1 19 20 2 16 8 21 lcdvbaselfl ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ∈ ( LFnl ‘ 𝑈 ) )
23 3 5 6 16 17 18 22 9 ellkr2 ⊢ ( 𝜑 → ( 𝑋 ∈ ( ( LKer ‘ 𝑈 ) ‘ ( 𝑆 ‘ 𝑋 ) ) ↔ ( ( 𝑆 ‘ 𝑋 ) ‘ 𝑋 ) = 𝑍 ) )
24 23 biimpar ⊢ ( ( 𝜑 ∧ ( ( 𝑆 ‘ 𝑋 ) ‘ 𝑋 ) = 𝑍 ) → 𝑋 ∈ ( ( LKer ‘ 𝑈 ) ‘ ( 𝑆 ‘ 𝑋 ) ) )
25 1 10 2 3 16 17 7 8 9 hdmaplkr ⊢ ( 𝜑 → ( ( LKer ‘ 𝑈 ) ‘ ( 𝑆 ‘ 𝑋 ) ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑋 } ) )
26 25 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑆 ‘ 𝑋 ) ‘ 𝑋 ) = 𝑍 ) → ( ( LKer ‘ 𝑈 ) ‘ ( 𝑆 ‘ 𝑋 ) ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑋 } ) )
27 24 26 eleqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑆 ‘ 𝑋 ) ‘ 𝑋 ) = 𝑍 ) → 𝑋 ∈ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑋 } ) )
28 27 ex ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝑋 ) ‘ 𝑋 ) = 𝑍 → 𝑋 ∈ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑋 } ) ) )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 0 ) → ( ( ( 𝑆 ‘ 𝑋 ) ‘ 𝑋 ) = 𝑍 → 𝑋 ∈ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑋 } ) ) )
30 15 29 mtod ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 0 ) → ¬ ( ( 𝑆 ‘ 𝑋 ) ‘ 𝑋 ) = 𝑍 )
31 30 neqned ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 0 ) → ( ( 𝑆 ‘ 𝑋 ) ‘ 𝑋 ) ≠ 𝑍 )
32 31 ex ⊢ ( 𝜑 → ( 𝑋 ≠ 0 → ( ( 𝑆 ‘ 𝑋 ) ‘ 𝑋 ) ≠ 𝑍 ) )
33 32 necon4d ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝑋 ) ‘ 𝑋 ) = 𝑍 → 𝑋 = 0 ) )
34 33 imp ⊢ ( ( 𝜑 ∧ ( ( 𝑆 ‘ 𝑋 ) ‘ 𝑋 ) = 𝑍 ) → 𝑋 = 0 )
35 fveq2 ⊢ ( 𝑋 = 0 → ( ( 𝑆 ‘ 𝑋 ) ‘ 𝑋 ) = ( ( 𝑆 ‘ 𝑋 ) ‘ 0 ) )
36 5 6 4 16 lfl0 ⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝑆 ‘ 𝑋 ) ∈ ( LFnl ‘ 𝑈 ) ) → ( ( 𝑆 ‘ 𝑋 ) ‘ 0 ) = 𝑍 )
37 18 22 36 syl2anc ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑋 ) ‘ 0 ) = 𝑍 )
38 35 37 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑋 = 0 ) → ( ( 𝑆 ‘ 𝑋 ) ‘ 𝑋 ) = 𝑍 )
39 34 38 impbida ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝑋 ) ‘ 𝑋 ) = 𝑍 ↔ 𝑋 = 0 ) )