Metamath Proof Explorer


Theorem isphld

Description: Properties that determine a pre-Hilbert (inner product) space. (Contributed by Mario Carneiro, 18-Nov-2013) (Revised by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses isphld.v φ V = Base W
isphld.a φ + ˙ = + W
isphld.s φ · ˙ = W
isphld.i φ I = 𝑖 W
isphld.z φ 0 ˙ = 0 W
isphld.f φ F = Scalar W
isphld.k φ K = Base F
isphld.p φ ˙ = + F
isphld.t φ × ˙ = F
isphld.c φ ˙ = * F
isphld.o φ O = 0 F
isphld.l φ W LVec
isphld.r φ F *-Ring
isphld.cl φ x V y V x I y K
isphld.d φ q K x V y V z V q · ˙ x + ˙ y I z = q × ˙ x I z ˙ y I z
isphld.ns φ x V x I x = O x = 0 ˙
isphld.cj φ x V y V ˙ x I y = y I x
Assertion isphld φ W PreHil

Proof

Step Hyp Ref Expression
1 isphld.v φ V = Base W
2 isphld.a φ + ˙ = + W
3 isphld.s φ · ˙ = W
4 isphld.i φ I = 𝑖 W
5 isphld.z φ 0 ˙ = 0 W
6 isphld.f φ F = Scalar W
7 isphld.k φ K = Base F
8 isphld.p φ ˙ = + F
9 isphld.t φ × ˙ = F
10 isphld.c φ ˙ = * F
11 isphld.o φ O = 0 F
12 isphld.l φ W LVec
13 isphld.r φ F *-Ring
14 isphld.cl φ x V y V x I y K
15 isphld.d φ q K x V y V z V q · ˙ x + ˙ y I z = q × ˙ x I z ˙ y I z
16 isphld.ns φ x V x I x = O x = 0 ˙
17 isphld.cj φ x V y V ˙ x I y = y I x
18 6 13 eqeltrrd φ Scalar W *-Ring
19 oveq1 y = w y 𝑖 W x = w 𝑖 W x
20 19 cbvmptv y Base W y 𝑖 W x = w Base W w 𝑖 W x
21 14 3expib φ x V y V x I y K
22 1 eleq2d φ x V x Base W
23 1 eleq2d φ y V y Base W
24 22 23 anbi12d φ x V y V x Base W y Base W
25 4 oveqd φ x I y = x 𝑖 W y
26 6 fveq2d φ Base F = Base Scalar W
27 7 26 eqtrd φ K = Base Scalar W
28 25 27 eleq12d φ x I y K x 𝑖 W y Base Scalar W
29 21 24 28 3imtr3d φ x Base W y Base W x 𝑖 W y Base Scalar W
30 29 impl φ x Base W y Base W x 𝑖 W y Base Scalar W
31 30 an32s φ y Base W x Base W x 𝑖 W y Base Scalar W
32 oveq1 w = x w 𝑖 W y = x 𝑖 W y
33 32 cbvmptv w Base W w 𝑖 W y = x Base W x 𝑖 W y
34 31 33 fmptd φ y Base W w Base W w 𝑖 W y : Base W Base Scalar W
35 34 ralrimiva φ y Base W w Base W w 𝑖 W y : Base W Base Scalar W
36 oveq2 y = z w 𝑖 W y = w 𝑖 W z
37 36 mpteq2dv y = z w Base W w 𝑖 W y = w Base W w 𝑖 W z
38 37 feq1d y = z w Base W w 𝑖 W y : Base W Base Scalar W w Base W w 𝑖 W z : Base W Base Scalar W
39 38 rspccva y Base W w Base W w 𝑖 W y : Base W Base Scalar W z Base W w Base W w 𝑖 W z : Base W Base Scalar W
40 35 39 sylan φ z Base W w Base W w 𝑖 W z : Base W Base Scalar W
41 eqidd φ z Base W Scalar W = Scalar W
42 15 3exp φ q K x V y V z V q · ˙ x + ˙ y I z = q × ˙ x I z ˙ y I z
43 27 eleq2d φ q K q Base Scalar W
44 3anrot z V x V y V x V y V z V
45 1 eleq2d φ z V z Base W
46 45 22 23 3anbi123d φ z V x V y V z Base W x Base W y Base W
47 44 46 syl5bbr φ x V y V z V z Base W x Base W y Base W
48 3 oveqd φ q · ˙ x = q W x
49 eqidd φ y = y
50 2 48 49 oveq123d φ q · ˙ x + ˙ y = q W x + W y
51 eqidd φ z = z
52 4 50 51 oveq123d φ q · ˙ x + ˙ y I z = q W x + W y 𝑖 W z
53 6 fveq2d φ + F = + Scalar W
54 8 53 eqtrd φ ˙ = + Scalar W
55 6 fveq2d φ F = Scalar W
56 9 55 eqtrd φ × ˙ = Scalar W
57 eqidd φ q = q
58 4 oveqd φ x I z = x 𝑖 W z
59 56 57 58 oveq123d φ q × ˙ x I z = q Scalar W x 𝑖 W z
60 4 oveqd φ y I z = y 𝑖 W z
61 54 59 60 oveq123d φ q × ˙ x I z ˙ y I z = q Scalar W x 𝑖 W z + Scalar W y 𝑖 W z
62 52 61 eqeq12d φ q · ˙ x + ˙ y I z = q × ˙ x I z ˙ y I z q W x + W y 𝑖 W z = q Scalar W x 𝑖 W z + Scalar W y 𝑖 W z
63 47 62 imbi12d φ x V y V z V q · ˙ x + ˙ y I z = q × ˙ x I z ˙ y I z z Base W x Base W y Base W q W x + W y 𝑖 W z = q Scalar W x 𝑖 W z + Scalar W y 𝑖 W z
64 42 43 63 3imtr3d φ q Base Scalar W z Base W x Base W y Base W q W x + W y 𝑖 W z = q Scalar W x 𝑖 W z + Scalar W y 𝑖 W z
65 64 imp31 φ q Base Scalar W z Base W x Base W y Base W q W x + W y 𝑖 W z = q Scalar W x 𝑖 W z + Scalar W y 𝑖 W z
66 65 3exp2 φ q Base Scalar W z Base W x Base W y Base W q W x + W y 𝑖 W z = q Scalar W x 𝑖 W z + Scalar W y 𝑖 W z
67 66 impancom φ z Base W q Base Scalar W x Base W y Base W q W x + W y 𝑖 W z = q Scalar W x 𝑖 W z + Scalar W y 𝑖 W z
68 67 3imp2 φ z Base W q Base Scalar W x Base W y Base W q W x + W y 𝑖 W z = q Scalar W x 𝑖 W z + Scalar W y 𝑖 W z
69 lveclmod W LVec W LMod
70 12 69 syl φ W LMod
71 70 adantr φ z Base W W LMod
72 71 adantr φ z Base W q Base Scalar W x Base W y Base W W LMod
73 eqid Base W = Base W
74 eqid LSubSp W = LSubSp W
75 73 74 lss1 W LMod Base W LSubSp W
76 72 75 syl φ z Base W q Base Scalar W x Base W y Base W Base W LSubSp W
77 eqid Scalar W = Scalar W
78 eqid Base Scalar W = Base Scalar W
79 eqid + W = + W
80 eqid W = W
81 77 78 79 80 74 lsscl Base W LSubSp W q Base Scalar W x Base W y Base W q W x + W y Base W
82 76 81 sylancom φ z Base W q Base Scalar W x Base W y Base W q W x + W y Base W
83 oveq1 w = q W x + W y w 𝑖 W z = q W x + W y 𝑖 W z
84 eqid w Base W w 𝑖 W z = w Base W w 𝑖 W z
85 ovex w 𝑖 W z V
86 83 84 85 fvmpt3i q W x + W y Base W w Base W w 𝑖 W z q W x + W y = q W x + W y 𝑖 W z
87 82 86 syl φ z Base W q Base Scalar W x Base W y Base W w Base W w 𝑖 W z q W x + W y = q W x + W y 𝑖 W z
88 simpr2 φ z Base W q Base Scalar W x Base W y Base W x Base W
89 oveq1 w = x w 𝑖 W z = x 𝑖 W z
90 89 84 85 fvmpt3i x Base W w Base W w 𝑖 W z x = x 𝑖 W z
91 88 90 syl φ z Base W q Base Scalar W x Base W y Base W w Base W w 𝑖 W z x = x 𝑖 W z
92 91 oveq2d φ z Base W q Base Scalar W x Base W y Base W q Scalar W w Base W w 𝑖 W z x = q Scalar W x 𝑖 W z
93 simpr3 φ z Base W q Base Scalar W x Base W y Base W y Base W
94 oveq1 w = y w 𝑖 W z = y 𝑖 W z
95 94 84 85 fvmpt3i y Base W w Base W w 𝑖 W z y = y 𝑖 W z
96 93 95 syl φ z Base W q Base Scalar W x Base W y Base W w Base W w 𝑖 W z y = y 𝑖 W z
97 92 96 oveq12d φ z Base W q Base Scalar W x Base W y Base W q Scalar W w Base W w 𝑖 W z x + Scalar W w Base W w 𝑖 W z y = q Scalar W x 𝑖 W z + Scalar W y 𝑖 W z
98 68 87 97 3eqtr4d φ z Base W q Base Scalar W x Base W y Base W w Base W w 𝑖 W z q W x + W y = q Scalar W w Base W w 𝑖 W z x + Scalar W w Base W w 𝑖 W z y
99 98 ralrimivvva φ z Base W q Base Scalar W x Base W y Base W w Base W w 𝑖 W z q W x + W y = q Scalar W w Base W w 𝑖 W z x + Scalar W w Base W w 𝑖 W z y
100 77 lmodring W LMod Scalar W Ring
101 rlmlmod Scalar W Ring ringLMod Scalar W LMod
102 70 100 101 3syl φ ringLMod Scalar W LMod
103 102 adantr φ z Base W ringLMod Scalar W LMod
104 rlmbas Base Scalar W = Base ringLMod Scalar W
105 fvex Scalar W V
106 rlmsca Scalar W V Scalar W = Scalar ringLMod Scalar W
107 105 106 ax-mp Scalar W = Scalar ringLMod Scalar W
108 rlmplusg + Scalar W = + ringLMod Scalar W
109 rlmvsca Scalar W = ringLMod Scalar W
110 73 104 77 107 78 79 108 80 109 islmhm2 W LMod ringLMod Scalar W LMod w Base W w 𝑖 W z W LMHom ringLMod Scalar W w Base W w 𝑖 W z : Base W Base Scalar W Scalar W = Scalar W q Base Scalar W x Base W y Base W w Base W w 𝑖 W z q W x + W y = q Scalar W w Base W w 𝑖 W z x + Scalar W w Base W w 𝑖 W z y
111 71 103 110 syl2anc φ z Base W w Base W w 𝑖 W z W LMHom ringLMod Scalar W w Base W w 𝑖 W z : Base W Base Scalar W Scalar W = Scalar W q Base Scalar W x Base W y Base W w Base W w 𝑖 W z q W x + W y = q Scalar W w Base W w 𝑖 W z x + Scalar W w Base W w 𝑖 W z y
112 40 41 99 111 mpbir3and φ z Base W w Base W w 𝑖 W z W LMHom ringLMod Scalar W
113 112 ralrimiva φ z Base W w Base W w 𝑖 W z W LMHom ringLMod Scalar W
114 oveq2 z = x w 𝑖 W z = w 𝑖 W x
115 114 mpteq2dv z = x w Base W w 𝑖 W z = w Base W w 𝑖 W x
116 115 eleq1d z = x w Base W w 𝑖 W z W LMHom ringLMod Scalar W w Base W w 𝑖 W x W LMHom ringLMod Scalar W
117 116 rspccva z Base W w Base W w 𝑖 W z W LMHom ringLMod Scalar W x Base W w Base W w 𝑖 W x W LMHom ringLMod Scalar W
118 113 117 sylan φ x Base W w Base W w 𝑖 W x W LMHom ringLMod Scalar W
119 20 118 eqeltrid φ x Base W y Base W y 𝑖 W x W LMHom ringLMod Scalar W
120 16 3exp φ x V x I x = O x = 0 ˙
121 4 oveqd φ x I x = x 𝑖 W x
122 6 fveq2d φ 0 F = 0 Scalar W
123 11 122 eqtrd φ O = 0 Scalar W
124 121 123 eqeq12d φ x I x = O x 𝑖 W x = 0 Scalar W
125 5 eqeq2d φ x = 0 ˙ x = 0 W
126 124 125 imbi12d φ x I x = O x = 0 ˙ x 𝑖 W x = 0 Scalar W x = 0 W
127 120 22 126 3imtr3d φ x Base W x 𝑖 W x = 0 Scalar W x = 0 W
128 127 imp φ x Base W x 𝑖 W x = 0 Scalar W x = 0 W
129 17 3expib φ x V y V ˙ x I y = y I x
130 6 fveq2d φ * F = * Scalar W
131 10 130 eqtrd φ ˙ = * Scalar W
132 131 25 fveq12d φ ˙ x I y = x 𝑖 W y * Scalar W
133 4 oveqd φ y I x = y 𝑖 W x
134 132 133 eqeq12d φ ˙ x I y = y I x x 𝑖 W y * Scalar W = y 𝑖 W x
135 129 24 134 3imtr3d φ x Base W y Base W x 𝑖 W y * Scalar W = y 𝑖 W x
136 135 expdimp φ x Base W y Base W x 𝑖 W y * Scalar W = y 𝑖 W x
137 136 ralrimiv φ x Base W y Base W x 𝑖 W y * Scalar W = y 𝑖 W x
138 119 128 137 3jca φ x Base W y Base W y 𝑖 W x W LMHom ringLMod Scalar W x 𝑖 W x = 0 Scalar W x = 0 W y Base W x 𝑖 W y * Scalar W = y 𝑖 W x
139 138 ralrimiva φ x Base W y Base W y 𝑖 W x W LMHom ringLMod Scalar W x 𝑖 W x = 0 Scalar W x = 0 W y Base W x 𝑖 W y * Scalar W = y 𝑖 W x
140 eqid 𝑖 W = 𝑖 W
141 eqid 0 W = 0 W
142 eqid * Scalar W = * Scalar W
143 eqid 0 Scalar W = 0 Scalar W
144 73 77 140 141 142 143 isphl W PreHil W LVec Scalar W *-Ring x Base W y Base W y 𝑖 W x W LMHom ringLMod Scalar W x 𝑖 W x = 0 Scalar W x = 0 W y Base W x 𝑖 W y * Scalar W = y 𝑖 W x
145 12 18 139 144 syl3anbrc φ W PreHil