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

Theorem ip0l 20785
Description: Inner product with a zero first argument. Part of proof of Theorem 6.44 of [Ponnusamy] p. 361. (Contributed by NM, 5-Feb-2007.) (Revised by Mario Carneiro, 7-Oct-2015.)
Hypotheses
Ref Expression
phlsrng.f 𝐹 = (Scalar‘𝑊)
phllmhm.h , = (·𝑖𝑊)
phllmhm.v 𝑉 = (Base‘𝑊)
ip0l.z 𝑍 = (0g𝐹)
ip0l.o 0 = (0g𝑊)
Assertion
Ref Expression
ip0l ((𝑊 ∈ PreHil ∧ 𝐴𝑉) → ( 0 , 𝐴) = 𝑍)

Proof of Theorem ip0l
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 phllmod 20779 . . . . 5 (𝑊 ∈ PreHil → 𝑊 ∈ LMod)
2 lmodgrp 20074 . . . . 5 (𝑊 ∈ LMod → 𝑊 ∈ Grp)
3 phllmhm.v . . . . . 6 𝑉 = (Base‘𝑊)
4 ip0l.o . . . . . 6 0 = (0g𝑊)
53, 4grpidcl 18551 . . . . 5 (𝑊 ∈ Grp → 0𝑉)
61, 2, 53syl 18 . . . 4 (𝑊 ∈ PreHil → 0𝑉)
76adantr 480 . . 3 ((𝑊 ∈ PreHil ∧ 𝐴𝑉) → 0𝑉)
8 oveq1 7267 . . . 4 (𝑥 = 0 → (𝑥 , 𝐴) = ( 0 , 𝐴))
9 eqid 2737 . . . 4 (𝑥𝑉 ↦ (𝑥 , 𝐴)) = (𝑥𝑉 ↦ (𝑥 , 𝐴))
10 ovex 7293 . . . 4 ( 0 , 𝐴) ∈ V
118, 9, 10fvmpt 6862 . . 3 ( 0𝑉 → ((𝑥𝑉 ↦ (𝑥 , 𝐴))‘ 0 ) = ( 0 , 𝐴))
127, 11syl 17 . 2 ((𝑊 ∈ PreHil ∧ 𝐴𝑉) → ((𝑥𝑉 ↦ (𝑥 , 𝐴))‘ 0 ) = ( 0 , 𝐴))
13 phlsrng.f . . . 4 𝐹 = (Scalar‘𝑊)
14 phllmhm.h . . . 4 , = (·𝑖𝑊)
1513, 14, 3, 9phllmhm 20781 . . 3 ((𝑊 ∈ PreHil ∧ 𝐴𝑉) → (𝑥𝑉 ↦ (𝑥 , 𝐴)) ∈ (𝑊 LMHom (ringLMod‘𝐹)))
16 lmghm 20237 . . 3 ((𝑥𝑉 ↦ (𝑥 , 𝐴)) ∈ (𝑊 LMHom (ringLMod‘𝐹)) → (𝑥𝑉 ↦ (𝑥 , 𝐴)) ∈ (𝑊 GrpHom (ringLMod‘𝐹)))
17 ip0l.z . . . . 5 𝑍 = (0g𝐹)
18 rlm0 20411 . . . . 5 (0g𝐹) = (0g‘(ringLMod‘𝐹))
1917, 18eqtri 2765 . . . 4 𝑍 = (0g‘(ringLMod‘𝐹))
204, 19ghmid 18784 . . 3 ((𝑥𝑉 ↦ (𝑥 , 𝐴)) ∈ (𝑊 GrpHom (ringLMod‘𝐹)) → ((𝑥𝑉 ↦ (𝑥 , 𝐴))‘ 0 ) = 𝑍)
2115, 16, 203syl 18 . 2 ((𝑊 ∈ PreHil ∧ 𝐴𝑉) → ((𝑥𝑉 ↦ (𝑥 , 𝐴))‘ 0 ) = 𝑍)
2212, 21eqtr3d 2779 1 ((𝑊 ∈ PreHil ∧ 𝐴𝑉) → ( 0 , 𝐴) = 𝑍)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1539  wcel 2107  cmpt 5158  cfv 6423  (class class class)co 7260  Basecbs 16856  Scalarcsca 16909  ·𝑖cip 16911  0gc0g 17094  Grpcgrp 18521   GrpHom cghm 18775  LModclmod 20067   LMHom clmhm 20225  ringLModcrglmod 20375  PreHilcphl 20773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5210  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7571  ax-cnex 10874  ax-resscn 10875  ax-1cn 10876  ax-icn 10877  ax-addcl 10878  ax-addrcl 10879  ax-mulcl 10880  ax-mulrcl 10881  ax-mulcom 10882  ax-addass 10883  ax-mulass 10884  ax-distr 10885  ax-i2m1 10886  ax-1ne0 10887  ax-1rid 10888  ax-rnegex 10889  ax-rrecex 10890  ax-cnre 10891  ax-pre-lttri 10892  ax-pre-lttrn 10893  ax-pre-ltadd 10894  ax-pre-mulgt0 10895
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-reu 3069  df-rmo 3070  df-rab 3071  df-v 3429  df-sbc 3717  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4259  df-if 4462  df-pw 4537  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4842  df-iun 4928  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5485  df-eprel 5491  df-po 5499  df-so 5500  df-fr 5540  df-we 5542  df-xp 5591  df-rel 5592  df-cnv 5593  df-co 5594  df-dm 5595  df-rn 5596  df-res 5597  df-ima 5598  df-pred 6196  df-ord 6259  df-on 6260  df-lim 6261  df-suc 6262  df-iota 6381  df-fun 6425  df-fn 6426  df-f 6427  df-f1 6428  df-fo 6429  df-f1o 6430  df-fv 6431  df-riota 7217  df-ov 7263  df-oprab 7264  df-mpo 7265  df-om 7693  df-2nd 7810  df-frecs 8073  df-wrecs 8104  df-recs 8178  df-rdg 8217  df-er 8461  df-en 8697  df-dom 8698  df-sdom 8699  df-pnf 10958  df-mnf 10959  df-xr 10960  df-ltxr 10961  df-le 10962  df-sub 11153  df-neg 11154  df-nn 11920  df-2 11982  df-3 11983  df-4 11984  df-5 11985  df-6 11986  df-7 11987  df-8 11988  df-sets 16809  df-slot 16827  df-ndx 16839  df-base 16857  df-plusg 16919  df-sca 16922  df-vsca 16923  df-ip 16924  df-0g 17096  df-mgm 18270  df-sgrp 18319  df-mnd 18330  df-grp 18524  df-ghm 18776  df-lmod 20069  df-lmhm 20228  df-lvec 20309  df-sra 20378  df-rgmod 20379  df-phl 20775
This theorem is referenced by:  ip0r  20786  ipeq0  20787  ocvlss  20821  cphip0l  24309
  Copyright terms: Public domain W3C validator