Metamath Proof Explorer

Theorem ltexprlem7

Description: Lemma for Proposition 9-3.5(iv) of Gleason p. 123. (Contributed by NM, 8-Apr-1996) (Revised by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ltexprlem.1 
 |-  C = { x | E. y ( -. y e. A /\ ( y +Q x ) e. B ) }
2 1 ltexprlem5 
 |-  ( ( B e. P. /\ A C. B ) -> C e. P. )
3 ltaddpr 
 |-  ( ( A e. P. /\ C e. P. ) -> A
4 addclpr 
 |-  ( ( A e. P. /\ C e. P. ) -> ( A +P. C ) e. P. )
5 ltprord 
 |-  ( ( A e. P. /\ ( A +P. C ) e. P. ) -> ( A 
 A C. ( A +P. C ) ) )
6 4 5 syldan 
 |-  ( ( A e. P. /\ C e. P. ) -> ( A 
 A C. ( A +P. C ) ) )
7 3 6 mpbid 
 |-  ( ( A e. P. /\ C e. P. ) -> A C. ( A +P. C ) )
8 7 pssssd 
 |-  ( ( A e. P. /\ C e. P. ) -> A C_ ( A +P. C ) )
9 8 sseld 
 |-  ( ( A e. P. /\ C e. P. ) -> ( w e. A -> w e. ( A +P. C ) ) )
10 9 2a1d 
 |-  ( ( A e. P. /\ C e. P. ) -> ( B e. P. -> ( w e. B -> ( w e. A -> w e. ( A +P. C ) ) ) ) )
11 10 com4r 
 |-  ( w e. A -> ( ( A e. P. /\ C e. P. ) -> ( B e. P. -> ( w e. B -> w e. ( A +P. C ) ) ) ) )
12 11 expd 
 |-  ( w e. A -> ( A e. P. -> ( C e. P. -> ( B e. P. -> ( w e. B -> w e. ( A +P. C ) ) ) ) ) )
13 prnmadd 
 |-  ( ( B e. P. /\ w e. B ) -> E. v ( w +Q v ) e. B )
14 13 ex 
 |-  ( B e. P. -> ( w e. B -> E. v ( w +Q v ) e. B ) )
15 elprnq 
 |-  ( ( B e. P. /\ ( w +Q v ) e. B ) -> ( w +Q v ) e. Q. )
16 addnqf 
 |-  +Q : ( Q. X. Q. ) --> Q.
17 16 fdmi 
 |-  dom +Q = ( Q. X. Q. )
18 0nnq 
 |-  -. (/) e. Q.
19 17 18 ndmovrcl 
 |-  ( ( w +Q v ) e. Q. -> ( w e. Q. /\ v e. Q. ) )
20 15 19 syl 
 |-  ( ( B e. P. /\ ( w +Q v ) e. B ) -> ( w e. Q. /\ v e. Q. ) )
21 20 simpld 
 |-  ( ( B e. P. /\ ( w +Q v ) e. B ) -> w e. Q. )
22 vex 
 |-  v e. _V
23 22 prlem934 
 |-  ( A e. P. -> E. z e. A -. ( z +Q v ) e. A )
24 23 adantr 
 |-  ( ( A e. P. /\ C e. P. ) -> E. z e. A -. ( z +Q v ) e. A )
25 prub 
 |-  ( ( ( A e. P. /\ z e. A ) /\ w e. Q. ) -> ( -. w e. A -> z
26 ltexnq 
 |-  ( w e. Q. -> ( z  E. x ( z +Q x ) = w ) )
27 26 adantl 
 |-  ( ( ( A e. P. /\ z e. A ) /\ w e. Q. ) -> ( z  E. x ( z +Q x ) = w ) )
28 25 27 sylibd 
 |-  ( ( ( A e. P. /\ z e. A ) /\ w e. Q. ) -> ( -. w e. A -> E. x ( z +Q x ) = w ) )
29 28 ex 
 |-  ( ( A e. P. /\ z e. A ) -> ( w e. Q. -> ( -. w e. A -> E. x ( z +Q x ) = w ) ) )
30 29 ad2ant2r 
 |-  ( ( ( A e. P. /\ C e. P. ) /\ ( z e. A /\ -. ( z +Q v ) e. A ) ) -> ( w e. Q. -> ( -. w e. A -> E. x ( z +Q x ) = w ) ) )
31 vex 
 |-  z e. _V
32 vex 
 |-  x e. _V
33 addcomnq 
 |-  ( f +Q g ) = ( g +Q f )
34 addassnq 
 |-  ( ( f +Q g ) +Q h ) = ( f +Q ( g +Q h ) )
35 31 22 32 33 34 caov32 
 |-  ( ( z +Q v ) +Q x ) = ( ( z +Q x ) +Q v )
36 oveq1 
 |-  ( ( z +Q x ) = w -> ( ( z +Q x ) +Q v ) = ( w +Q v ) )
37 35 36 eqtrid 
 |-  ( ( z +Q x ) = w -> ( ( z +Q v ) +Q x ) = ( w +Q v ) )
38 37 eleq1d 
 |-  ( ( z +Q x ) = w -> ( ( ( z +Q v ) +Q x ) e. B <-> ( w +Q v ) e. B ) )
39 38 biimpar 
 |-  ( ( ( z +Q x ) = w /\ ( w +Q v ) e. B ) -> ( ( z +Q v ) +Q x ) e. B )
40 ovex 
 |-  ( z +Q v ) e. _V
41 eleq1 
 |-  ( y = ( z +Q v ) -> ( y e. A <-> ( z +Q v ) e. A ) )
42 41 notbid 
 |-  ( y = ( z +Q v ) -> ( -. y e. A <-> -. ( z +Q v ) e. A ) )
43 oveq1 
 |-  ( y = ( z +Q v ) -> ( y +Q x ) = ( ( z +Q v ) +Q x ) )
44 43 eleq1d 
 |-  ( y = ( z +Q v ) -> ( ( y +Q x ) e. B <-> ( ( z +Q v ) +Q x ) e. B ) )
45 42 44 anbi12d 
 |-  ( y = ( z +Q v ) -> ( ( -. y e. A /\ ( y +Q x ) e. B ) <-> ( -. ( z +Q v ) e. A /\ ( ( z +Q v ) +Q x ) e. B ) ) )
46 40 45 spcev 
 |-  ( ( -. ( z +Q v ) e. A /\ ( ( z +Q v ) +Q x ) e. B ) -> E. y ( -. y e. A /\ ( y +Q x ) e. B ) )
47 1 eqabri 
 |-  ( x e. C <-> E. y ( -. y e. A /\ ( y +Q x ) e. B ) )
48 46 47 sylibr 
 |-  ( ( -. ( z +Q v ) e. A /\ ( ( z +Q v ) +Q x ) e. B ) -> x e. C )
49 39 48 sylan2 
 |-  ( ( -. ( z +Q v ) e. A /\ ( ( z +Q x ) = w /\ ( w +Q v ) e. B ) ) -> x e. C )
50 df-plp 
 |-  +P. = ( x e. P. , w e. P. |-> { z | E. f e. x E. v e. w z = ( f +Q v ) } )
51 addclnq 
 |-  ( ( f e. Q. /\ v e. Q. ) -> ( f +Q v ) e. Q. )
52 50 51 genpprecl 
 |-  ( ( A e. P. /\ C e. P. ) -> ( ( z e. A /\ x e. C ) -> ( z +Q x ) e. ( A +P. C ) ) )
53 49 52 sylan2i 
 |-  ( ( A e. P. /\ C e. P. ) -> ( ( z e. A /\ ( -. ( z +Q v ) e. A /\ ( ( z +Q x ) = w /\ ( w +Q v ) e. B ) ) ) -> ( z +Q x ) e. ( A +P. C ) ) )
54 53 exp4d 
 |-  ( ( A e. P. /\ C e. P. ) -> ( z e. A -> ( -. ( z +Q v ) e. A -> ( ( ( z +Q x ) = w /\ ( w +Q v ) e. B ) -> ( z +Q x ) e. ( A +P. C ) ) ) ) )
55 54 imp42 
 |-  ( ( ( ( A e. P. /\ C e. P. ) /\ ( z e. A /\ -. ( z +Q v ) e. A ) ) /\ ( ( z +Q x ) = w /\ ( w +Q v ) e. B ) ) -> ( z +Q x ) e. ( A +P. C ) )
56 eleq1 
 |-  ( ( z +Q x ) = w -> ( ( z +Q x ) e. ( A +P. C ) <-> w e. ( A +P. C ) ) )
57 56 ad2antrl 
 |-  ( ( ( ( A e. P. /\ C e. P. ) /\ ( z e. A /\ -. ( z +Q v ) e. A ) ) /\ ( ( z +Q x ) = w /\ ( w +Q v ) e. B ) ) -> ( ( z +Q x ) e. ( A +P. C ) <-> w e. ( A +P. C ) ) )
58 55 57 mpbid 
 |-  ( ( ( ( A e. P. /\ C e. P. ) /\ ( z e. A /\ -. ( z +Q v ) e. A ) ) /\ ( ( z +Q x ) = w /\ ( w +Q v ) e. B ) ) -> w e. ( A +P. C ) )
59 58 exp32 
 |-  ( ( ( A e. P. /\ C e. P. ) /\ ( z e. A /\ -. ( z +Q v ) e. A ) ) -> ( ( z +Q x ) = w -> ( ( w +Q v ) e. B -> w e. ( A +P. C ) ) ) )
60 59 exlimdv 
 |-  ( ( ( A e. P. /\ C e. P. ) /\ ( z e. A /\ -. ( z +Q v ) e. A ) ) -> ( E. x ( z +Q x ) = w -> ( ( w +Q v ) e. B -> w e. ( A +P. C ) ) ) )
61 30 60 syl6d 
 |-  ( ( ( A e. P. /\ C e. P. ) /\ ( z e. A /\ -. ( z +Q v ) e. A ) ) -> ( w e. Q. -> ( -. w e. A -> ( ( w +Q v ) e. B -> w e. ( A +P. C ) ) ) ) )
62 24 61 rexlimddv 
 |-  ( ( A e. P. /\ C e. P. ) -> ( w e. Q. -> ( -. w e. A -> ( ( w +Q v ) e. B -> w e. ( A +P. C ) ) ) ) )
63 62 com14 
 |-  ( ( w +Q v ) e. B -> ( w e. Q. -> ( -. w e. A -> ( ( A e. P. /\ C e. P. ) -> w e. ( A +P. C ) ) ) ) )
64 63 adantl 
 |-  ( ( B e. P. /\ ( w +Q v ) e. B ) -> ( w e. Q. -> ( -. w e. A -> ( ( A e. P. /\ C e. P. ) -> w e. ( A +P. C ) ) ) ) )
65 21 64 mpd 
 |-  ( ( B e. P. /\ ( w +Q v ) e. B ) -> ( -. w e. A -> ( ( A e. P. /\ C e. P. ) -> w e. ( A +P. C ) ) ) )
66 65 ex 
 |-  ( B e. P. -> ( ( w +Q v ) e. B -> ( -. w e. A -> ( ( A e. P. /\ C e. P. ) -> w e. ( A +P. C ) ) ) ) )
67 66 exlimdv 
 |-  ( B e. P. -> ( E. v ( w +Q v ) e. B -> ( -. w e. A -> ( ( A e. P. /\ C e. P. ) -> w e. ( A +P. C ) ) ) ) )
68 14 67 syld 
 |-  ( B e. P. -> ( w e. B -> ( -. w e. A -> ( ( A e. P. /\ C e. P. ) -> w e. ( A +P. C ) ) ) ) )
69 68 com4t 
 |-  ( -. w e. A -> ( ( A e. P. /\ C e. P. ) -> ( B e. P. -> ( w e. B -> w e. ( A +P. C ) ) ) ) )
70 69 expd 
 |-  ( -. w e. A -> ( A e. P. -> ( C e. P. -> ( B e. P. -> ( w e. B -> w e. ( A +P. C ) ) ) ) ) )
71 12 70 pm2.61i 
 |-  ( A e. P. -> ( C e. P. -> ( B e. P. -> ( w e. B -> w e. ( A +P. C ) ) ) ) )
72 2 71 syl5 
 |-  ( A e. P. -> ( ( B e. P. /\ A C. B ) -> ( B e. P. -> ( w e. B -> w e. ( A +P. C ) ) ) ) )
73 72 expd 
 |-  ( A e. P. -> ( B e. P. -> ( A C. B -> ( B e. P. -> ( w e. B -> w e. ( A +P. C ) ) ) ) ) )
74 73 com34 
 |-  ( A e. P. -> ( B e. P. -> ( B e. P. -> ( A C. B -> ( w e. B -> w e. ( A +P. C ) ) ) ) ) )
75 74 pm2.43d 
 |-  ( A e. P. -> ( B e. P. -> ( A C. B -> ( w e. B -> w e. ( A +P. C ) ) ) ) )
76 75 imp31 
 |-  ( ( ( A e. P. /\ B e. P. ) /\ A C. B ) -> ( w e. B -> w e. ( A +P. C ) ) )
77 76 ssrdv 
 |-  ( ( ( A e. P. /\ B e. P. ) /\ A C. B ) -> B C_ ( A +P. C ) )