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 ⊢φ→B=BaseK
phlpropd.2 ⊢φ→B=BaseL
phlpropd.3 ⊢φ∧x∈B∧y∈B→x+Ky=x+Ly
phlpropd.4 ⊢φ→F=Scalar⁡K
phlpropd.5 ⊢φ→F=Scalar⁡L
phlpropd.6 ⊢P=BaseF
phlpropd.7 ⊢φ∧x∈P∧y∈B→x⋅Ky=x⋅Ly
phlpropd.8 ⊢φ∧x∈B∧y∈B→x⋅𝑖⁡Ky=x⋅𝑖⁡Ly
Assertion phlpropd ⊢φ→K∈PreHil↔L∈PreHil

Proof

Step Hyp Ref Expression
1 phlpropd.1 ⊢φ→B=BaseK
2 phlpropd.2 ⊢φ→B=BaseL
3 phlpropd.3 ⊢φ∧x∈B∧y∈B→x+Ky=x+Ly
4 phlpropd.4 ⊢φ→F=Scalar⁡K
5 phlpropd.5 ⊢φ→F=Scalar⁡L
6 phlpropd.6 ⊢P=BaseF
7 phlpropd.7 ⊢φ∧x∈P∧y∈B→x⋅Ky=x⋅Ly
8 phlpropd.8 ⊢φ∧x∈B∧y∈B→x⋅𝑖⁡Ky=x⋅𝑖⁡Ly
9 1 2 3 4 5 6 7 lvecpropd ⊢φ→K∈LVec↔L∈LVec
10 4 5 eqtr3d ⊢φ→Scalar⁡K=Scalar⁡L
11 10 eleq1d ⊢φ→Scalar⁡K∈*-Ring↔Scalar⁡L∈*-Ring
12 8 oveqrspc2v ⊢φ∧b∈B∧a∈B→b⋅𝑖⁡Ka=b⋅𝑖⁡La
13 12 anass1rs ⊢φ∧a∈B∧b∈B→b⋅𝑖⁡Ka=b⋅𝑖⁡La
14 13 mpteq2dva ⊢φ∧a∈B→b∈B⟼b⋅𝑖⁡Ka=b∈B⟼b⋅𝑖⁡La
15 1 adantr ⊢φ∧a∈B→B=BaseK
16 15 mpteq1d ⊢φ∧a∈B→b∈B⟼b⋅𝑖⁡Ka=b∈BaseK⟼b⋅𝑖⁡Ka
17 2 adantr ⊢φ∧a∈B→B=BaseL
18 17 mpteq1d ⊢φ∧a∈B→b∈B⟼b⋅𝑖⁡La=b∈BaseL⟼b⋅𝑖⁡La
19 14 16 18 3eqtr3d ⊢φ∧a∈B→b∈BaseK⟼b⋅𝑖⁡Ka=b∈BaseL⟼b⋅𝑖⁡La
20 rlmbas ⊢BaseF=BaseringLMod⁡F
21 6 20 eqtri ⊢P=BaseringLMod⁡F
22 21 a1i ⊢φ→P=BaseringLMod⁡F
23 fvex ⊢Scalar⁡K∈V
24 4 23 eqeltrdi ⊢φ→F∈V
25 rlmsca ⊢F∈V→F=Scalar⁡ringLMod⁡F
26 24 25 syl ⊢φ→F=Scalar⁡ringLMod⁡F
27 eqidd ⊢φ∧x∈P∧y∈P→x+ringLMod⁡Fy=x+ringLMod⁡Fy
28 eqidd ⊢φ∧x∈P∧y∈P→x⋅ringLMod⁡Fy=x⋅ringLMod⁡Fy
29 1 22 2 22 4 26 5 26 6 6 3 27 7 28 lmhmpropd ⊢φ→KLMHomringLMod⁡F=LLMHomringLMod⁡F
30 4 fveq2d ⊢φ→ringLMod⁡F=ringLMod⁡Scalar⁡K
31 30 oveq2d ⊢φ→KLMHomringLMod⁡F=KLMHomringLMod⁡Scalar⁡K
32 5 fveq2d ⊢φ→ringLMod⁡F=ringLMod⁡Scalar⁡L
33 32 oveq2d ⊢φ→LLMHomringLMod⁡F=LLMHomringLMod⁡Scalar⁡L
34 29 31 33 3eqtr3d ⊢φ→KLMHomringLMod⁡Scalar⁡K=LLMHomringLMod⁡Scalar⁡L
35 34 adantr ⊢φ∧a∈B→KLMHomringLMod⁡Scalar⁡K=LLMHomringLMod⁡Scalar⁡L
36 19 35 eleq12d ⊢φ∧a∈B→b∈BaseK⟼b⋅𝑖⁡Ka∈KLMHomringLMod⁡Scalar⁡K↔b∈BaseL⟼b⋅𝑖⁡La∈LLMHomringLMod⁡Scalar⁡L
37 8 oveqrspc2v ⊢φ∧a∈B∧a∈B→a⋅𝑖⁡Ka=a⋅𝑖⁡La
38 37 anabsan2 ⊢φ∧a∈B→a⋅𝑖⁡Ka=a⋅𝑖⁡La
39 10 fveq2d ⊢φ→0Scalar⁡K=0Scalar⁡L
40 39 adantr ⊢φ∧a∈B→0Scalar⁡K=0Scalar⁡L
41 38 40 eqeq12d ⊢φ∧a∈B→a⋅𝑖⁡Ka=0Scalar⁡K↔a⋅𝑖⁡La=0Scalar⁡L
42 1 2 3 grpidpropd ⊢φ→0K=0L
43 42 adantr ⊢φ∧a∈B→0K=0L
44 43 eqeq2d ⊢φ∧a∈B→a=0K↔a=0L
45 41 44 imbi12d ⊢φ∧a∈B→a⋅𝑖⁡Ka=0Scalar⁡K→a=0K↔a⋅𝑖⁡La=0Scalar⁡L→a=0L
46 10 fveq2d ⊢φ→*Scalar⁡K=*Scalar⁡L
47 46 adantr ⊢φ∧a∈B∧b∈B→*Scalar⁡K=*Scalar⁡L
48 8 oveqrspc2v ⊢φ∧a∈B∧b∈B→a⋅𝑖⁡Kb=a⋅𝑖⁡Lb
49 47 48 fveq12d ⊢φ∧a∈B∧b∈B→a⋅𝑖⁡Kb*Scalar⁡K=a⋅𝑖⁡Lb*Scalar⁡L
50 49 anassrs ⊢φ∧a∈B∧b∈B→a⋅𝑖⁡Kb*Scalar⁡K=a⋅𝑖⁡Lb*Scalar⁡L
51 50 13 eqeq12d ⊢φ∧a∈B∧b∈B→a⋅𝑖⁡Kb*Scalar⁡K=b⋅𝑖⁡Ka↔a⋅𝑖⁡Lb*Scalar⁡L=b⋅𝑖⁡La
52 51 ralbidva ⊢φ∧a∈B→∀b∈Ba⋅𝑖⁡Kb*Scalar⁡K=b⋅𝑖⁡Ka↔∀b∈Ba⋅𝑖⁡Lb*Scalar⁡L=b⋅𝑖⁡La
53 15 raleqdv ⊢φ∧a∈B→∀b∈Ba⋅𝑖⁡Kb*Scalar⁡K=b⋅𝑖⁡Ka↔∀b∈BaseKa⋅𝑖⁡Kb*Scalar⁡K=b⋅𝑖⁡Ka
54 17 raleqdv ⊢φ∧a∈B→∀b∈Ba⋅𝑖⁡Lb*Scalar⁡L=b⋅𝑖⁡La↔∀b∈BaseLa⋅𝑖⁡Lb*Scalar⁡L=b⋅𝑖⁡La
55 52 53 54 3bitr3d ⊢φ∧a∈B→∀b∈BaseKa⋅𝑖⁡Kb*Scalar⁡K=b⋅𝑖⁡Ka↔∀b∈BaseLa⋅𝑖⁡Lb*Scalar⁡L=b⋅𝑖⁡La
56 36 45 55 3anbi123d ⊢φ∧a∈B→b∈BaseK⟼b⋅𝑖⁡Ka∈KLMHomringLMod⁡Scalar⁡K∧a⋅𝑖⁡Ka=0Scalar⁡K→a=0K∧∀b∈BaseKa⋅𝑖⁡Kb*Scalar⁡K=b⋅𝑖⁡Ka↔b∈BaseL⟼b⋅𝑖⁡La∈LLMHomringLMod⁡Scalar⁡L∧a⋅𝑖⁡La=0Scalar⁡L→a=0L∧∀b∈BaseLa⋅𝑖⁡Lb*Scalar⁡L=b⋅𝑖⁡La
57 56 ralbidva ⊢φ→∀a∈Bb∈BaseK⟼b⋅𝑖⁡Ka∈KLMHomringLMod⁡Scalar⁡K∧a⋅𝑖⁡Ka=0Scalar⁡K→a=0K∧∀b∈BaseKa⋅𝑖⁡Kb*Scalar⁡K=b⋅𝑖⁡Ka↔∀a∈Bb∈BaseL⟼b⋅𝑖⁡La∈LLMHomringLMod⁡Scalar⁡L∧a⋅𝑖⁡La=0Scalar⁡L→a=0L∧∀b∈BaseLa⋅𝑖⁡Lb*Scalar⁡L=b⋅𝑖⁡La
58 1 raleqdv ⊢φ→∀a∈Bb∈BaseK⟼b⋅𝑖⁡Ka∈KLMHomringLMod⁡Scalar⁡K∧a⋅𝑖⁡Ka=0Scalar⁡K→a=0K∧∀b∈BaseKa⋅𝑖⁡Kb*Scalar⁡K=b⋅𝑖⁡Ka↔∀a∈BaseKb∈BaseK⟼b⋅𝑖⁡Ka∈KLMHomringLMod⁡Scalar⁡K∧a⋅𝑖⁡Ka=0Scalar⁡K→a=0K∧∀b∈BaseKa⋅𝑖⁡Kb*Scalar⁡K=b⋅𝑖⁡Ka
59 2 raleqdv ⊢φ→∀a∈Bb∈BaseL⟼b⋅𝑖⁡La∈LLMHomringLMod⁡Scalar⁡L∧a⋅𝑖⁡La=0Scalar⁡L→a=0L∧∀b∈BaseLa⋅𝑖⁡Lb*Scalar⁡L=b⋅𝑖⁡La↔∀a∈BaseLb∈BaseL⟼b⋅𝑖⁡La∈LLMHomringLMod⁡Scalar⁡L∧a⋅𝑖⁡La=0Scalar⁡L→a=0L∧∀b∈BaseLa⋅𝑖⁡Lb*Scalar⁡L=b⋅𝑖⁡La
60 57 58 59 3bitr3d ⊢φ→∀a∈BaseKb∈BaseK⟼b⋅𝑖⁡Ka∈KLMHomringLMod⁡Scalar⁡K∧a⋅𝑖⁡Ka=0Scalar⁡K→a=0K∧∀b∈BaseKa⋅𝑖⁡Kb*Scalar⁡K=b⋅𝑖⁡Ka↔∀a∈BaseLb∈BaseL⟼b⋅𝑖⁡La∈LLMHomringLMod⁡Scalar⁡L∧a⋅𝑖⁡La=0Scalar⁡L→a=0L∧∀b∈BaseLa⋅𝑖⁡Lb*Scalar⁡L=b⋅𝑖⁡La
61 9 11 60 3anbi123d ⊢φ→K∈LVec∧Scalar⁡K∈*-Ring∧∀a∈BaseKb∈BaseK⟼b⋅𝑖⁡Ka∈KLMHomringLMod⁡Scalar⁡K∧a⋅𝑖⁡Ka=0Scalar⁡K→a=0K∧∀b∈BaseKa⋅𝑖⁡Kb*Scalar⁡K=b⋅𝑖⁡Ka↔L∈LVec∧Scalar⁡L∈*-Ring∧∀a∈BaseLb∈BaseL⟼b⋅𝑖⁡La∈LLMHomringLMod⁡Scalar⁡L∧a⋅𝑖⁡La=0Scalar⁡L→a=0L∧∀b∈BaseLa⋅𝑖⁡Lb*Scalar⁡L=b⋅𝑖⁡La
62 eqid ⊢BaseK=BaseK
63 eqid ⊢Scalar⁡K=Scalar⁡K
64 eqid ⊢⋅𝑖⁡K=⋅𝑖⁡K
65 eqid ⊢0K=0K
66 eqid ⊢*Scalar⁡K=*Scalar⁡K
67 eqid ⊢0Scalar⁡K=0Scalar⁡K
68 62 63 64 65 66 67 isphl ⊢K∈PreHil↔K∈LVec∧Scalar⁡K∈*-Ring∧∀a∈BaseKb∈BaseK⟼b⋅𝑖⁡Ka∈KLMHomringLMod⁡Scalar⁡K∧a⋅𝑖⁡Ka=0Scalar⁡K→a=0K∧∀b∈BaseKa⋅𝑖⁡Kb*Scalar⁡K=b⋅𝑖⁡Ka
69 eqid ⊢BaseL=BaseL
70 eqid ⊢Scalar⁡L=Scalar⁡L
71 eqid ⊢⋅𝑖⁡L=⋅𝑖⁡L
72 eqid ⊢0L=0L
73 eqid ⊢*Scalar⁡L=*Scalar⁡L
74 eqid ⊢0Scalar⁡L=0Scalar⁡L
75 69 70 71 72 73 74 isphl ⊢L∈PreHil↔L∈LVec∧Scalar⁡L∈*-Ring∧∀a∈BaseLb∈BaseL⟼b⋅𝑖⁡La∈LLMHomringLMod⁡Scalar⁡L∧a⋅𝑖⁡La=0Scalar⁡L→a=0L∧∀b∈BaseLa⋅𝑖⁡Lb*Scalar⁡L=b⋅𝑖⁡La
76 61 68 75 3bitr4g ⊢φ→K∈PreHil↔L∈PreHil