Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  isnvlem Structured version   Visualization version   GIF version

Theorem isnvlem 28379
 Description: Lemma for isnv 28381. (Contributed by NM, 11-Nov-2006.) (New usage is discouraged.)
Hypotheses
Ref Expression
isnvlem.1 𝑋 = ran 𝐺
isnvlem.2 𝑍 = (GId‘𝐺)
Assertion
Ref Expression
isnvlem ((𝐺 ∈ V ∧ 𝑆 ∈ V ∧ 𝑁 ∈ V) → (⟨⟨𝐺, 𝑆⟩, 𝑁⟩ ∈ NrmCVec ↔ (⟨𝐺, 𝑆⟩ ∈ CVecOLD𝑁:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥)) ∧ ∀𝑦𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))))
Distinct variable groups:   𝑥,𝑦,𝐺   𝑥,𝑁,𝑦   𝑥,𝑆,𝑦   𝑥,𝑋,𝑦
Allowed substitution hints:   𝑍(𝑥,𝑦)

Proof of Theorem isnvlem
Dummy variables 𝑔 𝑛 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-nv 28361 . . 3 NrmCVec = {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ (⟨𝑔, 𝑠⟩ ∈ CVecOLD𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))}
21eleq2i 2902 . 2 (⟨⟨𝐺, 𝑆⟩, 𝑁⟩ ∈ NrmCVec ↔ ⟨⟨𝐺, 𝑆⟩, 𝑁⟩ ∈ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ (⟨𝑔, 𝑠⟩ ∈ CVecOLD𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))})
3 opeq1 4795 . . . . 5 (𝑔 = 𝐺 → ⟨𝑔, 𝑠⟩ = ⟨𝐺, 𝑠⟩)
43eleq1d 2895 . . . 4 (𝑔 = 𝐺 → (⟨𝑔, 𝑠⟩ ∈ CVecOLD ↔ ⟨𝐺, 𝑠⟩ ∈ CVecOLD))
5 rneq 5799 . . . . . 6 (𝑔 = 𝐺 → ran 𝑔 = ran 𝐺)
6 isnvlem.1 . . . . . 6 𝑋 = ran 𝐺
75, 6syl6eqr 2872 . . . . 5 (𝑔 = 𝐺 → ran 𝑔 = 𝑋)
87feq2d 6493 . . . 4 (𝑔 = 𝐺 → (𝑛:ran 𝑔⟶ℝ ↔ 𝑛:𝑋⟶ℝ))
9 fveq2 6663 . . . . . . . . 9 (𝑔 = 𝐺 → (GId‘𝑔) = (GId‘𝐺))
10 isnvlem.2 . . . . . . . . 9 𝑍 = (GId‘𝐺)
119, 10syl6eqr 2872 . . . . . . . 8 (𝑔 = 𝐺 → (GId‘𝑔) = 𝑍)
1211eqeq2d 2830 . . . . . . 7 (𝑔 = 𝐺 → (𝑥 = (GId‘𝑔) ↔ 𝑥 = 𝑍))
1312imbi2d 343 . . . . . 6 (𝑔 = 𝐺 → (((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ↔ ((𝑛𝑥) = 0 → 𝑥 = 𝑍)))
14 oveq 7154 . . . . . . . . 9 (𝑔 = 𝐺 → (𝑥𝑔𝑦) = (𝑥𝐺𝑦))
1514fveq2d 6667 . . . . . . . 8 (𝑔 = 𝐺 → (𝑛‘(𝑥𝑔𝑦)) = (𝑛‘(𝑥𝐺𝑦)))
1615breq1d 5067 . . . . . . 7 (𝑔 = 𝐺 → ((𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)) ↔ (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))
177, 16raleqbidv 3400 . . . . . 6 (𝑔 = 𝐺 → (∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)) ↔ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))
1813, 173anbi13d 1432 . . . . 5 (𝑔 = 𝐺 → ((((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))) ↔ (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))))
197, 18raleqbidv 3400 . . . 4 (𝑔 = 𝐺 → (∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))) ↔ ∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))))
204, 8, 193anbi123d 1430 . . 3 (𝑔 = 𝐺 → ((⟨𝑔, 𝑠⟩ ∈ CVecOLD𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))) ↔ (⟨𝐺, 𝑠⟩ ∈ CVecOLD𝑛:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))))
21 opeq2 4796 . . . . 5 (𝑠 = 𝑆 → ⟨𝐺, 𝑠⟩ = ⟨𝐺, 𝑆⟩)
2221eleq1d 2895 . . . 4 (𝑠 = 𝑆 → (⟨𝐺, 𝑠⟩ ∈ CVecOLD ↔ ⟨𝐺, 𝑆⟩ ∈ CVecOLD))
23 oveq 7154 . . . . . . . 8 (𝑠 = 𝑆 → (𝑦𝑠𝑥) = (𝑦𝑆𝑥))
2423fveqeq2d 6671 . . . . . . 7 (𝑠 = 𝑆 → ((𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ↔ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥))))
2524ralbidv 3195 . . . . . 6 (𝑠 = 𝑆 → (∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ↔ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥))))
26253anbi2d 1435 . . . . 5 (𝑠 = 𝑆 → ((((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))) ↔ (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))))
2726ralbidv 3195 . . . 4 (𝑠 = 𝑆 → (∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))) ↔ ∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))))
2822, 273anbi13d 1432 . . 3 (𝑠 = 𝑆 → ((⟨𝐺, 𝑠⟩ ∈ CVecOLD𝑛:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))) ↔ (⟨𝐺, 𝑆⟩ ∈ CVecOLD𝑛:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))))
29 feq1 6488 . . . 4 (𝑛 = 𝑁 → (𝑛:𝑋⟶ℝ ↔ 𝑁:𝑋⟶ℝ))
30 fveq1 6662 . . . . . . . 8 (𝑛 = 𝑁 → (𝑛𝑥) = (𝑁𝑥))
3130eqeq1d 2821 . . . . . . 7 (𝑛 = 𝑁 → ((𝑛𝑥) = 0 ↔ (𝑁𝑥) = 0))
3231imbi1d 344 . . . . . 6 (𝑛 = 𝑁 → (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ↔ ((𝑁𝑥) = 0 → 𝑥 = 𝑍)))
33 fveq1 6662 . . . . . . . 8 (𝑛 = 𝑁 → (𝑛‘(𝑦𝑆𝑥)) = (𝑁‘(𝑦𝑆𝑥)))
3430oveq2d 7164 . . . . . . . 8 (𝑛 = 𝑁 → ((abs‘𝑦) · (𝑛𝑥)) = ((abs‘𝑦) · (𝑁𝑥)))
3533, 34eqeq12d 2835 . . . . . . 7 (𝑛 = 𝑁 → ((𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ↔ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥))))
3635ralbidv 3195 . . . . . 6 (𝑛 = 𝑁 → (∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ↔ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥))))
37 fveq1 6662 . . . . . . . 8 (𝑛 = 𝑁 → (𝑛‘(𝑥𝐺𝑦)) = (𝑁‘(𝑥𝐺𝑦)))
38 fveq1 6662 . . . . . . . . 9 (𝑛 = 𝑁 → (𝑛𝑦) = (𝑁𝑦))
3930, 38oveq12d 7166 . . . . . . . 8 (𝑛 = 𝑁 → ((𝑛𝑥) + (𝑛𝑦)) = ((𝑁𝑥) + (𝑁𝑦)))
4037, 39breq12d 5070 . . . . . . 7 (𝑛 = 𝑁 → ((𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)) ↔ (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))
4140ralbidv 3195 . . . . . 6 (𝑛 = 𝑁 → (∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)) ↔ ∀𝑦𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))
4232, 36, 413anbi123d 1430 . . . . 5 (𝑛 = 𝑁 → ((((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))) ↔ (((𝑁𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥)) ∧ ∀𝑦𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))))
4342ralbidv 3195 . . . 4 (𝑛 = 𝑁 → (∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))) ↔ ∀𝑥𝑋 (((𝑁𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥)) ∧ ∀𝑦𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))))
4429, 433anbi23d 1433 . . 3 (𝑛 = 𝑁 → ((⟨𝐺, 𝑆⟩ ∈ CVecOLD𝑛:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))) ↔ (⟨𝐺, 𝑆⟩ ∈ CVecOLD𝑁:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥)) ∧ ∀𝑦𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))))
4520, 28, 44eloprabg 7254 . 2 ((𝐺 ∈ V ∧ 𝑆 ∈ V ∧ 𝑁 ∈ V) → (⟨⟨𝐺, 𝑆⟩, 𝑁⟩ ∈ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ (⟨𝑔, 𝑠⟩ ∈ CVecOLD𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))} ↔ (⟨𝐺, 𝑆⟩ ∈ CVecOLD𝑁:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥)) ∧ ∀𝑦𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))))
462, 45syl5bb 285 1 ((𝐺 ∈ V ∧ 𝑆 ∈ V ∧ 𝑁 ∈ V) → (⟨⟨𝐺, 𝑆⟩, 𝑁⟩ ∈ NrmCVec ↔ (⟨𝐺, 𝑆⟩ ∈ CVecOLD𝑁:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥)) ∧ ∀𝑦𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1082   = wceq 1531   ∈ wcel 2108  ∀wral 3136  Vcvv 3493  ⟨cop 4565   class class class wbr 5057  ran crn 5549  ⟶wf 6344  ‘cfv 6348  (class class class)co 7148  {coprab 7149  ℂcc 10527  ℝcr 10528  0cc0 10529   + caddc 10532   · cmul 10534   ≤ cle 10668  abscabs 14585  GIdcgi 28259  CVecOLDcvc 28327  NrmCVeccnv 28353 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pr 5320 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-fv 6356  df-ov 7151  df-oprab 7152  df-nv 28361 This theorem is referenced by:  isnv  28381
 Copyright terms: Public domain W3C validator