Metamath Proof Explorer

Theorem hdmapval0

Description: Value of map from vectors to functionals at zero. Note: we use dvh3dim for convenience, even though 3 dimensions aren't necessary at this point. TODO: I think either this or hdmapeq0 could be derived from the other to shorten proof. (Contributed by NM, 17-May-2015)

Ref Expression
Hypotheses hdmapval0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hdmapval0.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hdmapval0.o ⊢ 0 = ( 0g ‘ 𝑈 )
hdmapval0.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
hdmapval0.q ⊢ 𝑄 = ( 0g ‘ 𝐶 )
hdmapval0.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hdmapval0.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion hdmapval0 ( 𝜑 → ( 𝑆 ‘ 0 ) = 𝑄 )

Proof

Step Hyp Ref Expression
1 hdmapval0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmapval0.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hdmapval0.o ⊢ 0 = ( 0g ‘ 𝑈 )
4 hdmapval0.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
5 hdmapval0.q ⊢ 𝑄 = ( 0g ‘ 𝐶 )
6 hdmapval0.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
7 hdmapval0.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
9 eqid ⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
10 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
11 eqid ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
12 eqid ⊢ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
13 1 10 11 2 8 3 12 7 dvheveccl ⊢ ( 𝜑 → ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ∈ ( ( Base ‘ 𝑈 ) ∖ { 0 } ) )
14 13 eldifad ⊢ ( 𝜑 → ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ∈ ( Base ‘ 𝑈 ) )
15 1 2 7 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
16 8 3 lmod0vcl ⊢ ( 𝑈 ∈ LMod → 0 ∈ ( Base ‘ 𝑈 ) )
17 15 16 syl ⊢ ( 𝜑 → 0 ∈ ( Base ‘ 𝑈 ) )
18 1 2 8 9 7 14 17 dvh3dim ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( Base ‘ 𝑈 ) ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , 0 } ) )
19 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
20 eqid ⊢ ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
21 eqid ⊢ ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
22 7 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , 0 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
23 17 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , 0 } ) ) → 0 ∈ ( Base ‘ 𝑈 ) )
24 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , 0 } ) ) → 𝑥 ∈ ( Base ‘ 𝑈 ) )
25 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
26 8 25 9 15 14 17 lspprcl ⊢ ( 𝜑 → ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , 0 } ) ∈ ( LSubSp ‘ 𝑈 ) )
27 8 9 15 14 17 lspprid1 ⊢ ( 𝜑 → ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ∈ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , 0 } ) )
28 25 9 15 26 27 lspsnel5a ⊢ ( 𝜑 → ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } ) ⊆ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , 0 } ) )
29 8 9 15 14 17 lspprid2 ⊢ ( 𝜑 → 0 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , 0 } ) )
30 25 9 15 26 29 lspsnel5a ⊢ ( 𝜑 → ( ( LSpan ‘ 𝑈 ) ‘ { 0 } ) ⊆ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , 0 } ) )
31 28 30 unssd ⊢ ( 𝜑 → ( ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } ) ∪ ( ( LSpan ‘ 𝑈 ) ‘ { 0 } ) ) ⊆ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , 0 } ) )
32 31 ssneld ⊢ ( 𝜑 → ( ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , 0 } ) → ¬ 𝑥 ∈ ( ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } ) ∪ ( ( LSpan ‘ 𝑈 ) ‘ { 0 } ) ) ) )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , 0 } ) → ¬ 𝑥 ∈ ( ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } ) ∪ ( ( LSpan ‘ 𝑈 ) ‘ { 0 } ) ) ) )
34 33 3impia ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , 0 } ) ) → ¬ 𝑥 ∈ ( ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } ) ∪ ( ( LSpan ‘ 𝑈 ) ‘ { 0 } ) ) )
35 1 12 2 8 9 4 19 20 21 6 22 23 24 34 hdmapval2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , 0 } ) ) → ( 𝑆 ‘ 0 ) = ( ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ 𝑥 , ( ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ) , 𝑥 ⟩ ) , 0 ⟩ ) )
36 eqid ⊢ ( LSpan ‘ 𝐶 ) = ( LSpan ‘ 𝐶 )
37 eqid ⊢ ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
38 1 2 8 3 4 19 5 20 7 13 hvmapcl2 ⊢ ( 𝜑 → ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ) ∈ ( ( Base ‘ 𝐶 ) ∖ { 𝑄 } ) )
39 38 eldifad ⊢ ( 𝜑 → ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ) ∈ ( Base ‘ 𝐶 ) )
40 39 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , 0 } ) ) → ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ) ∈ ( Base ‘ 𝐶 ) )
41 1 2 8 3 9 4 36 37 20 7 13 mapdhvmap ⊢ ( 𝜑 → ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } ) ) = ( ( LSpan ‘ 𝐶 ) ‘ { ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ) } ) )
42 41 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , 0 } ) ) → ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } ) ) = ( ( LSpan ‘ 𝐶 ) ‘ { ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ) } ) )
43 1 2 7 dvhlvec ⊢ ( 𝜑 → 𝑈 ∈ LVec )
44 43 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , 0 } ) ) → 𝑈 ∈ LVec )
45 14 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , 0 } ) ) → ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ∈ ( Base ‘ 𝑈 ) )
46 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , 0 } ) ) → ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , 0 } ) )
47 8 9 44 24 45 23 46 lspindpi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , 0 } ) ) → ( ( ( LSpan ‘ 𝑈 ) ‘ { 𝑥 } ) ≠ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } ) ∧ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑥 } ) ≠ ( ( LSpan ‘ 𝑈 ) ‘ { 0 } ) ) )
48 47 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , 0 } ) ) → ( ( LSpan ‘ 𝑈 ) ‘ { 𝑥 } ) ≠ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } ) )
49 48 necomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , 0 } ) ) → ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ } ) ≠ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑥 } ) )
50 13 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , 0 } ) ) → ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ∈ ( ( Base ‘ 𝑈 ) ∖ { 0 } ) )
51 1 2 8 3 9 4 19 36 37 21 22 40 42 49 50 24 hdmap1cl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , 0 } ) ) → ( ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ) , 𝑥 ⟩ ) ∈ ( Base ‘ 𝐶 ) )
52 1 2 8 3 4 19 5 21 22 51 24 hdmap1val0 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , 0 } ) ) → ( ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ 𝑥 , ( ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , ( ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ ) , 𝑥 ⟩ ) , 0 ⟩ ) = 𝑄 )
53 35 52 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , 0 } ) ) → ( 𝑆 ‘ 0 ) = 𝑄 )
54 53 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( Base ‘ 𝑈 ) ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩ , 0 } ) → ( 𝑆 ‘ 0 ) = 𝑄 ) )
55 18 54 mpd ⊢ ( 𝜑 → ( 𝑆 ‘ 0 ) = 𝑄 )