MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imsmetlem Structured version   Visualization version   GIF version
Theorem imsmetlem 30378
Description: Lemma for imsmet 30379. (Contributed by NM, 29-Nov-2006.) (New usage is discouraged.)
Hypotheses
Ref Expression
imsmetlem.1 𝑋 = (BaseSetβ€˜π‘ˆ)
imsmetlem.2 𝐺 = ( +𝑣 β€˜π‘ˆ)
imsmetlem.7 𝑀 = (invβ€˜πΊ)
imsmetlem.4 𝑆 = ( ·𝑠OLD β€˜π‘ˆ)
imsmetlem.5 𝑍 = (0vecβ€˜π‘ˆ)
imsmetlem.6 𝑁 = (normCVβ€˜π‘ˆ)
imsmetlem.8 𝐷 = (IndMetβ€˜π‘ˆ)
imsmetlem.9 π‘ˆ ∈ NrmCVec
Assertion
Ref Expression
imsmetlem 𝐷 ∈ (Metβ€˜π‘‹)
Proof of Theorem imsmetlem
Dummy variables π‘₯ 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 imsmetlem.1 . . 3 𝑋 = (BaseSetβ€˜π‘ˆ)
21fvexi 6895 . 2 𝑋 ∈ V
3 imsmetlem.9 . . 3 π‘ˆ ∈ NrmCVec
4 imsmetlem.8 . . . 4 𝐷 = (IndMetβ€˜π‘ˆ)
51, 4imsdf 30377 . . 3 (π‘ˆ ∈ NrmCVec β†’ 𝐷:(𝑋 Γ— 𝑋)βŸΆβ„)
63, 5ax-mp 5 . 2 𝐷:(𝑋 Γ— 𝑋)βŸΆβ„
7 imsmetlem.2 . . . . . 6 𝐺 = ( +𝑣 β€˜π‘ˆ)
8 imsmetlem.4 . . . . . 6 𝑆 = ( ·𝑠OLD β€˜π‘ˆ)
9 imsmetlem.6 . . . . . 6 𝑁 = (normCVβ€˜π‘ˆ)
101, 7, 8, 9, 4imsdval2 30375 . . . . 5 ((π‘ˆ ∈ NrmCVec ∧ π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (π‘₯𝐷𝑦) = (π‘β€˜(π‘₯𝐺(-1𝑆𝑦))))
113, 10mp3an1 1444 . . . 4 ((π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (π‘₯𝐷𝑦) = (π‘β€˜(π‘₯𝐺(-1𝑆𝑦))))
1211eqeq1d 2726 . . 3 ((π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ ((π‘₯𝐷𝑦) = 0 ↔ (π‘β€˜(π‘₯𝐺(-1𝑆𝑦))) = 0))
13 neg1cn 12322 . . . . . 6 -1 ∈ β„‚
141, 8nvscl 30314 . . . . . 6 ((π‘ˆ ∈ NrmCVec ∧ -1 ∈ β„‚ ∧ 𝑦 ∈ 𝑋) β†’ (-1𝑆𝑦) ∈ 𝑋)
153, 13, 14mp3an12 1447 . . . . 5 (𝑦 ∈ 𝑋 β†’ (-1𝑆𝑦) ∈ 𝑋)
161, 7nvgcl 30308 . . . . . 6 ((π‘ˆ ∈ NrmCVec ∧ π‘₯ ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋) β†’ (π‘₯𝐺(-1𝑆𝑦)) ∈ 𝑋)
173, 16mp3an1 1444 . . . . 5 ((π‘₯ ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋) β†’ (π‘₯𝐺(-1𝑆𝑦)) ∈ 𝑋)
1815, 17sylan2 592 . . . 4 ((π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (π‘₯𝐺(-1𝑆𝑦)) ∈ 𝑋)
19 imsmetlem.5 . . . . 5 𝑍 = (0vecβ€˜π‘ˆ)
201, 19, 9nvz 30357 . . . 4 ((π‘ˆ ∈ NrmCVec ∧ (π‘₯𝐺(-1𝑆𝑦)) ∈ 𝑋) β†’ ((π‘β€˜(π‘₯𝐺(-1𝑆𝑦))) = 0 ↔ (π‘₯𝐺(-1𝑆𝑦)) = 𝑍))
213, 18, 20sylancr 586 . . 3 ((π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ ((π‘β€˜(π‘₯𝐺(-1𝑆𝑦))) = 0 ↔ (π‘₯𝐺(-1𝑆𝑦)) = 𝑍))
221, 19nvzcl 30322 . . . . . . 7 (π‘ˆ ∈ NrmCVec β†’ 𝑍 ∈ 𝑋)
233, 22ax-mp 5 . . . . . 6 𝑍 ∈ 𝑋
241, 7nvrcan 30312 . . . . . . 7 ((π‘ˆ ∈ NrmCVec ∧ ((π‘₯𝐺(-1𝑆𝑦)) ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) β†’ (((π‘₯𝐺(-1𝑆𝑦))𝐺𝑦) = (𝑍𝐺𝑦) ↔ (π‘₯𝐺(-1𝑆𝑦)) = 𝑍))
253, 24mpan 687 . . . . . 6 (((π‘₯𝐺(-1𝑆𝑦)) ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (((π‘₯𝐺(-1𝑆𝑦))𝐺𝑦) = (𝑍𝐺𝑦) ↔ (π‘₯𝐺(-1𝑆𝑦)) = 𝑍))
2623, 25mp3an2 1445 . . . . 5 (((π‘₯𝐺(-1𝑆𝑦)) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (((π‘₯𝐺(-1𝑆𝑦))𝐺𝑦) = (𝑍𝐺𝑦) ↔ (π‘₯𝐺(-1𝑆𝑦)) = 𝑍))
2718, 26sylancom 587 . . . 4 ((π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (((π‘₯𝐺(-1𝑆𝑦))𝐺𝑦) = (𝑍𝐺𝑦) ↔ (π‘₯𝐺(-1𝑆𝑦)) = 𝑍))
28 simpl 482 . . . . . . 7 ((π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ π‘₯ ∈ 𝑋)
2915adantl 481 . . . . . . 7 ((π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (-1𝑆𝑦) ∈ 𝑋)
30 simpr 484 . . . . . . 7 ((π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ 𝑦 ∈ 𝑋)
311, 7nvass 30310 . . . . . . . 8 ((π‘ˆ ∈ NrmCVec ∧ (π‘₯ ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) β†’ ((π‘₯𝐺(-1𝑆𝑦))𝐺𝑦) = (π‘₯𝐺((-1𝑆𝑦)𝐺𝑦)))
323, 31mpan 687 . . . . . . 7 ((π‘₯ ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ ((π‘₯𝐺(-1𝑆𝑦))𝐺𝑦) = (π‘₯𝐺((-1𝑆𝑦)𝐺𝑦)))
3328, 29, 30, 32syl3anc 1368 . . . . . 6 ((π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ ((π‘₯𝐺(-1𝑆𝑦))𝐺𝑦) = (π‘₯𝐺((-1𝑆𝑦)𝐺𝑦)))
341, 7, 8, 19nvlinv 30340 . . . . . . . . 9 ((π‘ˆ ∈ NrmCVec ∧ 𝑦 ∈ 𝑋) β†’ ((-1𝑆𝑦)𝐺𝑦) = 𝑍)
353, 34mpan 687 . . . . . . . 8 (𝑦 ∈ 𝑋 β†’ ((-1𝑆𝑦)𝐺𝑦) = 𝑍)
3635adantl 481 . . . . . . 7 ((π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ ((-1𝑆𝑦)𝐺𝑦) = 𝑍)
3736oveq2d 7417 . . . . . 6 ((π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (π‘₯𝐺((-1𝑆𝑦)𝐺𝑦)) = (π‘₯𝐺𝑍))
381, 7, 19nv0rid 30323 . . . . . . . 8 ((π‘ˆ ∈ NrmCVec ∧ π‘₯ ∈ 𝑋) β†’ (π‘₯𝐺𝑍) = π‘₯)
393, 38mpan 687 . . . . . . 7 (π‘₯ ∈ 𝑋 β†’ (π‘₯𝐺𝑍) = π‘₯)
4039adantr 480 . . . . . 6 ((π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (π‘₯𝐺𝑍) = π‘₯)
4133, 37, 403eqtrd 2768 . . . . 5 ((π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ ((π‘₯𝐺(-1𝑆𝑦))𝐺𝑦) = π‘₯)
421, 7, 19nv0lid 30324 . . . . . . 7 ((π‘ˆ ∈ NrmCVec ∧ 𝑦 ∈ 𝑋) β†’ (𝑍𝐺𝑦) = 𝑦)
433, 42mpan 687 . . . . . 6 (𝑦 ∈ 𝑋 β†’ (𝑍𝐺𝑦) = 𝑦)
4443adantl 481 . . . . 5 ((π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (𝑍𝐺𝑦) = 𝑦)
4541, 44eqeq12d 2740 . . . 4 ((π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (((π‘₯𝐺(-1𝑆𝑦))𝐺𝑦) = (𝑍𝐺𝑦) ↔ π‘₯ = 𝑦))
4627, 45bitr3d 281 . . 3 ((π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ ((π‘₯𝐺(-1𝑆𝑦)) = 𝑍 ↔ π‘₯ = 𝑦))
4712, 21, 463bitrd 305 . 2 ((π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ ((π‘₯𝐷𝑦) = 0 ↔ π‘₯ = 𝑦))
48 simpr 484 . . . . . . 7 ((𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋) β†’ π‘₯ ∈ 𝑋)
491, 8nvscl 30314 . . . . . . . . 9 ((π‘ˆ ∈ NrmCVec ∧ -1 ∈ β„‚ ∧ 𝑧 ∈ 𝑋) β†’ (-1𝑆𝑧) ∈ 𝑋)
503, 13, 49mp3an12 1447 . . . . . . . 8 (𝑧 ∈ 𝑋 β†’ (-1𝑆𝑧) ∈ 𝑋)
5150adantr 480 . . . . . . 7 ((𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋) β†’ (-1𝑆𝑧) ∈ 𝑋)
521, 7nvgcl 30308 . . . . . . . 8 ((π‘ˆ ∈ NrmCVec ∧ π‘₯ ∈ 𝑋 ∧ (-1𝑆𝑧) ∈ 𝑋) β†’ (π‘₯𝐺(-1𝑆𝑧)) ∈ 𝑋)
533, 52mp3an1 1444 . . . . . . 7 ((π‘₯ ∈ 𝑋 ∧ (-1𝑆𝑧) ∈ 𝑋) β†’ (π‘₯𝐺(-1𝑆𝑧)) ∈ 𝑋)
5448, 51, 53syl2anc 583 . . . . . 6 ((𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋) β†’ (π‘₯𝐺(-1𝑆𝑧)) ∈ 𝑋)
55543adant3 1129 . . . . 5 ((𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (π‘₯𝐺(-1𝑆𝑧)) ∈ 𝑋)
561, 7nvgcl 30308 . . . . . . . 8 ((π‘ˆ ∈ NrmCVec ∧ 𝑧 ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋) β†’ (𝑧𝐺(-1𝑆𝑦)) ∈ 𝑋)
573, 56mp3an1 1444 . . . . . . 7 ((𝑧 ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋) β†’ (𝑧𝐺(-1𝑆𝑦)) ∈ 𝑋)
5815, 57sylan2 592 . . . . . 6 ((𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (𝑧𝐺(-1𝑆𝑦)) ∈ 𝑋)
59583adant2 1128 . . . . 5 ((𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (𝑧𝐺(-1𝑆𝑦)) ∈ 𝑋)
601, 7, 9nvtri 30358 . . . . . 6 ((π‘ˆ ∈ NrmCVec ∧ (π‘₯𝐺(-1𝑆𝑧)) ∈ 𝑋 ∧ (𝑧𝐺(-1𝑆𝑦)) ∈ 𝑋) β†’ (π‘β€˜((π‘₯𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦)))) ≀ ((π‘β€˜(π‘₯𝐺(-1𝑆𝑧))) + (π‘β€˜(𝑧𝐺(-1𝑆𝑦)))))
613, 60mp3an1 1444 . . . . 5 (((π‘₯𝐺(-1𝑆𝑧)) ∈ 𝑋 ∧ (𝑧𝐺(-1𝑆𝑦)) ∈ 𝑋) β†’ (π‘β€˜((π‘₯𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦)))) ≀ ((π‘β€˜(π‘₯𝐺(-1𝑆𝑧))) + (π‘β€˜(𝑧𝐺(-1𝑆𝑦)))))
6255, 59, 61syl2anc 583 . . . 4 ((𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (π‘β€˜((π‘₯𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦)))) ≀ ((π‘β€˜(π‘₯𝐺(-1𝑆𝑧))) + (π‘β€˜(𝑧𝐺(-1𝑆𝑦)))))
63113adant1 1127 . . . . 5 ((𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (π‘₯𝐷𝑦) = (π‘β€˜(π‘₯𝐺(-1𝑆𝑦))))
64 simp1 1133 . . . . . . . 8 ((𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ 𝑧 ∈ 𝑋)
65153ad2ant3 1132 . . . . . . . 8 ((𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (-1𝑆𝑦) ∈ 𝑋)
661, 7nvass 30310 . . . . . . . . 9 ((π‘ˆ ∈ NrmCVec ∧ ((π‘₯𝐺(-1𝑆𝑧)) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋)) β†’ (((π‘₯𝐺(-1𝑆𝑧))𝐺𝑧)𝐺(-1𝑆𝑦)) = ((π‘₯𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦))))
673, 66mpan 687 . . . . . . . 8 (((π‘₯𝐺(-1𝑆𝑧)) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋) β†’ (((π‘₯𝐺(-1𝑆𝑧))𝐺𝑧)𝐺(-1𝑆𝑦)) = ((π‘₯𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦))))
6855, 64, 65, 67syl3anc 1368 . . . . . . 7 ((𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (((π‘₯𝐺(-1𝑆𝑧))𝐺𝑧)𝐺(-1𝑆𝑦)) = ((π‘₯𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦))))
69 simpl 482 . . . . . . . . . . 11 ((𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋) β†’ 𝑧 ∈ 𝑋)
701, 7nvass 30310 . . . . . . . . . . . 12 ((π‘ˆ ∈ NrmCVec ∧ (π‘₯ ∈ 𝑋 ∧ (-1𝑆𝑧) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) β†’ ((π‘₯𝐺(-1𝑆𝑧))𝐺𝑧) = (π‘₯𝐺((-1𝑆𝑧)𝐺𝑧)))
713, 70mpan 687 . . . . . . . . . . 11 ((π‘₯ ∈ 𝑋 ∧ (-1𝑆𝑧) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) β†’ ((π‘₯𝐺(-1𝑆𝑧))𝐺𝑧) = (π‘₯𝐺((-1𝑆𝑧)𝐺𝑧)))
7248, 51, 69, 71syl3anc 1368 . . . . . . . . . 10 ((𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋) β†’ ((π‘₯𝐺(-1𝑆𝑧))𝐺𝑧) = (π‘₯𝐺((-1𝑆𝑧)𝐺𝑧)))
731, 7, 8, 19nvlinv 30340 . . . . . . . . . . . . 13 ((π‘ˆ ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) β†’ ((-1𝑆𝑧)𝐺𝑧) = 𝑍)
743, 73mpan 687 . . . . . . . . . . . 12 (𝑧 ∈ 𝑋 β†’ ((-1𝑆𝑧)𝐺𝑧) = 𝑍)
7574adantr 480 . . . . . . . . . . 11 ((𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋) β†’ ((-1𝑆𝑧)𝐺𝑧) = 𝑍)
7675oveq2d 7417 . . . . . . . . . 10 ((𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋) β†’ (π‘₯𝐺((-1𝑆𝑧)𝐺𝑧)) = (π‘₯𝐺𝑍))
7739adantl 481 . . . . . . . . . 10 ((𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋) β†’ (π‘₯𝐺𝑍) = π‘₯)
7872, 76, 773eqtrd 2768 . . . . . . . . 9 ((𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋) β†’ ((π‘₯𝐺(-1𝑆𝑧))𝐺𝑧) = π‘₯)
79783adant3 1129 . . . . . . . 8 ((𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ ((π‘₯𝐺(-1𝑆𝑧))𝐺𝑧) = π‘₯)
8079oveq1d 7416 . . . . . . 7 ((𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (((π‘₯𝐺(-1𝑆𝑧))𝐺𝑧)𝐺(-1𝑆𝑦)) = (π‘₯𝐺(-1𝑆𝑦)))
8168, 80eqtr3d 2766 . . . . . 6 ((𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ ((π‘₯𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦))) = (π‘₯𝐺(-1𝑆𝑦)))
8281fveq2d 6885 . . . . 5 ((𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (π‘β€˜((π‘₯𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦)))) = (π‘β€˜(π‘₯𝐺(-1𝑆𝑦))))
8363, 82eqtr4d 2767 . . . 4 ((𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (π‘₯𝐷𝑦) = (π‘β€˜((π‘₯𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦)))))
841, 7, 8, 9, 4imsdval2 30375 . . . . . . . 8 ((π‘ˆ ∈ NrmCVec ∧ 𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋) β†’ (𝑧𝐷π‘₯) = (π‘β€˜(𝑧𝐺(-1𝑆π‘₯))))
853, 84mp3an1 1444 . . . . . . 7 ((𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋) β†’ (𝑧𝐷π‘₯) = (π‘β€˜(𝑧𝐺(-1𝑆π‘₯))))
861, 7, 8, 9nvdif 30354 . . . . . . . 8 ((π‘ˆ ∈ NrmCVec ∧ 𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋) β†’ (π‘β€˜(𝑧𝐺(-1𝑆π‘₯))) = (π‘β€˜(π‘₯𝐺(-1𝑆𝑧))))
873, 86mp3an1 1444 . . . . . . 7 ((𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋) β†’ (π‘β€˜(𝑧𝐺(-1𝑆π‘₯))) = (π‘β€˜(π‘₯𝐺(-1𝑆𝑧))))
8885, 87eqtrd 2764 . . . . . 6 ((𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋) β†’ (𝑧𝐷π‘₯) = (π‘β€˜(π‘₯𝐺(-1𝑆𝑧))))
89883adant3 1129 . . . . 5 ((𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (𝑧𝐷π‘₯) = (π‘β€˜(π‘₯𝐺(-1𝑆𝑧))))
901, 7, 8, 9, 4imsdval2 30375 . . . . . . 7 ((π‘ˆ ∈ NrmCVec ∧ 𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (𝑧𝐷𝑦) = (π‘β€˜(𝑧𝐺(-1𝑆𝑦))))
913, 90mp3an1 1444 . . . . . 6 ((𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (𝑧𝐷𝑦) = (π‘β€˜(𝑧𝐺(-1𝑆𝑦))))
92913adant2 1128 . . . . 5 ((𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (𝑧𝐷𝑦) = (π‘β€˜(𝑧𝐺(-1𝑆𝑦))))
9389, 92oveq12d 7419 . . . 4 ((𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ ((𝑧𝐷π‘₯) + (𝑧𝐷𝑦)) = ((π‘β€˜(π‘₯𝐺(-1𝑆𝑧))) + (π‘β€˜(𝑧𝐺(-1𝑆𝑦)))))
9462, 83, 933brtr4d 5170 . . 3 ((𝑧 ∈ 𝑋 ∧ π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) β†’ (π‘₯𝐷𝑦) ≀ ((𝑧𝐷π‘₯) + (𝑧𝐷𝑦)))
95943coml 1124 . 2 ((π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) β†’ (π‘₯𝐷𝑦) ≀ ((𝑧𝐷π‘₯) + (𝑧𝐷𝑦)))
962, 6, 47, 95ismeti 24152 1 𝐷 ∈ (Metβ€˜π‘‹)
Colors of variables: wff setvar class
Syntax hints:   ↔ wb 205   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   class class class wbr 5138   Γ— cxp 5664  βŸΆwf 6529  β€˜cfv 6533  (class class class)co 7401  β„‚cc 11103  β„cr 11104  0cc0 11105  1c1 11106   + caddc 11108   ≀ cle 11245  -cneg 11441  Metcmet 21213  invcgn 30179  NrmCVeccnv 30272   +𝑣 cpv 30273  BaseSetcba 30274   ·𝑠OLD cns 30275  0veccn0v 30276  normCVcnmcv 30278  IndMetcims 30279
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-cnex 11161  ax-resscn 11162  ax-1cn 11163  ax-icn 11164  ax-addcl 11165  ax-addrcl 11166  ax-mulcl 11167  ax-mulrcl 11168  ax-mulcom 11169  ax-addass 11170  ax-mulass 11171  ax-distr 11172  ax-i2m1 11173  ax-1ne0 11174  ax-1rid 11175  ax-rnegex 11176  ax-rrecex 11177  ax-cnre 11178  ax-pre-lttri 11179  ax-pre-lttrn 11180  ax-pre-ltadd 11181  ax-pre-mulgt0 11182  ax-pre-sup 11183
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-om 7849  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-er 8698  df-map 8817  df-en 8935  df-dom 8936  df-sdom 8937  df-sup 9432  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-n0 12469  df-z 12555  df-uz 12819  df-rp 12971  df-seq 13963  df-exp 14024  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-met 21221  df-grpo 30181  df-gid 30182  df-ginv 30183  df-gdiv 30184  df-ablo 30233  df-vc 30247  df-nv 30280  df-va 30283  df-ba 30284  df-sm 30285  df-0v 30286  df-vs 30287  df-nmcv 30288  df-ims 30289
This theorem is referenced by:  imsmet  30379
  Copyright terms: Public domain W3C validator