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	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hdmapfval.e	⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
	hdmapfval.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hdmapfval.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	hdmapfval.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
	hdmapfval.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	hdmapfval.d	⊢ 𝐷 = ( Base ‘ 𝐶 )
	hdmapfval.j	⊢ 𝐽 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
	hdmapfval.i	⊢ 𝐼 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
	hdmapfval.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
	hdmapfval.k	⊢ ( 𝜑 → ( 𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻 ) )
	hdmapval.t	⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
Assertion	hdmapval	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑇 ) = ( ℩ 𝑦 ∈ 𝐷 ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑇 ⟩ ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		hdmapval.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hdmapfval.e	⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
3		hdmapfval.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		hdmapfval.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		hdmapfval.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
6		hdmapfval.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
7		hdmapfval.d	⊢ 𝐷 = ( Base ‘ 𝐶 )
8		hdmapfval.j	⊢ 𝐽 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
9		hdmapfval.i	⊢ 𝐼 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
10		hdmapfval.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
11		hdmapfval.k	⊢ ( 𝜑 → ( 𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻 ) )
12		hdmapval.t	⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
13	1 2 3 4 5 6 7 8 9 10 11	hdmapfval	⊢ ( 𝜑 → 𝑆 = ( 𝑡 ∈ 𝑉 ↦ ( ℩ 𝑦 ∈ 𝐷 ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) )
14	13	fveq1d	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑇 ) = ( ( 𝑡 ∈ 𝑉 ↦ ( ℩ 𝑦 ∈ 𝐷 ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) ‘ 𝑇 ) )
15		riotaex	⊢ ( ℩ 𝑦 ∈ 𝐷 ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑇 ⟩ ) ) ) ∈ V
16		sneq	⊢ ( 𝑡 = 𝑇 → { 𝑡 } = { 𝑇 } )
17	16	fveq2d	⊢ ( 𝑡 = 𝑇 → ( 𝑁 ‘ { 𝑡 } ) = ( 𝑁 ‘ { 𝑇 } ) )
18	17	uneq2d	⊢ ( 𝑡 = 𝑇 → ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑡 } ) ) = ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) )
19	18	eleq2d	⊢ ( 𝑡 = 𝑇 → ( 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑡 } ) ) ↔ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) ) )
20	19	notbid	⊢ ( 𝑡 = 𝑇 → ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑡 } ) ) ↔ ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) ) )
21		oteq3	⊢ ( 𝑡 = 𝑇 → ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑡 ⟩ = ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑇 ⟩ )
22	21	fveq2d	⊢ ( 𝑡 = 𝑇 → ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑇 ⟩ ) )
23	22	eqeq2d	⊢ ( 𝑡 = 𝑇 → ( 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ↔ 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑇 ⟩ ) ) )
24	20 23	imbi12d	⊢ ( 𝑡 = 𝑇 → ( ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ↔ ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑇 ⟩ ) ) ) )
25	24	ralbidv	⊢ ( 𝑡 = 𝑇 → ( ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ↔ ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑇 ⟩ ) ) ) )
26	25	riotabidv	⊢ ( 𝑡 = 𝑇 → ( ℩ 𝑦 ∈ 𝐷 ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) = ( ℩ 𝑦 ∈ 𝐷 ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑇 ⟩ ) ) ) )
27		eqid	⊢ ( 𝑡 ∈ 𝑉 ↦ ( ℩ 𝑦 ∈ 𝐷 ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) = ( 𝑡 ∈ 𝑉 ↦ ( ℩ 𝑦 ∈ 𝐷 ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) )
28	26 27	fvmptg	⊢ ( ( 𝑇 ∈ 𝑉 ∧ ( ℩ 𝑦 ∈ 𝐷 ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑇 ⟩ ) ) ) ∈ V ) → ( ( 𝑡 ∈ 𝑉 ↦ ( ℩ 𝑦 ∈ 𝐷 ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) ‘ 𝑇 ) = ( ℩ 𝑦 ∈ 𝐷 ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑇 ⟩ ) ) ) )
29	12 15 28	sylancl	⊢ ( 𝜑 → ( ( 𝑡 ∈ 𝑉 ↦ ( ℩ 𝑦 ∈ 𝐷 ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑡 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑡 ⟩ ) ) ) ) ‘ 𝑇 ) = ( ℩ 𝑦 ∈ 𝐷 ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑇 ⟩ ) ) ) )
30	14 29	eqtrd	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑇 ) = ( ℩ 𝑦 ∈ 𝐷 ∀ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ∪ ( 𝑁 ‘ { 𝑇 } ) ) → 𝑦 = ( 𝐼 ‘ ⟨ 𝑧 , ( 𝐼 ‘ ⟨ 𝐸 , ( 𝐽 ‘ 𝐸 ) , 𝑧 ⟩ ) , 𝑇 ⟩ ) ) ) )