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

Proof

Step Hyp Ref Expression
1 phlpropd.1 ⊢ φ → B = Base K
2 phlpropd.2 ⊢ φ → B = Base L
3 phlpropd.3 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x + K y = x + L y
4 phlpropd.4 ⊢ φ → F = Scalar ⁡ K
5 phlpropd.5 ⊢ φ → F = Scalar ⁡ L
6 phlpropd.6 ⊢ P = Base F
7 phlpropd.7 ⊢ φ ∧ x ∈ P ∧ y ∈ B → x ⋅ K y = x ⋅ L y
8 phlpropd.8 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x ⋅ 𝑖 ⁡ K y = x ⋅ 𝑖 ⁡ L y
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 ⋅ 𝑖 ⁡ K a = b ⋅ 𝑖 ⁡ L a
13 12 anass1rs ⊢ φ ∧ a ∈ B ∧ b ∈ B → b ⋅ 𝑖 ⁡ K a = b ⋅ 𝑖 ⁡ L a
14 13 mpteq2dva ⊢ φ ∧ a ∈ B → b ∈ B ⟼ b ⋅ 𝑖 ⁡ K a = b ∈ B ⟼ b ⋅ 𝑖 ⁡ L a
15 1 adantr ⊢ φ ∧ a ∈ B → B = Base K
16 15 mpteq1d ⊢ φ ∧ a ∈ B → b ∈ B ⟼ b ⋅ 𝑖 ⁡ K a = b ∈ Base K ⟼ b ⋅ 𝑖 ⁡ K a
17 2 adantr ⊢ φ ∧ a ∈ B → B = Base L
18 17 mpteq1d ⊢ φ ∧ a ∈ B → b ∈ B ⟼ b ⋅ 𝑖 ⁡ L a = b ∈ Base L ⟼ b ⋅ 𝑖 ⁡ L a
19 14 16 18 3eqtr3d ⊢ φ ∧ a ∈ B → b ∈ Base K ⟼ b ⋅ 𝑖 ⁡ K a = b ∈ Base L ⟼ b ⋅ 𝑖 ⁡ L a
20 rlmbas ⊢ Base F = Base ringLMod ⁡ F
21 6 20 eqtri ⊢ P = Base ringLMod ⁡ F
22 21 a1i ⊢ φ → P = Base ringLMod ⁡ 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 ⁡ F y = x + ringLMod ⁡ F y
28 eqidd ⊢ φ ∧ x ∈ P ∧ y ∈ P → x ⋅ ringLMod ⁡ F y = x ⋅ ringLMod ⁡ F y
29 1 22 2 22 4 26 5 26 6 6 3 27 7 28 lmhmpropd ⊢ φ → K LMHom ringLMod ⁡ F = L LMHom ringLMod ⁡ F
30 4 fveq2d ⊢ φ → ringLMod ⁡ F = ringLMod ⁡ Scalar ⁡ K
31 30 oveq2d ⊢ φ → K LMHom ringLMod ⁡ F = K LMHom ringLMod ⁡ Scalar ⁡ K
32 5 fveq2d ⊢ φ → ringLMod ⁡ F = ringLMod ⁡ Scalar ⁡ L
33 32 oveq2d ⊢ φ → L LMHom ringLMod ⁡ F = L LMHom ringLMod ⁡ Scalar ⁡ L
34 29 31 33 3eqtr3d ⊢ φ → K LMHom ringLMod ⁡ Scalar ⁡ K = L LMHom ringLMod ⁡ Scalar ⁡ L
35 34 adantr ⊢ φ ∧ a ∈ B → K LMHom ringLMod ⁡ Scalar ⁡ K = L LMHom ringLMod ⁡ Scalar ⁡ L
36 19 35 eleq12d ⊢ φ ∧ a ∈ B → b ∈ Base K ⟼ b ⋅ 𝑖 ⁡ K a ∈ K LMHom ringLMod ⁡ Scalar ⁡ K ↔ b ∈ Base L ⟼ b ⋅ 𝑖 ⁡ L a ∈ L LMHom ringLMod ⁡ Scalar ⁡ L
37 8 oveqrspc2v ⊢ φ ∧ a ∈ B ∧ a ∈ B → a ⋅ 𝑖 ⁡ K a = a ⋅ 𝑖 ⁡ L a
38 37 anabsan2 ⊢ φ ∧ a ∈ B → a ⋅ 𝑖 ⁡ K a = a ⋅ 𝑖 ⁡ L a
39 10 fveq2d ⊢ φ → 0 Scalar ⁡ K = 0 Scalar ⁡ L
40 39 adantr ⊢ φ ∧ a ∈ B → 0 Scalar ⁡ K = 0 Scalar ⁡ L
41 38 40 eqeq12d ⊢ φ ∧ a ∈ B → a ⋅ 𝑖 ⁡ K a = 0 Scalar ⁡ K ↔ a ⋅ 𝑖 ⁡ L a = 0 Scalar ⁡ L
42 1 2 3 grpidpropd ⊢ φ → 0 K = 0 L
43 42 adantr ⊢ φ ∧ a ∈ B → 0 K = 0 L
44 43 eqeq2d ⊢ φ ∧ a ∈ B → a = 0 K ↔ a = 0 L
45 41 44 imbi12d ⊢ φ ∧ a ∈ B → a ⋅ 𝑖 ⁡ K a = 0 Scalar ⁡ K → a = 0 K ↔ a ⋅ 𝑖 ⁡ L a = 0 Scalar ⁡ L → a = 0 L
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 ⋅ 𝑖 ⁡ K b = a ⋅ 𝑖 ⁡ L b
49 47 48 fveq12d ⊢ φ ∧ a ∈ B ∧ b ∈ B → a ⋅ 𝑖 ⁡ K b * Scalar ⁡ K = a ⋅ 𝑖 ⁡ L b * Scalar ⁡ L
50 49 anassrs ⊢ φ ∧ a ∈ B ∧ b ∈ B → a ⋅ 𝑖 ⁡ K b * Scalar ⁡ K = a ⋅ 𝑖 ⁡ L b * Scalar ⁡ L
51 50 13 eqeq12d ⊢ φ ∧ a ∈ B ∧ b ∈ B → a ⋅ 𝑖 ⁡ K b * Scalar ⁡ K = b ⋅ 𝑖 ⁡ K a ↔ a ⋅ 𝑖 ⁡ L b * Scalar ⁡ L = b ⋅ 𝑖 ⁡ L a
52 51 ralbidva ⊢ φ ∧ a ∈ B → ∀ b ∈ B a ⋅ 𝑖 ⁡ K b * Scalar ⁡ K = b ⋅ 𝑖 ⁡ K a ↔ ∀ b ∈ B a ⋅ 𝑖 ⁡ L b * Scalar ⁡ L = b ⋅ 𝑖 ⁡ L a
53 15 raleqdv ⊢ φ ∧ a ∈ B → ∀ b ∈ B a ⋅ 𝑖 ⁡ K b * Scalar ⁡ K = b ⋅ 𝑖 ⁡ K a ↔ ∀ b ∈ Base K a ⋅ 𝑖 ⁡ K b * Scalar ⁡ K = b ⋅ 𝑖 ⁡ K a
54 17 raleqdv ⊢ φ ∧ a ∈ B → ∀ b ∈ B a ⋅ 𝑖 ⁡ L b * Scalar ⁡ L = b ⋅ 𝑖 ⁡ L a ↔ ∀ b ∈ Base L a ⋅ 𝑖 ⁡ L b * Scalar ⁡ L = b ⋅ 𝑖 ⁡ L a
55 52 53 54 3bitr3d ⊢ φ ∧ a ∈ B → ∀ b ∈ Base K a ⋅ 𝑖 ⁡ K b * Scalar ⁡ K = b ⋅ 𝑖 ⁡ K a ↔ ∀ b ∈ Base L a ⋅ 𝑖 ⁡ L b * Scalar ⁡ L = b ⋅ 𝑖 ⁡ L a
56 36 45 55 3anbi123d ⊢ φ ∧ a ∈ B → b ∈ Base K ⟼ b ⋅ 𝑖 ⁡ K a ∈ K LMHom ringLMod ⁡ Scalar ⁡ K ∧ a ⋅ 𝑖 ⁡ K a = 0 Scalar ⁡ K → a = 0 K ∧ ∀ b ∈ Base K a ⋅ 𝑖 ⁡ K b * Scalar ⁡ K = b ⋅ 𝑖 ⁡ K a ↔ b ∈ Base L ⟼ b ⋅ 𝑖 ⁡ L a ∈ L LMHom ringLMod ⁡ Scalar ⁡ L ∧ a ⋅ 𝑖 ⁡ L a = 0 Scalar ⁡ L → a = 0 L ∧ ∀ b ∈ Base L a ⋅ 𝑖 ⁡ L b * Scalar ⁡ L = b ⋅ 𝑖 ⁡ L a
57 56 ralbidva ⊢ φ → ∀ a ∈ B b ∈ Base K ⟼ b ⋅ 𝑖 ⁡ K a ∈ K LMHom ringLMod ⁡ Scalar ⁡ K ∧ a ⋅ 𝑖 ⁡ K a = 0 Scalar ⁡ K → a = 0 K ∧ ∀ b ∈ Base K a ⋅ 𝑖 ⁡ K b * Scalar ⁡ K = b ⋅ 𝑖 ⁡ K a ↔ ∀ a ∈ B b ∈ Base L ⟼ b ⋅ 𝑖 ⁡ L a ∈ L LMHom ringLMod ⁡ Scalar ⁡ L ∧ a ⋅ 𝑖 ⁡ L a = 0 Scalar ⁡ L → a = 0 L ∧ ∀ b ∈ Base L a ⋅ 𝑖 ⁡ L b * Scalar ⁡ L = b ⋅ 𝑖 ⁡ L a
58 1 raleqdv ⊢ φ → ∀ a ∈ B b ∈ Base K ⟼ b ⋅ 𝑖 ⁡ K a ∈ K LMHom ringLMod ⁡ Scalar ⁡ K ∧ a ⋅ 𝑖 ⁡ K a = 0 Scalar ⁡ K → a = 0 K ∧ ∀ b ∈ Base K a ⋅ 𝑖 ⁡ K b * Scalar ⁡ K = b ⋅ 𝑖 ⁡ K a ↔ ∀ a ∈ Base K b ∈ Base K ⟼ b ⋅ 𝑖 ⁡ K a ∈ K LMHom ringLMod ⁡ Scalar ⁡ K ∧ a ⋅ 𝑖 ⁡ K a = 0 Scalar ⁡ K → a = 0 K ∧ ∀ b ∈ Base K a ⋅ 𝑖 ⁡ K b * Scalar ⁡ K = b ⋅ 𝑖 ⁡ K a
59 2 raleqdv ⊢ φ → ∀ a ∈ B b ∈ Base L ⟼ b ⋅ 𝑖 ⁡ L a ∈ L LMHom ringLMod ⁡ Scalar ⁡ L ∧ a ⋅ 𝑖 ⁡ L a = 0 Scalar ⁡ L → a = 0 L ∧ ∀ b ∈ Base L a ⋅ 𝑖 ⁡ L b * Scalar ⁡ L = b ⋅ 𝑖 ⁡ L a ↔ ∀ a ∈ Base L b ∈ Base L ⟼ b ⋅ 𝑖 ⁡ L a ∈ L LMHom ringLMod ⁡ Scalar ⁡ L ∧ a ⋅ 𝑖 ⁡ L a = 0 Scalar ⁡ L → a = 0 L ∧ ∀ b ∈ Base L a ⋅ 𝑖 ⁡ L b * Scalar ⁡ L = b ⋅ 𝑖 ⁡ L a
60 57 58 59 3bitr3d ⊢ φ → ∀ a ∈ Base K b ∈ Base K ⟼ b ⋅ 𝑖 ⁡ K a ∈ K LMHom ringLMod ⁡ Scalar ⁡ K ∧ a ⋅ 𝑖 ⁡ K a = 0 Scalar ⁡ K → a = 0 K ∧ ∀ b ∈ Base K a ⋅ 𝑖 ⁡ K b * Scalar ⁡ K = b ⋅ 𝑖 ⁡ K a ↔ ∀ a ∈ Base L b ∈ Base L ⟼ b ⋅ 𝑖 ⁡ L a ∈ L LMHom ringLMod ⁡ Scalar ⁡ L ∧ a ⋅ 𝑖 ⁡ L a = 0 Scalar ⁡ L → a = 0 L ∧ ∀ b ∈ Base L a ⋅ 𝑖 ⁡ L b * Scalar ⁡ L = b ⋅ 𝑖 ⁡ L a
61 9 11 60 3anbi123d ⊢ φ → K ∈ LVec ∧ Scalar ⁡ K ∈ *-Ring ∧ ∀ a ∈ Base K b ∈ Base K ⟼ b ⋅ 𝑖 ⁡ K a ∈ K LMHom ringLMod ⁡ Scalar ⁡ K ∧ a ⋅ 𝑖 ⁡ K a = 0 Scalar ⁡ K → a = 0 K ∧ ∀ b ∈ Base K a ⋅ 𝑖 ⁡ K b * Scalar ⁡ K = b ⋅ 𝑖 ⁡ K a ↔ L ∈ LVec ∧ Scalar ⁡ L ∈ *-Ring ∧ ∀ a ∈ Base L b ∈ Base L ⟼ b ⋅ 𝑖 ⁡ L a ∈ L LMHom ringLMod ⁡ Scalar ⁡ L ∧ a ⋅ 𝑖 ⁡ L a = 0 Scalar ⁡ L → a = 0 L ∧ ∀ b ∈ Base L a ⋅ 𝑖 ⁡ L b * Scalar ⁡ L = b ⋅ 𝑖 ⁡ L a
62 eqid ⊢ Base K = Base K
63 eqid ⊢ Scalar ⁡ K = Scalar ⁡ K
64 eqid ⊢ ⋅ 𝑖 ⁡ K = ⋅ 𝑖 ⁡ K
65 eqid ⊢ 0 K = 0 K
66 eqid ⊢ * Scalar ⁡ K = * Scalar ⁡ K
67 eqid ⊢ 0 Scalar ⁡ K = 0 Scalar ⁡ K
68 62 63 64 65 66 67 isphl ⊢ K ∈ PreHil ↔ K ∈ LVec ∧ Scalar ⁡ K ∈ *-Ring ∧ ∀ a ∈ Base K b ∈ Base K ⟼ b ⋅ 𝑖 ⁡ K a ∈ K LMHom ringLMod ⁡ Scalar ⁡ K ∧ a ⋅ 𝑖 ⁡ K a = 0 Scalar ⁡ K → a = 0 K ∧ ∀ b ∈ Base K a ⋅ 𝑖 ⁡ K b * Scalar ⁡ K = b ⋅ 𝑖 ⁡ K a
69 eqid ⊢ Base L = Base L
70 eqid ⊢ Scalar ⁡ L = Scalar ⁡ L
71 eqid ⊢ ⋅ 𝑖 ⁡ L = ⋅ 𝑖 ⁡ L
72 eqid ⊢ 0 L = 0 L
73 eqid ⊢ * Scalar ⁡ L = * Scalar ⁡ L
74 eqid ⊢ 0 Scalar ⁡ L = 0 Scalar ⁡ L
75 69 70 71 72 73 74 isphl ⊢ L ∈ PreHil ↔ L ∈ LVec ∧ Scalar ⁡ L ∈ *-Ring ∧ ∀ a ∈ Base L b ∈ Base L ⟼ b ⋅ 𝑖 ⁡ L a ∈ L LMHom ringLMod ⁡ Scalar ⁡ L ∧ a ⋅ 𝑖 ⁡ L a = 0 Scalar ⁡ L → a = 0 L ∧ ∀ b ∈ Base L a ⋅ 𝑖 ⁡ L b * Scalar ⁡ L = b ⋅ 𝑖 ⁡ L a
76 61 68 75 3bitr4g ⊢ φ → K ∈ PreHil ↔ L ∈ PreHil