This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid 
 |-  ( ( 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 imbitrid 
 |-  ( ( 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 )