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

Theorem isnvlem 27353
 Description: Lemma for isnv 27355. (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 27335 . . 3 NrmCVec = {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ (⟨𝑔, 𝑠⟩ ∈ CVecOLD𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))}
21eleq2i 2690 . 2 (⟨⟨𝐺, 𝑆⟩, 𝑁⟩ ∈ NrmCVec ↔ ⟨⟨𝐺, 𝑆⟩, 𝑁⟩ ∈ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ (⟨𝑔, 𝑠⟩ ∈ CVecOLD𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))})
3 opeq1 4377 . . . . 5 (𝑔 = 𝐺 → ⟨𝑔, 𝑠⟩ = ⟨𝐺, 𝑠⟩)
43eleq1d 2683 . . . 4 (𝑔 = 𝐺 → (⟨𝑔, 𝑠⟩ ∈ CVecOLD ↔ ⟨𝐺, 𝑠⟩ ∈ CVecOLD))
5 rneq 5321 . . . . . 6 (𝑔 = 𝐺 → ran 𝑔 = ran 𝐺)
6 isnvlem.1 . . . . . 6 𝑋 = ran 𝐺
75, 6syl6eqr 2673 . . . . 5 (𝑔 = 𝐺 → ran 𝑔 = 𝑋)
87feq2d 5998 . . . 4 (𝑔 = 𝐺 → (𝑛:ran 𝑔⟶ℝ ↔ 𝑛:𝑋⟶ℝ))
9 fveq2 6158 . . . . . . . . 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 6621 . . . . . . . . 9 (𝑔 = 𝐺 → (𝑥𝑔𝑦) = (𝑥𝐺𝑦))
1514fveq2d 6162 . . . . . . . 8 (𝑔 = 𝐺 → (𝑛‘(𝑥𝑔𝑦)) = (𝑛‘(𝑥𝐺𝑦)))
1615breq1d 4633 . . . . . . 7 (𝑔 = 𝐺 → ((𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)) ↔ (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))
177, 16raleqbidv 3145 . . . . . 6 (𝑔 = 𝐺 → (∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)) ↔ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))
1813, 173anbi13d 1398 . . . . 5 (𝑔 = 𝐺 → ((((𝑛𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))) ↔ (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))))
197, 18raleqbidv 3145 . . . 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 4378 . . . . 5 (𝑠 = 𝑆 → ⟨𝐺, 𝑠⟩ = ⟨𝐺, 𝑆⟩)
2221eleq1d 2683 . . . 4 (𝑠 = 𝑆 → (⟨𝐺, 𝑠⟩ ∈ CVecOLD ↔ ⟨𝐺, 𝑆⟩ ∈ CVecOLD))
23 oveq 6621 . . . . . . . . 9 (𝑠 = 𝑆 → (𝑦𝑠𝑥) = (𝑦𝑆𝑥))
2423fveq2d 6162 . . . . . . . 8 (𝑠 = 𝑆 → (𝑛‘(𝑦𝑠𝑥)) = (𝑛‘(𝑦𝑆𝑥)))
2524eqeq1d 2623 . . . . . . 7 (𝑠 = 𝑆 → ((𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ↔ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥))))
2625ralbidv 2982 . . . . . 6 (𝑠 = 𝑆 → (∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ↔ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥))))
27263anbi2d 1401 . . . . 5 (𝑠 = 𝑆 → ((((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))) ↔ (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))))
2827ralbidv 2982 . . . 4 (𝑠 = 𝑆 → (∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))) ↔ ∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))))
2922, 283anbi13d 1398 . . 3 (𝑠 = 𝑆 → ((⟨𝐺, 𝑠⟩ ∈ CVecOLD𝑛:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))) ↔ (⟨𝐺, 𝑆⟩ ∈ CVecOLD𝑛:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))))))
30 feq1 5993 . . . 4 (𝑛 = 𝑁 → (𝑛:𝑋⟶ℝ ↔ 𝑁:𝑋⟶ℝ))
31 fveq1 6157 . . . . . . . 8 (𝑛 = 𝑁 → (𝑛𝑥) = (𝑁𝑥))
3231eqeq1d 2623 . . . . . . 7 (𝑛 = 𝑁 → ((𝑛𝑥) = 0 ↔ (𝑁𝑥) = 0))
3332imbi1d 331 . . . . . 6 (𝑛 = 𝑁 → (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ↔ ((𝑁𝑥) = 0 → 𝑥 = 𝑍)))
34 fveq1 6157 . . . . . . . 8 (𝑛 = 𝑁 → (𝑛‘(𝑦𝑆𝑥)) = (𝑁‘(𝑦𝑆𝑥)))
3531oveq2d 6631 . . . . . . . 8 (𝑛 = 𝑁 → ((abs‘𝑦) · (𝑛𝑥)) = ((abs‘𝑦) · (𝑁𝑥)))
3634, 35eqeq12d 2636 . . . . . . 7 (𝑛 = 𝑁 → ((𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ↔ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥))))
3736ralbidv 2982 . . . . . 6 (𝑛 = 𝑁 → (∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ↔ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥))))
38 fveq1 6157 . . . . . . . 8 (𝑛 = 𝑁 → (𝑛‘(𝑥𝐺𝑦)) = (𝑁‘(𝑥𝐺𝑦)))
39 fveq1 6157 . . . . . . . . 9 (𝑛 = 𝑁 → (𝑛𝑦) = (𝑁𝑦))
4031, 39oveq12d 6633 . . . . . . . 8 (𝑛 = 𝑁 → ((𝑛𝑥) + (𝑛𝑦)) = ((𝑁𝑥) + (𝑁𝑦)))
4138, 40breq12d 4636 . . . . . . 7 (𝑛 = 𝑁 → ((𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)) ↔ (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))
4241ralbidv 2982 . . . . . 6 (𝑛 = 𝑁 → (∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)) ↔ ∀𝑦𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))
4333, 37, 423anbi123d 1396 . . . . 5 (𝑛 = 𝑁 → ((((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))) ↔ (((𝑁𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥)) ∧ ∀𝑦𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))))
4443ralbidv 2982 . . . 4 (𝑛 = 𝑁 → (∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦))) ↔ ∀𝑥𝑋 (((𝑁𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥)) ∧ ∀𝑦𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦)))))
4530, 443anbi23d 1399 . . 3 (𝑛 = 𝑁 → ((⟨𝐺, 𝑆⟩ ∈ CVecOLD𝑛:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑛𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑛𝑥)) ∧ ∀𝑦𝑋 (𝑛‘(𝑥𝐺𝑦)) ≤ ((𝑛𝑥) + (𝑛𝑦)))) ↔ (⟨𝐺, 𝑆⟩ ∈ CVecOLD𝑁:𝑋⟶ℝ ∧ ∀𝑥𝑋 (((𝑁𝑥) = 0 → 𝑥 = 𝑍) ∧ ∀𝑦 ∈ ℂ (𝑁‘(𝑦𝑆𝑥)) = ((abs‘𝑦) · (𝑁𝑥)) ∧ ∀𝑦𝑋 (𝑁‘(𝑥𝐺𝑦)) ≤ ((𝑁𝑥) + (𝑁𝑦))))))
4620, 29, 45eloprabg 6713 . 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 2908  Vcvv 3190  ⟨cop 4161   class class class wbr 4623  ran crn 5085  ⟶wf 5853  ‘cfv 5857  (class class class)co 6615  {coprab 6616  ℂcc 9894  ℝcr 9895  0cc0 9896   + caddc 9899   · cmul 9901   ≤ cle 10035  abscabs 13924  GIdcgi 27232  CVecOLDcvc 27301  NrmCVeccnv 27327 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 4751  ax-nul 4759  ax-pr 4877 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 2913  df-rex 2914  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-uni 4410  df-br 4624  df-opab 4684  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-fv 5865  df-ov 6618  df-oprab 6619  df-nv 27335 This theorem is referenced by:  isnv  27355
 Copyright terms: Public domain W3C validator