Metamath Proof Explorer

Theorem hdmapval2lem

Description: Lemma for hdmapval2 . (Contributed by NM, 15-May-2015)

Ref Expression
Hypotheses hdmapval2.h ⊢ H = LHyp ⁡ K
hdmapval2.e ⊢ E = I ↾ Base K I ↾ LTrn ⁡ K ⁡ W
hdmapval2.u ⊢ U = DVecH ⁡ K ⁡ W
hdmapval2.v ⊢ V = Base U
hdmapval2.n ⊢ N = LSpan ⁡ U
hdmapval2.c ⊢ C = LCDual ⁡ K ⁡ W
hdmapval2.d ⊢ D = Base C
hdmapval2.j ⊢ J = HVMap ⁡ K ⁡ W
hdmapval2.i ⊢ I = HDMap1 ⁡ K ⁡ W
hdmapval2.s ⊢ S = HDMap ⁡ K ⁡ W
hdmapval2.k ⊢ φ → K ∈ HL ∧ W ∈ H
hdmapval2.t ⊢ φ → T ∈ V
hdmapval2.f ⊢ φ → F ∈ D
Assertion hdmapval2lem ⊢ φ → S ⁡ T = F ↔ ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ T → F = I ⁡ z I ⁡ E J ⁡ E z T

Proof

Step Hyp Ref Expression
1 hdmapval2.h ⊢ H = LHyp ⁡ K
2 hdmapval2.e ⊢ E = I ↾ Base K I ↾ LTrn ⁡ K ⁡ W
3 hdmapval2.u ⊢ U = DVecH ⁡ K ⁡ W
4 hdmapval2.v ⊢ V = Base U
5 hdmapval2.n ⊢ N = LSpan ⁡ U
6 hdmapval2.c ⊢ C = LCDual ⁡ K ⁡ W
7 hdmapval2.d ⊢ D = Base C
8 hdmapval2.j ⊢ J = HVMap ⁡ K ⁡ W
9 hdmapval2.i ⊢ I = HDMap1 ⁡ K ⁡ W
10 hdmapval2.s ⊢ S = HDMap ⁡ K ⁡ W
11 hdmapval2.k ⊢ φ → K ∈ HL ∧ W ∈ H
12 hdmapval2.t ⊢ φ → T ∈ V
13 hdmapval2.f ⊢ φ → F ∈ D
14 1 2 3 4 5 6 7 8 9 10 11 12 hdmapval ⊢ φ → S ⁡ T = ι h ∈ D | ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ T → h = I ⁡ z I ⁡ E J ⁡ E z T
15 14 eqeq1d ⊢ φ → S ⁡ T = F ↔ ι h ∈ D | ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ T → h = I ⁡ z I ⁡ E J ⁡ E z T = F
16 eqid ⊢ 0 U = 0 U
17 eqid ⊢ LSpan ⁡ C = LSpan ⁡ C
18 eqid ⊢ mapd ⁡ K ⁡ W = mapd ⁡ K ⁡ W
19 eqid ⊢ Base K = Base K
20 eqid ⊢ LTrn ⁡ K ⁡ W = LTrn ⁡ K ⁡ W
21 1 19 20 3 4 16 2 11 dvheveccl ⊢ φ → E ∈ V ∖ 0 U
22 1 3 4 16 5 6 17 18 8 11 21 mapdhvmap ⊢ φ → mapd ⁡ K ⁡ W ⁡ N ⁡ E = LSpan ⁡ C ⁡ J ⁡ E
23 eqid ⊢ 0 C = 0 C
24 1 3 4 16 6 7 23 8 11 21 hvmapcl2 ⊢ φ → J ⁡ E ∈ D ∖ 0 C
25 24 eldifad ⊢ φ → J ⁡ E ∈ D
26 1 3 4 16 5 6 7 17 18 9 11 22 21 25 12 hdmap1eu ⊢ φ → ∃! h ∈ D ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ T → h = I ⁡ z I ⁡ E J ⁡ E z T
27 nfv ⊢ Ⅎ h φ
28 nfcvd ⊢ φ → Ⅎ _ h F
29 nfvd ⊢ φ → Ⅎ h ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ T → F = I ⁡ z I ⁡ E J ⁡ E z T
30 eqeq1 ⊢ h = F → h = I ⁡ z I ⁡ E J ⁡ E z T ↔ F = I ⁡ z I ⁡ E J ⁡ E z T
31 30 imbi2d ⊢ h = F → ¬ z ∈ N ⁡ E ∪ N ⁡ T → h = I ⁡ z I ⁡ E J ⁡ E z T ↔ ¬ z ∈ N ⁡ E ∪ N ⁡ T → F = I ⁡ z I ⁡ E J ⁡ E z T
32 31 ralbidv ⊢ h = F → ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ T → h = I ⁡ z I ⁡ E J ⁡ E z T ↔ ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ T → F = I ⁡ z I ⁡ E J ⁡ E z T
33 32 adantl ⊢ φ ∧ h = F → ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ T → h = I ⁡ z I ⁡ E J ⁡ E z T ↔ ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ T → F = I ⁡ z I ⁡ E J ⁡ E z T
34 27 28 29 13 33 riota2df ⊢ φ ∧ ∃! h ∈ D ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ T → h = I ⁡ z I ⁡ E J ⁡ E z T → ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ T → F = I ⁡ z I ⁡ E J ⁡ E z T ↔ ι h ∈ D | ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ T → h = I ⁡ z I ⁡ E J ⁡ E z T = F
35 26 34 mpdan ⊢ φ → ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ T → F = I ⁡ z I ⁡ E J ⁡ E z T ↔ ι h ∈ D | ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ T → h = I ⁡ z I ⁡ E J ⁡ E z T = F
36 15 35 bitr4d ⊢ φ → S ⁡ T = F ↔ ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ T → F = I ⁡ z I ⁡ E J ⁡ E z T