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 
|- ( ph -> B = ( Base ` K ) )
phlpropd.2 
|- ( ph -> B = ( Base ` L ) )
phlpropd.3 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
phlpropd.4 
|- ( ph -> F = ( Scalar ` K ) )
phlpropd.5 
|- ( ph -> F = ( Scalar ` L ) )
phlpropd.6 
|- P = ( Base ` F )
phlpropd.7 
|- ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` L ) y ) )
phlpropd.8 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .i ` K ) y ) = ( x ( .i ` L ) y ) )
Assertion phlpropd 
|- ( ph -> ( K e. PreHil <-> L e. PreHil ) )

Proof

Step Hyp Ref Expression
1 phlpropd.1 
 |-  ( ph -> B = ( Base ` K ) )
2 phlpropd.2 
 |-  ( ph -> B = ( Base ` L ) )
3 phlpropd.3 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
4 phlpropd.4 
 |-  ( ph -> F = ( Scalar ` K ) )
5 phlpropd.5 
 |-  ( ph -> F = ( Scalar ` L ) )
6 phlpropd.6 
 |-  P = ( Base ` F )
7 phlpropd.7 
 |-  ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` L ) y ) )
8 phlpropd.8 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .i ` K ) y ) = ( x ( .i ` L ) y ) )
9 1 2 3 4 5 6 7 lvecpropd 
 |-  ( ph -> ( K e. LVec <-> L e. LVec ) )
10 4 5 eqtr3d 
 |-  ( ph -> ( Scalar ` K ) = ( Scalar ` L ) )
11 10 eleq1d 
 |-  ( ph -> ( ( Scalar ` K ) e. *Ring <-> ( Scalar ` L ) e. *Ring ) )
12 8 oveqrspc2v 
 |-  ( ( ph /\ ( b e. B /\ a e. B ) ) -> ( b ( .i ` K ) a ) = ( b ( .i ` L ) a ) )
13 12 anass1rs 
 |-  ( ( ( ph /\ a e. B ) /\ b e. B ) -> ( b ( .i ` K ) a ) = ( b ( .i ` L ) a ) )
14 13 mpteq2dva 
 |-  ( ( ph /\ a e. B ) -> ( b e. B |-> ( b ( .i ` K ) a ) ) = ( b e. B |-> ( b ( .i ` L ) a ) ) )
15 1 adantr 
 |-  ( ( ph /\ a e. B ) -> B = ( Base ` K ) )
16 15 mpteq1d 
 |-  ( ( ph /\ a e. B ) -> ( b e. B |-> ( b ( .i ` K ) a ) ) = ( b e. ( Base ` K ) |-> ( b ( .i ` K ) a ) ) )
17 2 adantr 
 |-  ( ( ph /\ a e. B ) -> B = ( Base ` L ) )
18 17 mpteq1d 
 |-  ( ( ph /\ a e. B ) -> ( b e. B |-> ( b ( .i ` L ) a ) ) = ( b e. ( Base ` L ) |-> ( b ( .i ` L ) a ) ) )
19 14 16 18 3eqtr3d 
 |-  ( ( ph /\ a e. B ) -> ( b e. ( Base ` K ) |-> ( b ( .i ` K ) a ) ) = ( b e. ( Base ` L ) |-> ( b ( .i ` L ) a ) ) )
20 rlmbas 
 |-  ( Base ` F ) = ( Base ` ( ringLMod ` F ) )
21 6 20 eqtri 
 |-  P = ( Base ` ( ringLMod ` F ) )
22 21 a1i 
 |-  ( ph -> P = ( Base ` ( ringLMod ` F ) ) )
23 fvex 
 |-  ( Scalar ` K ) e. _V
24 4 23 eqeltrdi 
 |-  ( ph -> F e. _V )
25 rlmsca 
 |-  ( F e. _V -> F = ( Scalar ` ( ringLMod ` F ) ) )
26 24 25 syl 
 |-  ( ph -> F = ( Scalar ` ( ringLMod ` F ) ) )
27 eqidd 
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( x ( +g ` ( ringLMod ` F ) ) y ) = ( x ( +g ` ( ringLMod ` F ) ) y ) )
28 eqidd 
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( x ( .s ` ( ringLMod ` F ) ) y ) = ( x ( .s ` ( ringLMod ` F ) ) y ) )
29 1 22 2 22 4 26 5 26 6 6 3 27 7 28 lmhmpropd 
 |-  ( ph -> ( K LMHom ( ringLMod ` F ) ) = ( L LMHom ( ringLMod ` F ) ) )
30 4 fveq2d 
 |-  ( ph -> ( ringLMod ` F ) = ( ringLMod ` ( Scalar ` K ) ) )
31 30 oveq2d 
 |-  ( ph -> ( K LMHom ( ringLMod ` F ) ) = ( K LMHom ( ringLMod ` ( Scalar ` K ) ) ) )
32 5 fveq2d 
 |-  ( ph -> ( ringLMod ` F ) = ( ringLMod ` ( Scalar ` L ) ) )
33 32 oveq2d 
 |-  ( ph -> ( L LMHom ( ringLMod ` F ) ) = ( L LMHom ( ringLMod ` ( Scalar ` L ) ) ) )
34 29 31 33 3eqtr3d 
 |-  ( ph -> ( K LMHom ( ringLMod ` ( Scalar ` K ) ) ) = ( L LMHom ( ringLMod ` ( Scalar ` L ) ) ) )
35 34 adantr 
 |-  ( ( ph /\ a e. B ) -> ( K LMHom ( ringLMod ` ( Scalar ` K ) ) ) = ( L LMHom ( ringLMod ` ( Scalar ` L ) ) ) )
36 19 35 eleq12d 
 |-  ( ( ph /\ a e. B ) -> ( ( b e. ( Base ` K ) |-> ( b ( .i ` K ) a ) ) e. ( K LMHom ( ringLMod ` ( Scalar ` K ) ) ) <-> ( b e. ( Base ` L ) |-> ( b ( .i ` L ) a ) ) e. ( L LMHom ( ringLMod ` ( Scalar ` L ) ) ) ) )
37 8 oveqrspc2v 
 |-  ( ( ph /\ ( a e. B /\ a e. B ) ) -> ( a ( .i ` K ) a ) = ( a ( .i ` L ) a ) )
38 37 anabsan2 
 |-  ( ( ph /\ a e. B ) -> ( a ( .i ` K ) a ) = ( a ( .i ` L ) a ) )
39 10 fveq2d 
 |-  ( ph -> ( 0g ` ( Scalar ` K ) ) = ( 0g ` ( Scalar ` L ) ) )
40 39 adantr 
 |-  ( ( ph /\ a e. B ) -> ( 0g ` ( Scalar ` K ) ) = ( 0g ` ( Scalar ` L ) ) )
41 38 40 eqeq12d 
 |-  ( ( ph /\ a e. B ) -> ( ( a ( .i ` K ) a ) = ( 0g ` ( Scalar ` K ) ) <-> ( a ( .i ` L ) a ) = ( 0g ` ( Scalar ` L ) ) ) )
42 1 2 3 grpidpropd 
 |-  ( ph -> ( 0g ` K ) = ( 0g ` L ) )
43 42 adantr 
 |-  ( ( ph /\ a e. B ) -> ( 0g ` K ) = ( 0g ` L ) )
44 43 eqeq2d 
 |-  ( ( ph /\ a e. B ) -> ( a = ( 0g ` K ) <-> a = ( 0g ` L ) ) )
45 41 44 imbi12d 
 |-  ( ( ph /\ a e. B ) -> ( ( ( a ( .i ` K ) a ) = ( 0g ` ( Scalar ` K ) ) -> a = ( 0g ` K ) ) <-> ( ( a ( .i ` L ) a ) = ( 0g ` ( Scalar ` L ) ) -> a = ( 0g ` L ) ) ) )
46 10 fveq2d 
 |-  ( ph -> ( *r ` ( Scalar ` K ) ) = ( *r ` ( Scalar ` L ) ) )
47 46 adantr 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( *r ` ( Scalar ` K ) ) = ( *r ` ( Scalar ` L ) ) )
48 8 oveqrspc2v 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( a ( .i ` K ) b ) = ( a ( .i ` L ) b ) )
49 47 48 fveq12d 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( ( *r ` ( Scalar ` K ) ) ` ( a ( .i ` K ) b ) ) = ( ( *r ` ( Scalar ` L ) ) ` ( a ( .i ` L ) b ) ) )
50 49 anassrs 
 |-  ( ( ( ph /\ a e. B ) /\ b e. B ) -> ( ( *r ` ( Scalar ` K ) ) ` ( a ( .i ` K ) b ) ) = ( ( *r ` ( Scalar ` L ) ) ` ( a ( .i ` L ) b ) ) )
51 50 13 eqeq12d 
 |-  ( ( ( ph /\ a e. B ) /\ b e. B ) -> ( ( ( *r ` ( Scalar ` K ) ) ` ( a ( .i ` K ) b ) ) = ( b ( .i ` K ) a ) <-> ( ( *r ` ( Scalar ` L ) ) ` ( a ( .i ` L ) b ) ) = ( b ( .i ` L ) a ) ) )
52 51 ralbidva 
 |-  ( ( ph /\ a e. B ) -> ( A. b e. B ( ( *r ` ( Scalar ` K ) ) ` ( a ( .i ` K ) b ) ) = ( b ( .i ` K ) a ) <-> A. b e. B ( ( *r ` ( Scalar ` L ) ) ` ( a ( .i ` L ) b ) ) = ( b ( .i ` L ) a ) ) )
53 15 raleqdv 
 |-  ( ( ph /\ a e. B ) -> ( A. b e. B ( ( *r ` ( Scalar ` K ) ) ` ( a ( .i ` K ) b ) ) = ( b ( .i ` K ) a ) <-> A. b e. ( Base ` K ) ( ( *r ` ( Scalar ` K ) ) ` ( a ( .i ` K ) b ) ) = ( b ( .i ` K ) a ) ) )
54 17 raleqdv 
 |-  ( ( ph /\ a e. B ) -> ( A. b e. B ( ( *r ` ( Scalar ` L ) ) ` ( a ( .i ` L ) b ) ) = ( b ( .i ` L ) a ) <-> A. b e. ( Base ` L ) ( ( *r ` ( Scalar ` L ) ) ` ( a ( .i ` L ) b ) ) = ( b ( .i ` L ) a ) ) )
55 52 53 54 3bitr3d 
 |-  ( ( ph /\ a e. B ) -> ( A. b e. ( Base ` K ) ( ( *r ` ( Scalar ` K ) ) ` ( a ( .i ` K ) b ) ) = ( b ( .i ` K ) a ) <-> A. b e. ( Base ` L ) ( ( *r ` ( Scalar ` L ) ) ` ( a ( .i ` L ) b ) ) = ( b ( .i ` L ) a ) ) )
56 36 45 55 3anbi123d 
 |-  ( ( ph /\ a e. B ) -> ( ( ( b e. ( Base ` K ) |-> ( b ( .i ` K ) a ) ) e. ( K LMHom ( ringLMod ` ( Scalar ` K ) ) ) /\ ( ( a ( .i ` K ) a ) = ( 0g ` ( Scalar ` K ) ) -> a = ( 0g ` K ) ) /\ A. b e. ( Base ` K ) ( ( *r ` ( Scalar ` K ) ) ` ( a ( .i ` K ) b ) ) = ( b ( .i ` K ) a ) ) <-> ( ( b e. ( Base ` L ) |-> ( b ( .i ` L ) a ) ) e. ( L LMHom ( ringLMod ` ( Scalar ` L ) ) ) /\ ( ( a ( .i ` L ) a ) = ( 0g ` ( Scalar ` L ) ) -> a = ( 0g ` L ) ) /\ A. b e. ( Base ` L ) ( ( *r ` ( Scalar ` L ) ) ` ( a ( .i ` L ) b ) ) = ( b ( .i ` L ) a ) ) ) )
57 56 ralbidva 
 |-  ( ph -> ( A. a e. B ( ( b e. ( Base ` K ) |-> ( b ( .i ` K ) a ) ) e. ( K LMHom ( ringLMod ` ( Scalar ` K ) ) ) /\ ( ( a ( .i ` K ) a ) = ( 0g ` ( Scalar ` K ) ) -> a = ( 0g ` K ) ) /\ A. b e. ( Base ` K ) ( ( *r ` ( Scalar ` K ) ) ` ( a ( .i ` K ) b ) ) = ( b ( .i ` K ) a ) ) <-> A. a e. B ( ( b e. ( Base ` L ) |-> ( b ( .i ` L ) a ) ) e. ( L LMHom ( ringLMod ` ( Scalar ` L ) ) ) /\ ( ( a ( .i ` L ) a ) = ( 0g ` ( Scalar ` L ) ) -> a = ( 0g ` L ) ) /\ A. b e. ( Base ` L ) ( ( *r ` ( Scalar ` L ) ) ` ( a ( .i ` L ) b ) ) = ( b ( .i ` L ) a ) ) ) )
58 1 raleqdv 
 |-  ( ph -> ( A. a e. B ( ( b e. ( Base ` K ) |-> ( b ( .i ` K ) a ) ) e. ( K LMHom ( ringLMod ` ( Scalar ` K ) ) ) /\ ( ( a ( .i ` K ) a ) = ( 0g ` ( Scalar ` K ) ) -> a = ( 0g ` K ) ) /\ A. b e. ( Base ` K ) ( ( *r ` ( Scalar ` K ) ) ` ( a ( .i ` K ) b ) ) = ( b ( .i ` K ) a ) ) <-> A. a e. ( Base ` K ) ( ( b e. ( Base ` K ) |-> ( b ( .i ` K ) a ) ) e. ( K LMHom ( ringLMod ` ( Scalar ` K ) ) ) /\ ( ( a ( .i ` K ) a ) = ( 0g ` ( Scalar ` K ) ) -> a = ( 0g ` K ) ) /\ A. b e. ( Base ` K ) ( ( *r ` ( Scalar ` K ) ) ` ( a ( .i ` K ) b ) ) = ( b ( .i ` K ) a ) ) ) )
59 2 raleqdv 
 |-  ( ph -> ( A. a e. B ( ( b e. ( Base ` L ) |-> ( b ( .i ` L ) a ) ) e. ( L LMHom ( ringLMod ` ( Scalar ` L ) ) ) /\ ( ( a ( .i ` L ) a ) = ( 0g ` ( Scalar ` L ) ) -> a = ( 0g ` L ) ) /\ A. b e. ( Base ` L ) ( ( *r ` ( Scalar ` L ) ) ` ( a ( .i ` L ) b ) ) = ( b ( .i ` L ) a ) ) <-> A. a e. ( Base ` L ) ( ( b e. ( Base ` L ) |-> ( b ( .i ` L ) a ) ) e. ( L LMHom ( ringLMod ` ( Scalar ` L ) ) ) /\ ( ( a ( .i ` L ) a ) = ( 0g ` ( Scalar ` L ) ) -> a = ( 0g ` L ) ) /\ A. b e. ( Base ` L ) ( ( *r ` ( Scalar ` L ) ) ` ( a ( .i ` L ) b ) ) = ( b ( .i ` L ) a ) ) ) )
60 57 58 59 3bitr3d 
 |-  ( ph -> ( A. a e. ( Base ` K ) ( ( b e. ( Base ` K ) |-> ( b ( .i ` K ) a ) ) e. ( K LMHom ( ringLMod ` ( Scalar ` K ) ) ) /\ ( ( a ( .i ` K ) a ) = ( 0g ` ( Scalar ` K ) ) -> a = ( 0g ` K ) ) /\ A. b e. ( Base ` K ) ( ( *r ` ( Scalar ` K ) ) ` ( a ( .i ` K ) b ) ) = ( b ( .i ` K ) a ) ) <-> A. a e. ( Base ` L ) ( ( b e. ( Base ` L ) |-> ( b ( .i ` L ) a ) ) e. ( L LMHom ( ringLMod ` ( Scalar ` L ) ) ) /\ ( ( a ( .i ` L ) a ) = ( 0g ` ( Scalar ` L ) ) -> a = ( 0g ` L ) ) /\ A. b e. ( Base ` L ) ( ( *r ` ( Scalar ` L ) ) ` ( a ( .i ` L ) b ) ) = ( b ( .i ` L ) a ) ) ) )
61 9 11 60 3anbi123d 
 |-  ( ph -> ( ( K e. LVec /\ ( Scalar ` K ) e. *Ring /\ A. a e. ( Base ` K ) ( ( b e. ( Base ` K ) |-> ( b ( .i ` K ) a ) ) e. ( K LMHom ( ringLMod ` ( Scalar ` K ) ) ) /\ ( ( a ( .i ` K ) a ) = ( 0g ` ( Scalar ` K ) ) -> a = ( 0g ` K ) ) /\ A. b e. ( Base ` K ) ( ( *r ` ( Scalar ` K ) ) ` ( a ( .i ` K ) b ) ) = ( b ( .i ` K ) a ) ) ) <-> ( L e. LVec /\ ( Scalar ` L ) e. *Ring /\ A. a e. ( Base ` L ) ( ( b e. ( Base ` L ) |-> ( b ( .i ` L ) a ) ) e. ( L LMHom ( ringLMod ` ( Scalar ` L ) ) ) /\ ( ( a ( .i ` L ) a ) = ( 0g ` ( Scalar ` L ) ) -> a = ( 0g ` L ) ) /\ A. b e. ( Base ` L ) ( ( *r ` ( Scalar ` L ) ) ` ( a ( .i ` L ) b ) ) = ( b ( .i ` L ) a ) ) ) ) )
62 eqid 
 |-  ( Base ` K ) = ( Base ` K )
63 eqid 
 |-  ( Scalar ` K ) = ( Scalar ` K )
64 eqid 
 |-  ( .i ` K ) = ( .i ` K )
65 eqid 
 |-  ( 0g ` K ) = ( 0g ` K )
66 eqid 
 |-  ( *r ` ( Scalar ` K ) ) = ( *r ` ( Scalar ` K ) )
67 eqid 
 |-  ( 0g ` ( Scalar ` K ) ) = ( 0g ` ( Scalar ` K ) )
68 62 63 64 65 66 67 isphl 
 |-  ( K e. PreHil <-> ( K e. LVec /\ ( Scalar ` K ) e. *Ring /\ A. a e. ( Base ` K ) ( ( b e. ( Base ` K ) |-> ( b ( .i ` K ) a ) ) e. ( K LMHom ( ringLMod ` ( Scalar ` K ) ) ) /\ ( ( a ( .i ` K ) a ) = ( 0g ` ( Scalar ` K ) ) -> a = ( 0g ` K ) ) /\ A. b e. ( Base ` K ) ( ( *r ` ( Scalar ` K ) ) ` ( a ( .i ` K ) b ) ) = ( b ( .i ` K ) a ) ) ) )
69 eqid 
 |-  ( Base ` L ) = ( Base ` L )
70 eqid 
 |-  ( Scalar ` L ) = ( Scalar ` L )
71 eqid 
 |-  ( .i ` L ) = ( .i ` L )
72 eqid 
 |-  ( 0g ` L ) = ( 0g ` L )
73 eqid 
 |-  ( *r ` ( Scalar ` L ) ) = ( *r ` ( Scalar ` L ) )
74 eqid 
 |-  ( 0g ` ( Scalar ` L ) ) = ( 0g ` ( Scalar ` L ) )
75 69 70 71 72 73 74 isphl 
 |-  ( L e. PreHil <-> ( L e. LVec /\ ( Scalar ` L ) e. *Ring /\ A. a e. ( Base ` L ) ( ( b e. ( Base ` L ) |-> ( b ( .i ` L ) a ) ) e. ( L LMHom ( ringLMod ` ( Scalar ` L ) ) ) /\ ( ( a ( .i ` L ) a ) = ( 0g ` ( Scalar ` L ) ) -> a = ( 0g ` L ) ) /\ A. b e. ( Base ` L ) ( ( *r ` ( Scalar ` L ) ) ` ( a ( .i ` L ) b ) ) = ( b ( .i ` L ) a ) ) ) )
76 61 68 75 3bitr4g 
 |-  ( ph -> ( K e. PreHil <-> L e. PreHil ) )