Metamath Proof Explorer

Theorem reclem4pr

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

Ref Expression
Hypothesis reclempr.1 
|- B = { x | E. y ( x
Assertion reclem4pr 
|- ( A e. P. -> ( A .P. B ) = 1P )

Proof

Step Hyp Ref Expression
1 reclempr.1 
 |-  B = { x | E. y ( x
2 1 reclem2pr 
 |-  ( A e. P. -> B e. P. )
3 df-mp 
 |-  .P. = ( y e. P. , w e. P. |-> { u | E. f e. y E. g e. w u = ( f .Q g ) } )
4 mulclnq 
 |-  ( ( f e. Q. /\ g e. Q. ) -> ( f .Q g ) e. Q. )
5 3 4 genpelv 
 |-  ( ( A e. P. /\ B e. P. ) -> ( w e. ( A .P. B ) <-> E. z e. A E. x e. B w = ( z .Q x ) ) )
6 2 5 mpdan 
 |-  ( A e. P. -> ( w e. ( A .P. B ) <-> E. z e. A E. x e. B w = ( z .Q x ) ) )
7 1 abeq2i 
 |-  ( x e. B <-> E. y ( x
8 ltrelnq 
 |-
9 8 brel 
 |-  ( x  ( x e. Q. /\ y e. Q. ) )
10 9 simprd 
 |-  ( x  y e. Q. )
11 elprnq 
 |-  ( ( A e. P. /\ z e. A ) -> z e. Q. )
12 ltmnq 
 |-  ( z e. Q. -> ( x  ( z .Q x )
13 11 12 syl 
 |-  ( ( A e. P. /\ z e. A ) -> ( x  ( z .Q x )
14 13 biimpd 
 |-  ( ( A e. P. /\ z e. A ) -> ( x  ( z .Q x )
15 14 adantr 
 |-  ( ( ( A e. P. /\ z e. A ) /\ y e. Q. ) -> ( x  ( z .Q x )
16 recclnq 
 |-  ( y e. Q. -> ( *Q ` y ) e. Q. )
17 prub 
 |-  ( ( ( A e. P. /\ z e. A ) /\ ( *Q ` y ) e. Q. ) -> ( -. ( *Q ` y ) e. A -> z
18 16 17 sylan2 
 |-  ( ( ( A e. P. /\ z e. A ) /\ y e. Q. ) -> ( -. ( *Q ` y ) e. A -> z
19 ltmnq 
 |-  ( y e. Q. -> ( z  ( y .Q z )
20 mulcomnq 
 |-  ( y .Q z ) = ( z .Q y )
21 20 a1i 
 |-  ( y e. Q. -> ( y .Q z ) = ( z .Q y ) )
22 recidnq 
 |-  ( y e. Q. -> ( y .Q ( *Q ` y ) ) = 1Q )
23 21 22 breq12d 
 |-  ( y e. Q. -> ( ( y .Q z )  ( z .Q y )
24 19 23 bitrd 
 |-  ( y e. Q. -> ( z  ( z .Q y )
25 24 adantl 
 |-  ( ( ( A e. P. /\ z e. A ) /\ y e. Q. ) -> ( z  ( z .Q y )
26 18 25 sylibd 
 |-  ( ( ( A e. P. /\ z e. A ) /\ y e. Q. ) -> ( -. ( *Q ` y ) e. A -> ( z .Q y )
27 15 26 anim12d 
 |-  ( ( ( A e. P. /\ z e. A ) /\ y e. Q. ) -> ( ( x  ( ( z .Q x )
28 ltsonq 
 |-
29 28 8 sotri 
 |-  ( ( ( z .Q x )  ( z .Q x )
30 27 29 syl6 
 |-  ( ( ( A e. P. /\ z e. A ) /\ y e. Q. ) -> ( ( x  ( z .Q x )
31 30 exp4b 
 |-  ( ( A e. P. /\ z e. A ) -> ( y e. Q. -> ( x  ( -. ( *Q ` y ) e. A -> ( z .Q x )
32 10 31 syl5 
 |-  ( ( A e. P. /\ z e. A ) -> ( x  ( x  ( -. ( *Q ` y ) e. A -> ( z .Q x )
33 32 pm2.43d 
 |-  ( ( A e. P. /\ z e. A ) -> ( x  ( -. ( *Q ` y ) e. A -> ( z .Q x )
34 33 impd 
 |-  ( ( A e. P. /\ z e. A ) -> ( ( x  ( z .Q x )
35 34 exlimdv 
 |-  ( ( A e. P. /\ z e. A ) -> ( E. y ( x  ( z .Q x )
36 7 35 syl5bi 
 |-  ( ( A e. P. /\ z e. A ) -> ( x e. B -> ( z .Q x )
37 breq1 
 |-  ( w = ( z .Q x ) -> ( w  ( z .Q x )
38 37 biimprcd 
 |-  ( ( z .Q x )  ( w = ( z .Q x ) -> w
39 36 38 syl6 
 |-  ( ( A e. P. /\ z e. A ) -> ( x e. B -> ( w = ( z .Q x ) -> w
40 39 expimpd 
 |-  ( A e. P. -> ( ( z e. A /\ x e. B ) -> ( w = ( z .Q x ) -> w
41 40 rexlimdvv 
 |-  ( A e. P. -> ( E. z e. A E. x e. B w = ( z .Q x ) -> w
42 6 41 sylbid 
 |-  ( A e. P. -> ( w e. ( A .P. B ) -> w
43 df-1p 
 |-  1P = { w | w
44 43 abeq2i 
 |-  ( w e. 1P <-> w
45 42 44 syl6ibr 
 |-  ( A e. P. -> ( w e. ( A .P. B ) -> w e. 1P ) )
46 45 ssrdv 
 |-  ( A e. P. -> ( A .P. B ) C_ 1P )
47 1 reclem3pr 
 |-  ( A e. P. -> 1P C_ ( A .P. B ) )
48 46 47 eqssd 
 |-  ( A e. P. -> ( A .P. B ) = 1P )