Theorem ltexprlem3

Description: Lemma for Proposition 9-3.5(iv) of Gleason p. 123. (Contributed by NM, 6-Apr-1996) (New usage is discouraged.)

	Ref	Expression
Hypothesis	ltexprlem.1	|- C = { x | E. y ( -. y e. A /\ ( y +Q x ) e. B ) }
Assertion	ltexprlem3	|- ( B e. P. -> ( x e. C -> A. z ( z z e. C ) ) )

Proof

Step	Hyp	Ref	Expression
1		ltexprlem.1	|- C = { x | E. y ( -. y e. A /\ ( y +Q x ) e. B ) }
2		elprnq	|- ( ( B e. P. /\ ( y +Q x ) e. B ) -> ( y +Q x ) e. Q. )
3		addnqf	|- +Q : ( Q. X. Q. ) --> Q.
4	3	fdmi	|- dom +Q = ( Q. X. Q. )
5		0nnq	|- -. (/) e. Q.
6	4 5	ndmovrcl	|- ( ( y +Q x ) e. Q. -> ( y e. Q. /\ x e. Q. ) )
7	6	simpld	|- ( ( y +Q x ) e. Q. -> y e. Q. )
8		ltanq	|- ( y e. Q. -> ( z ( y +Q z )
9	2 7 8	3syl	|- ( ( B e. P. /\ ( y +Q x ) e. B ) -> ( z ( y +Q z )
10		prcdnq	|- ( ( B e. P. /\ ( y +Q x ) e. B ) -> ( ( y +Q z ) ( y +Q z ) e. B ) )
11	9 10	sylbid	|- ( ( B e. P. /\ ( y +Q x ) e. B ) -> ( z ( y +Q z ) e. B ) )
12	11	impancom	|- ( ( B e. P. /\ z ( ( y +Q x ) e. B -> ( y +Q z ) e. B ) )
13	12	anim2d	|- ( ( B e. P. /\ z ( ( -. y e. A /\ ( y +Q x ) e. B ) -> ( -. y e. A /\ ( y +Q z ) e. B ) ) )
14	13	eximdv	|- ( ( B e. P. /\ z ( E. y ( -. y e. A /\ ( y +Q x ) e. B ) -> E. y ( -. y e. A /\ ( y +Q z ) e. B ) ) )
15	1	abeq2i	|- ( x e. C <-> E. y ( -. y e. A /\ ( y +Q x ) e. B ) )
16		vex	|- z e. _V
17		oveq2	|- ( x = z -> ( y +Q x ) = ( y +Q z ) )
18	17	eleq1d	|- ( x = z -> ( ( y +Q x ) e. B <-> ( y +Q z ) e. B ) )
19	18	anbi2d	|- ( x = z -> ( ( -. y e. A /\ ( y +Q x ) e. B ) <-> ( -. y e. A /\ ( y +Q z ) e. B ) ) )
20	19	exbidv	|- ( x = z -> ( E. y ( -. y e. A /\ ( y +Q x ) e. B ) <-> E. y ( -. y e. A /\ ( y +Q z ) e. B ) ) )
21	16 20 1	elab2	|- ( z e. C <-> E. y ( -. y e. A /\ ( y +Q z ) e. B ) )
22	14 15 21	3imtr4g	|- ( ( B e. P. /\ z ( x e. C -> z e. C ) )
23	22	ex	|- ( B e. P. -> ( z ( x e. C -> z e. C ) ) )
24	23	com23	|- ( B e. P. -> ( x e. C -> ( z z e. C ) ) )
25	24	alrimdv	|- ( B e. P. -> ( x e. C -> A. z ( z z e. C ) ) )