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 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
phlpropd.2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
phlpropd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
phlpropd.4 ⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝐾 ) )
phlpropd.5 ⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝐿 ) )
phlpropd.6 ⊢ 𝑃 = ( Base ‘ 𝐹 )
phlpropd.7 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) )
phlpropd.8 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑖 ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑖 ‘ 𝐿 ) 𝑦 ) )
Assertion phlpropd ( 𝜑 → ( 𝐾 ∈ PreHil ↔ 𝐿 ∈ PreHil ) )

Proof

Step Hyp Ref Expression
1 phlpropd.1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2 phlpropd.2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
3 phlpropd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
4 phlpropd.4 ⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝐾 ) )
5 phlpropd.5 ⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝐿 ) )
6 phlpropd.6 ⊢ 𝑃 = ( Base ‘ 𝐹 )
7 phlpropd.7 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) )
8 phlpropd.8 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑖 ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑖 ‘ 𝐿 ) 𝑦 ) )
9 1 2 3 4 5 6 7 lvecpropd ⊢ ( 𝜑 → ( 𝐾 ∈ LVec ↔ 𝐿 ∈ LVec ) )
10 4 5 eqtr3d ⊢ ( 𝜑 → ( Scalar ‘ 𝐾 ) = ( Scalar ‘ 𝐿 ) )
11 10 eleq1d ⊢ ( 𝜑 → ( ( Scalar ‘ 𝐾 ) ∈ *-Ring ↔ ( Scalar ‘ 𝐿 ) ∈ *-Ring ) )
12 8 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ) → ( 𝑏 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) = ( 𝑏 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) )
13 12 anass1rs ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) = ( 𝑏 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) )
14 13 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝑏 ∈ 𝐵 ↦ ( 𝑏 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) ) = ( 𝑏 ∈ 𝐵 ↦ ( 𝑏 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) ) )
15 1 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝐵 = ( Base ‘ 𝐾 ) )
16 15 mpteq1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝑏 ∈ 𝐵 ↦ ( 𝑏 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) ) = ( 𝑏 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑏 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) ) )
17 2 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝐵 = ( Base ‘ 𝐿 ) )
18 17 mpteq1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝑏 ∈ 𝐵 ↦ ( 𝑏 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) ) = ( 𝑏 ∈ ( Base ‘ 𝐿 ) ↦ ( 𝑏 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) ) )
19 14 16 18 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝑏 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑏 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) ) = ( 𝑏 ∈ ( Base ‘ 𝐿 ) ↦ ( 𝑏 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) ) )
20 rlmbas ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ ( ringLMod ‘ 𝐹 ) )
21 6 20 eqtri ⊢ 𝑃 = ( Base ‘ ( ringLMod ‘ 𝐹 ) )
22 21 a1i ⊢ ( 𝜑 → 𝑃 = ( Base ‘ ( ringLMod ‘ 𝐹 ) ) )
23 fvex ⊢ ( Scalar ‘ 𝐾 ) ∈ V
24 4 23 eqeltrdi ⊢ ( 𝜑 → 𝐹 ∈ V )
25 rlmsca ⊢ ( 𝐹 ∈ V → 𝐹 = ( Scalar ‘ ( ringLMod ‘ 𝐹 ) ) )
26 24 25 syl ⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ ( ringLMod ‘ 𝐹 ) ) )
27 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( 𝑥 ( +g ‘ ( ringLMod ‘ 𝐹 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ ( ringLMod ‘ 𝐹 ) ) 𝑦 ) )
28 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( 𝑥 ( ·𝑠 ‘ ( ringLMod ‘ 𝐹 ) ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ ( ringLMod ‘ 𝐹 ) ) 𝑦 ) )
29 1 22 2 22 4 26 5 26 6 6 3 27 7 28 lmhmpropd ⊢ ( 𝜑 → ( 𝐾 LMHom ( ringLMod ‘ 𝐹 ) ) = ( 𝐿 LMHom ( ringLMod ‘ 𝐹 ) ) )
30 4 fveq2d ⊢ ( 𝜑 → ( ringLMod ‘ 𝐹 ) = ( ringLMod ‘ ( Scalar ‘ 𝐾 ) ) )
31 30 oveq2d ⊢ ( 𝜑 → ( 𝐾 LMHom ( ringLMod ‘ 𝐹 ) ) = ( 𝐾 LMHom ( ringLMod ‘ ( Scalar ‘ 𝐾 ) ) ) )
32 5 fveq2d ⊢ ( 𝜑 → ( ringLMod ‘ 𝐹 ) = ( ringLMod ‘ ( Scalar ‘ 𝐿 ) ) )
33 32 oveq2d ⊢ ( 𝜑 → ( 𝐿 LMHom ( ringLMod ‘ 𝐹 ) ) = ( 𝐿 LMHom ( ringLMod ‘ ( Scalar ‘ 𝐿 ) ) ) )
34 29 31 33 3eqtr3d ⊢ ( 𝜑 → ( 𝐾 LMHom ( ringLMod ‘ ( Scalar ‘ 𝐾 ) ) ) = ( 𝐿 LMHom ( ringLMod ‘ ( Scalar ‘ 𝐿 ) ) ) )
35 34 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝐾 LMHom ( ringLMod ‘ ( Scalar ‘ 𝐾 ) ) ) = ( 𝐿 LMHom ( ringLMod ‘ ( Scalar ‘ 𝐿 ) ) ) )
36 19 35 eleq12d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( 𝑏 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑏 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) ) ∈ ( 𝐾 LMHom ( ringLMod ‘ ( Scalar ‘ 𝐾 ) ) ) ↔ ( 𝑏 ∈ ( Base ‘ 𝐿 ) ↦ ( 𝑏 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) ) ∈ ( 𝐿 LMHom ( ringLMod ‘ ( Scalar ‘ 𝐿 ) ) ) ) )
37 8 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ) → ( 𝑎 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) = ( 𝑎 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) )
38 37 anabsan2 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝑎 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) = ( 𝑎 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) )
39 10 fveq2d ⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐾 ) ) = ( 0g ‘ ( Scalar ‘ 𝐿 ) ) )
40 39 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 0g ‘ ( Scalar ‘ 𝐾 ) ) = ( 0g ‘ ( Scalar ‘ 𝐿 ) ) )
41 38 40 eqeq12d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( 𝑎 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) = ( 0g ‘ ( Scalar ‘ 𝐾 ) ) ↔ ( 𝑎 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) = ( 0g ‘ ( Scalar ‘ 𝐿 ) ) ) )
42 1 2 3 grpidpropd ⊢ ( 𝜑 → ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐿 ) )
43 42 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐿 ) )
44 43 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝑎 = ( 0g ‘ 𝐾 ) ↔ 𝑎 = ( 0g ‘ 𝐿 ) ) )
45 41 44 imbi12d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( ( 𝑎 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) = ( 0g ‘ ( Scalar ‘ 𝐾 ) ) → 𝑎 = ( 0g ‘ 𝐾 ) ) ↔ ( ( 𝑎 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) = ( 0g ‘ ( Scalar ‘ 𝐿 ) ) → 𝑎 = ( 0g ‘ 𝐿 ) ) ) )
46 10 fveq2d ⊢ ( 𝜑 → ( *𝑟 ‘ ( Scalar ‘ 𝐾 ) ) = ( *𝑟 ‘ ( Scalar ‘ 𝐿 ) ) )
47 46 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( *𝑟 ‘ ( Scalar ‘ 𝐾 ) ) = ( *𝑟 ‘ ( Scalar ‘ 𝐿 ) ) )
48 8 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( ·𝑖 ‘ 𝐾 ) 𝑏 ) = ( 𝑎 ( ·𝑖 ‘ 𝐿 ) 𝑏 ) )
49 47 48 fveq12d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( *𝑟 ‘ ( Scalar ‘ 𝐾 ) ) ‘ ( 𝑎 ( ·𝑖 ‘ 𝐾 ) 𝑏 ) ) = ( ( *𝑟 ‘ ( Scalar ‘ 𝐿 ) ) ‘ ( 𝑎 ( ·𝑖 ‘ 𝐿 ) 𝑏 ) ) )
50 49 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( ( *𝑟 ‘ ( Scalar ‘ 𝐾 ) ) ‘ ( 𝑎 ( ·𝑖 ‘ 𝐾 ) 𝑏 ) ) = ( ( *𝑟 ‘ ( Scalar ‘ 𝐿 ) ) ‘ ( 𝑎 ( ·𝑖 ‘ 𝐿 ) 𝑏 ) ) )
51 50 13 eqeq12d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( ( ( *𝑟 ‘ ( Scalar ‘ 𝐾 ) ) ‘ ( 𝑎 ( ·𝑖 ‘ 𝐾 ) 𝑏 ) ) = ( 𝑏 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) ↔ ( ( *𝑟 ‘ ( Scalar ‘ 𝐿 ) ) ‘ ( 𝑎 ( ·𝑖 ‘ 𝐿 ) 𝑏 ) ) = ( 𝑏 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) ) )
52 51 ralbidva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ∀ 𝑏 ∈ 𝐵 ( ( *𝑟 ‘ ( Scalar ‘ 𝐾 ) ) ‘ ( 𝑎 ( ·𝑖 ‘ 𝐾 ) 𝑏 ) ) = ( 𝑏 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) ↔ ∀ 𝑏 ∈ 𝐵 ( ( *𝑟 ‘ ( Scalar ‘ 𝐿 ) ) ‘ ( 𝑎 ( ·𝑖 ‘ 𝐿 ) 𝑏 ) ) = ( 𝑏 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) ) )
53 15 raleqdv ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ∀ 𝑏 ∈ 𝐵 ( ( *𝑟 ‘ ( Scalar ‘ 𝐾 ) ) ‘ ( 𝑎 ( ·𝑖 ‘ 𝐾 ) 𝑏 ) ) = ( 𝑏 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) ↔ ∀ 𝑏 ∈ ( Base ‘ 𝐾 ) ( ( *𝑟 ‘ ( Scalar ‘ 𝐾 ) ) ‘ ( 𝑎 ( ·𝑖 ‘ 𝐾 ) 𝑏 ) ) = ( 𝑏 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) ) )
54 17 raleqdv ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ∀ 𝑏 ∈ 𝐵 ( ( *𝑟 ‘ ( Scalar ‘ 𝐿 ) ) ‘ ( 𝑎 ( ·𝑖 ‘ 𝐿 ) 𝑏 ) ) = ( 𝑏 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) ↔ ∀ 𝑏 ∈ ( Base ‘ 𝐿 ) ( ( *𝑟 ‘ ( Scalar ‘ 𝐿 ) ) ‘ ( 𝑎 ( ·𝑖 ‘ 𝐿 ) 𝑏 ) ) = ( 𝑏 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) ) )
55 52 53 54 3bitr3d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ∀ 𝑏 ∈ ( Base ‘ 𝐾 ) ( ( *𝑟 ‘ ( Scalar ‘ 𝐾 ) ) ‘ ( 𝑎 ( ·𝑖 ‘ 𝐾 ) 𝑏 ) ) = ( 𝑏 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) ↔ ∀ 𝑏 ∈ ( Base ‘ 𝐿 ) ( ( *𝑟 ‘ ( Scalar ‘ 𝐿 ) ) ‘ ( 𝑎 ( ·𝑖 ‘ 𝐿 ) 𝑏 ) ) = ( 𝑏 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) ) )
56 36 45 55 3anbi123d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( ( 𝑏 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑏 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) ) ∈ ( 𝐾 LMHom ( ringLMod ‘ ( Scalar ‘ 𝐾 ) ) ) ∧ ( ( 𝑎 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) = ( 0g ‘ ( Scalar ‘ 𝐾 ) ) → 𝑎 = ( 0g ‘ 𝐾 ) ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐾 ) ( ( *𝑟 ‘ ( Scalar ‘ 𝐾 ) ) ‘ ( 𝑎 ( ·𝑖 ‘ 𝐾 ) 𝑏 ) ) = ( 𝑏 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) ) ↔ ( ( 𝑏 ∈ ( Base ‘ 𝐿 ) ↦ ( 𝑏 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) ) ∈ ( 𝐿 LMHom ( ringLMod ‘ ( Scalar ‘ 𝐿 ) ) ) ∧ ( ( 𝑎 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) = ( 0g ‘ ( Scalar ‘ 𝐿 ) ) → 𝑎 = ( 0g ‘ 𝐿 ) ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐿 ) ( ( *𝑟 ‘ ( Scalar ‘ 𝐿 ) ) ‘ ( 𝑎 ( ·𝑖 ‘ 𝐿 ) 𝑏 ) ) = ( 𝑏 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) ) ) )
57 56 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑎 ∈ 𝐵 ( ( 𝑏 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑏 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) ) ∈ ( 𝐾 LMHom ( ringLMod ‘ ( Scalar ‘ 𝐾 ) ) ) ∧ ( ( 𝑎 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) = ( 0g ‘ ( Scalar ‘ 𝐾 ) ) → 𝑎 = ( 0g ‘ 𝐾 ) ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐾 ) ( ( *𝑟 ‘ ( Scalar ‘ 𝐾 ) ) ‘ ( 𝑎 ( ·𝑖 ‘ 𝐾 ) 𝑏 ) ) = ( 𝑏 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) ) ↔ ∀ 𝑎 ∈ 𝐵 ( ( 𝑏 ∈ ( Base ‘ 𝐿 ) ↦ ( 𝑏 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) ) ∈ ( 𝐿 LMHom ( ringLMod ‘ ( Scalar ‘ 𝐿 ) ) ) ∧ ( ( 𝑎 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) = ( 0g ‘ ( Scalar ‘ 𝐿 ) ) → 𝑎 = ( 0g ‘ 𝐿 ) ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐿 ) ( ( *𝑟 ‘ ( Scalar ‘ 𝐿 ) ) ‘ ( 𝑎 ( ·𝑖 ‘ 𝐿 ) 𝑏 ) ) = ( 𝑏 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) ) ) )
58 1 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑎 ∈ 𝐵 ( ( 𝑏 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑏 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) ) ∈ ( 𝐾 LMHom ( ringLMod ‘ ( Scalar ‘ 𝐾 ) ) ) ∧ ( ( 𝑎 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) = ( 0g ‘ ( Scalar ‘ 𝐾 ) ) → 𝑎 = ( 0g ‘ 𝐾 ) ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐾 ) ( ( *𝑟 ‘ ( Scalar ‘ 𝐾 ) ) ‘ ( 𝑎 ( ·𝑖 ‘ 𝐾 ) 𝑏 ) ) = ( 𝑏 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) ) ↔ ∀ 𝑎 ∈ ( Base ‘ 𝐾 ) ( ( 𝑏 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑏 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) ) ∈ ( 𝐾 LMHom ( ringLMod ‘ ( Scalar ‘ 𝐾 ) ) ) ∧ ( ( 𝑎 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) = ( 0g ‘ ( Scalar ‘ 𝐾 ) ) → 𝑎 = ( 0g ‘ 𝐾 ) ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐾 ) ( ( *𝑟 ‘ ( Scalar ‘ 𝐾 ) ) ‘ ( 𝑎 ( ·𝑖 ‘ 𝐾 ) 𝑏 ) ) = ( 𝑏 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) ) ) )
59 2 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑎 ∈ 𝐵 ( ( 𝑏 ∈ ( Base ‘ 𝐿 ) ↦ ( 𝑏 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) ) ∈ ( 𝐿 LMHom ( ringLMod ‘ ( Scalar ‘ 𝐿 ) ) ) ∧ ( ( 𝑎 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) = ( 0g ‘ ( Scalar ‘ 𝐿 ) ) → 𝑎 = ( 0g ‘ 𝐿 ) ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐿 ) ( ( *𝑟 ‘ ( Scalar ‘ 𝐿 ) ) ‘ ( 𝑎 ( ·𝑖 ‘ 𝐿 ) 𝑏 ) ) = ( 𝑏 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) ) ↔ ∀ 𝑎 ∈ ( Base ‘ 𝐿 ) ( ( 𝑏 ∈ ( Base ‘ 𝐿 ) ↦ ( 𝑏 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) ) ∈ ( 𝐿 LMHom ( ringLMod ‘ ( Scalar ‘ 𝐿 ) ) ) ∧ ( ( 𝑎 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) = ( 0g ‘ ( Scalar ‘ 𝐿 ) ) → 𝑎 = ( 0g ‘ 𝐿 ) ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐿 ) ( ( *𝑟 ‘ ( Scalar ‘ 𝐿 ) ) ‘ ( 𝑎 ( ·𝑖 ‘ 𝐿 ) 𝑏 ) ) = ( 𝑏 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) ) ) )
60 57 58 59 3bitr3d ⊢ ( 𝜑 → ( ∀ 𝑎 ∈ ( Base ‘ 𝐾 ) ( ( 𝑏 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑏 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) ) ∈ ( 𝐾 LMHom ( ringLMod ‘ ( Scalar ‘ 𝐾 ) ) ) ∧ ( ( 𝑎 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) = ( 0g ‘ ( Scalar ‘ 𝐾 ) ) → 𝑎 = ( 0g ‘ 𝐾 ) ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐾 ) ( ( *𝑟 ‘ ( Scalar ‘ 𝐾 ) ) ‘ ( 𝑎 ( ·𝑖 ‘ 𝐾 ) 𝑏 ) ) = ( 𝑏 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) ) ↔ ∀ 𝑎 ∈ ( Base ‘ 𝐿 ) ( ( 𝑏 ∈ ( Base ‘ 𝐿 ) ↦ ( 𝑏 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) ) ∈ ( 𝐿 LMHom ( ringLMod ‘ ( Scalar ‘ 𝐿 ) ) ) ∧ ( ( 𝑎 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) = ( 0g ‘ ( Scalar ‘ 𝐿 ) ) → 𝑎 = ( 0g ‘ 𝐿 ) ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐿 ) ( ( *𝑟 ‘ ( Scalar ‘ 𝐿 ) ) ‘ ( 𝑎 ( ·𝑖 ‘ 𝐿 ) 𝑏 ) ) = ( 𝑏 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) ) ) )
61 9 11 60 3anbi123d ⊢ ( 𝜑 → ( ( 𝐾 ∈ LVec ∧ ( Scalar ‘ 𝐾 ) ∈ *-Ring ∧ ∀ 𝑎 ∈ ( Base ‘ 𝐾 ) ( ( 𝑏 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑏 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) ) ∈ ( 𝐾 LMHom ( ringLMod ‘ ( Scalar ‘ 𝐾 ) ) ) ∧ ( ( 𝑎 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) = ( 0g ‘ ( Scalar ‘ 𝐾 ) ) → 𝑎 = ( 0g ‘ 𝐾 ) ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐾 ) ( ( *𝑟 ‘ ( Scalar ‘ 𝐾 ) ) ‘ ( 𝑎 ( ·𝑖 ‘ 𝐾 ) 𝑏 ) ) = ( 𝑏 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) ) ) ↔ ( 𝐿 ∈ LVec ∧ ( Scalar ‘ 𝐿 ) ∈ *-Ring ∧ ∀ 𝑎 ∈ ( Base ‘ 𝐿 ) ( ( 𝑏 ∈ ( Base ‘ 𝐿 ) ↦ ( 𝑏 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) ) ∈ ( 𝐿 LMHom ( ringLMod ‘ ( Scalar ‘ 𝐿 ) ) ) ∧ ( ( 𝑎 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) = ( 0g ‘ ( Scalar ‘ 𝐿 ) ) → 𝑎 = ( 0g ‘ 𝐿 ) ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐿 ) ( ( *𝑟 ‘ ( Scalar ‘ 𝐿 ) ) ‘ ( 𝑎 ( ·𝑖 ‘ 𝐿 ) 𝑏 ) ) = ( 𝑏 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) ) ) ) )
62 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
63 eqid ⊢ ( Scalar ‘ 𝐾 ) = ( Scalar ‘ 𝐾 )
64 eqid ⊢ ( ·𝑖 ‘ 𝐾 ) = ( ·𝑖 ‘ 𝐾 )
65 eqid ⊢ ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐾 )
66 eqid ⊢ ( *𝑟 ‘ ( Scalar ‘ 𝐾 ) ) = ( *𝑟 ‘ ( Scalar ‘ 𝐾 ) )
67 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝐾 ) ) = ( 0g ‘ ( Scalar ‘ 𝐾 ) )
68 62 63 64 65 66 67 isphl ⊢ ( 𝐾 ∈ PreHil ↔ ( 𝐾 ∈ LVec ∧ ( Scalar ‘ 𝐾 ) ∈ *-Ring ∧ ∀ 𝑎 ∈ ( Base ‘ 𝐾 ) ( ( 𝑏 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑏 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) ) ∈ ( 𝐾 LMHom ( ringLMod ‘ ( Scalar ‘ 𝐾 ) ) ) ∧ ( ( 𝑎 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) = ( 0g ‘ ( Scalar ‘ 𝐾 ) ) → 𝑎 = ( 0g ‘ 𝐾 ) ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐾 ) ( ( *𝑟 ‘ ( Scalar ‘ 𝐾 ) ) ‘ ( 𝑎 ( ·𝑖 ‘ 𝐾 ) 𝑏 ) ) = ( 𝑏 ( ·𝑖 ‘ 𝐾 ) 𝑎 ) ) ) )
69 eqid ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
70 eqid ⊢ ( Scalar ‘ 𝐿 ) = ( Scalar ‘ 𝐿 )
71 eqid ⊢ ( ·𝑖 ‘ 𝐿 ) = ( ·𝑖 ‘ 𝐿 )
72 eqid ⊢ ( 0g ‘ 𝐿 ) = ( 0g ‘ 𝐿 )
73 eqid ⊢ ( *𝑟 ‘ ( Scalar ‘ 𝐿 ) ) = ( *𝑟 ‘ ( Scalar ‘ 𝐿 ) )
74 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝐿 ) ) = ( 0g ‘ ( Scalar ‘ 𝐿 ) )
75 69 70 71 72 73 74 isphl ⊢ ( 𝐿 ∈ PreHil ↔ ( 𝐿 ∈ LVec ∧ ( Scalar ‘ 𝐿 ) ∈ *-Ring ∧ ∀ 𝑎 ∈ ( Base ‘ 𝐿 ) ( ( 𝑏 ∈ ( Base ‘ 𝐿 ) ↦ ( 𝑏 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) ) ∈ ( 𝐿 LMHom ( ringLMod ‘ ( Scalar ‘ 𝐿 ) ) ) ∧ ( ( 𝑎 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) = ( 0g ‘ ( Scalar ‘ 𝐿 ) ) → 𝑎 = ( 0g ‘ 𝐿 ) ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐿 ) ( ( *𝑟 ‘ ( Scalar ‘ 𝐿 ) ) ‘ ( 𝑎 ( ·𝑖 ‘ 𝐿 ) 𝑏 ) ) = ( 𝑏 ( ·𝑖 ‘ 𝐿 ) 𝑎 ) ) ) )
76 61 68 75 3bitr4g ⊢ ( 𝜑 → ( 𝐾 ∈ PreHil ↔ 𝐿 ∈ PreHil ) )