Metamath Proof Explorer

Theorem rlocisunit

Description: Characterize the units of the localization L of a ring R at S as the elements with a "numerator" P in the saturation T of S . (Contributed by Thierry Arnoux, 6-Jun-2026)

Ref Expression
Hypotheses rlocisunit.b 
|- B = ( Base ` R )
rlocisunit.m 
|- .x. = ( .r ` R )
rlocisunit.l 
|- L = ( R RLocal S )
rlocisunit.w 
|- W = ( Unit ` L )
rlocisunit.r 
|- ( ph -> R e. CRing )
rlocisunit.s 
|- ( ph -> S e. ( SubMnd ` ( mulGrp ` R ) ) )
rlocisunit.e 
|- .~ = ( R ~RL S )
rlocisunit.p 
|- ( ph -> P e. B )
rlocisunit.q 
|- ( ph -> Q e. S )
rlocisunit.t 
|- T = { r e. B | E. s e. B ( r .x. s ) e. S }
Assertion rlocisunit 
|- ( ph -> ( [ <. P , Q >. ] .~ e. W <-> P e. T ) )

Proof

Step Hyp Ref Expression
1 rlocisunit.b 
 |-  B = ( Base ` R )
2 rlocisunit.m 
 |-  .x. = ( .r ` R )
3 rlocisunit.l 
 |-  L = ( R RLocal S )
4 rlocisunit.w 
 |-  W = ( Unit ` L )
5 rlocisunit.r 
 |-  ( ph -> R e. CRing )
6 rlocisunit.s 
 |-  ( ph -> S e. ( SubMnd ` ( mulGrp ` R ) ) )
7 rlocisunit.e 
 |-  .~ = ( R ~RL S )
8 rlocisunit.p 
 |-  ( ph -> P e. B )
9 rlocisunit.q 
 |-  ( ph -> Q e. S )
10 rlocisunit.t 
 |-  T = { r e. B | E. s e. B ( r .x. s ) e. S }
11 10 eleq2i 
 |-  ( P e. T <-> P e. { r e. B | E. s e. B ( r .x. s ) e. S } )
12 oveq1 
 |-  ( r = P -> ( r .x. s ) = ( P .x. s ) )
13 12 eleq1d 
 |-  ( r = P -> ( ( r .x. s ) e. S <-> ( P .x. s ) e. S ) )
14 13 rexbidv 
 |-  ( r = P -> ( E. s e. B ( r .x. s ) e. S <-> E. s e. B ( P .x. s ) e. S ) )
15 14 elrab 
 |-  ( P e. { r e. B | E. s e. B ( r .x. s ) e. S } <-> ( P e. B /\ E. s e. B ( P .x. s ) e. S ) )
16 11 15 bitri 
 |-  ( P e. T <-> ( P e. B /\ E. s e. B ( P .x. s ) e. S ) )
17 8 biantrurd 
 |-  ( ph -> ( E. s e. B ( P .x. s ) e. S <-> ( P e. B /\ E. s e. B ( P .x. s ) e. S ) ) )
18 16 17 bitr4id 
 |-  ( ph -> ( P e. T <-> E. s e. B ( P .x. s ) e. S ) )
19 eqid 
 |-  ( Base ` L ) = ( Base ` L )
20 eqid 
 |-  ( .r ` L ) = ( .r ` L )
21 eqid 
 |-  ( 1r ` L ) = ( 1r ` L )
22 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
23 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
24 22 23 ringidval 
 |-  ( 1r ` R ) = ( 0g ` ( mulGrp ` R ) )
25 24 subm0cl 
 |-  ( S e. ( SubMnd ` ( mulGrp ` R ) ) -> ( 1r ` R ) e. S )
26 6 25 syl 
 |-  ( ph -> ( 1r ` R ) e. S )
27 8 26 opelxpd 
 |-  ( ph -> <. P , ( 1r ` R ) >. e. ( B X. S ) )
28 7 ovexi 
 |-  .~ e. _V
29 28 ecelqsi 
 |-  ( <. P , ( 1r ` R ) >. e. ( B X. S ) -> [ <. P , ( 1r ` R ) >. ] .~ e. ( ( B X. S ) /. .~ ) )
30 27 29 syl 
 |-  ( ph -> [ <. P , ( 1r ` R ) >. ] .~ e. ( ( B X. S ) /. .~ ) )
31 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
32 eqid 
 |-  ( -g ` R ) = ( -g ` R )
33 eqid 
 |-  ( B X. S ) = ( B X. S )
34 22 1 mgpbas 
 |-  B = ( Base ` ( mulGrp ` R ) )
35 34 submss 
 |-  ( S e. ( SubMnd ` ( mulGrp ` R ) ) -> S C_ B )
36 6 35 syl 
 |-  ( ph -> S C_ B )
37 1 31 2 32 33 3 7 5 36 rlocbas 
 |-  ( ph -> ( ( B X. S ) /. .~ ) = ( Base ` L ) )
38 30 37 eleqtrd 
 |-  ( ph -> [ <. P , ( 1r ` R ) >. ] .~ e. ( Base ` L ) )
39 eqid 
 |-  ( +g ` R ) = ( +g ` R )
40 1 2 39 3 7 5 6 rloccring 
 |-  ( ph -> L e. CRing )
41 19 4 20 21 38 40 isunitc 
 |-  ( ph -> ( [ <. P , ( 1r ` R ) >. ] .~ e. W <-> E. x e. ( Base ` L ) ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) )
42 5 crngringd 
 |-  ( ph -> R e. Ring )
43 42 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) /\ t e. S ) /\ ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) ) -> R e. Ring )
44 36 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) /\ t e. S ) /\ ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) ) -> S C_ B )
45 simplr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) /\ t e. S ) /\ ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) ) -> t e. S )
46 44 45 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) /\ t e. S ) /\ ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) ) -> t e. B )
47 simpllr 
 |-  ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) -> r e. B )
48 47 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) /\ t e. S ) /\ ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) ) -> r e. B )
49 1 2 43 46 48 ringcld 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) /\ t e. S ) /\ ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) ) -> ( t .x. r ) e. B )
50 oveq2 
 |-  ( u = ( t .x. r ) -> ( P .x. u ) = ( P .x. ( t .x. r ) ) )
51 50 eleq1d 
 |-  ( u = ( t .x. r ) -> ( ( P .x. u ) e. S <-> ( P .x. ( t .x. r ) ) e. S ) )
52 51 adantl 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) /\ t e. S ) /\ ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) ) /\ u = ( t .x. r ) ) -> ( ( P .x. u ) e. S <-> ( P .x. ( t .x. r ) ) e. S ) )
53 5 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) /\ t e. S ) /\ ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) ) -> R e. CRing )
54 8 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) /\ t e. S ) /\ ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) ) -> P e. B )
55 1 2 53 54 46 48 crng12d 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) /\ t e. S ) /\ ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) ) -> ( P .x. ( t .x. r ) ) = ( t .x. ( P .x. r ) ) )
56 1 2 43 54 48 ringcld 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) /\ t e. S ) /\ ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) ) -> ( P .x. r ) e. B )
57 1 2 23 43 56 ringridmd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) /\ t e. S ) /\ ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) ) -> ( ( P .x. r ) .x. ( 1r ` R ) ) = ( P .x. r ) )
58 57 oveq2d 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) /\ t e. S ) /\ ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) ) -> ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( P .x. r ) ) )
59 55 58 eqtr4d 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) /\ t e. S ) /\ ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) ) -> ( P .x. ( t .x. r ) ) = ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) )
60 simpr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) /\ t e. S ) /\ ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) ) -> ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) )
61 36 26 sseldd 
 |-  ( ph -> ( 1r ` R ) e. B )
62 61 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) /\ t e. S ) /\ ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) ) -> ( 1r ` R ) e. B )
63 simplr 
 |-  ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) -> s e. S )
64 63 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) /\ t e. S ) /\ ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) ) -> s e. S )
65 44 64 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) /\ t e. S ) /\ ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) ) -> s e. B )
66 1 2 43 62 65 ringcld 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) /\ t e. S ) /\ ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) ) -> ( ( 1r ` R ) .x. s ) e. B )
67 1 2 23 43 66 ringlidmd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) /\ t e. S ) /\ ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) ) -> ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) = ( ( 1r ` R ) .x. s ) )
68 1 2 23 43 65 ringlidmd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) /\ t e. S ) /\ ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) ) -> ( ( 1r ` R ) .x. s ) = s )
69 67 68 eqtrd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) /\ t e. S ) /\ ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) ) -> ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) = s )
70 69 oveq2d 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) /\ t e. S ) /\ ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) ) -> ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) = ( t .x. s ) )
71 59 60 70 3eqtrd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) /\ t e. S ) /\ ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) ) -> ( P .x. ( t .x. r ) ) = ( t .x. s ) )
72 22 2 mgpplusg 
 |-  .x. = ( +g ` ( mulGrp ` R ) )
73 6 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) /\ t e. S ) /\ ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) ) -> S e. ( SubMnd ` ( mulGrp ` R ) ) )
74 72 73 45 64 submcld 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) /\ t e. S ) /\ ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) ) -> ( t .x. s ) e. S )
75 71 74 eqeltrd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) /\ t e. S ) /\ ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) ) -> ( P .x. ( t .x. r ) ) e. S )
76 49 52 75 rspcedvd 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) /\ t e. S ) /\ ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) ) -> E. u e. B ( P .x. u ) e. S )
77 simp-5l 
 |-  ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) -> ph )
78 simpr 
 |-  ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) -> x = [ <. r , s >. ] .~ )
79 78 oveq2d 
 |-  ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) -> ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) [ <. r , s >. ] .~ ) )
80 simp-4r 
 |-  ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) -> ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) )
81 5 ad2antrr 
 |-  ( ( ( ph /\ r e. B ) /\ s e. S ) -> R e. CRing )
82 6 ad2antrr 
 |-  ( ( ( ph /\ r e. B ) /\ s e. S ) -> S e. ( SubMnd ` ( mulGrp ` R ) ) )
83 8 ad2antrr 
 |-  ( ( ( ph /\ r e. B ) /\ s e. S ) -> P e. B )
84 simplr 
 |-  ( ( ( ph /\ r e. B ) /\ s e. S ) -> r e. B )
85 82 25 syl 
 |-  ( ( ( ph /\ r e. B ) /\ s e. S ) -> ( 1r ` R ) e. S )
86 simpr 
 |-  ( ( ( ph /\ r e. B ) /\ s e. S ) -> s e. S )
87 1 2 39 3 7 81 82 83 84 85 86 20 rlocmulval 
 |-  ( ( ( ph /\ r e. B ) /\ s e. S ) -> ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) [ <. r , s >. ] .~ ) = [ <. ( P .x. r ) , ( ( 1r ` R ) .x. s ) >. ] .~ )
88 77 47 63 87 syl21anc 
 |-  ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) -> ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) [ <. r , s >. ] .~ ) = [ <. ( P .x. r ) , ( ( 1r ` R ) .x. s ) >. ] .~ )
89 79 80 88 3eqtr3rd 
 |-  ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) -> [ <. ( P .x. r ) , ( ( 1r ` R ) .x. s ) >. ] .~ = ( 1r ` L ) )
90 eqid 
 |-  [ <. ( 1r ` R ) , ( 1r ` R ) >. ] .~ = [ <. ( 1r ` R ) , ( 1r ` R ) >. ] .~
91 31 23 3 7 5 6 90 rloc1r 
 |-  ( ph -> [ <. ( 1r ` R ) , ( 1r ` R ) >. ] .~ = ( 1r ` L ) )
92 91 ad5antr 
 |-  ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) -> [ <. ( 1r ` R ) , ( 1r ` R ) >. ] .~ = ( 1r ` L ) )
93 89 92 eqtr4d 
 |-  ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) -> [ <. ( P .x. r ) , ( ( 1r ` R ) .x. s ) >. ] .~ = [ <. ( 1r ` R ) , ( 1r ` R ) >. ] .~ )
94 81 adantr 
 |-  ( ( ( ( ph /\ r e. B ) /\ s e. S ) /\ [ <. ( P .x. r ) , ( ( 1r ` R ) .x. s ) >. ] .~ = [ <. ( 1r ` R ) , ( 1r ` R ) >. ] .~ ) -> R e. CRing )
95 82 adantr 
 |-  ( ( ( ( ph /\ r e. B ) /\ s e. S ) /\ [ <. ( P .x. r ) , ( ( 1r ` R ) .x. s ) >. ] .~ = [ <. ( 1r ` R ) , ( 1r ` R ) >. ] .~ ) -> S e. ( SubMnd ` ( mulGrp ` R ) ) )
96 42 ad2antrr 
 |-  ( ( ( ph /\ r e. B ) /\ s e. S ) -> R e. Ring )
97 1 2 96 83 84 ringcld 
 |-  ( ( ( ph /\ r e. B ) /\ s e. S ) -> ( P .x. r ) e. B )
98 97 adantr 
 |-  ( ( ( ( ph /\ r e. B ) /\ s e. S ) /\ [ <. ( P .x. r ) , ( ( 1r ` R ) .x. s ) >. ] .~ = [ <. ( 1r ` R ) , ( 1r ` R ) >. ] .~ ) -> ( P .x. r ) e. B )
99 72 82 85 86 submcld 
 |-  ( ( ( ph /\ r e. B ) /\ s e. S ) -> ( ( 1r ` R ) .x. s ) e. S )
100 99 adantr 
 |-  ( ( ( ( ph /\ r e. B ) /\ s e. S ) /\ [ <. ( P .x. r ) , ( ( 1r ` R ) .x. s ) >. ] .~ = [ <. ( 1r ` R ) , ( 1r ` R ) >. ] .~ ) -> ( ( 1r ` R ) .x. s ) e. S )
101 61 ad3antrrr 
 |-  ( ( ( ( ph /\ r e. B ) /\ s e. S ) /\ [ <. ( P .x. r ) , ( ( 1r ` R ) .x. s ) >. ] .~ = [ <. ( 1r ` R ) , ( 1r ` R ) >. ] .~ ) -> ( 1r ` R ) e. B )
102 95 25 syl 
 |-  ( ( ( ( ph /\ r e. B ) /\ s e. S ) /\ [ <. ( P .x. r ) , ( ( 1r ` R ) .x. s ) >. ] .~ = [ <. ( 1r ` R ) , ( 1r ` R ) >. ] .~ ) -> ( 1r ` R ) e. S )
103 simpr 
 |-  ( ( ( ( ph /\ r e. B ) /\ s e. S ) /\ [ <. ( P .x. r ) , ( ( 1r ` R ) .x. s ) >. ] .~ = [ <. ( 1r ` R ) , ( 1r ` R ) >. ] .~ ) -> [ <. ( P .x. r ) , ( ( 1r ` R ) .x. s ) >. ] .~ = [ <. ( 1r ` R ) , ( 1r ` R ) >. ] .~ )
104 1 7 2 94 95 98 100 101 102 103 erld2 
 |-  ( ( ( ( ph /\ r e. B ) /\ s e. S ) /\ [ <. ( P .x. r ) , ( ( 1r ` R ) .x. s ) >. ] .~ = [ <. ( 1r ` R ) , ( 1r ` R ) >. ] .~ ) -> E. t e. S ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) )
105 77 47 63 93 104 syl1111anc 
 |-  ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) -> E. t e. S ( t .x. ( ( P .x. r ) .x. ( 1r ` R ) ) ) = ( t .x. ( ( 1r ` R ) .x. ( ( 1r ` R ) .x. s ) ) ) )
106 76 105 r19.29a 
 |-  ( ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ s e. S ) /\ x = [ <. r , s >. ] .~ ) -> E. u e. B ( P .x. u ) e. S )
107 106 r19.29an 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) /\ r e. B ) /\ E. s e. S x = [ <. r , s >. ] .~ ) -> E. u e. B ( P .x. u ) e. S )
108 37 eleq2d 
 |-  ( ph -> ( x e. ( ( B X. S ) /. .~ ) <-> x e. ( Base ` L ) ) )
109 108 biimpar 
 |-  ( ( ph /\ x e. ( Base ` L ) ) -> x e. ( ( B X. S ) /. .~ ) )
110 109 adantr 
 |-  ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) -> x e. ( ( B X. S ) /. .~ ) )
111 110 elrlocbasi 
 |-  ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) -> E. r e. B E. s e. S x = [ <. r , s >. ] .~ )
112 107 111 r19.29a 
 |-  ( ( ( ph /\ x e. ( Base ` L ) ) /\ ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) -> E. u e. B ( P .x. u ) e. S )
113 112 r19.29an 
 |-  ( ( ph /\ E. x e. ( Base ` L ) ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) ) -> E. u e. B ( P .x. u ) e. S )
114 simplr 
 |-  ( ( ( ph /\ u e. B ) /\ ( P .x. u ) e. S ) -> u e. B )
115 simpr 
 |-  ( ( ( ph /\ u e. B ) /\ ( P .x. u ) e. S ) -> ( P .x. u ) e. S )
116 114 115 opelxpd 
 |-  ( ( ( ph /\ u e. B ) /\ ( P .x. u ) e. S ) -> <. u , ( P .x. u ) >. e. ( B X. S ) )
117 28 ecelqsi 
 |-  ( <. u , ( P .x. u ) >. e. ( B X. S ) -> [ <. u , ( P .x. u ) >. ] .~ e. ( ( B X. S ) /. .~ ) )
118 116 117 syl 
 |-  ( ( ( ph /\ u e. B ) /\ ( P .x. u ) e. S ) -> [ <. u , ( P .x. u ) >. ] .~ e. ( ( B X. S ) /. .~ ) )
119 37 ad2antrr 
 |-  ( ( ( ph /\ u e. B ) /\ ( P .x. u ) e. S ) -> ( ( B X. S ) /. .~ ) = ( Base ` L ) )
120 118 119 eleqtrd 
 |-  ( ( ( ph /\ u e. B ) /\ ( P .x. u ) e. S ) -> [ <. u , ( P .x. u ) >. ] .~ e. ( Base ` L ) )
121 oveq2 
 |-  ( x = [ <. u , ( P .x. u ) >. ] .~ -> ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) [ <. u , ( P .x. u ) >. ] .~ ) )
122 121 eqeq1d 
 |-  ( x = [ <. u , ( P .x. u ) >. ] .~ -> ( ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) <-> ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) [ <. u , ( P .x. u ) >. ] .~ ) = ( 1r ` L ) ) )
123 122 adantl 
 |-  ( ( ( ( ph /\ u e. B ) /\ ( P .x. u ) e. S ) /\ x = [ <. u , ( P .x. u ) >. ] .~ ) -> ( ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) <-> ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) [ <. u , ( P .x. u ) >. ] .~ ) = ( 1r ` L ) ) )
124 5 ad2antrr 
 |-  ( ( ( ph /\ u e. B ) /\ ( P .x. u ) e. S ) -> R e. CRing )
125 6 ad2antrr 
 |-  ( ( ( ph /\ u e. B ) /\ ( P .x. u ) e. S ) -> S e. ( SubMnd ` ( mulGrp ` R ) ) )
126 8 ad2antrr 
 |-  ( ( ( ph /\ u e. B ) /\ ( P .x. u ) e. S ) -> P e. B )
127 125 25 syl 
 |-  ( ( ( ph /\ u e. B ) /\ ( P .x. u ) e. S ) -> ( 1r ` R ) e. S )
128 1 2 39 3 7 124 125 126 114 127 115 20 rlocmulval 
 |-  ( ( ( ph /\ u e. B ) /\ ( P .x. u ) e. S ) -> ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) [ <. u , ( P .x. u ) >. ] .~ ) = [ <. ( P .x. u ) , ( ( 1r ` R ) .x. ( P .x. u ) ) >. ] .~ )
129 1 31 23 2 32 33 7 5 6 erler 
 |-  ( ph -> .~ Er ( B X. S ) )
130 129 ad2antrr 
 |-  ( ( ( ph /\ u e. B ) /\ ( P .x. u ) e. S ) -> .~ Er ( B X. S ) )
131 eqidd 
 |-  ( ( ( ph /\ u e. B ) /\ ( P .x. u ) e. S ) -> <. ( 1r ` R ) , ( 1r ` R ) >. = <. ( 1r ` R ) , ( 1r ` R ) >. )
132 eqidd 
 |-  ( ( ( ph /\ u e. B ) /\ ( P .x. u ) e. S ) -> ( P .x. u ) = ( P .x. u ) )
133 42 ad2antrr 
 |-  ( ( ( ph /\ u e. B ) /\ ( P .x. u ) e. S ) -> R e. Ring )
134 1 2 133 126 114 ringcld 
 |-  ( ( ( ph /\ u e. B ) /\ ( P .x. u ) e. S ) -> ( P .x. u ) e. B )
135 1 2 23 133 134 ringlidmd 
 |-  ( ( ( ph /\ u e. B ) /\ ( P .x. u ) e. S ) -> ( ( 1r ` R ) .x. ( P .x. u ) ) = ( P .x. u ) )
136 132 135 opeq12d 
 |-  ( ( ( ph /\ u e. B ) /\ ( P .x. u ) e. S ) -> <. ( P .x. u ) , ( ( 1r ` R ) .x. ( P .x. u ) ) >. = <. ( P .x. u ) , ( P .x. u ) >. )
137 61 ad2antrr 
 |-  ( ( ( ph /\ u e. B ) /\ ( P .x. u ) e. S ) -> ( 1r ` R ) e. B )
138 1 2 23 133 134 ringridmd 
 |-  ( ( ( ph /\ u e. B ) /\ ( P .x. u ) e. S ) -> ( ( P .x. u ) .x. ( 1r ` R ) ) = ( P .x. u ) )
139 138 eqcomd 
 |-  ( ( ( ph /\ u e. B ) /\ ( P .x. u ) e. S ) -> ( P .x. u ) = ( ( P .x. u ) .x. ( 1r ` R ) ) )
140 1 7 124 125 2 131 136 137 134 127 115 115 139 139 erlbr2d 
 |-  ( ( ( ph /\ u e. B ) /\ ( P .x. u ) e. S ) -> <. ( 1r ` R ) , ( 1r ` R ) >. .~ <. ( P .x. u ) , ( ( 1r ` R ) .x. ( P .x. u ) ) >. )
141 130 140 erthi 
 |-  ( ( ( ph /\ u e. B ) /\ ( P .x. u ) e. S ) -> [ <. ( 1r ` R ) , ( 1r ` R ) >. ] .~ = [ <. ( P .x. u ) , ( ( 1r ` R ) .x. ( P .x. u ) ) >. ] .~ )
142 31 23 3 7 124 125 90 rloc1r 
 |-  ( ( ( ph /\ u e. B ) /\ ( P .x. u ) e. S ) -> [ <. ( 1r ` R ) , ( 1r ` R ) >. ] .~ = ( 1r ` L ) )
143 128 141 142 3eqtr2d 
 |-  ( ( ( ph /\ u e. B ) /\ ( P .x. u ) e. S ) -> ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) [ <. u , ( P .x. u ) >. ] .~ ) = ( 1r ` L ) )
144 120 123 143 rspcedvd 
 |-  ( ( ( ph /\ u e. B ) /\ ( P .x. u ) e. S ) -> E. x e. ( Base ` L ) ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) )
145 144 r19.29an 
 |-  ( ( ph /\ E. u e. B ( P .x. u ) e. S ) -> E. x e. ( Base ` L ) ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) )
146 113 145 impbida 
 |-  ( ph -> ( E. x e. ( Base ` L ) ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) x ) = ( 1r ` L ) <-> E. u e. B ( P .x. u ) e. S ) )
147 oveq2 
 |-  ( u = s -> ( P .x. u ) = ( P .x. s ) )
148 147 eleq1d 
 |-  ( u = s -> ( ( P .x. u ) e. S <-> ( P .x. s ) e. S ) )
149 148 cbvrexvw 
 |-  ( E. u e. B ( P .x. u ) e. S <-> E. s e. B ( P .x. s ) e. S )
150 149 a1i 
 |-  ( ph -> ( E. u e. B ( P .x. u ) e. S <-> E. s e. B ( P .x. s ) e. S ) )
151 41 146 150 3bitrd 
 |-  ( ph -> ( [ <. P , ( 1r ` R ) >. ] .~ e. W <-> E. s e. B ( P .x. s ) e. S ) )
152 5 adantr 
 |-  ( ( ph /\ Q e. S ) -> R e. CRing )
153 6 adantr 
 |-  ( ( ph /\ Q e. S ) -> S e. ( SubMnd ` ( mulGrp ` R ) ) )
154 simpr 
 |-  ( ( ph /\ Q e. S ) -> Q e. S )
155 1 23 7 3 4 152 153 154 rlocinvunit 
 |-  ( ( ph /\ Q e. S ) -> [ <. ( 1r ` R ) , Q >. ] .~ e. W )
156 9 155 mpdan 
 |-  ( ph -> [ <. ( 1r ` R ) , Q >. ] .~ e. W )
157 156 biantrud 
 |-  ( ph -> ( [ <. P , ( 1r ` R ) >. ] .~ e. W <-> ( [ <. P , ( 1r ` R ) >. ] .~ e. W /\ [ <. ( 1r ` R ) , Q >. ] .~ e. W ) ) )
158 1 2 39 3 7 5 6 8 61 26 9 20 rlocmulval 
 |-  ( ph -> ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) [ <. ( 1r ` R ) , Q >. ] .~ ) = [ <. ( P .x. ( 1r ` R ) ) , ( ( 1r ` R ) .x. Q ) >. ] .~ )
159 1 2 23 42 8 ringridmd 
 |-  ( ph -> ( P .x. ( 1r ` R ) ) = P )
160 36 9 sseldd 
 |-  ( ph -> Q e. B )
161 1 2 23 42 160 ringlidmd 
 |-  ( ph -> ( ( 1r ` R ) .x. Q ) = Q )
162 159 161 opeq12d 
 |-  ( ph -> <. ( P .x. ( 1r ` R ) ) , ( ( 1r ` R ) .x. Q ) >. = <. P , Q >. )
163 162 eceq1d 
 |-  ( ph -> [ <. ( P .x. ( 1r ` R ) ) , ( ( 1r ` R ) .x. Q ) >. ] .~ = [ <. P , Q >. ] .~ )
164 158 163 eqtrd 
 |-  ( ph -> ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) [ <. ( 1r ` R ) , Q >. ] .~ ) = [ <. P , Q >. ] .~ )
165 164 eleq1d 
 |-  ( ph -> ( ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) [ <. ( 1r ` R ) , Q >. ] .~ ) e. W <-> [ <. P , Q >. ] .~ e. W ) )
166 61 9 opelxpd 
 |-  ( ph -> <. ( 1r ` R ) , Q >. e. ( B X. S ) )
167 28 ecelqsi 
 |-  ( <. ( 1r ` R ) , Q >. e. ( B X. S ) -> [ <. ( 1r ` R ) , Q >. ] .~ e. ( ( B X. S ) /. .~ ) )
168 166 167 syl 
 |-  ( ph -> [ <. ( 1r ` R ) , Q >. ] .~ e. ( ( B X. S ) /. .~ ) )
169 168 37 eleqtrd 
 |-  ( ph -> [ <. ( 1r ` R ) , Q >. ] .~ e. ( Base ` L ) )
170 4 20 19 unitmulclb 
 |-  ( ( L e. CRing /\ [ <. P , ( 1r ` R ) >. ] .~ e. ( Base ` L ) /\ [ <. ( 1r ` R ) , Q >. ] .~ e. ( Base ` L ) ) -> ( ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) [ <. ( 1r ` R ) , Q >. ] .~ ) e. W <-> ( [ <. P , ( 1r ` R ) >. ] .~ e. W /\ [ <. ( 1r ` R ) , Q >. ] .~ e. W ) ) )
171 40 38 169 170 syl3anc 
 |-  ( ph -> ( ( [ <. P , ( 1r ` R ) >. ] .~ ( .r ` L ) [ <. ( 1r ` R ) , Q >. ] .~ ) e. W <-> ( [ <. P , ( 1r ` R ) >. ] .~ e. W /\ [ <. ( 1r ` R ) , Q >. ] .~ e. W ) ) )
172 165 171 bitr3d 
 |-  ( ph -> ( [ <. P , Q >. ] .~ e. W <-> ( [ <. P , ( 1r ` R ) >. ] .~ e. W /\ [ <. ( 1r ` R ) , Q >. ] .~ e. W ) ) )
173 157 172 bitr4d 
 |-  ( ph -> ( [ <. P , ( 1r ` R ) >. ] .~ e. W <-> [ <. P , Q >. ] .~ e. W ) )
174 18 151 173 3bitr2rd 
 |-  ( ph -> ( [ <. P , Q >. ] .~ e. W <-> P e. T ) )