Theorem prlem934a 3931

Description: Sublemma for Lemma 9-3.4 of [Gleason] p. 122.

Hypothesis

Ref	Expression
prlem934a.1	|- B e. V

Assertion

Ref	Expression
prlem934a	|- (C e. N. -> (((B e. Q. /\ A.x(x e. A -> (x +Q B) e. A)) /\ y e. A) -> (y +Q ([<.C, 1o>.] ~Q .Q B)) e. A))

Distinct variable group(s):   x,y,A   x,B,y   x,C,y

Proof of Theorem prlem934a

Step	Hyp	Ref	Expression
1		opeq1 1876	. . . . . . 7 |- (w = 1o -> <.w, 1o>. = <.1o, 1o>.)
2		eceq2 3215	. . . . . . 7 |- (<.w, 1o>. = <.1o, 1o>. -> [<.w, 1o>.] ~Q = [<.1o, 1o>.] ~Q )
3	1, 2	syl 12	. . . . . 6 |- (w = 1o -> [<.w, 1o>.] ~Q = [<.1o, 1o>.] ~Q )
4	3	opreq1d 3012	. . . . 5 |- (w = 1o -> ([<.w, 1o>.] ~Q .Q B) = ([<.1o, 1o>.] ~Q .Q B))
5	4	opreq2d 3013	. . . 4 |- (w = 1o -> (y +Q ([<.w, 1o>.] ~Q .Q B)) = (y +Q ([<.1o, 1o>.] ~Q .Q B)))
6	5	eleq1d 1155	. . 3 |- (w = 1o -> ((y +Q ([<.w, 1o>.] ~Q .Q B)) e. A <-> (y +Q ([<.1o, 1o>.] ~Q .Q B)) e. A))
7	6	imbi2d 464	. 2 |- (w = 1o -> ((((B e. Q. /\ A.x(x e. A -> (x +Q B) e. A)) /\ y e. A) -> (y +Q ([<.w, 1o>.] ~Q .Q B)) e. A) <-> (((B e. Q. /\ A.x(x e. A -> (x +Q B) e. A)) /\ y e. A) -> (y +Q ([<.1o, 1o>.] ~Q .Q B)) e. A)))
8		opeq1 1876	. . . . . . 7 |- (w = z -> <.w, 1o>. = <.z, 1o>.)
9		eceq2 3215	. . . . . . 7 |- (<.w, 1o>. = <.z, 1o>. -> [<.w, 1o>.] ~Q = [<.z, 1o>.] ~Q )
10	8, 9	syl 12	. . . . . 6 |- (w = z -> [<.w, 1o>.] ~Q = [<.z, 1o>.] ~Q )
11	10	opreq1d 3012	. . . . 5 |- (w = z -> ([<.w, 1o>.] ~Q .Q B) = ([<.z, 1o>.] ~Q .Q B))
12	11	opreq2d 3013	. . . 4 |- (w = z -> (y +Q ([<.w, 1o>.] ~Q .Q B)) = (y +Q ([<.z, 1o>.] ~Q .Q B)))
13	12	eleq1d 1155	. . 3 |- (w = z -> ((y +Q ([<.w, 1o>.] ~Q .Q B)) e. A <-> (y +Q ([<.z, 1o>.] ~Q .Q B)) e. A))
14	13	imbi2d 464	. 2 |- (w = z -> ((((B e. Q. /\ A.x(x e. A -> (x +Q B) e. A)) /\ y e. A) -> (y +Q ([<.w, 1o>.] ~Q .Q B)) e. A) <-> (((B e. Q. /\ A.x(x e. A -> (x +Q B) e. A)) /\ y e. A) -> (y +Q ([<.z, 1o>.] ~Q .Q B)) e. A)))
15		opeq1 1876	. . . . . . 7 |- (w = (z +N 1o) -> <.w, 1o>. = <.(z +N 1o), 1o>.)
16		eceq2 3215	. . . . . . 7 |- (<.w, 1o>. = <.(z +N 1o), 1o>. -> [<.w, 1o>.] ~Q = [<.(z +N 1o), 1o>.] ~Q )
17	15, 16	syl 12	. . . . . 6 |- (w = (z +N 1o) -> [<.w, 1o>.] ~Q = [<.(z +N 1o), 1o>.] ~Q )
18	17	opreq1d 3012	. . . . 5 |- (w = (z +N 1o) -> ([<.w, 1o>.] ~Q .Q B) = ([<.(z +N 1o), 1o>.] ~Q .Q B))
19	18	opreq2d 3013	. . . 4 |- (w = (z +N 1o) -> (y +Q ([<.w, 1o>.] ~Q .Q B)) = (y +Q ([<.(z +N 1o), 1o>.] ~Q .Q B)))
20	19	eleq1d 1155	. . 3 |- (w = (z +N 1o) -> ((y +Q ([<.w, 1o>.] ~Q .Q B)) e. A <-> (y +Q ([<.(z +N 1o), 1o>.] ~Q .Q B)) e. A))
21	20	imbi2d 464	. 2 |- (w = (z +N 1o) -> ((((B e. Q. /\ A.x(x e. A -> (x +Q B) e. A)) /\ y e. A) -> (y +Q ([<.w, 1o>.] ~Q .Q B)) e. A) <-> (((B e. Q. /\ A.x(x e. A -> (x +Q B) e. A)) /\ y e. A) -> (y +Q ([<.(z +N 1o), 1o>.] ~Q .Q B)) e. A)))
22		opeq1 1876	. . . . . . 7 |- (w = C -> <.w, 1o>. = <.C, 1o>.)
23		eceq2 3215	. . . . . . 7 |- (<.w, 1o>. = <.C, 1o>. -> [<.w, 1o>.] ~Q = [<.C, 1o>.] ~Q )
24	22, 23	syl 12	. . . . . 6 |- (w = C -> [<.w, 1o>.] ~Q = [<.C, 1o>.] ~Q )
25	24	opreq1d 3012	. . . . 5 |- (w = C -> ([<.w, 1o>.] ~Q .Q B) = ([<.C, 1o>.] ~Q .Q B))
26	25	opreq2d 3013	. . . 4 |- (w = C -> (y +Q ([<.w, 1o>.] ~Q .Q B)) = (y +Q ([<.C, 1o>.] ~Q .Q B)))
27	26	eleq1d 1155	. . 3 |- (w = C -> ((y +Q ([<.w, 1o>.] ~Q .Q B)) e. A <-> (y +Q ([<.C, 1o>.] ~Q .Q B)) e. A))
28	27	imbi2d 464	. 2 |- (w = C -> ((((B e. Q. /\ A.x(x e. A -> (x +Q B) e. A)) /\ y e. A) -> (y +Q ([<.w, 1o>.] ~Q .Q B)) e. A) <-> (((B e. Q. /\ A.x(x e. A -> (x +Q B) e. A)) /\ y e. A) -> (y +Q ([<.C, 1o>.] ~Q .Q B)) e. A)))
29		eleq1 1149	. . . . . 6 |- (x = y -> (x e. A <-> y e. A))
30		opreq1 3006	. . . . . . 7 |- (x = y -> (x +Q B) = (y +Q B))
31	30	eleq1d 1155	. . . . . 6 |- (x = y -> ((x +Q B) e. A <-> (y +Q B) e. A))
32	29, 31	imbi12d 474	. . . . 5 |- (x = y -> ((x e. A -> (x +Q B) e. A) <-> (y e. A -> (y +Q B) e. A)))
33	32	a4b1 928	. . . 4 |- (A.x(x e. A -> (x +Q B) e. A) -> (y e. A -> (y +Q B) e. A))
34		mulidpq 3863	. . . . . . . . 9 |- (B e. Q. -> (B .Q 1Q) = B)
35		prlem934a.1	. . . . . . . . . 10 |- B e. V
36		1q 3851	. . . . . . . . . . 11 |- 1Q e. Q.
37	36	elisseti 1355	. . . . . . . . . 10 |- 1Q e. V
38	35, 37	mulcompq 3858	. . . . . . . . 9 |- (B .Q 1Q) = (1Q .Q B)
39	34, 38	syl5eqr 1138	. . . . . . . 8 |- (B e. Q. -> (1Q .Q B) = B)
40		df-1q 3837	. . . . . . . . 9 |- 1Q = [<.1o, 1o>.] ~Q
41	40	opreq1i 3009	. . . . . . . 8 |- (1Q .Q B) = ([<.1o, 1o>.] ~Q .Q B)
42	39, 41	syl5eqr 1138	. . . . . . 7 |- (B e. Q. -> ([<.1o, 1o>.] ~Q .Q B) = B)
43	42	opreq2d 3013	. . . . . 6 |- (B e. Q. -> (y +Q ([<.1o, 1o>.] ~Q .Q B)) = (y +Q B))
44	43	eleq1d 1155	. . . . 5 |- (B e. Q. -> ((y +Q ([<.1o, 1o>.] ~Q .Q B)) e. A <-> (y +Q B) e. A))
45	44	biimprd 136	. . . 4 |- (B e. Q. -> ((y +Q B) e. A -> (y +Q ([<.1o, 1o>.] ~Q .Q B)) e. A))
46	33, 45	sylan9r 360	. . 3 |- ((B e. Q. /\ A.x(x e. A -> (x +Q B) e. A)) -> (y e. A -> (y +Q ([<.1o, 1o>.] ~Q .Q B)) e. A))
47	46	imp 277	. 2 |- (((B e. Q. /\ A.x(x e. A -> (x +Q B) e. A)) /\ y e. A) -> (y +Q ([<.1o, 1o>.] ~Q .Q B)) e. A)
48		oprex 3018	. . . . . . . 8 |- (y +Q ([<.z, 1o>.] ~Q .Q B)) e. V
49		eleq1 1149	. . . . . . . . 9 |- (x = (y +Q ([<.z, 1o>.] ~Q .Q B)) -> (x e. A <-> (y +Q ([<.z, 1o>.] ~Q .Q B)) e. A))
50		opreq1 3006	. . . . . . . . . 10 |- (x = (y +Q ([<.z, 1o>.] ~Q .Q B)) -> (x +Q B) = ((y +Q ([<.z, 1o>.] ~Q .Q B)) +Q B))
51	50	eleq1d 1155	. . . . . . . . 9 |- (x = (y +Q ([<.z, 1o>.] ~Q .Q B)) -> ((x +Q B) e. A <-> ((y +Q ([<.z, 1o>.] ~Q .Q B)) +Q B) e. A))
52	49, 51	imbi12d 474	. . . . . . . 8 |- (x = (y +Q ([<.z, 1o>.] ~Q .Q B)) -> ((x e. A -> (x +Q B) e. A) <-> ((y +Q ([<.z, 1o>.] ~Q .Q B)) e. A -> ((y +Q ([<.z, 1o>.] ~Q .Q B)) +Q B) e. A)))
53	48, 52	cla4v 1400	. . . . . . 7 |- (A.x(x e. A -> (x +Q B) e. A) -> ((y +Q ([<.z, 1o>.] ~Q .Q B)) e. A -> ((y +Q ([<.z, 1o>.] ~Q .Q B)) +Q B) e. A))
54	34, 38	syl5reqr 1139	. . . . . . . . . . . . . 14 |- (B e. Q. -> B = (1Q .Q B))
55	54	opreq2d 3013	. . . . . . . . . . . . 13 |- (B