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

Theorem isnvlem 27921
Description: Lemma for isnv 27923. (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 27903 . . 3 NrmCVec = {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ (⟨𝑔, 𝑠⟩ ∈ CVecOLD𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))}
21eleq2i 2836 . 2 (⟨⟨𝐺, 𝑆⟩, 𝑁⟩ ∈ NrmCVec ↔ ⟨⟨𝐺, 𝑆⟩, 𝑁⟩ ∈ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ (⟨𝑔, 𝑠⟩ ∈ CVecOLD𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))})
3 opeq1 4559 . . . . 5 (𝑔 = 𝐺 → ⟨𝑔, 𝑠⟩ = ⟨𝐺, 𝑠⟩)
43eleq1d 2829 . . . 4 (𝑔 = 𝐺 → (⟨𝑔, 𝑠⟩ ∈ CVecOLD ↔ ⟨𝐺, 𝑠⟩ ∈ CVecOLD))
5 rneq 5519 . . . . . 6 (𝑔 = 𝐺 → ran 𝑔 = ran 𝐺)
6 isnvlem.1 . . . . . 6 𝑋 = ran 𝐺
75, 6syl6eqr 2817 . . . . 5 (𝑔 = 𝐺 → ran 𝑔 = 𝑋)
87feq2d 6209 . . . 4 (𝑔 = 𝐺 → (𝑛:ran 𝑔⟶ℝ ↔ 𝑛:𝑋⟶ℝ))
9 fveq2 6375 . . . . . . . . 9 (𝑔 = 𝐺 → (GId‘𝑔) = (GId‘𝐺))
10 isnvlem.2 . . . . . . . . 9 𝑍 = (GId‘𝐺)
119, 10syl6eqr 2817 . . . . . . . 8 (𝑔 = 𝐺 → (GId‘𝑔) = 𝑍)
1211eqeq2d 2775 . . . . . . 7 (𝑔 = 𝐺 → (𝑥 = (GId‘𝑔) ↔ 𝑥 = 𝑍))
1312imbi2d 331 . . . . . 6 (𝑔 = 𝐺 → (((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ↔ ((𝑛𝑥) = 0 → 𝑥 = 𝑍)))
14 oveq 6848 . . . . . . . . 9 (𝑔 = 𝐺 → (𝑥𝑔𝑦) = (𝑥𝐺𝑦))
1514fveq2d 6379 . . . . . . . 8 (𝑔 = 𝐺 → (𝑛‘(𝑥𝑔𝑦)) = (𝑛‘(𝑥𝐺𝑦)))
1615breq1d 4819 . . . . . . 7 (𝑔 = 𝐺 → ((𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)) ↔ (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))
177, 16raleqbidv 3300 . . . . . 6 (𝑔 = 𝐺 → (∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)) ↔ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))
1813, 173anbi13d 1562 . . . . 5 (𝑔 = 𝐺 → ((((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))) ↔ (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))))
197, 18raleqbidv 3300 . . . 4 (𝑔 = 𝐺 → (∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))) ↔ ∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))))
204, 8, 193anbi123d 1560 . . 3 (𝑔 = 𝐺 → ((⟨𝑔, 𝑠⟩ ∈ CVecOLD𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))) ↔ (⟨𝐺, 𝑠⟩ ∈ CVecOLD𝑛:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))))
21 opeq2 4560 . . . . 5 (𝑠 = 𝑆 → ⟨𝐺, 𝑠⟩ = ⟨𝐺, 𝑆⟩)
2221eleq1d 2829 . . . 4 (𝑠 = 𝑆 → (⟨𝐺, 𝑠⟩ ∈ CVecOLD ↔ ⟨𝐺, 𝑆⟩ ∈ CVecOLD))
23 oveq 6848 . . . . . . . 8 (𝑠 = 𝑆 → (𝑦𝑠𝑥) = (𝑦𝑆𝑥))
2423fveqeq2d 6383 . . . . . . 7 (𝑠 = 𝑆 → ((𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ↔ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥))))
2524ralbidv 3133 . . . . . 6 (𝑠 = 𝑆 → (∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ↔ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥))))
26253anbi2d 1565 . . . . 5 (𝑠 = 𝑆 → ((((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))) ↔ (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))))
2726ralbidv 3133 . . . 4 (𝑠 = 𝑆 → (∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))) ↔ ∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))))
2822, 273anbi13d 1562 . . 3 (𝑠 = 𝑆 → ((⟨𝐺, 𝑠⟩ ∈ CVecOLD𝑛:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))) ↔ (⟨𝐺, 𝑆⟩ ∈ CVecOLD𝑛:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))))
29 feq1 6204 . . . 4 (𝑛 = 𝑁 → (𝑛:𝑋⟶ℝ ↔ 𝑁:𝑋⟶ℝ))
30 fveq1 6374 . . . . . . . 8 (𝑛 = 𝑁 → (𝑛𝑥) = (𝑁𝑥))
3130eqeq1d 2767 . . . . . . 7 (𝑛 = 𝑁 → ((𝑛𝑥) = 0 ↔ (𝑁𝑥) = 0))
3231imbi1d 332 . . . . . 6 (𝑛 = 𝑁 → (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ↔ ((𝑁𝑥) = 0 → 𝑥 = 𝑍)))
33 fveq1 6374 . . . . . . . 8 (𝑛 = 𝑁 → (𝑛‘(𝑦𝑆𝑥)) = (𝑁‘(𝑦𝑆𝑥)))
3430oveq2d 6858 . . . . . . . 8 (𝑛 = 𝑁 → ((abs‘𝑦) · (𝑛𝑥)) = ((abs‘𝑦) · (𝑁𝑥)))
3533, 34eqeq12d 2780 . . . . . . 7 (𝑛 = 𝑁 → ((𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ↔ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥))))
3635ralbidv 3133 . . . . . 6 (𝑛 = 𝑁 → (∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ↔ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥))))
37 fveq1 6374 . . . . . . . 8 (𝑛 = 𝑁 → (𝑛‘(𝑥𝐺𝑦)) = (𝑁‘(𝑥𝐺𝑦)))
38 fveq1 6374 . . . . . . . . 9 (𝑛 = 𝑁 → (𝑛𝑦) = (𝑁𝑦))
3930, 38oveq12d 6860 . . . . . . . 8 (𝑛 = 𝑁 → ((𝑛𝑥) + (𝑛𝑦)) = ((𝑁𝑥) + (𝑁𝑦)))
4037, 39breq12d 4822 . . . . . . 7 (𝑛 = 𝑁 → ((𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)) ↔ (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))
4140ralbidv 3133 . . . . . 6 (𝑛 = 𝑁 → (∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)) ↔ ∀𝑦𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))
4232, 36, 413anbi123d 1560 . . . . 5 (𝑛 = 𝑁 → ((((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))) ↔ (((𝑁𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥)) ∧ ∀𝑦𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))))
4342ralbidv 3133 . . . 4 (𝑛 = 𝑁 → (∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))) ↔ ∀𝑥𝑋 (((𝑁𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥)) ∧ ∀𝑦𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))))
4429, 433anbi23d 1563 . . 3 (𝑛 = 𝑁 → ((⟨𝐺, 𝑆⟩ ∈ CVecOLD𝑛:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))) ↔ (⟨𝐺, 𝑆⟩ ∈ CVecOLD𝑁:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥)) ∧ ∀𝑦𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))))
4520, 28, 44eloprabg 6946 . 2 ((𝐺 ∈ V ∧ 𝑆 ∈ V ∧ 𝑁 ∈ V) → (⟨⟨𝐺, 𝑆⟩, 𝑁⟩ ∈ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ (⟨𝑔, 𝑠⟩ ∈ CVecOLD𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))} ↔ (⟨𝐺, 𝑆⟩ ∈ CVecOLD𝑁:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥)) ∧ ∀𝑦𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))))
462, 45syl5bb 274 1 ((𝐺 ∈ V ∧ 𝑆 ∈ V ∧ 𝑁 ∈ V) → (⟨⟨𝐺, 𝑆⟩, 𝑁⟩ ∈ NrmCVec ↔ (⟨𝐺, 𝑆⟩ ∈ CVecOLD𝑁:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥)) ∧ ∀𝑦𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  w3a 1107   = wceq 1652  wcel 2155  wral 3055  Vcvv 3350  cop 4340   class class class wbr 4809  ran crn 5278  wf 6064  cfv 6068  (class class class)co 6842  {coprab 6843  cc 10187  cr 10188  0cc0 10189   + caddc 10192   · cmul 10194  cle 10329  abscabs 14259  GIdcgi 27801  CVecOLDcvc 27869  NrmCVeccnv 27895
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pr 5062
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-br 4810  df-opab 4872  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-fv 6076  df-ov 6845  df-oprab 6846  df-nv 27903
This theorem is referenced by:  isnv  27923
  Copyright terms: Public domain W3C validator