# Metamath Proof Explorer

## Theorem phlpropd

Description: If two structures have the same components (properties), one is a pre-Hilbert space iff the other one is. (Contributed by Mario Carneiro, 8-Oct-2015)

Ref Expression
Hypotheses phlpropd.1 ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{K}}$
phlpropd.2 ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{L}}$
phlpropd.3 ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {x}{+}_{{K}}{y}={x}{+}_{{L}}{y}$
phlpropd.4 ${⊢}{\phi }\to {F}=\mathrm{Scalar}\left({K}\right)$
phlpropd.5 ${⊢}{\phi }\to {F}=\mathrm{Scalar}\left({L}\right)$
phlpropd.6 ${⊢}{P}={\mathrm{Base}}_{{F}}$
phlpropd.7 ${⊢}\left({\phi }\wedge \left({x}\in {P}\wedge {y}\in {B}\right)\right)\to {x}{\cdot }_{{K}}{y}={x}{\cdot }_{{L}}{y}$
phlpropd.8 ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {x}{\cdot }_{𝑖}\left({K}\right){y}={x}{\cdot }_{𝑖}\left({L}\right){y}$
Assertion phlpropd ${⊢}{\phi }\to \left({K}\in \mathrm{PreHil}↔{L}\in \mathrm{PreHil}\right)$

### Proof

Step Hyp Ref Expression
1 phlpropd.1 ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{K}}$
2 phlpropd.2 ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{L}}$
3 phlpropd.3 ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {x}{+}_{{K}}{y}={x}{+}_{{L}}{y}$
4 phlpropd.4 ${⊢}{\phi }\to {F}=\mathrm{Scalar}\left({K}\right)$
5 phlpropd.5 ${⊢}{\phi }\to {F}=\mathrm{Scalar}\left({L}\right)$
6 phlpropd.6 ${⊢}{P}={\mathrm{Base}}_{{F}}$
7 phlpropd.7 ${⊢}\left({\phi }\wedge \left({x}\in {P}\wedge {y}\in {B}\right)\right)\to {x}{\cdot }_{{K}}{y}={x}{\cdot }_{{L}}{y}$
8 phlpropd.8 ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {x}{\cdot }_{𝑖}\left({K}\right){y}={x}{\cdot }_{𝑖}\left({L}\right){y}$
9 1 2 3 4 5 6 7 lvecpropd ${⊢}{\phi }\to \left({K}\in \mathrm{LVec}↔{L}\in \mathrm{LVec}\right)$
10 4 5 eqtr3d ${⊢}{\phi }\to \mathrm{Scalar}\left({K}\right)=\mathrm{Scalar}\left({L}\right)$
11 10 eleq1d ${⊢}{\phi }\to \left(\mathrm{Scalar}\left({K}\right)\in \mathrm{*-Ring}↔\mathrm{Scalar}\left({L}\right)\in \mathrm{*-Ring}\right)$
12 8 oveqrspc2v ${⊢}\left({\phi }\wedge \left({b}\in {B}\wedge {a}\in {B}\right)\right)\to {b}{\cdot }_{𝑖}\left({K}\right){a}={b}{\cdot }_{𝑖}\left({L}\right){a}$
13 12 anass1rs ${⊢}\left(\left({\phi }\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\to {b}{\cdot }_{𝑖}\left({K}\right){a}={b}{\cdot }_{𝑖}\left({L}\right){a}$
14 13 mpteq2dva ${⊢}\left({\phi }\wedge {a}\in {B}\right)\to \left({b}\in {B}⟼{b}{\cdot }_{𝑖}\left({K}\right){a}\right)=\left({b}\in {B}⟼{b}{\cdot }_{𝑖}\left({L}\right){a}\right)$
15 1 adantr ${⊢}\left({\phi }\wedge {a}\in {B}\right)\to {B}={\mathrm{Base}}_{{K}}$
16 15 mpteq1d ${⊢}\left({\phi }\wedge {a}\in {B}\right)\to \left({b}\in {B}⟼{b}{\cdot }_{𝑖}\left({K}\right){a}\right)=\left({b}\in {\mathrm{Base}}_{{K}}⟼{b}{\cdot }_{𝑖}\left({K}\right){a}\right)$
17 2 adantr ${⊢}\left({\phi }\wedge {a}\in {B}\right)\to {B}={\mathrm{Base}}_{{L}}$
18 17 mpteq1d ${⊢}\left({\phi }\wedge {a}\in {B}\right)\to \left({b}\in {B}⟼{b}{\cdot }_{𝑖}\left({L}\right){a}\right)=\left({b}\in {\mathrm{Base}}_{{L}}⟼{b}{\cdot }_{𝑖}\left({L}\right){a}\right)$
19 14 16 18 3eqtr3d ${⊢}\left({\phi }\wedge {a}\in {B}\right)\to \left({b}\in {\mathrm{Base}}_{{K}}⟼{b}{\cdot }_{𝑖}\left({K}\right){a}\right)=\left({b}\in {\mathrm{Base}}_{{L}}⟼{b}{\cdot }_{𝑖}\left({L}\right){a}\right)$
20 rlmbas ${⊢}{\mathrm{Base}}_{{F}}={\mathrm{Base}}_{\mathrm{ringLMod}\left({F}\right)}$
21 6 20 eqtri ${⊢}{P}={\mathrm{Base}}_{\mathrm{ringLMod}\left({F}\right)}$
22 21 a1i ${⊢}{\phi }\to {P}={\mathrm{Base}}_{\mathrm{ringLMod}\left({F}\right)}$
23 fvex ${⊢}\mathrm{Scalar}\left({K}\right)\in \mathrm{V}$
24 4 23 eqeltrdi ${⊢}{\phi }\to {F}\in \mathrm{V}$
25 rlmsca ${⊢}{F}\in \mathrm{V}\to {F}=\mathrm{Scalar}\left(\mathrm{ringLMod}\left({F}\right)\right)$
26 24 25 syl ${⊢}{\phi }\to {F}=\mathrm{Scalar}\left(\mathrm{ringLMod}\left({F}\right)\right)$
27 eqidd ${⊢}\left({\phi }\wedge \left({x}\in {P}\wedge {y}\in {P}\right)\right)\to {x}{+}_{\mathrm{ringLMod}\left({F}\right)}{y}={x}{+}_{\mathrm{ringLMod}\left({F}\right)}{y}$
28 eqidd ${⊢}\left({\phi }\wedge \left({x}\in {P}\wedge {y}\in {P}\right)\right)\to {x}{\cdot }_{\mathrm{ringLMod}\left({F}\right)}{y}={x}{\cdot }_{\mathrm{ringLMod}\left({F}\right)}{y}$
29 1 22 2 22 4 26 5 26 6 6 3 27 7 28 lmhmpropd ${⊢}{\phi }\to {K}\mathrm{LMHom}\mathrm{ringLMod}\left({F}\right)={L}\mathrm{LMHom}\mathrm{ringLMod}\left({F}\right)$
30 4 fveq2d ${⊢}{\phi }\to \mathrm{ringLMod}\left({F}\right)=\mathrm{ringLMod}\left(\mathrm{Scalar}\left({K}\right)\right)$
31 30 oveq2d ${⊢}{\phi }\to {K}\mathrm{LMHom}\mathrm{ringLMod}\left({F}\right)={K}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({K}\right)\right)$
32 5 fveq2d ${⊢}{\phi }\to \mathrm{ringLMod}\left({F}\right)=\mathrm{ringLMod}\left(\mathrm{Scalar}\left({L}\right)\right)$
33 32 oveq2d ${⊢}{\phi }\to {L}\mathrm{LMHom}\mathrm{ringLMod}\left({F}\right)={L}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({L}\right)\right)$
34 29 31 33 3eqtr3d ${⊢}{\phi }\to {K}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({K}\right)\right)={L}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({L}\right)\right)$
35 34 adantr ${⊢}\left({\phi }\wedge {a}\in {B}\right)\to {K}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({K}\right)\right)={L}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({L}\right)\right)$
36 19 35 eleq12d ${⊢}\left({\phi }\wedge {a}\in {B}\right)\to \left(\left({b}\in {\mathrm{Base}}_{{K}}⟼{b}{\cdot }_{𝑖}\left({K}\right){a}\right)\in \left({K}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({K}\right)\right)\right)↔\left({b}\in {\mathrm{Base}}_{{L}}⟼{b}{\cdot }_{𝑖}\left({L}\right){a}\right)\in \left({L}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({L}\right)\right)\right)\right)$
37 8 oveqrspc2v ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {a}\in {B}\right)\right)\to {a}{\cdot }_{𝑖}\left({K}\right){a}={a}{\cdot }_{𝑖}\left({L}\right){a}$
38 37 anabsan2 ${⊢}\left({\phi }\wedge {a}\in {B}\right)\to {a}{\cdot }_{𝑖}\left({K}\right){a}={a}{\cdot }_{𝑖}\left({L}\right){a}$
39 10 fveq2d ${⊢}{\phi }\to {0}_{\mathrm{Scalar}\left({K}\right)}={0}_{\mathrm{Scalar}\left({L}\right)}$
40 39 adantr ${⊢}\left({\phi }\wedge {a}\in {B}\right)\to {0}_{\mathrm{Scalar}\left({K}\right)}={0}_{\mathrm{Scalar}\left({L}\right)}$
41 38 40 eqeq12d ${⊢}\left({\phi }\wedge {a}\in {B}\right)\to \left({a}{\cdot }_{𝑖}\left({K}\right){a}={0}_{\mathrm{Scalar}\left({K}\right)}↔{a}{\cdot }_{𝑖}\left({L}\right){a}={0}_{\mathrm{Scalar}\left({L}\right)}\right)$
42 1 2 3 grpidpropd ${⊢}{\phi }\to {0}_{{K}}={0}_{{L}}$
43 42 adantr ${⊢}\left({\phi }\wedge {a}\in {B}\right)\to {0}_{{K}}={0}_{{L}}$
44 43 eqeq2d ${⊢}\left({\phi }\wedge {a}\in {B}\right)\to \left({a}={0}_{{K}}↔{a}={0}_{{L}}\right)$
45 41 44 imbi12d ${⊢}\left({\phi }\wedge {a}\in {B}\right)\to \left(\left({a}{\cdot }_{𝑖}\left({K}\right){a}={0}_{\mathrm{Scalar}\left({K}\right)}\to {a}={0}_{{K}}\right)↔\left({a}{\cdot }_{𝑖}\left({L}\right){a}={0}_{\mathrm{Scalar}\left({L}\right)}\to {a}={0}_{{L}}\right)\right)$
46 10 fveq2d ${⊢}{\phi }\to {*}_{\mathrm{Scalar}\left({K}\right)}={*}_{\mathrm{Scalar}\left({L}\right)}$
47 46 adantr ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {*}_{\mathrm{Scalar}\left({K}\right)}={*}_{\mathrm{Scalar}\left({L}\right)}$
48 8 oveqrspc2v ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {a}{\cdot }_{𝑖}\left({K}\right){b}={a}{\cdot }_{𝑖}\left({L}\right){b}$
49 47 48 fveq12d ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {\left({a}{\cdot }_{𝑖}\left({K}\right){b}\right)}^{{*}_{\mathrm{Scalar}\left({K}\right)}}={\left({a}{\cdot }_{𝑖}\left({L}\right){b}\right)}^{{*}_{\mathrm{Scalar}\left({L}\right)}}$
50 49 anassrs ${⊢}\left(\left({\phi }\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\to {\left({a}{\cdot }_{𝑖}\left({K}\right){b}\right)}^{{*}_{\mathrm{Scalar}\left({K}\right)}}={\left({a}{\cdot }_{𝑖}\left({L}\right){b}\right)}^{{*}_{\mathrm{Scalar}\left({L}\right)}}$
51 50 13 eqeq12d ${⊢}\left(\left({\phi }\wedge {a}\in {B}\right)\wedge {b}\in {B}\right)\to \left({\left({a}{\cdot }_{𝑖}\left({K}\right){b}\right)}^{{*}_{\mathrm{Scalar}\left({K}\right)}}={b}{\cdot }_{𝑖}\left({K}\right){a}↔{\left({a}{\cdot }_{𝑖}\left({L}\right){b}\right)}^{{*}_{\mathrm{Scalar}\left({L}\right)}}={b}{\cdot }_{𝑖}\left({L}\right){a}\right)$
52 51 ralbidva ${⊢}\left({\phi }\wedge {a}\in {B}\right)\to \left(\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}{\left({a}{\cdot }_{𝑖}\left({K}\right){b}\right)}^{{*}_{\mathrm{Scalar}\left({K}\right)}}={b}{\cdot }_{𝑖}\left({K}\right){a}↔\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}{\left({a}{\cdot }_{𝑖}\left({L}\right){b}\right)}^{{*}_{\mathrm{Scalar}\left({L}\right)}}={b}{\cdot }_{𝑖}\left({L}\right){a}\right)$
53 15 raleqdv ${⊢}\left({\phi }\wedge {a}\in {B}\right)\to \left(\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}{\left({a}{\cdot }_{𝑖}\left({K}\right){b}\right)}^{{*}_{\mathrm{Scalar}\left({K}\right)}}={b}{\cdot }_{𝑖}\left({K}\right){a}↔\forall {b}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}{\left({a}{\cdot }_{𝑖}\left({K}\right){b}\right)}^{{*}_{\mathrm{Scalar}\left({K}\right)}}={b}{\cdot }_{𝑖}\left({K}\right){a}\right)$
54 17 raleqdv ${⊢}\left({\phi }\wedge {a}\in {B}\right)\to \left(\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}{\left({a}{\cdot }_{𝑖}\left({L}\right){b}\right)}^{{*}_{\mathrm{Scalar}\left({L}\right)}}={b}{\cdot }_{𝑖}\left({L}\right){a}↔\forall {b}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}{\left({a}{\cdot }_{𝑖}\left({L}\right){b}\right)}^{{*}_{\mathrm{Scalar}\left({L}\right)}}={b}{\cdot }_{𝑖}\left({L}\right){a}\right)$
55 52 53 54 3bitr3d ${⊢}\left({\phi }\wedge {a}\in {B}\right)\to \left(\forall {b}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}{\left({a}{\cdot }_{𝑖}\left({K}\right){b}\right)}^{{*}_{\mathrm{Scalar}\left({K}\right)}}={b}{\cdot }_{𝑖}\left({K}\right){a}↔\forall {b}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}{\left({a}{\cdot }_{𝑖}\left({L}\right){b}\right)}^{{*}_{\mathrm{Scalar}\left({L}\right)}}={b}{\cdot }_{𝑖}\left({L}\right){a}\right)$
56 36 45 55 3anbi123d ${⊢}\left({\phi }\wedge {a}\in {B}\right)\to \left(\left(\left({b}\in {\mathrm{Base}}_{{K}}⟼{b}{\cdot }_{𝑖}\left({K}\right){a}\right)\in \left({K}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({K}\right)\right)\right)\wedge \left({a}{\cdot }_{𝑖}\left({K}\right){a}={0}_{\mathrm{Scalar}\left({K}\right)}\to {a}={0}_{{K}}\right)\wedge \forall {b}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}{\left({a}{\cdot }_{𝑖}\left({K}\right){b}\right)}^{{*}_{\mathrm{Scalar}\left({K}\right)}}={b}{\cdot }_{𝑖}\left({K}\right){a}\right)↔\left(\left({b}\in {\mathrm{Base}}_{{L}}⟼{b}{\cdot }_{𝑖}\left({L}\right){a}\right)\in \left({L}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({L}\right)\right)\right)\wedge \left({a}{\cdot }_{𝑖}\left({L}\right){a}={0}_{\mathrm{Scalar}\left({L}\right)}\to {a}={0}_{{L}}\right)\wedge \forall {b}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}{\left({a}{\cdot }_{𝑖}\left({L}\right){b}\right)}^{{*}_{\mathrm{Scalar}\left({L}\right)}}={b}{\cdot }_{𝑖}\left({L}\right){a}\right)\right)$
57 56 ralbidva ${⊢}{\phi }\to \left(\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({b}\in {\mathrm{Base}}_{{K}}⟼{b}{\cdot }_{𝑖}\left({K}\right){a}\right)\in \left({K}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({K}\right)\right)\right)\wedge \left({a}{\cdot }_{𝑖}\left({K}\right){a}={0}_{\mathrm{Scalar}\left({K}\right)}\to {a}={0}_{{K}}\right)\wedge \forall {b}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}{\left({a}{\cdot }_{𝑖}\left({K}\right){b}\right)}^{{*}_{\mathrm{Scalar}\left({K}\right)}}={b}{\cdot }_{𝑖}\left({K}\right){a}\right)↔\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({b}\in {\mathrm{Base}}_{{L}}⟼{b}{\cdot }_{𝑖}\left({L}\right){a}\right)\in \left({L}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({L}\right)\right)\right)\wedge \left({a}{\cdot }_{𝑖}\left({L}\right){a}={0}_{\mathrm{Scalar}\left({L}\right)}\to {a}={0}_{{L}}\right)\wedge \forall {b}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}{\left({a}{\cdot }_{𝑖}\left({L}\right){b}\right)}^{{*}_{\mathrm{Scalar}\left({L}\right)}}={b}{\cdot }_{𝑖}\left({L}\right){a}\right)\right)$
58 1 raleqdv ${⊢}{\phi }\to \left(\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({b}\in {\mathrm{Base}}_{{K}}⟼{b}{\cdot }_{𝑖}\left({K}\right){a}\right)\in \left({K}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({K}\right)\right)\right)\wedge \left({a}{\cdot }_{𝑖}\left({K}\right){a}={0}_{\mathrm{Scalar}\left({K}\right)}\to {a}={0}_{{K}}\right)\wedge \forall {b}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}{\left({a}{\cdot }_{𝑖}\left({K}\right){b}\right)}^{{*}_{\mathrm{Scalar}\left({K}\right)}}={b}{\cdot }_{𝑖}\left({K}\right){a}\right)↔\forall {a}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left(\left({b}\in {\mathrm{Base}}_{{K}}⟼{b}{\cdot }_{𝑖}\left({K}\right){a}\right)\in \left({K}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({K}\right)\right)\right)\wedge \left({a}{\cdot }_{𝑖}\left({K}\right){a}={0}_{\mathrm{Scalar}\left({K}\right)}\to {a}={0}_{{K}}\right)\wedge \forall {b}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}{\left({a}{\cdot }_{𝑖}\left({K}\right){b}\right)}^{{*}_{\mathrm{Scalar}\left({K}\right)}}={b}{\cdot }_{𝑖}\left({K}\right){a}\right)\right)$
59 2 raleqdv ${⊢}{\phi }\to \left(\forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({b}\in {\mathrm{Base}}_{{L}}⟼{b}{\cdot }_{𝑖}\left({L}\right){a}\right)\in \left({L}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({L}\right)\right)\right)\wedge \left({a}{\cdot }_{𝑖}\left({L}\right){a}={0}_{\mathrm{Scalar}\left({L}\right)}\to {a}={0}_{{L}}\right)\wedge \forall {b}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}{\left({a}{\cdot }_{𝑖}\left({L}\right){b}\right)}^{{*}_{\mathrm{Scalar}\left({L}\right)}}={b}{\cdot }_{𝑖}\left({L}\right){a}\right)↔\forall {a}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\left(\left({b}\in {\mathrm{Base}}_{{L}}⟼{b}{\cdot }_{𝑖}\left({L}\right){a}\right)\in \left({L}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({L}\right)\right)\right)\wedge \left({a}{\cdot }_{𝑖}\left({L}\right){a}={0}_{\mathrm{Scalar}\left({L}\right)}\to {a}={0}_{{L}}\right)\wedge \forall {b}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}{\left({a}{\cdot }_{𝑖}\left({L}\right){b}\right)}^{{*}_{\mathrm{Scalar}\left({L}\right)}}={b}{\cdot }_{𝑖}\left({L}\right){a}\right)\right)$
60 57 58 59 3bitr3d ${⊢}{\phi }\to \left(\forall {a}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left(\left({b}\in {\mathrm{Base}}_{{K}}⟼{b}{\cdot }_{𝑖}\left({K}\right){a}\right)\in \left({K}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({K}\right)\right)\right)\wedge \left({a}{\cdot }_{𝑖}\left({K}\right){a}={0}_{\mathrm{Scalar}\left({K}\right)}\to {a}={0}_{{K}}\right)\wedge \forall {b}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}{\left({a}{\cdot }_{𝑖}\left({K}\right){b}\right)}^{{*}_{\mathrm{Scalar}\left({K}\right)}}={b}{\cdot }_{𝑖}\left({K}\right){a}\right)↔\forall {a}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\left(\left({b}\in {\mathrm{Base}}_{{L}}⟼{b}{\cdot }_{𝑖}\left({L}\right){a}\right)\in \left({L}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({L}\right)\right)\right)\wedge \left({a}{\cdot }_{𝑖}\left({L}\right){a}={0}_{\mathrm{Scalar}\left({L}\right)}\to {a}={0}_{{L}}\right)\wedge \forall {b}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}{\left({a}{\cdot }_{𝑖}\left({L}\right){b}\right)}^{{*}_{\mathrm{Scalar}\left({L}\right)}}={b}{\cdot }_{𝑖}\left({L}\right){a}\right)\right)$
61 9 11 60 3anbi123d ${⊢}{\phi }\to \left(\left({K}\in \mathrm{LVec}\wedge \mathrm{Scalar}\left({K}\right)\in \mathrm{*-Ring}\wedge \forall {a}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left(\left({b}\in {\mathrm{Base}}_{{K}}⟼{b}{\cdot }_{𝑖}\left({K}\right){a}\right)\in \left({K}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({K}\right)\right)\right)\wedge \left({a}{\cdot }_{𝑖}\left({K}\right){a}={0}_{\mathrm{Scalar}\left({K}\right)}\to {a}={0}_{{K}}\right)\wedge \forall {b}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}{\left({a}{\cdot }_{𝑖}\left({K}\right){b}\right)}^{{*}_{\mathrm{Scalar}\left({K}\right)}}={b}{\cdot }_{𝑖}\left({K}\right){a}\right)\right)↔\left({L}\in \mathrm{LVec}\wedge \mathrm{Scalar}\left({L}\right)\in \mathrm{*-Ring}\wedge \forall {a}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\left(\left({b}\in {\mathrm{Base}}_{{L}}⟼{b}{\cdot }_{𝑖}\left({L}\right){a}\right)\in \left({L}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({L}\right)\right)\right)\wedge \left({a}{\cdot }_{𝑖}\left({L}\right){a}={0}_{\mathrm{Scalar}\left({L}\right)}\to {a}={0}_{{L}}\right)\wedge \forall {b}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}{\left({a}{\cdot }_{𝑖}\left({L}\right){b}\right)}^{{*}_{\mathrm{Scalar}\left({L}\right)}}={b}{\cdot }_{𝑖}\left({L}\right){a}\right)\right)\right)$
62 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
63 eqid ${⊢}\mathrm{Scalar}\left({K}\right)=\mathrm{Scalar}\left({K}\right)$
64 eqid ${⊢}{\cdot }_{𝑖}\left({K}\right)={\cdot }_{𝑖}\left({K}\right)$
65 eqid ${⊢}{0}_{{K}}={0}_{{K}}$
66 eqid ${⊢}{*}_{\mathrm{Scalar}\left({K}\right)}={*}_{\mathrm{Scalar}\left({K}\right)}$
67 eqid ${⊢}{0}_{\mathrm{Scalar}\left({K}\right)}={0}_{\mathrm{Scalar}\left({K}\right)}$
68 62 63 64 65 66 67 isphl ${⊢}{K}\in \mathrm{PreHil}↔\left({K}\in \mathrm{LVec}\wedge \mathrm{Scalar}\left({K}\right)\in \mathrm{*-Ring}\wedge \forall {a}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left(\left({b}\in {\mathrm{Base}}_{{K}}⟼{b}{\cdot }_{𝑖}\left({K}\right){a}\right)\in \left({K}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({K}\right)\right)\right)\wedge \left({a}{\cdot }_{𝑖}\left({K}\right){a}={0}_{\mathrm{Scalar}\left({K}\right)}\to {a}={0}_{{K}}\right)\wedge \forall {b}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}{\left({a}{\cdot }_{𝑖}\left({K}\right){b}\right)}^{{*}_{\mathrm{Scalar}\left({K}\right)}}={b}{\cdot }_{𝑖}\left({K}\right){a}\right)\right)$
69 eqid ${⊢}{\mathrm{Base}}_{{L}}={\mathrm{Base}}_{{L}}$
70 eqid ${⊢}\mathrm{Scalar}\left({L}\right)=\mathrm{Scalar}\left({L}\right)$
71 eqid ${⊢}{\cdot }_{𝑖}\left({L}\right)={\cdot }_{𝑖}\left({L}\right)$
72 eqid ${⊢}{0}_{{L}}={0}_{{L}}$
73 eqid ${⊢}{*}_{\mathrm{Scalar}\left({L}\right)}={*}_{\mathrm{Scalar}\left({L}\right)}$
74 eqid ${⊢}{0}_{\mathrm{Scalar}\left({L}\right)}={0}_{\mathrm{Scalar}\left({L}\right)}$
75 69 70 71 72 73 74 isphl ${⊢}{L}\in \mathrm{PreHil}↔\left({L}\in \mathrm{LVec}\wedge \mathrm{Scalar}\left({L}\right)\in \mathrm{*-Ring}\wedge \forall {a}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\left(\left({b}\in {\mathrm{Base}}_{{L}}⟼{b}{\cdot }_{𝑖}\left({L}\right){a}\right)\in \left({L}\mathrm{LMHom}\mathrm{ringLMod}\left(\mathrm{Scalar}\left({L}\right)\right)\right)\wedge \left({a}{\cdot }_{𝑖}\left({L}\right){a}={0}_{\mathrm{Scalar}\left({L}\right)}\to {a}={0}_{{L}}\right)\wedge \forall {b}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}{\left({a}{\cdot }_{𝑖}\left({L}\right){b}\right)}^{{*}_{\mathrm{Scalar}\left({L}\right)}}={b}{\cdot }_{𝑖}\left({L}\right){a}\right)\right)$
76 61 68 75 3bitr4g ${⊢}{\phi }\to \left({K}\in \mathrm{PreHil}↔{L}\in \mathrm{PreHil}\right)$