hdmapfval - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > hdmapfval		Structured version Visualization version GIF version

Theorem hdmapfval 40290

Description: Map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 15-May-2015.)

**Hypotheses**
Ref	Expression
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	⊢ (𝜑 → (𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻))

**Assertion**
Ref	Expression
hdmapfval	⊢ (𝜑 → 𝑆 = (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩)))))

Distinct variable groups: 𝑦,𝑡,𝑧,𝐾 𝑦,𝐷 𝑡,𝐸,𝑦,𝑧 𝑡,𝐼,𝑦,𝑧 𝑡,𝑈,𝑦,𝑧 𝑡,𝑉,𝑦,𝑧 𝑡,𝑊,𝑦,𝑧 Allowed substitution hints: 𝜑(𝑦,𝑧,𝑡) 𝐴(𝑦,𝑧,𝑡) 𝐶(𝑦,𝑧,𝑡) 𝐷(𝑧,𝑡) 𝑆(𝑦,𝑧,𝑡) 𝐻(𝑦,𝑧,𝑡) 𝐽(𝑦,𝑧,𝑡) 𝑁(𝑦,𝑧,𝑡)

Proof of Theorem hdmapfval Dummy variables 𝑤 𝑒 𝑎 𝑖 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		hdmapfval.k	. 2 ⊢ (𝜑 → (𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻))
2		hdmapfval.s	. . . 4 ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)
3		hdmapval.h	. . . . . 6 ⊢ 𝐻 = (LHyp‘𝐾)
4	3	hdmapffval 40289	. . . . 5 ⊢ (𝐾 ∈ 𝐴 → (HDMap‘𝐾) = (𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))}))
5	4	fveq1d 6844	. . . 4 ⊢ (𝐾 ∈ 𝐴 → ((HDMap‘𝐾)‘𝑊) = ((𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))})‘𝑊))
6	2, 5	eqtrid 2788	. . 3 ⊢ (𝐾 ∈ 𝐴 → 𝑆 = ((𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))})‘𝑊))
7		fveq2 6842	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → ((LTrn‘𝐾)‘𝑤) = ((LTrn‘𝐾)‘𝑊))
8	7	reseq2d 5937	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → ( I ↾ ((LTrn‘𝐾)‘𝑤)) = ( I ↾ ((LTrn‘𝐾)‘𝑊)))
9	8	opeq2d 4837	. . . . . . 7 ⊢ (𝑤 = 𝑊 → ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩)
10		fveq2 6842	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → ((DVecH‘𝐾)‘𝑤) = ((DVecH‘𝐾)‘𝑊))
11		fveq2 6842	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → ((HDMap1‘𝐾)‘𝑤) = ((HDMap1‘𝐾)‘𝑊))
12		2fveq3 6847	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑊 → (Base‘((LCDual‘𝐾)‘𝑤)) = (Base‘((LCDual‘𝐾)‘𝑊)))
13		fveq2 6842	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑊 → ((HVMap‘𝐾)‘𝑤) = ((HVMap‘𝐾)‘𝑊))
14	13	fveq1d 6844	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑊 → (((HVMap‘𝐾)‘𝑤)‘𝑒) = (((HVMap‘𝐾)‘𝑊)‘𝑒))
15	14	oteq2d 4843	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑊 → ⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩ = ⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩)
16	15	fveq2d 6846	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑊 → (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩) = (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩))
17	16	oteq2d 4843	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑊 → ⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩ = ⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)
18	17	fveq2d 6846	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑊 → (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩) = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))
19	18	eqeq2d 2747	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑊 → (𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩) ↔ 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))
20	19	imbi2d 340	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑊 → ((¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)) ↔ (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))
21	20	ralbidv 3174	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑊 → (∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)) ↔ ∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))
22	12, 21	riotaeqbidv 7316	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑊 → (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))) = (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))
23	22	mpteq2dv 5207	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) = (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))))
24	23	eleq2d 2823	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → (𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))))
25	11, 24	sbceqbid 3746	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → ([((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ [((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))))
26	25	sbcbidv 3798	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → ([(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ [(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))))
27	10, 26	sbceqbid 3746	. . . . . . 7 ⊢ (𝑤 = 𝑊 → ([((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ [((DVecH‘𝐾)‘𝑊) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))))
28	9, 27	sbceqbid 3746	. . . . . 6 ⊢ (𝑤 = 𝑊 → ([⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ [⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ / 𝑒][((DVecH‘𝐾)‘𝑊) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))))
29		opex 5421	. . . . . . 7 ⊢ ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∈ V
30		fvex 6855	. . . . . . 7 ⊢ ((DVecH‘𝐾)‘𝑊) ∈ V
31		fvex 6855	. . . . . . 7 ⊢ (Base‘𝑢) ∈ V
32		simp1 1136	. . . . . . . . 9 ⊢ ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩)
33		hdmapfval.e	. . . . . . . . 9 ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩
34	32, 33	eqtr4di 2794	. . . . . . . 8 ⊢ ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑒 = 𝐸)
35		simp2 1137	. . . . . . . . 9 ⊢ ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑢 = ((DVecH‘𝐾)‘𝑊))
36		hdmapfval.u	. . . . . . . . 9 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
37	35, 36	eqtr4di 2794	. . . . . . . 8 ⊢ ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑢 = 𝑈)
38		simp3 1138	. . . . . . . . . 10 ⊢ ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑣 = (Base‘𝑢))
39	37	fveq2d 6846	. . . . . . . . . 10 ⊢ ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → (Base‘𝑢) = (Base‘𝑈))
40	38, 39	eqtrd 2776	. . . . . . . . 9 ⊢ ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑣 = (Base‘𝑈))
41		hdmapfval.v	. . . . . . . . 9 ⊢ 𝑉 = (Base‘𝑈)
42	40, 41	eqtr4di 2794	. . . . . . . 8 ⊢ ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑣 = 𝑉)
43		fvex 6855	. . . . . . . . . 10 ⊢ ((HDMap1‘𝐾)‘𝑊) ∈ V
44		id 22	. . . . . . . . . . . 12 ⊢ (𝑖 = ((HDMap1‘𝐾)‘𝑊) → 𝑖 = ((HDMap1‘𝐾)‘𝑊))
45		hdmapfval.i	. . . . . . . . . . . 12 ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)
46	44, 45	eqtr4di 2794	. . . . . . . . . . 11 ⊢ (𝑖 = ((HDMap1‘𝐾)‘𝑊) → 𝑖 = 𝐼)
47		fveq1 6841	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝐼 → (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩) = (𝐼‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))
48		fveq1 6841	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 𝐼 → (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩) = (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩))
49	48	oteq2d 4843	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝐼 → ⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩ = ⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)
50	49	fveq2d 6846	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝐼 → (𝐼‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩) = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))
51	47, 50	eqtrd 2776	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝐼 → (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩) = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))
52	51	eqeq2d 2747	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝐼 → (𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩) ↔ 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))
53	52	imbi2d 340	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝐼 → ((¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)) ↔ (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))
54	53	ralbidv 3174	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝐼 → (∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)) ↔ ∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))
55	54	riotabidv 7315	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝐼 → (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))) = (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))
56	55	mpteq2dv 5207	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝐼 → (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) = (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))))
57	56	eleq2d 2823	. . . . . . . . . . 11 ⊢ (𝑖 = 𝐼 → (𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))))
58	46, 57	syl 17	. . . . . . . . . 10 ⊢ (𝑖 = ((HDMap1‘𝐾)‘𝑊) → (𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))))))
59	43, 58	sbcie 3782	. . . . . . . . 9 ⊢ ([((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))))
60		simp3 1138	. . . . . . . . . . 11 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → 𝑣 = 𝑉)
61		hdmapfval.d	. . . . . . . . . . . . . 14 ⊢ 𝐷 = (Base‘𝐶)
62		hdmapfval.c	. . . . . . . . . . . . . . 15 ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)
63	62	fveq2i 6845	. . . . . . . . . . . . . 14 ⊢ (Base‘𝐶) = (Base‘((LCDual‘𝐾)‘𝑊))
64	61, 63	eqtr2i 2765	. . . . . . . . . . . . 13 ⊢ (Base‘((LCDual‘𝐾)‘𝑊)) = 𝐷
65	64	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (Base‘((LCDual‘𝐾)‘𝑊)) = 𝐷)
66		simp2 1137	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → 𝑢 = 𝑈)
67	66	fveq2d 6846	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (LSpan‘𝑢) = (LSpan‘𝑈))
68		hdmapfval.n	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑁 = (LSpan‘𝑈)
69	67, 68	eqtr4di 2794	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (LSpan‘𝑢) = 𝑁)
70		simp1 1136	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → 𝑒 = 𝐸)
71	70	sneqd 4598	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → {𝑒} = {𝐸})
72	69, 71	fveq12d 6849	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → ((LSpan‘𝑢)‘{𝑒}) = (𝑁‘{𝐸}))
73	69	fveq1d 6844	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → ((LSpan‘𝑢)‘{𝑡}) = (𝑁‘{𝑡}))
74	72, 73	uneq12d 4124	. . . . . . . . . . . . . . . 16 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) = ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})))
75	74	eleq2d 2823	. . . . . . . . . . . . . . 15 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) ↔ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡}))))
76	75	notbid 317	. . . . . . . . . . . . . 14 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) ↔ ¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡}))))
77	70	oteq1d 4842	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → ⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩ = ⟨𝐸, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩)
78	70	fveq2d 6846	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (((HVMap‘𝐾)‘𝑊)‘𝑒) = (((HVMap‘𝐾)‘𝑊)‘𝐸))
79		hdmapfval.j	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊)
80	79	fveq1i 6843	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐽‘𝐸) = (((HVMap‘𝐾)‘𝑊)‘𝐸)
81	78, 80	eqtr4di 2794	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (((HVMap‘𝐾)‘𝑊)‘𝑒) = (𝐽‘𝐸))
82	81	oteq2d 4843	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → ⟨𝐸, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩ = ⟨𝐸, (𝐽‘𝐸), 𝑧⟩)
83	77, 82	eqtrd 2776	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → ⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩ = ⟨𝐸, (𝐽‘𝐸), 𝑧⟩)
84	83	fveq2d 6846	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩) = (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩))
85	84	oteq2d 4843	. . . . . . . . . . . . . . . 16 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → ⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩ = ⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩)
86	85	fveq2d 6846	. . . . . . . . . . . . . . 15 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩) = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩))
87	86	eqeq2d 2747	. . . . . . . . . . . . . 14 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩) ↔ 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩)))
88	76, 87	imbi12d 344	. . . . . . . . . . . . 13 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → ((¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)) ↔ (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩))))
89	60, 88	raleqbidv 3319	. . . . . . . . . . . 12 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)) ↔ ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩))))
90	65, 89	riotaeqbidv 7316	. . . . . . . . . . 11 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩))) = (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩))))
91	60, 90	mpteq12dv 5196	. . . . . . . . . 10 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) = (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩)))))
92	91	eleq2d 2823	. . . . . . . . 9 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩))))))
93	59, 92	bitrid 282	. . . . . . . 8 ⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → ([((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩))))))
94	34, 37, 42, 93	syl3anc 1371	. . . . . . 7 ⊢ ((𝑒 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → ([((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩))))))
95	29, 30, 31, 94	sbc3ie 3825	. . . . . 6 ⊢ ([⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩ / 𝑒][((DVecH‘𝐾)‘𝑊) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩)))))
96	28, 95	bitrdi 286	. . . . 5 ⊢ (𝑤 = 𝑊 → ([⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩))))))
97	96	abbi1dv 2872	. . . 4 ⊢ (𝑤 = 𝑊 → {𝑎 ∣ [⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))} = (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩)))))
98		eqid 2736	. . . 4 ⊢ (𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))}) = (𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))})
99	97, 98, 41	mptfvmpt 7178	. . 3 ⊢ (𝑊 ∈ 𝐻 → ((𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑤))⟩ / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘⟨𝑧, (𝑖‘⟨𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧⟩), 𝑡⟩))))})‘𝑊) = (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩)))))
100	6, 99	sylan9eq 2796	. 2 ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻) → 𝑆 = (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩)))))
101	1, 100	syl 17	1 ⊢ (𝜑 → 𝑆 = (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑡⟩)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 {cab 2713 ∀wral 3064 [wsbc 3739 ∪ cun 3908 {csn 4586 ⟨cop 4592 ⟨cotp 4594 ↦ cmpt 5188 I cid 5530 ↾ cres 5635 ‘cfv 6496 ℩crio 7312 Basecbs 17083 LSpanclspn 20432 LHypclh 38447 LTrncltrn 38564 DVecHcdvh 39541 LCDualclcd 40049 HVMapchvm 40219 HDMap1chdma1 40254 HDMapchdma 40255

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pr 5384

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-ral 3065 df-rex 3074 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-sn 4587 df-pr 4589 df-op 4593 df-ot 4595 df-uni 4866 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-id 5531 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-riota 7313 df-hdmap 40257

This theorem is referenced by: hdmapval 40291 hdmapfnN 40292

W3C validator