Metamath Proof Explorer

Theorem reclem3pr

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

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

Proof

Step Hyp Ref Expression
1 reclempr.1 
 |-  B = { x | E. y ( x
2 df-1p 
 |-  1P = { w | w
3 2 eqabri 
 |-  ( w e. 1P <-> w
4 ltrnq 
 |-  ( w  ( *Q ` 1Q )
5 mulcomnq 
 |-  ( ( *Q ` 1Q ) .Q 1Q ) = ( 1Q .Q ( *Q ` 1Q ) )
6 1nq 
 |-  1Q e. Q.
7 recclnq 
 |-  ( 1Q e. Q. -> ( *Q ` 1Q ) e. Q. )
8 mulidnq 
 |-  ( ( *Q ` 1Q ) e. Q. -> ( ( *Q ` 1Q ) .Q 1Q ) = ( *Q ` 1Q ) )
9 6 7 8 mp2b 
 |-  ( ( *Q ` 1Q ) .Q 1Q ) = ( *Q ` 1Q )
10 recidnq 
 |-  ( 1Q e. Q. -> ( 1Q .Q ( *Q ` 1Q ) ) = 1Q )
11 6 10 ax-mp 
 |-  ( 1Q .Q ( *Q ` 1Q ) ) = 1Q
12 5 9 11 3eqtr3i 
 |-  ( *Q ` 1Q ) = 1Q
13 12 breq1i 
 |-  ( ( *Q ` 1Q )  1Q
14 4 13 bitri 
 |-  ( w  1Q
15 prlem936 
 |-  ( ( A e. P. /\ 1Q  E. v e. A -. ( v .Q ( *Q ` w ) ) e. A )
16 14 15 sylan2b 
 |-  ( ( A e. P. /\ w  E. v e. A -. ( v .Q ( *Q ` w ) ) e. A )
17 prnmax 
 |-  ( ( A e. P. /\ v e. A ) -> E. z e. A v
18 17 ad2ant2r 
 |-  ( ( ( A e. P. /\ w  E. z e. A v
19 elprnq 
 |-  ( ( A e. P. /\ v e. A ) -> v e. Q. )
20 19 ad2ant2r 
 |-  ( ( ( A e. P. /\ w  v e. Q. )
21 20 3adant3 
 |-  ( ( ( A e. P. /\ w  v e. Q. )
22 simp1r 
 |-  ( ( ( A e. P. /\ w  w
23 ltrelnq 
 |-
24 23 brel 
 |-  ( w  ( w e. Q. /\ 1Q e. Q. ) )
25 24 simpld 
 |-  ( w  w e. Q. )
26 22 25 syl 
 |-  ( ( ( A e. P. /\ w  w e. Q. )
27 simp3 
 |-  ( ( ( A e. P. /\ w  v
28 simp2r 
 |-  ( ( ( A e. P. /\ w  -. ( v .Q ( *Q ` w ) ) e. A )
29 ltrnq 
 |-  ( v  ( *Q ` z )
30 fvex 
 |-  ( *Q ` z ) e. _V
31 fvex 
 |-  ( *Q ` v ) e. _V
32 ltmnq 
 |-  ( u e. Q. -> ( x  ( u .Q x )
33 vex 
 |-  w e. _V
34 mulcomnq 
 |-  ( x .Q y ) = ( y .Q x )
35 30 31 32 33 34 caovord2 
 |-  ( w e. Q. -> ( ( *Q ` z )  ( ( *Q ` z ) .Q w )
36 29 35 bitrid 
 |-  ( w e. Q. -> ( v  ( ( *Q ` z ) .Q w )
37 36 adantl 
 |-  ( ( v e. Q. /\ w e. Q. ) -> ( v  ( ( *Q ` z ) .Q w )
38 37 biimpd 
 |-  ( ( v e. Q. /\ w e. Q. ) -> ( v  ( ( *Q ` z ) .Q w )
39 mulcomnq 
 |-  ( v .Q ( *Q ` v ) ) = ( ( *Q ` v ) .Q v )
40 recidnq 
 |-  ( v e. Q. -> ( v .Q ( *Q ` v ) ) = 1Q )
41 39 40 eqtr3id 
 |-  ( v e. Q. -> ( ( *Q ` v ) .Q v ) = 1Q )
42 recidnq 
 |-  ( w e. Q. -> ( w .Q ( *Q ` w ) ) = 1Q )
43 41 42 oveqan12d 
 |-  ( ( v e. Q. /\ w e. Q. ) -> ( ( ( *Q ` v ) .Q v ) .Q ( w .Q ( *Q ` w ) ) ) = ( 1Q .Q 1Q ) )
44 vex 
 |-  v e. _V
45 mulassnq 
 |-  ( ( x .Q y ) .Q u ) = ( x .Q ( y .Q u ) )
46 fvex 
 |-  ( *Q ` w ) e. _V
47 31 44 33 34 45 46 caov4 
 |-  ( ( ( *Q ` v ) .Q v ) .Q ( w .Q ( *Q ` w ) ) ) = ( ( ( *Q ` v ) .Q w ) .Q ( v .Q ( *Q ` w ) ) )
48 mulidnq 
 |-  ( 1Q e. Q. -> ( 1Q .Q 1Q ) = 1Q )
49 6 48 ax-mp 
 |-  ( 1Q .Q 1Q ) = 1Q
50 43 47 49 3eqtr3g 
 |-  ( ( v e. Q. /\ w e. Q. ) -> ( ( ( *Q ` v ) .Q w ) .Q ( v .Q ( *Q ` w ) ) ) = 1Q )
51 recclnq 
 |-  ( v e. Q. -> ( *Q ` v ) e. Q. )
52 mulclnq 
 |-  ( ( ( *Q ` v ) e. Q. /\ w e. Q. ) -> ( ( *Q ` v ) .Q w ) e. Q. )
53 51 52 sylan 
 |-  ( ( v e. Q. /\ w e. Q. ) -> ( ( *Q ` v ) .Q w ) e. Q. )
54 recmulnq 
 |-  ( ( ( *Q ` v ) .Q w ) e. Q. -> ( ( *Q ` ( ( *Q ` v ) .Q w ) ) = ( v .Q ( *Q ` w ) ) <-> ( ( ( *Q ` v ) .Q w ) .Q ( v .Q ( *Q ` w ) ) ) = 1Q ) )
55 53 54 syl 
 |-  ( ( v e. Q. /\ w e. Q. ) -> ( ( *Q ` ( ( *Q ` v ) .Q w ) ) = ( v .Q ( *Q ` w ) ) <-> ( ( ( *Q ` v ) .Q w ) .Q ( v .Q ( *Q ` w ) ) ) = 1Q ) )
56 50 55 mpbird 
 |-  ( ( v e. Q. /\ w e. Q. ) -> ( *Q ` ( ( *Q ` v ) .Q w ) ) = ( v .Q ( *Q ` w ) ) )
57 56 eleq1d 
 |-  ( ( v e. Q. /\ w e. Q. ) -> ( ( *Q ` ( ( *Q ` v ) .Q w ) ) e. A <-> ( v .Q ( *Q ` w ) ) e. A ) )
58 57 notbid 
 |-  ( ( v e. Q. /\ w e. Q. ) -> ( -. ( *Q ` ( ( *Q ` v ) .Q w ) ) e. A <-> -. ( v .Q ( *Q ` w ) ) e. A ) )
59 58 biimprd 
 |-  ( ( v e. Q. /\ w e. Q. ) -> ( -. ( v .Q ( *Q ` w ) ) e. A -> -. ( *Q ` ( ( *Q ` v ) .Q w ) ) e. A ) )
60 38 59 anim12d 
 |-  ( ( v e. Q. /\ w e. Q. ) -> ( ( v  ( ( ( *Q ` z ) .Q w )
61 ovex 
 |-  ( ( *Q ` v ) .Q w ) e. _V
62 breq2 
 |-  ( y = ( ( *Q ` v ) .Q w ) -> ( ( ( *Q ` z ) .Q w )  ( ( *Q ` z ) .Q w )
63 fveq2 
 |-  ( y = ( ( *Q ` v ) .Q w ) -> ( *Q ` y ) = ( *Q ` ( ( *Q ` v ) .Q w ) ) )
64 63 eleq1d 
 |-  ( y = ( ( *Q ` v ) .Q w ) -> ( ( *Q ` y ) e. A <-> ( *Q ` ( ( *Q ` v ) .Q w ) ) e. A ) )
65 64 notbid 
 |-  ( y = ( ( *Q ` v ) .Q w ) -> ( -. ( *Q ` y ) e. A <-> -. ( *Q ` ( ( *Q ` v ) .Q w ) ) e. A ) )
66 62 65 anbi12d 
 |-  ( y = ( ( *Q ` v ) .Q w ) -> ( ( ( ( *Q ` z ) .Q w )  ( ( ( *Q ` z ) .Q w )
67 61 66 spcev 
 |-  ( ( ( ( *Q ` z ) .Q w )  E. y ( ( ( *Q ` z ) .Q w )
68 ovex 
 |-  ( ( *Q ` z ) .Q w ) e. _V
69 breq1 
 |-  ( x = ( ( *Q ` z ) .Q w ) -> ( x  ( ( *Q ` z ) .Q w )
70 69 anbi1d 
 |-  ( x = ( ( *Q ` z ) .Q w ) -> ( ( x  ( ( ( *Q ` z ) .Q w )
71 70 exbidv 
 |-  ( x = ( ( *Q ` z ) .Q w ) -> ( E. y ( x  E. y ( ( ( *Q ` z ) .Q w )
72 68 71 1 elab2 
 |-  ( ( ( *Q ` z ) .Q w ) e. B <-> E. y ( ( ( *Q ` z ) .Q w )
73 67 72 sylibr 
 |-  ( ( ( ( *Q ` z ) .Q w )  ( ( *Q ` z ) .Q w ) e. B )
74 60 73 syl6 
 |-  ( ( v e. Q. /\ w e. Q. ) -> ( ( v  ( ( *Q ` z ) .Q w ) e. B ) )
75 74 imp 
 |-  ( ( ( v e. Q. /\ w e. Q. ) /\ ( v  ( ( *Q ` z ) .Q w ) e. B )
76 21 26 27 28 75 syl22anc 
 |-  ( ( ( A e. P. /\ w  ( ( *Q ` z ) .Q w ) e. B )
77 23 brel 
 |-  ( v  ( v e. Q. /\ z e. Q. ) )
78 77 simprd 
 |-  ( v  z e. Q. )
79 78 3ad2ant3 
 |-  ( ( ( A e. P. /\ w  z e. Q. )
80 mulidnq 
 |-  ( w e. Q. -> ( w .Q 1Q ) = w )
81 mulcomnq 
 |-  ( w .Q 1Q ) = ( 1Q .Q w )
82 80 81 eqtr3di 
 |-  ( w e. Q. -> w = ( 1Q .Q w ) )
83 recidnq 
 |-  ( z e. Q. -> ( z .Q ( *Q ` z ) ) = 1Q )
84 83 oveq1d 
 |-  ( z e. Q. -> ( ( z .Q ( *Q ` z ) ) .Q w ) = ( 1Q .Q w ) )
85 mulassnq 
 |-  ( ( z .Q ( *Q ` z ) ) .Q w ) = ( z .Q ( ( *Q ` z ) .Q w ) )
86 84 85 eqtr3di 
 |-  ( z e. Q. -> ( 1Q .Q w ) = ( z .Q ( ( *Q ` z ) .Q w ) ) )
87 82 86 sylan9eqr 
 |-  ( ( z e. Q. /\ w e. Q. ) -> w = ( z .Q ( ( *Q ` z ) .Q w ) ) )
88 79 26 87 syl2anc 
 |-  ( ( ( A e. P. /\ w  w = ( z .Q ( ( *Q ` z ) .Q w ) ) )
89 oveq2 
 |-  ( x = ( ( *Q ` z ) .Q w ) -> ( z .Q x ) = ( z .Q ( ( *Q ` z ) .Q w ) ) )
90 89 rspceeqv 
 |-  ( ( ( ( *Q ` z ) .Q w ) e. B /\ w = ( z .Q ( ( *Q ` z ) .Q w ) ) ) -> E. x e. B w = ( z .Q x ) )
91 76 88 90 syl2anc 
 |-  ( ( ( A e. P. /\ w  E. x e. B w = ( z .Q x ) )
92 91 3expia 
 |-  ( ( ( A e. P. /\ w  ( v  E. x e. B w = ( z .Q x ) ) )
93 92 reximdv 
 |-  ( ( ( A e. P. /\ w  ( E. z e. A v  E. z e. A E. x e. B w = ( z .Q x ) ) )
94 1 reclem2pr 
 |-  ( A e. P. -> B e. P. )
95 df-mp 
 |-  .P. = ( y e. P. , w e. P. |-> { u | E. f e. y E. g e. w u = ( f .Q g ) } )
96 mulclnq 
 |-  ( ( f e. Q. /\ g e. Q. ) -> ( f .Q g ) e. Q. )
97 95 96 genpelv 
 |-  ( ( A e. P. /\ B e. P. ) -> ( w e. ( A .P. B ) <-> E. z e. A E. x e. B w = ( z .Q x ) ) )
98 94 97 mpdan 
 |-  ( A e. P. -> ( w e. ( A .P. B ) <-> E. z e. A E. x e. B w = ( z .Q x ) ) )
99 98 ad2antrr 
 |-  ( ( ( A e. P. /\ w  ( w e. ( A .P. B ) <-> E. z e. A E. x e. B w = ( z .Q x ) ) )
100 93 99 sylibrd 
 |-  ( ( ( A e. P. /\ w  ( E. z e. A v  w e. ( A .P. B ) ) )
101 18 100 mpd 
 |-  ( ( ( A e. P. /\ w  w e. ( A .P. B ) )
102 16 101 rexlimddv 
 |-  ( ( A e. P. /\ w  w e. ( A .P. B ) )
103 102 ex 
 |-  ( A e. P. -> ( w  w e. ( A .P. B ) ) )
104 3 103 biimtrid 
 |-  ( A e. P. -> ( w e. 1P -> w e. ( A .P. B ) ) )
105 104 ssrdv 
 |-  ( A e. P. -> 1P C_ ( A .P. B ) )