Theorem isphil 17195

Description: The predicate "is a pre-Hilbert space" (over a *-division ring)

Hypotheses

Ref	Expression
isphil.1	|- Q = Struct(8, f, T. )
isphil.k	|- K = (base` W)
isphil.p	|- P = (+g` W)
isphil.t	|- T = (.r` W)
isphil.i	|- I = (*v` W)
isphil.v	|- V = (vbase` W)
isphil.a	|- A = (vadd` W)
isphil.s	|- S = (vsca` W)
isphil.h	|- H = (ip` W)
isphil.10	|- N = (0g` W)
isphil.11	|- Z = (0vNEW` W)

Assertion

Ref	Expression
isphil	|- (W e. PreHil <-> (W e. Q /\ W e. LVec /\ A.q e. K A.x e. V A.y e. V A.z e. V ((xHy) e. K /\ ((((qSx)Ay)Hz) = ((qT(xHz))P(yHz)) /\ ((xHx) = N -> x = Z) /\ (I` (xHy)) = (yHx)))))

Distinct variable groups:   f,q,x,y,z,A   f,H,q,x,y,z   f,I,q,x,y,z   f,K,q,x,y,z   f,N   P,f,q,x,y,z   S,f,q,x,y,z   T,f,q,x,y,z   f,V,q,x,y,z   f,W,q,x,y,z   f,Z

Proof of Theorem isphil

Step	Hyp	Ref	Expression
1		df-prehil 17194	. . 3 |- PreHil = Struct(8, f, (f e. LVec /\ E.kE.pE.tE.iE.vE.aE.sE.h(((k = (base` f) /\ p = (+g` f)) /\ (t = (.r` f) /\ i = (*v` f))) /\ ((v = (vbase` f) /\ a = (vadd` f)) /\ (s = (vsca` f) /\ h = (ip` f))) /\ A.q e. k A.x e. v A.y e. v A.z e. v ((xhy) e. k /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = (0g` f) -> x = (0vNEW` f)) /\ (i` (xhy)) = (yhx))))))
2	1	eleq2i 1961	. 2 |- (W e. PreHil <-> W e. Struct(8, f, (f e. LVec /\ E.kE.pE.tE.iE.vE.aE.sE.h(((k = (base` f) /\ p = (+g` f)) /\ (t = (.r` f) /\ i = (*v` f))) /\ ((v = (vbase` f) /\ a = (vadd` f)) /\ (s = (vsca` f) /\ h = (ip` f))) /\ A.q e. k A.x e. v A.y e. v A.z e. v ((xhy) e. k /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = (0g` f) -> x = (0vNEW` f)) /\ (i` (xhy)) = (yhx)))))))
3		isphil.1	. . 3 |- Q = Struct(8, f, T. )
4		eleq1 1957	. . . 4 |- (f = W -> (f e. LVec <-> W e. LVec))
5		fveq2 4681	. . . . . . . . . . 11 |- (f = W -> (base` f) = (base` W))
6		isphil.k	. . . . . . . . . . 11 |- K = (base` W)
7	5, 6	syl6eqr 1946	. . . . . . . . . 10 |- (f = W -> (base` f) = K)
8	7	eqeq2d 1895	. . . . . . . . 9 |- (f = W -> (k = (base` f) <-> k = K))
9		fveq2 4681	. . . . . . . . . . 11 |- (f = W -> (+g` f) = (+g` W))
10		isphil.p	. . . . . . . . . . 11 |- P = (+g` W)
11	9, 10	syl6eqr 1946	. . . . . . . . . 10 |- (f = W -> (+g` f) = P)
12	11	eqeq2d 1895	. . . . . . . . 9 |- (f = W -> (p = (+g` f) <-> p = P))
13	8, 12	anbi12d 690	. . . . . . . 8 |- (f = W -> ((k = (base` f) /\ p = (+g` f)) <-> (k = K /\ p = P)))
14		fveq2 4681	. . . . . . . . . . 11 |- (f = W -> (.r` f) = (.r` W))
15		isphil.t	. . . . . . . . . . 11 |- T = (.r` W)
16	14, 15	syl6eqr 1946	. . . . . . . . . 10 |- (f = W -> (.r` f) = T)
17	16	eqeq2d 1895	. . . . . . . . 9 |- (f = W -> (t = (.r` f) <-> t = T))
18		fveq2 4681	. . . . . . . . . . 11 |- (f = W -> (*v` f) = (*v` W))
19		isphil.i	. . . . . . . . . . 11 |- I = (*v` W)
20	18, 19	syl6eqr 1946	. . . . . . . . . 10 |- (f = W -> (*v` f) = I)
21	20	eqeq2d 1895	. . . . . . . . 9 |- (f = W -> (i = (*v` f) <-> i = I))
22	17, 21	anbi12d 690	. . . . . . . 8 |- (f = W -> ((t = (.r` f) /\ i = (*v` f)) <-> (t = T /\ i = I)))
23	13, 22	anbi12d 690	. . . . . . 7 |- (f = W -> (((k = (base` f) /\ p = (+g` f)) /\ (t = (.r` f) /\ i = (*v` f))) <-> ((k = K /\ p = P) /\ (t = T /\ i = I))))
24		fveq2 4681	. . . . . . . . . . 11 |- (f = W -> (vbase` f) = (vbase` W))
25		isphil.v	. . . . . . . . . . 11 |- V = (vbase` W)
26	24, 25	syl6eqr 1946	. . . . . . . . . 10 |- (f = W -> (vbase` f) = V)
27	26	eqeq2d 1895	. . . . . . . . 9 |- (f = W -> (v = (vbase` f) <-> v = V))
28		fveq2 4681	. . . . . . . . . . 11 |- (f = W -> (vadd` f) = (vadd` W))
29		isphil.a	. . . . . . . . . . 11 |- A = (vadd` W)
30	28, 29	syl6eqr 1946	. . . . . . . . . 10 |- (f = W -> (vadd` f) = A)
31	30	eqeq2d 1895	. . . . . . . . 9 |- (f = W -> (a = (vadd` f) <-> a = A))
32	27, 31	anbi12d 690	. . . . . . . 8 |- (f = W -> ((v = (vbase` f) /\ a = (vadd` f)) <-> (v = V /\ a = A)))
33		fveq2 4681	. . . . . . . . . . 11 |- (f = W -> (vsca` f) = (vsca` W))
34		isphil.s	. . . . . . . . . . 11 |- S = (vsca` W)
35	33, 34	syl6eqr 1946	. . . . . . . . . 10 |- (f = W -> (vsca` f) = S)
36	35	eqeq2d 1895	. . . . . . . . 9 |- (f = W -> (s = (vsca` f) <-> s = S))
37		fveq2 4681	. . . . . . . . . . 11 |- (f = W -> (ip` f) = (ip` W))
38		isphil.h	. . . . . . . . . . 11 |- H = (ip` W)
39	37, 38	syl6eqr 1946	. . . . . . . . . 10 |- (f = W -> (ip` f) = H)
40	39	eqeq2d 1895	. . . . . . . . 9 |- (f = W -> (h = (ip` f) <-> h = H))
41	36, 40	anbi12d 690	. . . . . . . 8 |- (f = W -> ((s = (vsca` f) /\ h = (ip` f)) <-> (s = S /\ h = H)))
42	32, 41	anbi12d 690	. . . . . . 7 |- (f = W -> (((v = (vbase` f) /\ a = (vadd` f)) /\ (s = (vsca` f) /\ h = (ip` f))) <-> ((v = V /\ a = A) /\ (s = S /\ h = H))))
43		fveq2 4681	. . . . . . . . . . . . . 14 |- (f = W -> (0g` f) = (0g` W))
44		isphil.10	. . . . . . . . . . . . . 14 |- N = (0g` W)
45	43, 44	syl6eqr 1946	. . . . . . . . . . . . 13 |- (f = W -> (0g` f) = N)
46	45	eqeq2d 1895	. . . . . . . . . . . 12 |- (f = W -> ((xhx) = (0g` f) <-> (xhx) = N))
47		fveq2 4681	. . . . . . . . . . . . . 14 |- (f = W -> (0vNEW` f) = (0vNEW` W))
48		isphil.11	. . . . . . . . . . . . . 14 |- Z = (0vNEW` W)
49	47, 48	syl6eqr 1946	. . . . . . . . . . . . 13 |- (f = W -> (0vNEW` f) = Z)
50	49	eqeq2d 1895	. . . . . . . . . . . 12 |- (f = W -> (x = (0vNEW` f) <-> x = Z))
51	46, 50	imbi12d 688	. . . . . . . . . . 11 |- (f = W -> (((xhx) = (0g` f) -> x = (0vNEW` f)) <-> ((xhx) = N -> x = Z)))
52	51	3anbi2d 1173	. . . . . . . . . 10 |- (f = W -> (((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = (0g` f) -> x = (0vNEW` f)) /\ (i` (xhy)) = (yhx)) <-> ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx))))
53	52	anbi2d 678	. . . . . . . . 9 |- (f = W -> (((xhy) e. k /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = (0g` f) -> x = (0vNEW` f)) /\ (i` (xhy)) = (yhx))) <-> ((xhy) e. k /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx)))))
54	53	2ralbidv 2140	. . . . . . . 8 |- (f = W -> (A.y e. v A.z e. v ((xhy) e. k /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = (0g` f) -> x = (0vNEW` f)) /\ (i` (xhy)) = (yhx))) <-> A.y e. v A.z e. v ((xhy) e. k /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx)))))
55	54	2ralbidv 2140	. . . . . . 7 |- (f = W -> (A.q e. k A.x e. v A.y e. v A.z e. v ((xhy) e. k /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = (0g` f) -> x = (0vNEW` f)) /\ (i` (xhy)) = (yhx))) <-> A.q e. k A.x e. v A.y e. v A.z e. v ((xhy) e. k /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx)))))
56	23, 42, 55	3anbi123d 1168	. . . . . 6 |- (f = W -> ((((k = (base` f) /\ p = (+g` f)) /\ (t = (.r` f) /\ i = (*v` f))) /\ ((v = (vbase` f) /\ a = (vadd` f)) /\ (s = (vsca` f) /\ h = (ip` f))) /\ A.q e. k A.x e. v A.y e. v A.z e. v ((xhy) e. k /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = (0g` f) -> x = (0vNEW` f)) /\ (i` (xhy)) = (yhx)))) <-> (((k = K /\ p = P) /\ (t = T /\ i = I)) /\ ((v = V /\ a = A) /\ (s = S /\ h = H)) /\ A.q e. k A.x e. v A.y e. v A.z e. v ((xhy) e. k /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx))))))
57	56	4exbidv 1661	. . . . 5 |- (f = W -> (E.vE.aE.sE.h(((k = (base` f) /\ p = (+g` f)) /\ (t = (.r` f) /\ i = (*v` f))) /\ ((v = (vbase` f) /\ a = (vadd` f)) /\ (s = (vsca` f) /\ h = (ip` f))) /\ A.q e. k A.x e. v A.y e. v A.z e. v ((xhy) e. k /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = (0g` f) -> x = (0vNEW` f)) /\ (i` (xhy)) = (yhx)))) <-> E.vE.aE.sE.h(((k = K /\ p = P) /\ (t = T /\ i = I)) /\ ((v = V /\ a = A) /\ (s = S /\ h = H)) /\ A.q e. k A.x e. v A.y e. v A.z e. v ((xhy) e. k /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx))))))
58	57	4exbidv 1661	. . . 4 |- (f = W -> (E.kE.pE.tE.iE.vE.aE.sE.h(((k = (base` f) /\ p = (+g` f)) /\ (t = (.r` f) /\ i = (*v` f))) /\ ((v = (vbase` f) /\ a = (vadd` f)) /\ (s = (vsca` f) /\ h = (ip` f))) /\ A.q e. k A.x e. v A.y e. v A.z e. v ((xhy) e. k /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = (0g` f) -> x = (0vNEW` f)) /\ (i` (xhy)) = (yhx)))) <-> E.kE.pE.tE.iE.vE.aE.sE.h(((k = K /\ p = P) /\ (t = T /\ i = I)) /\ ((v = V /\ a = A) /\ (s = S /\ h = H)) /\ A.q e. k A.x e. v A.y e. v A.z e. v ((xhy) e. k /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx))))))
59	4, 58	anbi12d 690	. . 3 |- (f = W -> ((f e. LVec /\ E.kE.pE.tE.iE.vE.aE.sE.h(((k = (base` f) /\ p = (+g` f)) /\ (t = (.r` f) /\ i = (*v` f))) /\ ((v = (vbase` f) /\ a = (vadd` f)) /\ (s = (vsca` f) /\ h = (ip` f))) /\ A.q e. k A.x e. v A.y e. v A.z e. v ((xhy) e. k /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = (0g` f) -> x = (0vNEW` f)) /\ (i` (xhy)) = (yhx))))) <-> (W e. LVec /\ E.kE.pE.tE.iE.vE.aE.sE.h(((k = K /\ p = P) /\ (t = T /\ i = I)) /\ ((v = V /\ a = A) /\ (s = S /\ h = H)) /\ A.q e. k A.x e. v A.y e. v A.z e. v ((xhy) e. k /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx)))))))
60	3, 59	elstr2 16718	. 2 |- (W e. Struct(8, f, (f e. LVec /\ E.kE.pE.tE.iE.vE.aE.sE.h(((k = (base` f) /\ p = (+g` f)) /\ (t = (.r` f) /\ i = (*v` f))) /\ ((v = (vbase` f) /\ a = (vadd` f)) /\ (s = (vsca` f) /\ h = (ip` f))) /\ A.q e. k A.x e. v A.y e. v A.z e. v ((xhy) e. k /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = (0g` f) -> x = (0vNEW` f)) /\ (i` (xhy)) = (yhx)))))) <-> (W e. Q /\ (W e. LVec /\ E.kE.pE.tE.iE.vE.aE.sE.h(((k = K /\ p = P) /\ (t = T /\ i = I)) /\ ((v = V /\ a = A) /\ (s = S /\ h = H)) /\ A.q e. k A.x e. v A.y e. v A.z e. v ((xhy) e. k /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx)))))))
61		3anass 862	. . 3 |- ((W e. Q /\ W e. LVec /\ E.kE.pE.tE.iE.vE.aE.sE.h(((k = K /\ p = P) /\ (t = T /\ i = I)) /\ ((v = V /\ a = A) /\ (s = S /\ h = H)) /\ A.q e. k A.x e. v A.y e. v A.z e. v ((xhy) e. k /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx))))) <-> (W e. Q /\ (W e. LVec /\ E.kE.pE.tE.iE.vE.aE.sE.h(((k = K /\ p = P) /\ (t = T /\ i = I)) /\ ((v = V /\ a = A) /\ (s = S /\ h = H)) /\ A.q e. k A.x e. v A.y e. v A.z e. v ((xhy) e. k /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx)))))))
62		fvex 4689	. . . . . 6 |- (base` W) e. _V
63	6, 62	eqeltri 1967	. . . . 5 |- K e. _V
64		fvex 4689	. . . . . 6 |- (+g` W) e. _V
65	10, 64	eqeltri 1967	. . . . 5 |- P e. _V
66		fvex 4689	. . . . . 6 |- (.r` W) e. _V
67	15, 66	eqeltri 1967	. . . . 5 |- T e. _V
68		fvex 4689	. . . . . 6 |- (*v` W) e. _V
69	19, 68	eqeltri 1967	. . . . 5 |- I e. _V
70		fvex 4689	. . . . . 6 |- (vbase` W) e. _V
71	25, 70	eqeltri 1967	. . . . 5 |- V e. _V
72		fvex 4689	. . . . . 6 |- (vadd` W) e. _V
73	29, 72	eqeltri 1967	. . . . 5 |- A e. _V
74		fvex 4689	. . . . . 6 |- (vsca` W) e. _V
75	34, 74	eqeltri 1967	. . . . 5 |- S e. _V
76		fvex 4689	. . . . . 6 |- (ip` W) e. _V
77	38, 76	eqeltri 1967	. . . . 5 |- H e. _V
78		eleq2 1958	. . . . . . . . 9 |- (k = K -> ((xhy) e. k <-> (xhy) e. K))
79	78	anbi1d 679	. . . . . . . 8 |- (k = K -> (((xhy) e. k /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx))) <-> ((xhy) e. K /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx)))))
80	79	2ralbidv 2140	. . . . . . 7 |- (k = K -> (A.y e. v A.z e. v ((xhy) e. k /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx))) <-> A.y e. v A.z e. v ((xhy) e. K /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx)))))
81	80	ralbidv 2123	. . . . . 6 |- (k = K -> (A.x e. v A.y e. v A.z e. v ((xhy) e. k /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx))) <-> A.x e. v A.y e. v A.z e. v ((xhy) e. K /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx)))))
82	81	raleqbi1dv 2271	. . . . 5 |- (k = K -> (A.q e. k A.x e. v A.y e. v A.z e. v ((xhy) e. k /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx))) <-> A.q e. K A.x e. v A.y e. v A.z e. v ((xhy) e. K /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx)))))
83		opreq 4888	. . . . . . . . . 10 |- (p = P -> ((qt(xhz))p(yhz)) = ((qt(xhz))P(yhz)))
84	83	eqeq2d 1895	. . . . . . . . 9 |- (p = P -> ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) <-> (((qsx)ay)hz) = ((qt(xhz))P(yhz))))
85	84	3anbi1d 1172	. . . . . . . 8 |- (p = P -> (((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx)) <-> ((((qsx)ay)hz) = ((qt(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx))))
86	85	anbi2d 678	. . . . . . 7 |- (p = P -> (((xhy) e. K /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx))) <-> ((xhy) e. K /\ ((((qsx)ay)hz) = ((qt(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx)))))
87	86	2ralbidv 2140	. . . . . 6 |- (p = P -> (A.y e. v A.z e. v ((xhy) e. K /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx))) <-> A.y e. v A.z e. v ((xhy) e. K /\ ((((qsx)ay)hz) = ((qt(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx)))))
88	87	2ralbidv 2140	. . . . 5 |- (p = P -> (A.q e. K A.x e. v A.y e. v A.z e. v ((xhy) e. K /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx))) <-> A.q e. K A.x e. v A.y e. v A.z e. v ((xhy) e. K /\ ((((qsx)ay)hz) = ((qt(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx)))))
89		opreq 4888	. . . . . . . . . . 11 |- (t = T -> (qt(xhz)) = (qT(xhz)))
90	89	opreq1d 4897	. . . . . . . . . 10 |- (t = T -> ((qt(xhz))P(yhz)) = ((qT(xhz))P(yhz)))
91	90	eqeq2d 1895	. . . . . . . . 9 |- (t = T -> ((((qsx)ay)hz) = ((qt(xhz))P(yhz)) <-> (((qsx)ay)hz) = ((qT(xhz))P(yhz))))
92	91	3anbi1d 1172	. . . . . . . 8 |- (t = T -> (((((qsx)ay)hz) = ((qt(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx)) <-> ((((qsx)ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx))))
93	92	anbi2d 678	. . . . . . 7 |- (t = T -> (((xhy) e. K /\ ((((qsx)ay)hz) = ((qt(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx))) <-> ((xhy) e. K /\ ((((qsx)ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx)))))
94	93	2ralbidv 2140	. . . . . 6 |- (t = T -> (A.y e. v A.z e. v ((xhy) e. K /\ ((((qsx)ay)hz) = ((qt(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx))) <-> A.y e. v A.z e. v ((xhy) e. K /\ ((((qsx)ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx)))))
95	94	2ralbidv 2140	. . . . 5 |- (t = T -> (A.q e. K A.x e. v A.y e. v A.z e. v ((xhy) e. K /\ ((((qsx)ay)hz) = ((qt(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx))) <-> A.q e. K A.x e. v A.y e. v A.z e. v ((xhy) e. K /\ ((((qsx)ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx)))))
96		fveq1 4680	. . . . . . . . . 10 |- (i = I -> (i` (xhy)) = (I` (xhy)))
97	96	eqeq1d 1892	. . . . . . . . 9 |- (i = I -> ((i` (xhy)) = (yhx) <-> (I` (xhy)) = (yhx)))
98	97	3anbi3d 1174	. . . . . . . 8 |- (i = I -> (((((qsx)ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx)) <-> ((((qsx)ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx))))
99	98	anbi2d 678	. . . . . . 7 |- (i = I -> (((xhy) e. K /\ ((((qsx)ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx))) <-> ((xhy) e. K /\ ((((qsx)ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx)))))
100	99	2ralbidv 2140	. . . . . 6 |- (i = I -> (A.y e. v A.z e. v ((xhy) e. K /\ ((((qsx)ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx))) <-> A.y e. v A.z e. v ((xhy) e. K /\ ((((qsx)ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx)))))
101	100	2ralbidv 2140	. . . . 5 |- (i = I -> (A.q e. K A.x e. v A.y e. v A.z e. v ((xhy) e. K /\ ((((qsx)ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx))) <-> A.q e. K A.x e. v A.y e. v A.z e. v ((xhy) e. K /\ ((((qsx)ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx)))))
102		raleq 2266	. . . . . . . 8 |- (v = V -> (A.z e. v ((xhy) e. K /\ ((((qsx)ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx))) <-> A.z e. V ((xhy) e. K /\ ((((qsx)ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx)))))
103	102	raleqbi1dv 2271	. . . . . . 7 |- (v = V -> (A.y e. v A.z e. v ((xhy) e. K /\ ((((qsx)ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx))) <-> A.y e. V A.z e. V ((xhy) e. K /\ ((((qsx)ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx)))))
104	103	raleqbi1dv 2271	. . . . . 6 |- (v = V -> (A.x e. v A.y e. v A.z e. v ((xhy) e. K /\ ((((qsx)ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx))) <-> A.x e. V A.y e. V A.z e. V ((xhy) e. K /\ ((((qsx)ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx)))))
105	104	ralbidv 2123	. . . . 5 |- (v = V -> (A.q e. K A.x e. v A.y e. v A.z e. v ((xhy) e. K /\ ((((qsx)ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx))) <-> A.q e. K A.x e. V A.y e. V A.z e. V ((xhy) e. K /\ ((((qsx)ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx)))))
106		opreq 4888	. . . . . . . . . . 11 |- (a = A -> ((qsx)ay) = ((qsx)Ay))
107	106	opreq1d 4897	. . . . . . . . . 10 |- (a = A -> (((qsx)ay)hz) = (((qsx)Ay)hz))
108	107	eqeq1d 1892	. . . . . . . . 9 |- (a = A -> ((((qsx)ay)hz) = ((qT(xhz))P(yhz)) <-> (((qsx)Ay)hz) = ((qT(xhz))P(yhz))))
109	108	3anbi1d 1172	. . . . . . . 8 |- (a = A -> (((((qsx)ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx)) <-> ((((qsx)Ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx))))
110	109	anbi2d 678	. . . . . . 7 |- (a = A -> (((xhy) e. K /\ ((((qsx)ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx))) <-> ((xhy) e. K /\ ((((qsx)Ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx)))))
111	110	2ralbidv 2140	. . . . . 6 |- (a = A -> (A.y e. V A.z e. V ((xhy) e. K /\ ((((qsx)ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx))) <-> A.y e. V A.z e. V ((xhy) e. K /\ ((((qsx)Ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx)))))
112	111	2ralbidv 2140	. . . . 5 |- (a = A -> (A.q e. K A.x e. V A.y e. V A.z e. V ((xhy) e. K /\ ((((qsx)ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx))) <-> A.q e. K A.x e. V A.y e. V A.z e. V ((xhy) e. K /\ ((((qsx)Ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx)))))
113		opreq 4888	. . . . . . . . . . . 12 |- (s = S -> (qsx) = (qSx))
114	113	opreq1d 4897	. . . . . . . . . . 11 |- (s = S -> ((qsx)Ay) = ((qSx)Ay))
115	114	opreq1d 4897	. . . . . . . . . 10 |- (s = S -> (((qsx)Ay)hz) = (((qSx)Ay)hz))
116	115	eqeq1d 1892	. . . . . . . . 9 |- (s = S -> ((((qsx)Ay)hz) = ((qT(xhz))P(yhz)) <-> (((qSx)Ay)hz) = ((qT(xhz))P(yhz))))
117	116	3anbi1d 1172	. . . . . . . 8 |- (s = S -> (((((qsx)Ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx)) <-> ((((qSx)Ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx))))
118	117	anbi2d 678	. . . . . . 7 |- (s = S -> (((xhy) e. K /\ ((((qsx)Ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx))) <-> ((xhy) e. K /\ ((((qSx)Ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx)))))
119	118	2ralbidv 2140	. . . . . 6 |- (s = S -> (A.y e. V A.z e. V ((xhy) e. K /\ ((((qsx)Ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx))) <-> A.y e. V A.z e. V ((xhy) e. K /\ ((((qSx)Ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx)))))
120	119	2ralbidv 2140	. . . . 5 |- (s = S -> (A.q e. K A.x e. V A.y e. V A.z e. V ((xhy) e. K /\ ((((qsx)Ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx))) <-> A.q e. K A.x e. V A.y e. V A.z e. V ((xhy) e. K /\ ((((qSx)Ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx)))))
121		opreq 4888	. . . . . . . . 9 |- (h = H -> (xhy) = (xHy))
122	121	eleq1d 1963	. . . . . . . 8 |- (h = H -> ((xhy) e. K <-> (xHy) e. K))
123		opreq 4888	. . . . . . . . . 10 |- (h = H -> (((qSx)Ay)hz) = (((qSx)Ay)Hz))
124		opreq 4888	. . . . . . . . . . . 12 |- (h = H -> (xhz) = (xHz))
125	124	opreq2d 4898	. . . . . . . . . . 11 |- (h = H -> (qT(xhz)) = (qT(xHz)))
126		opreq 4888	. . . . . . . . . . 11 |- (h = H -> (yhz) = (yHz))
127	125, 126	opreq12d 4900	. . . . . . . . . 10 |- (h = H -> ((qT(xhz))P(yhz)) = ((qT(xHz))P(yHz)))
128	123, 127	eqeq12d 1899	. . . . . . . . 9 |- (h = H -> ((((qSx)Ay)hz) = ((qT(xhz))P(yhz)) <-> (((qSx)Ay)Hz) = ((qT(xHz))P(yHz))))
129		opreq 4888	. . . . . . . . . . 11 |- (h = H -> (xhx) = (xHx))
130	129	eqeq1d 1892	. . . . . . . . . 10 |- (h = H -> ((xhx) = N <-> (xHx) = N))
131	130	imbi1d 675	. . . . . . . . 9 |- (h = H -> (((xhx) = N -> x = Z) <-> ((xHx) = N -> x = Z)))
132	121	fveq2d 4685	. . . . . . . . . 10 |- (h = H -> (I` (xhy)) = (I` (xHy)))
133		opreq 4888	. . . . . . . . . 10 |- (h = H -> (yhx) = (yHx))
134	132, 133	eqeq12d 1899	. . . . . . . . 9 |- (h = H -> ((I` (xhy)) = (yhx) <-> (I` (xHy)) = (yHx)))
135	128, 131, 134	3anbi123d 1168	. . . . . . . 8 |- (h = H -> (((((qSx)Ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx)) <-> ((((qSx)Ay)Hz) = ((qT(xHz))P(yHz)) /\ ((xHx) = N -> x = Z) /\ (I` (xHy)) = (yHx))))
136	122, 135	anbi12d 690	. . . . . . 7 |- (h = H -> (((xhy) e. K /\ ((((qSx)Ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx))) <-> ((xHy) e. K /\ ((((qSx)Ay)Hz) = ((qT(xHz))P(yHz)) /\ ((xHx) = N -> x = Z) /\ (I` (xHy)) = (yHx)))))
137	136	2ralbidv 2140	. . . . . 6 |- (h = H -> (A.y e. V A.z e. V ((xhy) e. K /\ ((((qSx)Ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx))) <-> A.y e. V A.z e. V ((xHy) e. K /\ ((((qSx)Ay)Hz) = ((qT(xHz))P(yHz)) /\ ((xHx) = N -> x = Z) /\ (I` (xHy)) = (yHx)))))
138	137	2ralbidv 2140	. . . . 5 |- (h = H -> (A.q e. K A.x e. V A.y e. V A.z e. V ((xhy) e. K /\ ((((qSx)Ay)hz) = ((qT(xhz))P(yhz)) /\ ((xhx) = N -> x = Z) /\ (I` (xhy)) = (yhx))) <-> A.q e. K A.x e. V A.y e. V A.z e. V ((xHy) e. K /\ ((((qSx)Ay)Hz) = ((qT(xHz))P(yHz)) /\ ((xHx) = N -> x = Z) /\ (I` (xHy)) = (yHx)))))
139	63, 65, 67, 69, 71, 73, 75, 77, 82, 88, 95, 101, 105, 112, 120, 138	ceqsex8v 2333	. . . 4 |- (E.kE.pE.tE.iE.vE.aE.sE.h(((k = K /\ p = P) /\ (t = T /\ i = I)) /\ ((v = V /\ a = A) /\ (s = S /\ h = H)) /\ A.q e. k A.x e. v A.y e. v A.z e. v ((xhy) e. k /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx)))) <-> A.q e. K A.x e. V A.y e. V A.z e. V ((xHy) e. K /\ ((((qSx)Ay)Hz) = ((qT(xHz))P(yHz)) /\ ((xHx) = N -> x = Z) /\ (I` (xHy)) = (yHx))))
140	139	3anbi3i 1060	. . 3 |- ((W e. Q /\ W e. LVec /\ E.kE.pE.tE.iE.vE.aE.sE.h(((k = K /\ p = P) /\ (t = T /\ i = I)) /\ ((v = V /\ a = A) /\ (s = S /\ h = H)) /\ A.q e. k A.x e. v A.y e. v A.z e. v ((xhy) e. k /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx))))) <-> (W e. Q /\ W e. LVec /\ A.q e. K A.x e. V A.y e. V A.z e. V ((xHy) e. K /\ ((((qSx)Ay)Hz) = ((qT(xHz))P(yHz)) /\ ((xHx) = N -> x = Z) /\ (I` (xHy)) = (yHx)))))
141	61, 140	bitr3i 192	. 2 |- ((W e. Q /\ (W e. LVec /\ E.kE.pE.tE.iE.vE.aE.sE.h(((k = K /\ p = P) /\ (t = T /\ i = I)) /\ ((v = V /\ a = A) /\ (s = S /\ h = H)) /\ A.q e. k A.x e. v A.y e. v A.z e. v ((xhy) e. k /\ ((((qsx)ay)hz) = ((qt(xhz))p(yhz)) /\ ((xhx) = N -> x = Z) /\ (i` (xhy)) = (yhx)))))) <-> (W e. Q /\ W e. LVec /\ A.q e. K A.x e. V A.y e. V A.z e. V ((xHy) e. K /\ ((((qSx)Ay)Hz) = ((qT(xHz))P(yHz)) /\ ((xHx) = N -> x = Z) /\ (I` (xHy)) = (yHx)))))
142	2, 60, 141	3bitri 194	1 |- (W e. PreHil <-> (W e. Q /\ W e. LVec /\ A.q e. K A.x e. V A.y e. V A.z e. V ((xHy) e. K /\ ((((qSx)Ay)Hz) = ((qT(xHz))P(yHz)) /\ ((xHx) = N -> x = Z) /\ (I` (xHy)) = (yHx)))))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   T. wtru 1260   = wceq 1298   e. wcel 1300  E.wex 1326  A.wral 2105  _Vcvv 2292  ` cfv 3998  (class class class)co 4884  8c8 7151  Structcstru 16707  basecbs 16758  +_gcplusg 17080  0_gc0g 17082  ._rcmulr 17085  *_vcstv 17172  vbasecvbase 17180  vaddcvadd 17181  vscacvsca 17182  LVecclvec 17183  0vNEWczv 17189  ipcipr 17191  PreHilcprehil 17192

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-tru 1262  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-fv 4014  df-opr 4886  df-struct 16708  df-prehil 17194

Copyright terms: Public domain