# Metamath Proof Explorer

## Theorem isphl

Description: The predicate "is a generalized pre-Hilbert (inner product) space". (Contributed by NM, 22-Sep-2011) (Revised by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses isphl.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
isphl.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
isphl.h
isphl.o
isphl.i
isphl.z ${⊢}{Z}={0}_{{F}}$
Assertion isphl

### Proof

Step Hyp Ref Expression
1 isphl.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 isphl.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
3 isphl.h
4 isphl.o
5 isphl.i
6 isphl.z ${⊢}{Z}={0}_{{F}}$
7 fvexd ${⊢}{g}={W}\to {\mathrm{Base}}_{{g}}\in \mathrm{V}$
8 fvexd ${⊢}\left({g}={W}\wedge {v}={\mathrm{Base}}_{{g}}\right)\to {\cdot }_{𝑖}\left({g}\right)\in \mathrm{V}$
9 fvexd ${⊢}\left(\left({g}={W}\wedge {v}={\mathrm{Base}}_{{g}}\right)\wedge {h}={\cdot }_{𝑖}\left({g}\right)\right)\to \mathrm{Scalar}\left({g}\right)\in \mathrm{V}$
10 id ${⊢}{f}=\mathrm{Scalar}\left({g}\right)\to {f}=\mathrm{Scalar}\left({g}\right)$
11 simpll ${⊢}\left(\left({g}={W}\wedge {v}={\mathrm{Base}}_{{g}}\right)\wedge {h}={\cdot }_{𝑖}\left({g}\right)\right)\to {g}={W}$
12 11 fveq2d ${⊢}\left(\left({g}={W}\wedge {v}={\mathrm{Base}}_{{g}}\right)\wedge {h}={\cdot }_{𝑖}\left({g}\right)\right)\to \mathrm{Scalar}\left({g}\right)=\mathrm{Scalar}\left({W}\right)$
13 12 2 eqtr4di ${⊢}\left(\left({g}={W}\wedge {v}={\mathrm{Base}}_{{g}}\right)\wedge {h}={\cdot }_{𝑖}\left({g}\right)\right)\to \mathrm{Scalar}\left({g}\right)={F}$
14 10 13 sylan9eqr ${⊢}\left(\left(\left({g}={W}\wedge {v}={\mathrm{Base}}_{{g}}\right)\wedge {h}={\cdot }_{𝑖}\left({g}\right)\right)\wedge {f}=\mathrm{Scalar}\left({g}\right)\right)\to {f}={F}$
15 14 eleq1d ${⊢}\left(\left(\left({g}={W}\wedge {v}={\mathrm{Base}}_{{g}}\right)\wedge {h}={\cdot }_{𝑖}\left({g}\right)\right)\wedge {f}=\mathrm{Scalar}\left({g}\right)\right)\to \left({f}\in \mathrm{*-Ring}↔{F}\in \mathrm{*-Ring}\right)$
16 simpllr ${⊢}\left(\left(\left({g}={W}\wedge {v}={\mathrm{Base}}_{{g}}\right)\wedge {h}={\cdot }_{𝑖}\left({g}\right)\right)\wedge {f}=\mathrm{Scalar}\left({g}\right)\right)\to {v}={\mathrm{Base}}_{{g}}$
17 simplll ${⊢}\left(\left(\left({g}={W}\wedge {v}={\mathrm{Base}}_{{g}}\right)\wedge {h}={\cdot }_{𝑖}\left({g}\right)\right)\wedge {f}=\mathrm{Scalar}\left({g}\right)\right)\to {g}={W}$
18 17 fveq2d ${⊢}\left(\left(\left({g}={W}\wedge {v}={\mathrm{Base}}_{{g}}\right)\wedge {h}={\cdot }_{𝑖}\left({g}\right)\right)\wedge {f}=\mathrm{Scalar}\left({g}\right)\right)\to {\mathrm{Base}}_{{g}}={\mathrm{Base}}_{{W}}$
19 18 1 eqtr4di ${⊢}\left(\left(\left({g}={W}\wedge {v}={\mathrm{Base}}_{{g}}\right)\wedge {h}={\cdot }_{𝑖}\left({g}\right)\right)\wedge {f}=\mathrm{Scalar}\left({g}\right)\right)\to {\mathrm{Base}}_{{g}}={V}$
20 16 19 eqtrd ${⊢}\left(\left(\left({g}={W}\wedge {v}={\mathrm{Base}}_{{g}}\right)\wedge {h}={\cdot }_{𝑖}\left({g}\right)\right)\wedge {f}=\mathrm{Scalar}\left({g}\right)\right)\to {v}={V}$
21 simplr ${⊢}\left(\left(\left({g}={W}\wedge {v}={\mathrm{Base}}_{{g}}\right)\wedge {h}={\cdot }_{𝑖}\left({g}\right)\right)\wedge {f}=\mathrm{Scalar}\left({g}\right)\right)\to {h}={\cdot }_{𝑖}\left({g}\right)$
22 17 fveq2d ${⊢}\left(\left(\left({g}={W}\wedge {v}={\mathrm{Base}}_{{g}}\right)\wedge {h}={\cdot }_{𝑖}\left({g}\right)\right)\wedge {f}=\mathrm{Scalar}\left({g}\right)\right)\to {\cdot }_{𝑖}\left({g}\right)={\cdot }_{𝑖}\left({W}\right)$
23 22 3 eqtr4di
24 21 23 eqtrd
25 24 oveqd
26 20 25 mpteq12dv
27 14 fveq2d ${⊢}\left(\left(\left({g}={W}\wedge {v}={\mathrm{Base}}_{{g}}\right)\wedge {h}={\cdot }_{𝑖}\left({g}\right)\right)\wedge {f}=\mathrm{Scalar}\left({g}\right)\right)\to \mathrm{ringLMod}\left({f}\right)=\mathrm{ringLMod}\left({F}\right)$
28 17 27 oveq12d ${⊢}\left(\left(\left({g}={W}\wedge {v}={\mathrm{Base}}_{{g}}\right)\wedge {h}={\cdot }_{𝑖}\left({g}\right)\right)\wedge {f}=\mathrm{Scalar}\left({g}\right)\right)\to {g}\mathrm{LMHom}\mathrm{ringLMod}\left({f}\right)={W}\mathrm{LMHom}\mathrm{ringLMod}\left({F}\right)$
29 26 28 eleq12d
30 24 oveqd
31 14 fveq2d ${⊢}\left(\left(\left({g}={W}\wedge {v}={\mathrm{Base}}_{{g}}\right)\wedge {h}={\cdot }_{𝑖}\left({g}\right)\right)\wedge {f}=\mathrm{Scalar}\left({g}\right)\right)\to {0}_{{f}}={0}_{{F}}$
32 31 6 eqtr4di ${⊢}\left(\left(\left({g}={W}\wedge {v}={\mathrm{Base}}_{{g}}\right)\wedge {h}={\cdot }_{𝑖}\left({g}\right)\right)\wedge {f}=\mathrm{Scalar}\left({g}\right)\right)\to {0}_{{f}}={Z}$
33 30 32 eqeq12d
34 17 fveq2d ${⊢}\left(\left(\left({g}={W}\wedge {v}={\mathrm{Base}}_{{g}}\right)\wedge {h}={\cdot }_{𝑖}\left({g}\right)\right)\wedge {f}=\mathrm{Scalar}\left({g}\right)\right)\to {0}_{{g}}={0}_{{W}}$
35 34 4 eqtr4di
36 35 eqeq2d
37 33 36 imbi12d
38 14 fveq2d ${⊢}\left(\left(\left({g}={W}\wedge {v}={\mathrm{Base}}_{{g}}\right)\wedge {h}={\cdot }_{𝑖}\left({g}\right)\right)\wedge {f}=\mathrm{Scalar}\left({g}\right)\right)\to {*}_{{f}}={*}_{{F}}$
39 38 5 eqtr4di
40 24 oveqd
41 39 40 fveq12d
42 41 25 eqeq12d
43 20 42 raleqbidv
44 29 37 43 3anbi123d
45 20 44 raleqbidv
46 15 45 anbi12d
47 9 46 sbcied
48 8 47 sbcied
49 7 48 sbcied
50 df-phl
51 49 50 elrab2
52 3anass
53 51 52 bitr4i