Metamath Proof Explorer

Theorem hdmapval

Description: Value of map from vectors to functionals in the closed kernel dual space. This is the function sigma on line 27 above part 9 in Baer p. 48. We select a convenient fixed reference vector E to be <. 0 , 1 >. (corresponding to vector u on p. 48 line 7) whose span is the lattice isomorphism map of the fiducial atom P = ( ( ocK )W ) (see dvheveccl ). ( JE ) is a fixed reference functional determined by this vector (corresponding to u' on line 8; mapdhvmap shows in Baer's notation (Fu)* = Gu'). Baer's independent vectors v and w on line 7 correspond to our z that the A. z e. V ranges over. The middle term ( I<. E , ( JE ) , z >. ) provides isolation to allow E and T to assume the same value without conflict. Closure is shown by hdmapcl . If a separate auxiliary vector is known, hdmapval2 provides a version without quantification. (Contributed by NM, 15-May-2015)

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

Proof

Step Hyp Ref Expression
1 hdmapval.h ⊢ H = LHyp ⁡ K
2 hdmapfval.e ⊢ E = I ↾ Base K I ↾ LTrn ⁡ K ⁡ W
3 hdmapfval.u ⊢ U = DVecH ⁡ K ⁡ W
4 hdmapfval.v ⊢ V = Base U
5 hdmapfval.n ⊢ N = LSpan ⁡ U
6 hdmapfval.c ⊢ C = LCDual ⁡ K ⁡ W
7 hdmapfval.d ⊢ D = Base C
8 hdmapfval.j ⊢ J = HVMap ⁡ K ⁡ W
9 hdmapfval.i ⊢ I = HDMap1 ⁡ K ⁡ W
10 hdmapfval.s ⊢ S = HDMap ⁡ K ⁡ W
11 hdmapfval.k ⊢ φ → K ∈ A ∧ W ∈ H
12 hdmapval.t ⊢ φ → T ∈ V
13 1 2 3 4 5 6 7 8 9 10 11 hdmapfval ⊢ φ → S = t ∈ V ⟼ ι y ∈ D | ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ t → y = I ⁡ z I ⁡ E J ⁡ E z t
14 13 fveq1d ⊢ φ → S ⁡ T = t ∈ V ⟼ ι y ∈ D | ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ t → y = I ⁡ z I ⁡ E J ⁡ E z t ⁡ T
15 riotaex ⊢ ι y ∈ D | ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ T → y = I ⁡ z I ⁡ E J ⁡ E z T ∈ V
16 sneq ⊢ t = T → t = T
17 16 fveq2d ⊢ t = T → N ⁡ t = N ⁡ T
18 17 uneq2d ⊢ t = T → N ⁡ E ∪ N ⁡ t = N ⁡ E ∪ N ⁡ T
19 18 eleq2d ⊢ t = T → z ∈ N ⁡ E ∪ N ⁡ t ↔ z ∈ N ⁡ E ∪ N ⁡ T
20 19 notbid ⊢ t = T → ¬ z ∈ N ⁡ E ∪ N ⁡ t ↔ ¬ z ∈ N ⁡ E ∪ N ⁡ T
21 oteq3 ⊢ t = T → z I ⁡ E J ⁡ E z t = z I ⁡ E J ⁡ E z T
22 21 fveq2d ⊢ t = T → I ⁡ z I ⁡ E J ⁡ E z t = I ⁡ z I ⁡ E J ⁡ E z T
23 22 eqeq2d ⊢ t = T → y = I ⁡ z I ⁡ E J ⁡ E z t ↔ y = I ⁡ z I ⁡ E J ⁡ E z T
24 20 23 imbi12d ⊢ t = T → ¬ z ∈ N ⁡ E ∪ N ⁡ t → y = I ⁡ z I ⁡ E J ⁡ E z t ↔ ¬ z ∈ N ⁡ E ∪ N ⁡ T → y = I ⁡ z I ⁡ E J ⁡ E z T
25 24 ralbidv ⊢ t = T → ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ t → y = I ⁡ z I ⁡ E J ⁡ E z t ↔ ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ T → y = I ⁡ z I ⁡ E J ⁡ E z T
26 25 riotabidv ⊢ t = T → ι y ∈ D | ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ t → y = I ⁡ z I ⁡ E J ⁡ E z t = ι y ∈ D | ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ T → y = I ⁡ z I ⁡ E J ⁡ E z T
27 eqid ⊢ t ∈ V ⟼ ι y ∈ D | ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ t → y = I ⁡ z I ⁡ E J ⁡ E z t = t ∈ V ⟼ ι y ∈ D | ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ t → y = I ⁡ z I ⁡ E J ⁡ E z t
28 26 27 fvmptg ⊢ T ∈ V ∧ ι y ∈ D | ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ T → y = I ⁡ z I ⁡ E J ⁡ E z T ∈ V → t ∈ V ⟼ ι y ∈ D | ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ t → y = I ⁡ z I ⁡ E J ⁡ E z t ⁡ T = ι y ∈ D | ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ T → y = I ⁡ z I ⁡ E J ⁡ E z T
29 12 15 28 sylancl ⊢ φ → t ∈ V ⟼ ι y ∈ D | ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ t → y = I ⁡ z I ⁡ E J ⁡ E z t ⁡ T = ι y ∈ D | ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ T → y = I ⁡ z I ⁡ E J ⁡ E z T
30 14 29 eqtrd ⊢ φ → S ⁡ T = ι y ∈ D | ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ T → y = I ⁡ z I ⁡ E J ⁡ E z T