Theorem ltaprlem

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

	Ref	Expression
Assertion	ltaprlem	|- ( C e. P. -> ( A ( C +P. A )

Proof

Step	Hyp	Ref	Expression
1		ltrelpr	|-
2	1	brel	|- ( A ( A e. P. /\ B e. P. ) )
3	2	simpld	|- ( A A e. P. )
4		ltexpri	|- ( A E. x e. P. ( A +P. x ) = B )
5		addclpr	|- ( ( C e. P. /\ A e. P. ) -> ( C +P. A ) e. P. )
6		ltaddpr	|- ( ( ( C +P. A ) e. P. /\ x e. P. ) -> ( C +P. A )
7		addasspr	|- ( ( C +P. A ) +P. x ) = ( C +P. ( A +P. x ) )
8		oveq2	|- ( ( A +P. x ) = B -> ( C +P. ( A +P. x ) ) = ( C +P. B ) )
9	7 8	syl5eq	|- ( ( A +P. x ) = B -> ( ( C +P. A ) +P. x ) = ( C +P. B ) )
10	9	breq2d	|- ( ( A +P. x ) = B -> ( ( C +P. A ) ( C +P. A )
11	6 10	syl5ib	|- ( ( A +P. x ) = B -> ( ( ( C +P. A ) e. P. /\ x e. P. ) -> ( C +P. A )
12	11	expd	|- ( ( A +P. x ) = B -> ( ( C +P. A ) e. P. -> ( x e. P. -> ( C +P. A )
13	5 12	syl5	|- ( ( A +P. x ) = B -> ( ( C e. P. /\ A e. P. ) -> ( x e. P. -> ( C +P. A )
14	13	com3r	|- ( x e. P. -> ( ( A +P. x ) = B -> ( ( C e. P. /\ A e. P. ) -> ( C +P. A )
15	14	rexlimiv	|- ( E. x e. P. ( A +P. x ) = B -> ( ( C e. P. /\ A e. P. ) -> ( C +P. A )
16	4 15	syl	|- ( A ( ( C e. P. /\ A e. P. ) -> ( C +P. A )
17	3 16	sylan2i	|- ( A ( ( C e. P. /\ A ( C +P. A )
18	17	expd	|- ( A ( C e. P. -> ( A ( C +P. A )
19	18	pm2.43b	|- ( C e. P. -> ( A ( C +P. A )