Theorem lnoval 30688

Description: The set of linear operators between two normed complex vector spaces. (Contributed by NM, 6-Nov-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)

Hypotheses

Ref	Expression
lnoval.1	⊢ 𝑋 = (BaseSet‘𝑈)
lnoval.2	⊢ 𝑌 = (BaseSet‘𝑊)
lnoval.3	⊢ 𝐺 = ( +𝑣 ‘𝑈)
lnoval.4	⊢ 𝐻 = ( +𝑣 ‘𝑊)
lnoval.5	⊢ 𝑅 = ( ·𝑠OLD ‘𝑈)
lnoval.6	⊢ 𝑆 = ( ·𝑠OLD ‘𝑊)
lnoval.7	⊢ 𝐿 = (𝑈 LnOp 𝑊)

Assertion

Ref	Expression
lnoval	⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝐿 = {𝑡 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑡‘((𝑥𝑅𝑦)𝐺𝑧)) = ((𝑥𝑆(𝑡‘𝑦))𝐻(𝑡‘𝑧))})

Distinct variable groups:   𝑥,𝑡,𝑦,𝑧,𝑈   𝑡,𝑊,𝑥,𝑦,𝑧   𝑡,𝑋,𝑦,𝑧   𝑡,𝑌   𝑡,𝐺   𝑡,𝑅   𝑡,𝐻   𝑡,𝑆

Allowed substitution hints:   𝑅(𝑥,𝑦,𝑧)   𝑆(𝑥,𝑦,𝑧)   𝐺(𝑥,𝑦,𝑧)   𝐻(𝑥,𝑦,𝑧)   𝐿(𝑥,𝑦,𝑧,𝑡)   𝑋(𝑥)   𝑌(𝑥,𝑦,𝑧)

Proof of Theorem lnoval

Dummy variables 𝑢 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		lnoval.7	. 2 ⊢ 𝐿 = (𝑈 LnOp 𝑊)
2		fveq2 6861	. . . . . 6 ⊢ (𝑢 = 𝑈 → (BaseSet‘𝑢) = (BaseSet‘𝑈))
3		lnoval.1	. . . . . 6 ⊢ 𝑋 = (BaseSet‘𝑈)
4	2, 3	eqtr4di 2783	. . . . 5 ⊢ (𝑢 = 𝑈 → (BaseSet‘𝑢) = 𝑋)
5	4	oveq2d 7406	. . . 4 ⊢ (𝑢 = 𝑈 → ((BaseSet‘𝑤) ↑m (BaseSet‘𝑢)) = ((BaseSet‘𝑤) ↑m 𝑋))
6		fveq2 6861	. . . . . . . . . 10 ⊢ (𝑢 = 𝑈 → ( +𝑣 ‘𝑢) = ( +𝑣 ‘𝑈))
7		lnoval.3	. . . . . . . . . 10 ⊢ 𝐺 = ( +𝑣 ‘𝑈)
8	6, 7	eqtr4di 2783	. . . . . . . . 9 ⊢ (𝑢 = 𝑈 → ( +𝑣 ‘𝑢) = 𝐺)
9		fveq2 6861	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑈 → ( ·𝑠OLD ‘𝑢) = ( ·𝑠OLD ‘𝑈))
10		lnoval.5	. . . . . . . . . . 11 ⊢ 𝑅 = ( ·𝑠OLD ‘𝑈)
11	9, 10	eqtr4di 2783	. . . . . . . . . 10 ⊢ (𝑢 = 𝑈 → ( ·𝑠OLD ‘𝑢) = 𝑅)
12	11	oveqd 7407	. . . . . . . . 9 ⊢ (𝑢 = 𝑈 → (𝑥( ·𝑠OLD ‘𝑢)𝑦) = (𝑥𝑅𝑦))
13		eqidd 2731	. . . . . . . . 9 ⊢ (𝑢 = 𝑈 → 𝑧 = 𝑧)
14	8, 12, 13	oveq123d 7411	. . . . . . . 8 ⊢ (𝑢 = 𝑈 → ((𝑥( ·𝑠OLD ‘𝑢)𝑦)( +𝑣 ‘𝑢)𝑧) = ((𝑥𝑅𝑦)𝐺𝑧))
15	14	fveqeq2d 6869	. . . . . . 7 ⊢ (𝑢 = 𝑈 → ((𝑡‘((𝑥( ·𝑠OLD ‘𝑢)𝑦)( +𝑣 ‘𝑢)𝑧)) = ((𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧)) ↔ (𝑡‘((𝑥𝑅𝑦)𝐺𝑧)) = ((𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧))))
16	4, 15	raleqbidv 3321	. . . . . 6 ⊢ (𝑢 = 𝑈 → (∀𝑧 ∈ (BaseSet‘𝑢)(𝑡‘((𝑥( ·𝑠OLD ‘𝑢)𝑦)( +𝑣 ‘𝑢)𝑧)) = ((𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧)) ↔ ∀𝑧 ∈ 𝑋 (𝑡‘((𝑥𝑅𝑦)𝐺𝑧)) = ((𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧))))
17	4, 16	raleqbidv 3321	. . . . 5 ⊢ (𝑢 = 𝑈 → (∀𝑦 ∈ (BaseSet‘𝑢)∀𝑧 ∈ (BaseSet‘𝑢)(𝑡‘((𝑥( ·𝑠OLD ‘𝑢)𝑦)( +𝑣 ‘𝑢)𝑧)) = ((𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧)) ↔ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑡‘((𝑥𝑅𝑦)𝐺𝑧)) = ((𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧))))
18	17	ralbidv 3157	. . . 4 ⊢ (𝑢 = 𝑈 → (∀𝑥 ∈ ℂ ∀𝑦 ∈ (BaseSet‘𝑢)∀𝑧 ∈ (BaseSet‘𝑢)(𝑡‘((𝑥( ·𝑠OLD ‘𝑢)𝑦)( +𝑣 ‘𝑢)𝑧)) = ((𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧)) ↔ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑡‘((𝑥𝑅𝑦)𝐺𝑧)) = ((𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧))))
19	5, 18	rabeqbidv 3427	. . 3 ⊢ (𝑢 = 𝑈 → {𝑡 ∈ ((BaseSet‘𝑤) ↑m (BaseSet‘𝑢)) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ (BaseSet‘𝑢)∀𝑧 ∈ (BaseSet‘𝑢)(𝑡‘((𝑥( ·𝑠OLD ‘𝑢)𝑦)( +𝑣 ‘𝑢)𝑧)) = ((𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧))} = {𝑡 ∈ ((BaseSet‘𝑤) ↑m 𝑋) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑡‘((𝑥𝑅𝑦)𝐺𝑧)) = ((𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧))})
20		fveq2 6861	. . . . . 6 ⊢ (𝑤 = 𝑊 → (BaseSet‘𝑤) = (BaseSet‘𝑊))
21		lnoval.2	. . . . . 6 ⊢ 𝑌 = (BaseSet‘𝑊)
22	20, 21	eqtr4di 2783	. . . . 5 ⊢ (𝑤 = 𝑊 → (BaseSet‘𝑤) = 𝑌)
23	22	oveq1d 7405	. . . 4 ⊢ (𝑤 = 𝑊 → ((BaseSet‘𝑤) ↑m 𝑋) = (𝑌 ↑m 𝑋))
24		fveq2 6861	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → ( +𝑣 ‘𝑤) = ( +𝑣 ‘𝑊))
25		lnoval.4	. . . . . . . . 9 ⊢ 𝐻 = ( +𝑣 ‘𝑊)
26	24, 25	eqtr4di 2783	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → ( +𝑣 ‘𝑤) = 𝐻)
27		fveq2 6861	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → ( ·𝑠OLD ‘𝑤) = ( ·𝑠OLD ‘𝑊))
28		lnoval.6	. . . . . . . . . 10 ⊢ 𝑆 = ( ·𝑠OLD ‘𝑊)
29	27, 28	eqtr4di 2783	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → ( ·𝑠OLD ‘𝑤) = 𝑆)
30	29	oveqd 7407	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦)) = (𝑥𝑆(𝑡‘𝑦)))
31		eqidd 2731	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (𝑡‘𝑧) = (𝑡‘𝑧))
32	26, 30, 31	oveq123d 7411	. . . . . . 7 ⊢ (𝑤 = 𝑊 → ((𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧)) = ((𝑥𝑆(𝑡‘𝑦))𝐻(𝑡‘𝑧)))
33	32	eqeq2d 2741	. . . . . 6 ⊢ (𝑤 = 𝑊 → ((𝑡‘((𝑥𝑅𝑦)𝐺𝑧)) = ((𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧)) ↔ (𝑡‘((𝑥𝑅𝑦)𝐺𝑧)) = ((𝑥𝑆(𝑡‘𝑦))𝐻(𝑡‘𝑧))))
34	33	2ralbidv 3202	. . . . 5 ⊢ (𝑤 = 𝑊 → (∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑡‘((𝑥𝑅𝑦)𝐺𝑧)) = ((𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧)) ↔ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑡‘((𝑥𝑅𝑦)𝐺𝑧)) = ((𝑥𝑆(𝑡‘𝑦))𝐻(𝑡‘𝑧))))
35	34	ralbidv 3157	. . . 4 ⊢ (𝑤 = 𝑊 → (∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑡‘((𝑥𝑅𝑦)𝐺𝑧)) = ((𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧)) ↔ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑡‘((𝑥𝑅𝑦)𝐺𝑧)) = ((𝑥𝑆(𝑡‘𝑦))𝐻(𝑡‘𝑧))))
36	23, 35	rabeqbidv 3427	. . 3 ⊢ (𝑤 = 𝑊 → {𝑡 ∈ ((BaseSet‘𝑤) ↑m 𝑋) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑡‘((𝑥𝑅𝑦)𝐺𝑧)) = ((𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧))} = {𝑡 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑡‘((𝑥𝑅𝑦)𝐺𝑧)) = ((𝑥𝑆(𝑡‘𝑦))𝐻(𝑡‘𝑧))})
37		df-lno 30680	. . 3 ⊢ LnOp = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {𝑡 ∈ ((BaseSet‘𝑤) ↑m (BaseSet‘𝑢)) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ (BaseSet‘𝑢)∀𝑧 ∈ (BaseSet‘𝑢)(𝑡‘((𝑥( ·𝑠OLD ‘𝑢)𝑦)( +𝑣 ‘𝑢)𝑧)) = ((𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧))})
38		ovex 7423	. . . 4 ⊢ (𝑌 ↑m 𝑋) ∈ V
39	38	rabex 5297	. . 3 ⊢ {𝑡 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑡‘((𝑥𝑅𝑦)𝐺𝑧)) = ((𝑥𝑆(𝑡‘𝑦))𝐻(𝑡‘𝑧))} ∈ V
40	19, 36, 37, 39	ovmpo 7552	. 2 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑈 LnOp 𝑊) = {𝑡 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑡‘((𝑥𝑅𝑦)𝐺𝑧)) = ((𝑥𝑆(𝑡‘𝑦))𝐻(𝑡‘𝑧))})
41	1, 40	eqtrid 2777	1 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝐿 = {𝑡 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑡‘((𝑥𝑅𝑦)𝐺𝑧)) = ((𝑥𝑆(𝑡‘𝑦))𝐻(𝑡‘𝑧))})

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3045  {crab 3408  ‘cfv 6514  (class class class)co 7390   ↑_m cmap 8802  ℂcc 11073  NrmCVeccnv 30520   +_𝑣 cpv 30521  BaseSetcba 30522   ·_𝑠OLD cns 30523   LnOp clno 30676

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-iota 6467  df-fun 6516  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395  df-lno 30680

This theorem is referenced by:  islno  30689  hhlnoi  31836