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

Theorem isnvlem 27766
Description: Lemma for isnv 27768. (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 27748 . . 3 NrmCVec = {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ (⟨𝑔, 𝑠⟩ ∈ CVecOLD𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))}
21eleq2i 2823 . 2 (⟨⟨𝐺, 𝑆⟩, 𝑁⟩ ∈ NrmCVec ↔ ⟨⟨𝐺, 𝑆⟩, 𝑁⟩ ∈ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ (⟨𝑔, 𝑠⟩ ∈ CVecOLD𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))})
3 opeq1 4545 . . . . 5 (𝑔 = 𝐺 → ⟨𝑔, 𝑠⟩ = ⟨𝐺, 𝑠⟩)
43eleq1d 2816 . . . 4 (𝑔 = 𝐺 → (⟨𝑔, 𝑠⟩ ∈ CVecOLD ↔ ⟨𝐺, 𝑠⟩ ∈ CVecOLD))
5 rneq 5498 . . . . . 6 (𝑔 = 𝐺 → ran 𝑔 = ran 𝐺)
6 isnvlem.1 . . . . . 6 𝑋 = ran 𝐺
75, 6syl6eqr 2804 . . . . 5 (𝑔 = 𝐺 → ran 𝑔 = 𝑋)
87feq2d 6184 . . . 4 (𝑔 = 𝐺 → (𝑛:ran 𝑔⟶ℝ ↔ 𝑛:𝑋⟶ℝ))
9 fveq2 6344 . . . . . . . . 9 (𝑔 = 𝐺 → (GId‘𝑔) = (GId‘𝐺))
10 isnvlem.2 . . . . . . . . 9 𝑍 = (GId‘𝐺)
119, 10syl6eqr 2804 . . . . . . . 8 (𝑔 = 𝐺 → (GId‘𝑔) = 𝑍)
1211eqeq2d 2762 . . . . . . 7 (𝑔 = 𝐺 → (𝑥 = (GId‘𝑔) ↔ 𝑥 = 𝑍))
1312imbi2d 329 . . . . . 6 (𝑔 = 𝐺 → (((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ↔ ((𝑛𝑥) = 0 → 𝑥 = 𝑍)))
14 oveq 6811 . . . . . . . . 9 (𝑔 = 𝐺 → (𝑥𝑔𝑦) = (𝑥𝐺𝑦))
1514fveq2d 6348 . . . . . . . 8 (𝑔 = 𝐺 → (𝑛‘(𝑥𝑔𝑦)) = (𝑛‘(𝑥𝐺𝑦)))
1615breq1d 4806 . . . . . . 7 (𝑔 = 𝐺 → ((𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)) ↔ (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))
177, 16raleqbidv 3283 . . . . . 6 (𝑔 = 𝐺 → (∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)) ↔ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))
1813, 173anbi13d 1542 . . . . 5 (𝑔 = 𝐺 → ((((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))) ↔ (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))))
197, 18raleqbidv 3283 . . . 4 (𝑔 = 𝐺 → (∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))) ↔ ∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))))
204, 8, 193anbi123d 1540 . . 3 (𝑔 = 𝐺 → ((⟨𝑔, 𝑠⟩ ∈ CVecOLD𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))) ↔ (⟨𝐺, 𝑠⟩ ∈ CVecOLD𝑛:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))))
21 opeq2 4546 . . . . 5 (𝑠 = 𝑆 → ⟨𝐺, 𝑠⟩ = ⟨𝐺, 𝑆⟩)
2221eleq1d 2816 . . . 4 (𝑠 = 𝑆 → (⟨𝐺, 𝑠⟩ ∈ CVecOLD ↔ ⟨𝐺, 𝑆⟩ ∈ CVecOLD))
23 oveq 6811 . . . . . . . . 9 (𝑠 = 𝑆 → (𝑦𝑠𝑥) = (𝑦𝑆𝑥))
2423fveq2d 6348 . . . . . . . 8 (𝑠 = 𝑆 → (𝑛‘(𝑦𝑠𝑥)) = (𝑛‘(𝑦𝑆𝑥)))
2524eqeq1d 2754 . . . . . . 7 (𝑠 = 𝑆 → ((𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ↔ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥))))
2625ralbidv 3116 . . . . . 6 (𝑠 = 𝑆 → (∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ↔ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥))))
27263anbi2d 1545 . . . . 5 (𝑠 = 𝑆 → ((((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))) ↔ (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))))
2827ralbidv 3116 . . . 4 (𝑠 = 𝑆 → (∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))) ↔ ∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))))
2922, 283anbi13d 1542 . . 3 (𝑠 = 𝑆 → ((⟨𝐺, 𝑠⟩ ∈ CVecOLD𝑛:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))) ↔ (⟨𝐺, 𝑆⟩ ∈ CVecOLD𝑛:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))))
30 feq1 6179 . . . 4 (𝑛 = 𝑁 → (𝑛:𝑋⟶ℝ ↔ 𝑁:𝑋⟶ℝ))
31 fveq1 6343 . . . . . . . 8 (𝑛 = 𝑁 → (𝑛𝑥) = (𝑁𝑥))
3231eqeq1d 2754 . . . . . . 7 (𝑛 = 𝑁 → ((𝑛𝑥) = 0 ↔ (𝑁𝑥) = 0))
3332imbi1d 330 . . . . . 6 (𝑛 = 𝑁 → (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ↔ ((𝑁𝑥) = 0 → 𝑥 = 𝑍)))
34 fveq1 6343 . . . . . . . 8 (𝑛 = 𝑁 → (𝑛‘(𝑦𝑆𝑥)) = (𝑁‘(𝑦𝑆𝑥)))
3531oveq2d 6821 . . . . . . . 8 (𝑛 = 𝑁 → ((abs‘𝑦) · (𝑛𝑥)) = ((abs‘𝑦) · (𝑁𝑥)))
3634, 35eqeq12d 2767 . . . . . . 7 (𝑛 = 𝑁 → ((𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ↔ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥))))
3736ralbidv 3116 . . . . . 6 (𝑛 = 𝑁 → (∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ↔ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥))))
38 fveq1 6343 . . . . . . . 8 (𝑛 = 𝑁 → (𝑛‘(𝑥𝐺𝑦)) = (𝑁‘(𝑥𝐺𝑦)))
39 fveq1 6343 . . . . . . . . 9 (𝑛 = 𝑁 → (𝑛𝑦) = (𝑁𝑦))
4031, 39oveq12d 6823 . . . . . . . 8 (𝑛 = 𝑁 → ((𝑛𝑥) + (𝑛𝑦)) = ((𝑁𝑥) + (𝑁𝑦)))
4138, 40breq12d 4809 . . . . . . 7 (𝑛 = 𝑁 → ((𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)) ↔ (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))
4241ralbidv 3116 . . . . . 6 (𝑛 = 𝑁 → (∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)) ↔ ∀𝑦𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))
4333, 37, 423anbi123d 1540 . . . . 5 (𝑛 = 𝑁 → ((((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))) ↔ (((𝑁𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥)) ∧ ∀𝑦𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))))
4443ralbidv 3116 . . . 4 (𝑛 = 𝑁 → (∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))) ↔ ∀𝑥𝑋 (((𝑁𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥)) ∧ ∀𝑦𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))))
4530, 443anbi23d 1543 . . 3 (𝑛 = 𝑁 → ((⟨𝐺, 𝑆⟩ ∈ CVecOLD𝑛:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))) ↔ (⟨𝐺, 𝑆⟩ ∈ CVecOLD𝑁:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥)) ∧ ∀𝑦𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))))
4620, 29, 45eloprabg 6905 . 2 ((𝐺 ∈ V ∧ 𝑆 ∈ V ∧ 𝑁 ∈ V) → (⟨⟨𝐺, 𝑆⟩, 𝑁⟩ ∈ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ (⟨𝑔, 𝑠⟩ ∈ CVecOLD𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))} ↔ (⟨𝐺, 𝑆⟩ ∈ CVecOLD𝑁:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥)) ∧ ∀𝑦𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))))
472, 46syl5bb 272 1 ((𝐺 ∈ V ∧ 𝑆 ∈ V ∧ 𝑁 ∈ V) → (⟨⟨𝐺, 𝑆⟩, 𝑁⟩ ∈ NrmCVec ↔ (⟨𝐺, 𝑆⟩ ∈ CVecOLD𝑁:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥)) ∧ ∀𝑦𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  w3a 1072   = wceq 1624  wcel 2131  wral 3042  Vcvv 3332  cop 4319   class class class wbr 4796  ran crn 5259  wf 6037  cfv 6041  (class class class)co 6805  {coprab 6806  cc 10118  cr 10119  0cc0 10120   + caddc 10123   · cmul 10125  cle 10259  abscabs 14165  GIdcgi 27645  CVecOLDcvc 27714  NrmCVeccnv 27740
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-sep 4925  ax-nul 4933  ax-pr 5047
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ral 3047  df-rex 3048  df-rab 3051  df-v 3334  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4581  df-br 4797  df-opab 4857  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-fv 6049  df-ov 6808  df-oprab 6809  df-nv 27748
This theorem is referenced by:  isnv  27768
  Copyright terms: Public domain W3C validator