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

Theorem isnvlem 27326
Description: Lemma for isnv 27328. (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 27308 . . 3 NrmCVec = {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ (⟨𝑔, 𝑠⟩ ∈ CVecOLD𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))}
21eleq2i 2690 . 2 (⟨⟨𝐺, 𝑆⟩, 𝑁⟩ ∈ NrmCVec ↔ ⟨⟨𝐺, 𝑆⟩, 𝑁⟩ ∈ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ (⟨𝑔, 𝑠⟩ ∈ CVecOLD𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))})
3 opeq1 4372 . . . . 5 (𝑔 = 𝐺 → ⟨𝑔, 𝑠⟩ = ⟨𝐺, 𝑠⟩)
43eleq1d 2683 . . . 4 (𝑔 = 𝐺 → (⟨𝑔, 𝑠⟩ ∈ CVecOLD ↔ ⟨𝐺, 𝑠⟩ ∈ CVecOLD))
5 rneq 5313 . . . . . 6 (𝑔 = 𝐺 → ran 𝑔 = ran 𝐺)
6 isnvlem.1 . . . . . 6 𝑋 = ran 𝐺
75, 6syl6eqr 2673 . . . . 5 (𝑔 = 𝐺 → ran 𝑔 = 𝑋)
87feq2d 5990 . . . 4 (𝑔 = 𝐺 → (𝑛:ran 𝑔⟶ℝ ↔ 𝑛:𝑋⟶ℝ))
9 fveq2 6150 . . . . . . . . 9 (𝑔 = 𝐺 → (GId‘𝑔) = (GId‘𝐺))
10 isnvlem.2 . . . . . . . . 9 𝑍 = (GId‘𝐺)
119, 10syl6eqr 2673 . . . . . . . 8 (𝑔 = 𝐺 → (GId‘𝑔) = 𝑍)
1211eqeq2d 2631 . . . . . . 7 (𝑔 = 𝐺 → (𝑥 = (GId‘𝑔) ↔ 𝑥 = 𝑍))
1312imbi2d 330 . . . . . 6 (𝑔 = 𝐺 → (((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ↔ ((𝑛𝑥) = 0 → 𝑥 = 𝑍)))
14 oveq 6613 . . . . . . . . 9 (𝑔 = 𝐺 → (𝑥𝑔𝑦) = (𝑥𝐺𝑦))
1514fveq2d 6154 . . . . . . . 8 (𝑔 = 𝐺 → (𝑛‘(𝑥𝑔𝑦)) = (𝑛‘(𝑥𝐺𝑦)))
1615breq1d 4625 . . . . . . 7 (𝑔 = 𝐺 → ((𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)) ↔ (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))
177, 16raleqbidv 3141 . . . . . 6 (𝑔 = 𝐺 → (∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)) ↔ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))
1813, 173anbi13d 1398 . . . . 5 (𝑔 = 𝐺 → ((((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))) ↔ (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))))
197, 18raleqbidv 3141 . . . 4 (𝑔 = 𝐺 → (∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))) ↔ ∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))))
204, 8, 193anbi123d 1396 . . 3 (𝑔 = 𝐺 → ((⟨𝑔, 𝑠⟩ ∈ CVecOLD𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))) ↔ (⟨𝐺, 𝑠⟩ ∈ CVecOLD𝑛:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))))
21 opeq2 4373 . . . . 5 (𝑠 = 𝑆 → ⟨𝐺, 𝑠⟩ = ⟨𝐺, 𝑆⟩)
2221eleq1d 2683 . . . 4 (𝑠 = 𝑆 → (⟨𝐺, 𝑠⟩ ∈ CVecOLD ↔ ⟨𝐺, 𝑆⟩ ∈ CVecOLD))
23 oveq 6613 . . . . . . . . 9 (𝑠 = 𝑆 → (𝑦𝑠𝑥) = (𝑦𝑆𝑥))
2423fveq2d 6154 . . . . . . . 8 (𝑠 = 𝑆 → (𝑛‘(𝑦𝑠𝑥)) = (𝑛‘(𝑦𝑆𝑥)))
2524eqeq1d 2623 . . . . . . 7 (𝑠 = 𝑆 → ((𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ↔ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥))))
2625ralbidv 2980 . . . . . 6 (𝑠 = 𝑆 → (∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ↔ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥))))
27263anbi2d 1401 . . . . 5 (𝑠 = 𝑆 → ((((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))) ↔ (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))))
2827ralbidv 2980 . . . 4 (𝑠 = 𝑆 → (∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))) ↔ ∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))))
2922, 283anbi13d 1398 . . 3 (𝑠 = 𝑆 → ((⟨𝐺, 𝑠⟩ ∈ CVecOLD𝑛:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))) ↔ (⟨𝐺, 𝑆⟩ ∈ CVecOLD𝑛:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))))
30 feq1 5985 . . . 4 (𝑛 = 𝑁 → (𝑛:𝑋⟶ℝ ↔ 𝑁:𝑋⟶ℝ))
31 fveq1 6149 . . . . . . . 8 (𝑛 = 𝑁 → (𝑛𝑥) = (𝑁𝑥))
3231eqeq1d 2623 . . . . . . 7 (𝑛 = 𝑁 → ((𝑛𝑥) = 0 ↔ (𝑁𝑥) = 0))
3332imbi1d 331 . . . . . 6 (𝑛 = 𝑁 → (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ↔ ((𝑁𝑥) = 0 → 𝑥 = 𝑍)))
34 fveq1 6149 . . . . . . . 8 (𝑛 = 𝑁 → (𝑛‘(𝑦𝑆𝑥)) = (𝑁‘(𝑦𝑆𝑥)))
3531oveq2d 6623 . . . . . . . 8 (𝑛 = 𝑁 → ((abs‘𝑦) · (𝑛𝑥)) = ((abs‘𝑦) · (𝑁𝑥)))
3634, 35eqeq12d 2636 . . . . . . 7 (𝑛 = 𝑁 → ((𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ↔ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥))))
3736ralbidv 2980 . . . . . 6 (𝑛 = 𝑁 → (∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ↔ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥))))
38 fveq1 6149 . . . . . . . 8 (𝑛 = 𝑁 → (𝑛‘(𝑥𝐺𝑦)) = (𝑁‘(𝑥𝐺𝑦)))
39 fveq1 6149 . . . . . . . . 9 (𝑛 = 𝑁 → (𝑛𝑦) = (𝑁𝑦))
4031, 39oveq12d 6625 . . . . . . . 8 (𝑛 = 𝑁 → ((𝑛𝑥) + (𝑛𝑦)) = ((𝑁𝑥) + (𝑁𝑦)))
4138, 40breq12d 4628 . . . . . . 7 (𝑛 = 𝑁 → ((𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)) ↔ (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))
4241ralbidv 2980 . . . . . 6 (𝑛 = 𝑁 → (∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)) ↔ ∀𝑦𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))
4333, 37, 423anbi123d 1396 . . . . 5 (𝑛 = 𝑁 → ((((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))) ↔ (((𝑁𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥)) ∧ ∀𝑦𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))))
4443ralbidv 2980 . . . 4 (𝑛 = 𝑁 → (∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))) ↔ ∀𝑥𝑋 (((𝑁𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥)) ∧ ∀𝑦𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))))
4530, 443anbi23d 1399 . . 3 (𝑛 = 𝑁 → ((⟨𝐺, 𝑆⟩ ∈ CVecOLD𝑛:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))) ↔ (⟨𝐺, 𝑆⟩ ∈ CVecOLD𝑁:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥)) ∧ ∀𝑦𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))))
4620, 29, 45eloprabg 6704 . 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 1036   = wceq 1480  wcel 1987  wral 2907  Vcvv 3186  cop 4156   class class class wbr 4615  ran crn 5077  wf 5845  cfv 5849  (class class class)co 6607  {coprab 6608  cc 9881  cr 9882  0cc0 9883   + caddc 9886   · cmul 9888  cle 10022  abscabs 13911  GIdcgi 27205  CVecOLDcvc 27274  NrmCVeccnv 27300
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4743  ax-nul 4751  ax-pr 4869
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-nul 3894  df-if 4061  df-sn 4151  df-pr 4153  df-op 4157  df-uni 4405  df-br 4616  df-opab 4676  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-fv 5857  df-ov 6610  df-oprab 6611  df-nv 27308
This theorem is referenced by:  isnv  27328
  Copyright terms: Public domain W3C validator