Theorem islvec 17188

Description: The predicate "is a left vector space" (over a *-division ring)

Hypotheses

Ref	Expression
islvec.1	|- Q = Struct(7, f, T. )
islvec.k	|- K = (base` W)
islvec.p	|- P = (+g` W)
islvec.t	|- T = (.r` W)
islvec.v	|- V = (vbase` W)
islvec.a	|- A = (vadd` W)
islvec.s	|- S = (vsca` W)
islvec.u	|- U = (1rNEW` W)
islvec.9	|- G = {<.1, V>., <.2, A>.}

Assertion

Ref	Expression
islvec	|- (W e. LVec <-> (W e. Q /\ (W e. DivRing* /\ G e. AbelNEW /\ A.q e. K A.r e. K A.x e. V A.w e. V (((rSw) e. V /\ (rS(wAx)) = ((rSw)A(rSx)) /\ ((qPr)Sw) = ((qSw)A(rSw))) /\ ((qS(rSw)) = ((qTr)Sw) /\ (USw) = w)))))

Distinct variable groups:   f,q,r,w,x,A   f,K,q,r   P,f,q,r,w,x   S,f,q,r,w,x   T,f,q,r,w,x   U,f   f,V,q,r,w,x   f,W,q,r,w,x

Proof of Theorem islvec

Step	Hyp	Ref	Expression
1		df-lvec 17187	. . 3 |- LVec = Struct(7, f, (f e. DivRing* /\ E.kE.pE.tE.vE.aE.s((k = (base` f) /\ p = (+g` f) /\ t = (.r` f)) /\ (v = (vbase` f) /\ a = (vadd` f) /\ s = (vsca` f)) /\ ({<.1, v>., <.2, a>.} e. AbelNEW /\ A.q e. k A.r e. k A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ ((1rNEW` f)sw) = w))))))
2	1	eleq2i 1961	. 2 |- (W e. LVec <-> W e. Struct(7, f, (f e. DivRing* /\ E.kE.pE.tE.vE.aE.s((k = (base` f) /\ p = (+g` f) /\ t = (.r` f)) /\ (v = (vbase` f) /\ a = (vadd` f) /\ s = (vsca` f)) /\ ({<.1, v>., <.2, a>.} e. AbelNEW /\ A.q e. k A.r e. k A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ ((1rNEW` f)sw) = w)))))))
3		islvec.1	. . 3 |- Q = Struct(7, f, T. )
4		eleq1 1957	. . . 4 |- (f = W -> (f e. DivRing* <-> W e. DivRing*))
5		fveq2 4681	. . . . . . . . . 10 |- (f = W -> (base` f) = (base` W))
6		islvec.k	. . . . . . . . . 10 |- K = (base` W)
7	5, 6	syl6eqr 1946	. . . . . . . . 9 |- (f = W -> (base` f) = K)
8	7	eqeq2d 1895	. . . . . . . 8 |- (f = W -> (k = (base` f) <-> k = K))
9		fveq2 4681	. . . . . . . . . 10 |- (f = W -> (+g` f) = (+g` W))
10		islvec.p	. . . . . . . . . 10 |- P = (+g` W)
11	9, 10	syl6eqr 1946	. . . . . . . . 9 |- (f = W -> (+g` f) = P)
12	11	eqeq2d 1895	. . . . . . . 8 |- (f = W -> (p = (+g` f) <-> p = P))
13		fveq2 4681	. . . . . . . . . 10 |- (f = W -> (.r` f) = (.r` W))
14		islvec.t	. . . . . . . . . 10 |- T = (.r` W)
15	13, 14	syl6eqr 1946	. . . . . . . . 9 |- (f = W -> (.r` f) = T)
16	15	eqeq2d 1895	. . . . . . . 8 |- (f = W -> (t = (.r` f) <-> t = T))
17	8, 12, 16	3anbi123d 1168	. . . . . . 7 |- (f = W -> ((k = (base` f) /\ p = (+g` f) /\ t = (.r` f)) <-> (k = K /\ p = P /\ t = T)))
18		fveq2 4681	. . . . . . . . . 10 |- (f = W -> (vbase` f) = (vbase` W))
19		islvec.v	. . . . . . . . . 10 |- V = (vbase` W)
20	18, 19	syl6eqr 1946	. . . . . . . . 9 |- (f = W -> (vbase` f) = V)
21	20	eqeq2d 1895	. . . . . . . 8 |- (f = W -> (v = (vbase` f) <-> v = V))
22		fveq2 4681	. . . . . . . . . 10 |- (f = W -> (vadd` f) = (vadd` W))
23		islvec.a	. . . . . . . . . 10 |- A = (vadd` W)
24	22, 23	syl6eqr 1946	. . . . . . . . 9 |- (f = W -> (vadd` f) = A)
25	24	eqeq2d 1895	. . . . . . . 8 |- (f = W -> (a = (vadd` f) <-> a = A))
26		fveq2 4681	. . . . . . . . . 10 |- (f = W -> (vsca` f) = (vsca` W))
27		islvec.s	. . . . . . . . . 10 |- S = (vsca` W)
28	26, 27	syl6eqr 1946	. . . . . . . . 9 |- (f = W -> (vsca` f) = S)
29	28	eqeq2d 1895	. . . . . . . 8 |- (f = W -> (s = (vsca` f) <-> s = S))
30	21, 25, 29	3anbi123d 1168	. . . . . . 7 |- (f = W -> ((v = (vbase` f) /\ a = (vadd` f) /\ s = (vsca` f)) <-> (v = V /\ a = A /\ s = S)))
31		fveq2 4681	. . . . . . . . . . . . . . 15 |- (f = W -> (1rNEW` f) = (1rNEW` W))
32		islvec.u	. . . . . . . . . . . . . . 15 |- U = (1rNEW` W)
33	31, 32	syl6eqr 1946	. . . . . . . . . . . . . 14 |- (f = W -> (1rNEW` f) = U)
34	33	opreq1d 4897	. . . . . . . . . . . . 13 |- (f = W -> ((1rNEW` f)sw) = (Usw))
35	34	eqeq1d 1892	. . . . . . . . . . . 12 |- (f = W -> (((1rNEW` f)sw) = w <-> (Usw) = w))
36	35	anbi2d 678	. . . . . . . . . . 11 |- (f = W -> (((qs(rsw)) = ((qtr)sw) /\ ((1rNEW` f)sw) = w) <-> ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w)))
37	36	anbi2d 678	. . . . . . . . . 10 |- (f = W -> ((((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ ((1rNEW` f)sw) = w)) <-> (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w))))
38	37	2ralbidv 2140	. . . . . . . . 9 |- (f = W -> (A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ ((1rNEW` f)sw) = w)) <-> A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w))))
39	38	2ralbidv 2140	. . . . . . . 8 |- (f = W -> (A.q e. k A.r e. k A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ ((1rNEW` f)sw) = w)) <-> A.q e. k A.r e. k A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w))))
40	39	anbi2d 678	. . . . . . 7 |- (f = W -> (({<.1, v>., <.2, a>.} e. AbelNEW /\ A.q e. k A.r e. k A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ ((1rNEW` f)sw) = w))) <-> ({<.1, v>., <.2, a>.} e. AbelNEW /\ A.q e. k A.r e. k A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w)))))
41	17, 30, 40	3anbi123d 1168	. . . . . 6 |- (f = W -> (((k = (base` f) /\ p = (+g` f) /\ t = (.r` f)) /\ (v = (vbase` f) /\ a = (vadd` f) /\ s = (vsca` f)) /\ ({<.1, v>., <.2, a>.} e. AbelNEW /\ A.q e. k A.r e. k A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ ((1rNEW` f)sw) = w)))) <-> ((k = K /\ p = P /\ t = T) /\ (v = V /\ a = A /\ s = S) /\ ({<.1, v>., <.2, a>.} e. AbelNEW /\ A.q e. k A.r e. k A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w))))))
42	41	3exbidv 1660	. . . . 5 |- (f = W -> (E.vE.aE.s((k = (base` f) /\ p = (+g` f) /\ t = (.r` f)) /\ (v = (vbase` f) /\ a = (vadd` f) /\ s = (vsca` f)) /\ ({<.1, v>., <.2, a>.} e. AbelNEW /\ A.q e. k A.r e. k A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ ((1rNEW` f)sw) = w)))) <-> E.vE.aE.s((k = K /\ p = P /\ t = T) /\ (v = V /\ a = A /\ s = S) /\ ({<.1, v>., <.2, a>.} e. AbelNEW /\ A.q e. k A.r e. k A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w))))))
43	42	3exbidv 1660	. . . 4 |- (f = W -> (E.kE.pE.tE.vE.aE.s((k = (base` f) /\ p = (+g` f) /\ t = (.r` f)) /\ (v = (vbase` f) /\ a = (vadd` f) /\ s = (vsca` f)) /\ ({<.1, v>., <.2, a>.} e. AbelNEW /\ A.q e. k A.r e. k A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ ((1rNEW` f)sw) = w)))) <-> E.kE.pE.tE.vE.aE.s((k = K /\ p = P /\ t = T) /\ (v = V /\ a = A /\ s = S) /\ ({<.1, v>., <.2, a>.} e. AbelNEW /\ A.q e. k A.r e. k A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w))))))
44	4, 43	anbi12d 690	. . 3 |- (f = W -> ((f e. DivRing* /\ E.kE.pE.tE.vE.aE.s((k = (base` f) /\ p = (+g` f) /\ t = (.r` f)) /\ (v = (vbase` f) /\ a = (vadd` f) /\ s = (vsca` f)) /\ ({<.1, v>., <.2, a>.} e. AbelNEW /\ A.q e. k A.r e. k A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ ((1rNEW` f)sw) = w))))) <-> (W e. DivRing* /\ E.kE.pE.tE.vE.aE.s((k = K /\ p = P /\ t = T) /\ (v = V /\ a = A /\ s = S) /\ ({<.1, v>., <.2, a>.} e. AbelNEW /\ A.q e. k A.r e. k A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w)))))))
45	3, 44	elstr2 16718	. 2 |- (W e. Struct(7, f, (f e. DivRing* /\ E.kE.pE.tE.vE.aE.s((k = (base` f) /\ p = (+g` f) /\ t = (.r` f)) /\ (v = (vbase` f) /\ a = (vadd` f) /\ s = (vsca` f)) /\ ({<.1, v>., <.2, a>.} e. AbelNEW /\ A.q e. k A.r e. k A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ ((1rNEW` f)sw) = w)))))) <-> (W e. Q /\ (W e. DivRing* /\ E.kE.pE.tE.vE.aE.s((k = K /\ p = P /\ t = T) /\ (v = V /\ a = A /\ s = S) /\ ({<.1, v>., <.2, a>.} e. AbelNEW /\ A.q e. k A.r e. k A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w)))))))
46		fvex 4689	. . . . . . 7 |- (base` W) e. _V
47	6, 46	eqeltri 1967	. . . . . 6 |- K e. _V
48		fvex 4689	. . . . . . 7 |- (+g` W) e. _V
49	10, 48	eqeltri 1967	. . . . . 6 |- P e. _V
50		fvex 4689	. . . . . . 7 |- (.r` W) e. _V
51	14, 50	eqeltri 1967	. . . . . 6 |- T e. _V
52		fvex 4689	. . . . . . 7 |- (vbase` W) e. _V
53	19, 52	eqeltri 1967	. . . . . 6 |- V e. _V
54		fvex 4689	. . . . . . 7 |- (vadd` W) e. _V
55	23, 54	eqeltri 1967	. . . . . 6 |- A e. _V
56		fvex 4689	. . . . . . 7 |- (vsca` W) e. _V
57	27, 56	eqeltri 1967	. . . . . 6 |- S e. _V
58		id 73	. . . . . . . 8 |- (k = K -> k = K)
59		raleq 2266	. . . . . . . 8 |- (k = K -> (A.r e. k A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w)) <-> A.r e. K A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w))))
60	58, 59	raleqbidv 2274	. . . . . . 7 |- (k = K -> (A.q e. k A.r e. k A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w)) <-> A.q e. K A.r e. K A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w))))
61	60	anbi2d 678	. . . . . 6 |- (k = K -> (({<.1, v>., <.2, a>.} e. AbelNEW /\ A.q e. k A.r e. k A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w))) <-> ({<.1, v>., <.2, a>.} e. AbelNEW /\ A.q e. K A.r e. K A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w)))))
62		biidd 188	. . . . . . . . . . 11 |- (p = P -> ((rsw) e. v <-> (rsw) e. v))
63		biidd 188	. . . . . . . . . . 11 |- (p = P -> ((rs(wax)) = ((rsw)a(rsx)) <-> (rs(wax)) = ((rsw)a(rsx))))
64		opreq 4888	. . . . . . . . . . . . 13 |- (p = P -> (qpr) = (qPr))
65	64	opreq1d 4897	. . . . . . . . . . . 12 |- (p = P -> ((qpr)sw) = ((qPr)sw))
66	65	eqeq1d 1892	. . . . . . . . . . 11 |- (p = P -> (((qpr)sw) = ((qsw)a(rsw)) <-> ((qPr)sw) = ((qsw)a(rsw))))
67	62, 63, 66	3anbi123d 1168	. . . . . . . . . 10 |- (p = P -> (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) <-> ((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qPr)sw) = ((qsw)a(rsw)))))
68	67	anbi1d 679	. . . . . . . . 9 |- (p = P -> ((((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w)) <-> (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qPr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w))))
69	68	2ralbidv 2140	. . . . . . . 8 |- (p = P -> (A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w)) <-> A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qPr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w))))
70	69	2ralbidv 2140	. . . . . . 7 |- (p = P -> (A.q e. K A.r e. K A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w)) <-> A.q e. K A.r e. K A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qPr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w))))
71	70	anbi2d 678	. . . . . 6 |- (p = P -> (({<.1, v>., <.2, a>.} e. AbelNEW /\ A.q e. K A.r e. K A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w))) <-> ({<.1, v>., <.2, a>.} e. AbelNEW /\ A.q e. K A.r e. K A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qPr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w)))))
72		opreq 4888	. . . . . . . . . . . . 13 |- (t = T -> (qtr) = (qTr))
73	72	opreq1d 4897	. . . . . . . . . . . 12 |- (t = T -> ((qtr)sw) = ((qTr)sw))
74	73	eqeq2d 1895	. . . . . . . . . . 11 |- (t = T -> ((qs(rsw)) = ((qtr)sw) <-> (qs(rsw)) = ((qTr)sw)))
75	74	anbi1d 679	. . . . . . . . . 10 |- (t = T -> (((qs(rsw)) = ((qtr)sw) /\ (Usw) = w) <-> ((qs(rsw)) = ((qTr)sw) /\ (Usw) = w)))
76	75	anbi2d 678	. . . . . . . . 9 |- (t = T -> ((((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qPr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w)) <-> (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qPr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qTr)sw) /\ (Usw) = w))))
77	76	2ralbidv 2140	. . . . . . . 8 |- (t = T -> (A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qPr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w)) <-> A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qPr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qTr)sw) /\ (Usw) = w))))
78	77	2ralbidv 2140	. . . . . . 7 |- (t = T -> (A.q e. K A.r e. K A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qPr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w)) <-> A.q e. K A.r e. K A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qPr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qTr)sw) /\ (Usw) = w))))
79	78	anbi2d 678	. . . . . 6 |- (t = T -> (({<.1, v>., <.2, a>.} e. AbelNEW /\ A.q e. K A.r e. K A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qPr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w))) <-> ({<.1, v>., <.2, a>.} e. AbelNEW /\ A.q e. K A.r e. K A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qPr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qTr)sw) /\ (Usw) = w)))))
80		opeq2 3159	. . . . . . . . 9 |- (v = V -> <.1, v>. = <.1, V>.)
81		preq1 3098	. . . . . . . . 9 |- (<.1, v>. = <.1, V>. -> {<.1, v>., <.2, a>.} = {<.1, V>., <.2, a>.})
82	80, 81	syl 12	. . . . . . . 8 |- (v = V -> {<.1, v>., <.2, a>.} = {<.1, V>., <.2, a>.})
83	82	eleq1d 1963	. . . . . . 7 |- (v = V -> ({<.1, v>., <.2, a>.} e. AbelNEW <-> {<.1, V>., <.2, a>.} e. AbelNEW))
84		id 73	. . . . . . . . 9 |- (v = V -> v = V)
85		eleq2 1958	. . . . . . . . . . . 12 |- (v = V -> ((rsw) e. v <-> (rsw) e. V))
86		biidd 188	. . . . . . . . . . . 12 |- (v = V -> ((rs(wax)) = ((rsw)a(rsx)) <-> (rs(wax)) = ((rsw)a(rsx))))
87		biidd 188	. . . . . . . . . . . 12 |- (v = V -> (((qPr)sw) = ((qsw)a(rsw)) <-> ((qPr)sw) = ((qsw)a(rsw))))
88	85, 86, 87	3anbi123d 1168	. . . . . . . . . . 11 |- (v = V -> (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qPr)sw) = ((qsw)a(rsw))) <-> ((rsw) e. V /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qPr)sw) = ((qsw)a(rsw)))))
89	88	anbi1d 679	. . . . . . . . . 10 |- (v = V -> ((((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qPr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qTr)sw) /\ (Usw) = w)) <-> (((rsw) e. V /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qPr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qTr)sw) /\ (Usw) = w))))
90	84, 89	raleqbidv 2274	. . . . . . . . 9 |- (v = V -> (A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qPr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qTr)sw) /\ (Usw) = w)) <-> A.w e. V (((rsw) e. V /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qPr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qTr)sw) /\ (Usw) = w))))
91	84, 90	raleqbidv 2274	. . . . . . . 8 |- (v = V -> (A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qPr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qTr)sw) /\ (Usw) = w)) <-> A.x e. V A.w e. V (((rsw) e. V /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qPr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qTr)sw) /\ (Usw) = w))))
92	91	2ralbidv 2140	. . . . . . 7 |- (v = V -> (A.q e. K A.r e. K A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qPr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qTr)sw) /\ (Usw) = w)) <-> A.q e. K A.r e. K A.x e. V A.w e. V (((rsw) e. V /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qPr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qTr)sw) /\ (Usw) = w))))
93	83, 92	anbi12d 690	. . . . . 6 |- (v = V -> (({<.1, v>., <.2, a>.} e. AbelNEW /\ A.q e. K A.r e. K A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qPr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qTr)sw) /\ (Usw) = w))) <-> ({<.1, V>., <.2, a>.} e. AbelNEW /\ A.q e. K A.r e. K A.x e. V A.w e. V (((rsw) e. V /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qPr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qTr)sw) /\ (Usw) = w)))))
94		opeq2 3159	. . . . . . . . . 10 |- (a = A -> <.2, a>. = <.2, A>.)
95		preq2 3099	. . . . . . . . . 10 |- (<.2, a>. = <.2, A>. -> {<.1, V>., <.2, a>.} = {<.1, V>., <.2, A>.})
96	94, 95	syl 12	. . . . . . . . 9 |- (a = A -> {<.1, V>., <.2, a>.} = {<.1, V>., <.2, A>.})
97		islvec.9	. . . . . . . . 9 |- G = {<.1, V>., <.2, A>.}
98	96, 97	syl6eqr 1946	. . . . . . . 8 |- (a = A -> {<.1, V>., <.2, a>.} = G)
99	98	eleq1d 1963	. . . . . . 7 |- (a = A -> ({<.1, V>., <.2, a>.} e. AbelNEW <-> G e. AbelNEW))
100		biidd 188	. . . . . . . . . . 11 |- (a = A -> ((rsw) e. V <-> (rsw) e. V))
101		opreq 4888	. . . . . . . . . . . . 13 |- (a = A -> (wax) = (wAx))
102	101	opreq2d 4898	. . . . . . . . . . . 12 |- (a = A -> (rs(wax)) = (rs(wAx)))
103		opreq 4888	. . . . . . . . . . . 12 |- (a = A -> ((rsw)a(rsx)) = ((rsw)A(rsx)))
104	102, 103	eqeq12d 1899	. . . . . . . . . . 11 |- (a = A -> ((rs(wax)) = ((rsw)a(rsx)) <-> (rs(wAx)) = ((rsw)A(rsx))))
105		opreq 4888	. . . . . . . . . . . 12 |- (a = A -> ((qsw)a(rsw)) = ((qsw)A(rsw)))
106	105	eqeq2d 1895	. . . . . . . . . . 11 |- (a = A -> (((qPr)sw) = ((qsw)a(rsw)) <-> ((qPr)sw) = ((qsw)A(rsw))))
107	100, 104, 106	3anbi123d 1168	. . . . . . . . . 10 |- (a = A -> (((rsw) e. V /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qPr)sw) = ((qsw)a(rsw))) <-> ((rsw) e. V /\ (rs(wAx)) = ((rsw)A(rsx)) /\ ((qPr)sw) = ((qsw)A(rsw)))))
108	107	anbi1d 679	. . . . . . . . 9 |- (a = A -> ((((rsw) e. V /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qPr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qTr)sw) /\ (Usw) = w)) <-> (((rsw) e. V /\ (rs(wAx)) = ((rsw)A(rsx)) /\ ((qPr)sw) = ((qsw)A(rsw))) /\ ((qs(rsw)) = ((qTr)sw) /\ (Usw) = w))))
109	108	2ralbidv 2140	. . . . . . . 8 |- (a = A -> (A.x e. V A.w e. V (((rsw) e. V /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qPr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qTr)sw) /\ (Usw) = w)) <-> A.x e. V A.w e. V (((rsw) e. V /\ (rs(wAx)) = ((rsw)A(rsx)) /\ ((qPr)sw) = ((qsw)A(rsw))) /\ ((qs(rsw)) = ((qTr)sw) /\ (Usw) = w))))
110	109	2ralbidv 2140	. . . . . . 7 |- (a = A -> (A.q e. K A.r e. K A.x e. V A.w e. V (((rsw) e. V /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qPr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qTr)sw) /\ (Usw) = w)) <-> A.q e. K A.r e. K A.x e. V A.w e. V (((rsw) e. V /\ (rs(wAx)) = ((rsw)A(rsx)) /\ ((qPr)sw) = ((qsw)A(rsw))) /\ ((qs(rsw)) = ((qTr)sw) /\ (Usw) = w))))
111	99, 110	anbi12d 690	. . . . . 6 |- (a = A -> (({<.1, V>., <.2, a>.} e. AbelNEW /\ A.q e. K A.r e. K A.x e. V A.w e. V (((rsw) e. V /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qPr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qTr)sw) /\ (Usw) = w))) <-> (G e. AbelNEW /\ A.q e. K A.r e. K A.x e. V A.w e. V (((rsw) e. V /\ (rs(wAx)) = ((rsw)A(rsx)) /\ ((qPr)sw) = ((qsw)A(rsw))) /\ ((qs(rsw)) = ((qTr)sw) /\ (Usw) = w)))))
112		opreq 4888	. . . . . . . . . . . 12 |- (s = S -> (rsw) = (rSw))
113	112	eleq1d 1963	. . . . . . . . . . 11 |- (s = S -> ((rsw) e. V <-> (rSw) e. V))
114		opreq 4888	. . . . . . . . . . . 12 |- (s = S -> (rs(wAx)) = (rS(wAx)))
115		opreq 4888	. . . . . . . . . . . . 13 |- (s = S -> (rsx) = (rSx))
116	112, 115	opreq12d 4900	. . . . . . . . . . . 12 |- (s = S -> ((rsw)A(rsx)) = ((rSw)A(rSx)))
117	114, 116	eqeq12d 1899	. . . . . . . . . . 11 |- (s = S -> ((rs(wAx)) = ((rsw)A(rsx)) <-> (rS(wAx)) = ((rSw)A(rSx))))
118		opreq 4888	. . . . . . . . . . . 12 |- (s = S -> ((qPr)sw) = ((qPr)Sw))
119		opreq 4888	. . . . . . . . . . . . 13 |- (s = S -> (qsw) = (qSw))
120	119, 112	opreq12d 4900	. . . . . . . . . . . 12 |- (s = S -> ((qsw)A(rsw)) = ((qSw)A(rSw)))
121	118, 120	eqeq12d 1899	. . . . . . . . . . 11 |- (s = S -> (((qPr)sw) = ((qsw)A(rsw)) <-> ((qPr)Sw) = ((qSw)A(rSw))))
122	113, 117, 121	3anbi123d 1168	. . . . . . . . . 10 |- (s = S -> (((rsw) e. V /\ (rs(wAx)) = ((rsw)A(rsx)) /\ ((qPr)sw) = ((qsw)A(rsw))) <-> ((rSw) e. V /\ (rS(wAx)) = ((rSw)A(rSx)) /\ ((qPr)Sw) = ((qSw)A(rSw)))))
123		id 73	. . . . . . . . . . . . 13 |- (s = S -> s = S)
124		eqidd 1885	. . . . . . . . . . . . 13 |- (s = S -> q = q)
125	123, 124, 112	opreq123d 10153	. . . . . . . . . . . 12 |- (s = S -> (qs(rsw)) = (qS(rSw)))
126		opreq 4888	. . . . . . . . . . . 12 |- (s = S -> ((qTr)sw) = ((qTr)Sw))
127	125, 126	eqeq12d 1899	. . . . . . . . . . 11 |- (s = S -> ((qs(rsw)) = ((qTr)sw) <-> (qS(rSw)) = ((qTr)Sw)))
128		opreq 4888	. . . . . . . . . . . 12 |- (s = S -> (Usw) = (USw))
129	128	eqeq1d 1892	. . . . . . . . . . 11 |- (s = S -> ((Usw) = w <-> (USw) = w))
130	127, 129	anbi12d 690	. . . . . . . . . 10 |- (s = S -> (((qs(rsw)) = ((qTr)sw) /\ (Usw) = w) <-> ((qS(rSw)) = ((qTr)Sw) /\ (USw) = w)))
131	122, 130	anbi12d 690	. . . . . . . . 9 |- (s = S -> ((((rsw) e. V /\ (rs(wAx)) = ((rsw)A(rsx)) /\ ((qPr)sw) = ((qsw)A(rsw))) /\ ((qs(rsw)) = ((qTr)sw) /\ (Usw) = w)) <-> (((rSw) e. V /\ (rS(wAx)) = ((rSw)A(rSx)) /\ ((qPr)Sw) = ((qSw)A(rSw))) /\ ((qS(rSw)) = ((qTr)Sw) /\ (USw) = w))))
132	131	2ralbidv 2140	. . . . . . . 8 |- (s = S -> (A.x e. V A.w e. V (((rsw) e. V /\ (rs(wAx)) = ((rsw)A(rsx)) /\ ((qPr)sw) = ((qsw)A(rsw))) /\ ((qs(rsw)) = ((qTr)sw) /\ (Usw) = w)) <-> A.x e. V A.w e. V (((rSw) e. V /\ (rS(wAx)) = ((rSw)A(rSx)) /\ ((qPr)Sw) = ((qSw)A(rSw))) /\ ((qS(rSw)) = ((qTr)Sw) /\ (USw) = w))))
133	132	2ralbidv 2140	. . . . . . 7 |- (s = S -> (A.q e. K A.r e. K A.x e. V A.w e. V (((rsw) e. V /\ (rs(wAx)) = ((rsw)A(rsx)) /\ ((qPr)sw) = ((qsw)A(rsw))) /\ ((qs(rsw)) = ((qTr)sw) /\ (Usw) = w)) <-> A.q e. K A.r e. K A.x e. V A.w e. V (((rSw) e. V /\ (rS(wAx)) = ((rSw)A(rSx)) /\ ((qPr)Sw) = ((qSw)A(rSw))) /\ ((qS(rSw)) = ((qTr)Sw) /\ (USw) = w))))
134	133	anbi2d 678	. . . . . 6 |- (s = S -> ((G e. AbelNEW /\ A.q e. K A.r e. K A.x e. V A.w e. V (((rsw) e. V /\ (rs(wAx)) = ((rsw)A(rsx)) /\ ((qPr)sw) = ((qsw)A(rsw))) /\ ((qs(rsw)) = ((qTr)sw) /\ (Usw) = w))) <-> (G e. AbelNEW /\ A.q e. K A.r e. K A.x e. V A.w e. V (((rSw) e. V /\ (rS(wAx)) = ((rSw)A(rSx)) /\ ((qPr)Sw) = ((qSw)A(rSw))) /\ ((qS(rSw)) = ((qTr)Sw) /\ (USw) = w)))))
135	47, 49, 51, 53, 55, 57, 61, 71, 79, 93, 111, 134	ceqsex6v 2332	. . . . 5 |- (E.kE.pE.tE.vE.aE.s((k = K /\ p = P /\ t = T) /\ (v = V /\ a = A /\ s = S) /\ ({<.1, v>., <.2, a>.} e. AbelNEW /\ A.q e. k A.r e. k A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w)))) <-> (G e. AbelNEW /\ A.q e. K A.r e. K A.x e. V A.w e. V (((rSw) e. V /\ (rS(wAx)) = ((rSw)A(rSx)) /\ ((qPr)Sw) = ((qSw)A(rSw))) /\ ((qS(rSw)) = ((qTr)Sw) /\ (USw) = w))))
136	135	anbi2i 538	. . . 4 |- ((W e. DivRing* /\ E.kE.pE.tE.vE.aE.s((k = K /\ p = P /\ t = T) /\ (v = V /\ a = A /\ s = S) /\ ({<.1, v>., <.2, a>.} e. AbelNEW /\ A.q e. k A.r e. k A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w))))) <-> (W e. DivRing* /\ (G e. AbelNEW /\ A.q e. K A.r e. K A.x e. V A.w e. V (((rSw) e. V /\ (rS(wAx)) = ((rSw)A(rSx)) /\ ((qPr)Sw) = ((qSw)A(rSw))) /\ ((qS(rSw)) = ((qTr)Sw) /\ (USw) = w)))))
137		3anass 862	. . . . 5 |- ((W e. DivRing* /\ G e. AbelNEW /\ A.q e. K A.r e. K A.x e. V A.w e. V (((rSw) e. V /\ (rS(wAx)) = ((rSw)A(rSx)) /\ ((qPr)Sw) = ((qSw)A(rSw))) /\ ((qS(rSw)) = ((qTr)Sw) /\ (USw) = w))) <-> (W e. DivRing* /\ (G e. AbelNEW /\ A.q e. K A.r e. K A.x e. V A.w e. V (((rSw) e. V /\ (rS(wAx)) = ((rSw)A(rSx)) /\ ((qPr)Sw) = ((qSw)A(rSw))) /\ ((qS(rSw)) = ((qTr)Sw) /\ (USw) = w)))))
138	137	bicomi 189	. . . 4 |- ((W e. DivRing* /\ (G e. AbelNEW /\ A.q e. K A.r e. K A.x e. V A.w e. V (((rSw) e. V /\ (rS(wAx)) = ((rSw)A(rSx)) /\ ((qPr)Sw) = ((qSw)A(rSw))) /\ ((qS(rSw)) = ((qTr)Sw) /\ (USw) = w)))) <-> (W e. DivRing* /\ G e. AbelNEW /\ A.q e. K A.r e. K A.x e. V A.w e. V (((rSw) e. V /\ (rS(wAx)) = ((rSw)A(rSx)) /\ ((qPr)Sw) = ((qSw)A(rSw))) /\ ((qS(rSw)) = ((qTr)Sw) /\ (USw) = w))))
139	136, 138	bitri 190	. . 3 |- ((W e. DivRing* /\ E.kE.pE.tE.vE.aE.s((k = K /\ p = P /\ t = T) /\ (v = V /\ a = A /\ s = S) /\ ({<.1, v>., <.2, a>.} e. AbelNEW /\ A.q e. k A.r e. k A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w))))) <-> (W e. DivRing* /\ G e. AbelNEW /\ A.q e. K A.r e. K A.x e. V A.w e. V (((rSw) e. V /\ (rS(wAx)) = ((rSw)A(rSx)) /\ ((qPr)Sw) = ((qSw)A(rSw))) /\ ((qS(rSw)) = ((qTr)Sw) /\ (USw) = w))))
140	139	anbi2i 538	. 2 |- ((W e. Q /\ (W e. DivRing* /\ E.kE.pE.tE.vE.aE.s((k = K /\ p = P /\ t = T) /\ (v = V /\ a = A /\ s = S) /\ ({<.1, v>., <.2, a>.} e. AbelNEW /\ A.q e. k A.r e. k A.x e. v A.w e. v (((rsw) e. v /\ (rs(wax)) = ((rsw)a(rsx)) /\ ((qpr)sw) = ((qsw)a(rsw))) /\ ((qs(rsw)) = ((qtr)sw) /\ (Usw) = w)))))) <-> (W e. Q /\ (W e. DivRing* /\ G e. AbelNEW /\ A.q e. K A.r e. K A.x e. V A.w e. V (((rSw) e. V /\ (rS(wAx)) = ((rSw)A(rSx)) /\ ((qPr)Sw) = ((qSw)A(rSw))) /\ ((qS(rSw)) = ((qTr)Sw) /\ (USw) = w)))))
141	2, 45, 140	3bitri 194	1 |- (W e. LVec <-> (W e. Q /\ (W e. DivRing* /\ G e. AbelNEW /\ A.q e. K A.r e. K A.x e. V A.w e. V (((rSw) e. V /\ (rS(wAx)) = ((rSw)A(rSx)) /\ ((qPr)Sw) = ((qSw)A(rSw))) /\ ((qS(rSw)) = ((qTr)Sw) /\ (USw) = w)))))

Syntax hints:   <-> wb 163   /\ wa 240   /\ w3a 858   T. wtru 1260   = wceq 1298   e. wcel 1300  E.wex 1326  A.wral 2105  _Vcvv 2292  {cpr 3045  <.cop 3046  ` cfv 3998  (class class class)co 4884  1c1 6387  2c2 7145  7c7 7150  Structcstru 16707  basecbs 16758  +_gcplusg 17080  AbelNEWcabel 17084  ._rcmulr 17085  1_rNEWcur 17087  DivRing*csd 17177  vbasecvbase 17180  vaddcvadd 17181  vscacvsca 17182  LVecclvec 17183

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-lvec 17187

Copyright terms: Public domain