Theorem smfmullem2

Description: The multiplication of two sigma-measurable functions is measurable: this is the step (i) of the proof of Proposition 121E (d) of Fremlin1 p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smfmullem2.a	|- ( ph -> A e. RR )
	smfmullem2.k	|- K = { q e. ( QQ ^m ( 0 ... 3 ) ) | A. u e. ( ( q ` 0 ) (,) ( q ` 1 ) ) A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( u x. v ) < A }
	smfmullem2.u	|- ( ph -> U e. RR )
	smfmullem2.v	|- ( ph -> V e. RR )
	smfmullem2.l	|- ( ph -> ( U x. V ) < A )
	smfmullem2.p	|- ( ph -> P e. QQ )
	smfmullem2.r	|- ( ph -> R e. QQ )
	smfmullem2.s	|- ( ph -> S e. QQ )
	smfmullem2.z	|- ( ph -> Z e. QQ )
	smfmullem2.p2	|- ( ph -> P e. ( ( U - Y ) (,) U ) )
	smfmullem2.42	|- ( ph -> R e. ( U (,) ( U + Y ) ) )
	smfmullem2.w2	|- ( ph -> S e. ( ( V - Y ) (,) V ) )
	smfmullem2.z2	|- ( ph -> Z e. ( V (,) ( V + Y ) ) )
	smfmullem2.x	|- X = ( ( A - ( U x. V ) ) / ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) )
	smfmullem2.y	|- Y = if ( 1 <_ X , 1 , X )
Assertion	smfmullem2	|- ( ph -> E. q e. K ( U e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ V e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		smfmullem2.a	|- ( ph -> A e. RR )
2		smfmullem2.k	|- K = { q e. ( QQ ^m ( 0 ... 3 ) ) | A. u e. ( ( q ` 0 ) (,) ( q ` 1 ) ) A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( u x. v ) < A }
3		smfmullem2.u	|- ( ph -> U e. RR )
4		smfmullem2.v	|- ( ph -> V e. RR )
5		smfmullem2.l	|- ( ph -> ( U x. V ) < A )
6		smfmullem2.p	|- ( ph -> P e. QQ )
7		smfmullem2.r	|- ( ph -> R e. QQ )
8		smfmullem2.s	|- ( ph -> S e. QQ )
9		smfmullem2.z	|- ( ph -> Z e. QQ )
10		smfmullem2.p2	|- ( ph -> P e. ( ( U - Y ) (,) U ) )
11		smfmullem2.42	|- ( ph -> R e. ( U (,) ( U + Y ) ) )
12		smfmullem2.w2	|- ( ph -> S e. ( ( V - Y ) (,) V ) )
13		smfmullem2.z2	|- ( ph -> Z e. ( V (,) ( V + Y ) ) )
14		smfmullem2.x	|- X = ( ( A - ( U x. V ) ) / ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) )
15		smfmullem2.y	|- Y = if ( 1 <_ X , 1 , X )
16	6 7 8 9	s4cld	|- ( ph -> <" P R S Z "> e. Word QQ )
17		s4len	|- ( # ` <" P R S Z "> ) = 4
18	17	a1i	|- ( ph -> ( # ` <" P R S Z "> ) = 4 )
19	16 18	jca	|- ( ph -> ( <" P R S Z "> e. Word QQ /\ ( # ` <" P R S Z "> ) = 4 ) )
20		qex	|- QQ e. _V
21	20	a1i	|- ( ph -> QQ e. _V )
22		4nn0	|- 4 e. NN0
23	22	a1i	|- ( ph -> 4 e. NN0 )
24		wrdmap	|- ( ( QQ e. _V /\ 4 e. NN0 ) -> ( ( <" P R S Z "> e. Word QQ /\ ( # ` <" P R S Z "> ) = 4 ) <-> <" P R S Z "> e. ( QQ ^m ( 0 ..^ 4 ) ) ) )
25	21 23 24	syl2anc	|- ( ph -> ( ( <" P R S Z "> e. Word QQ /\ ( # ` <" P R S Z "> ) = 4 ) <-> <" P R S Z "> e. ( QQ ^m ( 0 ..^ 4 ) ) ) )
26	19 25	mpbid	|- ( ph -> <" P R S Z "> e. ( QQ ^m ( 0 ..^ 4 ) ) )
27		3z	|- 3 e. ZZ
28		fzval3	|- ( 3 e. ZZ -> ( 0 ... 3 ) = ( 0 ..^ ( 3 + 1 ) ) )
29	27 28	ax-mp	|- ( 0 ... 3 ) = ( 0 ..^ ( 3 + 1 ) )
30		3p1e4	|- ( 3 + 1 ) = 4
31	30	oveq2i	|- ( 0 ..^ ( 3 + 1 ) ) = ( 0 ..^ 4 )
32	29 31	eqtri	|- ( 0 ... 3 ) = ( 0 ..^ 4 )
33	32	eqcomi	|- ( 0 ..^ 4 ) = ( 0 ... 3 )
34	33	a1i	|- ( ph -> ( 0 ..^ 4 ) = ( 0 ... 3 ) )
35	34	oveq2d	|- ( ph -> ( QQ ^m ( 0 ..^ 4 ) ) = ( QQ ^m ( 0 ... 3 ) ) )
36	26 35	eleqtrd	|- ( ph -> <" P R S Z "> e. ( QQ ^m ( 0 ... 3 ) ) )
37		simpr	|- ( ( ph /\ u e. ( ( <" P R S Z "> ` 0 ) (,) ( <" P R S Z "> ` 1 ) ) ) -> u e. ( ( <" P R S Z "> ` 0 ) (,) ( <" P R S Z "> ` 1 ) ) )
38		s4fv0	|- ( P e. QQ -> ( <" P R S Z "> ` 0 ) = P )
39	6 38	syl	|- ( ph -> ( <" P R S Z "> ` 0 ) = P )
40		s4fv1	|- ( R e. QQ -> ( <" P R S Z "> ` 1 ) = R )
41	7 40	syl	|- ( ph -> ( <" P R S Z "> ` 1 ) = R )
42	39 41	oveq12d	|- ( ph -> ( ( <" P R S Z "> ` 0 ) (,) ( <" P R S Z "> ` 1 ) ) = ( P (,) R ) )
43	42	adantr	|- ( ( ph /\ u e. ( ( <" P R S Z "> ` 0 ) (,) ( <" P R S Z "> ` 1 ) ) ) -> ( ( <" P R S Z "> ` 0 ) (,) ( <" P R S Z "> ` 1 ) ) = ( P (,) R ) )
44	37 43	eleqtrd	|- ( ( ph /\ u e. ( ( <" P R S Z "> ` 0 ) (,) ( <" P R S Z "> ` 1 ) ) ) -> u e. ( P (,) R ) )
45		simpr	|- ( ( ph /\ v e. ( ( <" P R S Z "> ` 2 ) (,) ( <" P R S Z "> ` 3 ) ) ) -> v e. ( ( <" P R S Z "> ` 2 ) (,) ( <" P R S Z "> ` 3 ) ) )
46		s4fv2	|- ( S e. QQ -> ( <" P R S Z "> ` 2 ) = S )
47	8 46	syl	|- ( ph -> ( <" P R S Z "> ` 2 ) = S )
48		s4fv3	|- ( Z e. QQ -> ( <" P R S Z "> ` 3 ) = Z )
49	9 48	syl	|- ( ph -> ( <" P R S Z "> ` 3 ) = Z )
50	47 49	oveq12d	|- ( ph -> ( ( <" P R S Z "> ` 2 ) (,) ( <" P R S Z "> ` 3 ) ) = ( S (,) Z ) )
51	50	adantr	|- ( ( ph /\ v e. ( ( <" P R S Z "> ` 2 ) (,) ( <" P R S Z "> ` 3 ) ) ) -> ( ( <" P R S Z "> ` 2 ) (,) ( <" P R S Z "> ` 3 ) ) = ( S (,) Z ) )
52	45 51	eleqtrd	|- ( ( ph /\ v e. ( ( <" P R S Z "> ` 2 ) (,) ( <" P R S Z "> ` 3 ) ) ) -> v e. ( S (,) Z ) )
53		simpr	|- ( ( ph /\ v e. ( S (,) Z ) ) -> v e. ( S (,) Z ) )
54	52 53	syldan	|- ( ( ph /\ v e. ( ( <" P R S Z "> ` 2 ) (,) ( <" P R S Z "> ` 3 ) ) ) -> v e. ( S (,) Z ) )
55	54	adantlr	|- ( ( ( ph /\ u e. ( P (,) R ) ) /\ v e. ( ( <" P R S Z "> ` 2 ) (,) ( <" P R S Z "> ` 3 ) ) ) -> v e. ( S (,) Z ) )
56	1	ad2antrr	|- ( ( ( ph /\ u e. ( P (,) R ) ) /\ v e. ( S (,) Z ) ) -> A e. RR )
57	3	ad2antrr	|- ( ( ( ph /\ u e. ( P (,) R ) ) /\ v e. ( S (,) Z ) ) -> U e. RR )
58	4	ad2antrr	|- ( ( ( ph /\ u e. ( P (,) R ) ) /\ v e. ( S (,) Z ) ) -> V e. RR )
59	5	ad2antrr	|- ( ( ( ph /\ u e. ( P (,) R ) ) /\ v e. ( S (,) Z ) ) -> ( U x. V ) < A )
60	10	ad2antrr	|- ( ( ( ph /\ u e. ( P (,) R ) ) /\ v e. ( S (,) Z ) ) -> P e. ( ( U - Y ) (,) U ) )
61	11	ad2antrr	|- ( ( ( ph /\ u e. ( P (,) R ) ) /\ v e. ( S (,) Z ) ) -> R e. ( U (,) ( U + Y ) ) )
62	12	ad2antrr	|- ( ( ( ph /\ u e. ( P (,) R ) ) /\ v e. ( S (,) Z ) ) -> S e. ( ( V - Y ) (,) V ) )
63	13	ad2antrr	|- ( ( ( ph /\ u e. ( P (,) R ) ) /\ v e. ( S (,) Z ) ) -> Z e. ( V (,) ( V + Y ) ) )
64		simplr	|- ( ( ( ph /\ u e. ( P (,) R ) ) /\ v e. ( S (,) Z ) ) -> u e. ( P (,) R ) )
65		simpr	|- ( ( ( ph /\ u e. ( P (,) R ) ) /\ v e. ( S (,) Z ) ) -> v e. ( S (,) Z ) )
66	56 57 58 59 14 15 60 61 62 63 64 65	smfmullem1	|- ( ( ( ph /\ u e. ( P (,) R ) ) /\ v e. ( S (,) Z ) ) -> ( u x. v ) < A )
67	55 66	syldan	|- ( ( ( ph /\ u e. ( P (,) R ) ) /\ v e. ( ( <" P R S Z "> ` 2 ) (,) ( <" P R S Z "> ` 3 ) ) ) -> ( u x. v ) < A )
68	67	ralrimiva	|- ( ( ph /\ u e. ( P (,) R ) ) -> A. v e. ( ( <" P R S Z "> ` 2 ) (,) ( <" P R S Z "> ` 3 ) ) ( u x. v ) < A )
69	44 68	syldan	|- ( ( ph /\ u e. ( ( <" P R S Z "> ` 0 ) (,) ( <" P R S Z "> ` 1 ) ) ) -> A. v e. ( ( <" P R S Z "> ` 2 ) (,) ( <" P R S Z "> ` 3 ) ) ( u x. v ) < A )
70	69	ralrimiva	|- ( ph -> A. u e. ( ( <" P R S Z "> ` 0 ) (,) ( <" P R S Z "> ` 1 ) ) A. v e. ( ( <" P R S Z "> ` 2 ) (,) ( <" P R S Z "> ` 3 ) ) ( u x. v ) < A )
71	36 70	jca	|- ( ph -> ( <" P R S Z "> e. ( QQ ^m ( 0 ... 3 ) ) /\ A. u e. ( ( <" P R S Z "> ` 0 ) (,) ( <" P R S Z "> ` 1 ) ) A. v e. ( ( <" P R S Z "> ` 2 ) (,) ( <" P R S Z "> ` 3 ) ) ( u x. v ) < A ) )
72		fveq1	|- ( q = <" P R S Z "> -> ( q ` 0 ) = ( <" P R S Z "> ` 0 ) )
73		fveq1	|- ( q = <" P R S Z "> -> ( q ` 1 ) = ( <" P R S Z "> ` 1 ) )
74	72 73	oveq12d	|- ( q = <" P R S Z "> -> ( ( q ` 0 ) (,) ( q ` 1 ) ) = ( ( <" P R S Z "> ` 0 ) (,) ( <" P R S Z "> ` 1 ) ) )
75	74	raleqdv	|- ( q = <" P R S Z "> -> ( A. u e. ( ( q ` 0 ) (,) ( q ` 1 ) ) A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( u x. v ) < A <-> A. u e. ( ( <" P R S Z "> ` 0 ) (,) ( <" P R S Z "> ` 1 ) ) A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( u x. v ) < A ) )
76		fveq1	|- ( q = <" P R S Z "> -> ( q ` 2 ) = ( <" P R S Z "> ` 2 ) )
77		fveq1	|- ( q = <" P R S Z "> -> ( q ` 3 ) = ( <" P R S Z "> ` 3 ) )
78	76 77	oveq12d	|- ( q = <" P R S Z "> -> ( ( q ` 2 ) (,) ( q ` 3 ) ) = ( ( <" P R S Z "> ` 2 ) (,) ( <" P R S Z "> ` 3 ) ) )
79	78	raleqdv	|- ( q = <" P R S Z "> -> ( A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( u x. v ) < A <-> A. v e. ( ( <" P R S Z "> ` 2 ) (,) ( <" P R S Z "> ` 3 ) ) ( u x. v ) < A ) )
80	79	ralbidv	|- ( q = <" P R S Z "> -> ( A. u e. ( ( <" P R S Z "> ` 0 ) (,) ( <" P R S Z "> ` 1 ) ) A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( u x. v ) < A <-> A. u e. ( ( <" P R S Z "> ` 0 ) (,) ( <" P R S Z "> ` 1 ) ) A. v e. ( ( <" P R S Z "> ` 2 ) (,) ( <" P R S Z "> ` 3 ) ) ( u x. v ) < A ) )
81	75 80	bitrd	|- ( q = <" P R S Z "> -> ( A. u e. ( ( q ` 0 ) (,) ( q ` 1 ) ) A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( u x. v ) < A <-> A. u e. ( ( <" P R S Z "> ` 0 ) (,) ( <" P R S Z "> ` 1 ) ) A. v e. ( ( <" P R S Z "> ` 2 ) (,) ( <" P R S Z "> ` 3 ) ) ( u x. v ) < A ) )
82	81 2	elrab2	|- ( <" P R S Z "> e. K <-> ( <" P R S Z "> e. ( QQ ^m ( 0 ... 3 ) ) /\ A. u e. ( ( <" P R S Z "> ` 0 ) (,) ( <" P R S Z "> ` 1 ) ) A. v e. ( ( <" P R S Z "> ` 2 ) (,) ( <" P R S Z "> ` 3 ) ) ( u x. v ) < A ) )
83	71 82	sylibr	|- ( ph -> <" P R S Z "> e. K )
84		qssre	|- QQ C_ RR
85	84 6	sseldi	|- ( ph -> P e. RR )
86	85	rexrd	|- ( ph -> P e. RR* )
87	84 7	sseldi	|- ( ph -> R e. RR )
88	87	rexrd	|- ( ph -> R e. RR* )
89	15	a1i	|- ( ph -> Y = if ( 1 <_ X , 1 , X ) )
90		1rp	|- 1 e. RR+
91	90	a1i	|- ( ph -> 1 e. RR+ )
92	14	a1i	|- ( ph -> X = ( ( A - ( U x. V ) ) / ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) ) )
93	3 4	remulcld	|- ( ph -> ( U x. V ) e. RR )
94		difrp	|- ( ( ( U x. V ) e. RR /\ A e. RR ) -> ( ( U x. V ) < A <-> ( A - ( U x. V ) ) e. RR+ ) )
95	93 1 94	syl2anc	|- ( ph -> ( ( U x. V ) < A <-> ( A - ( U x. V ) ) e. RR+ ) )
96	5 95	mpbid	|- ( ph -> ( A - ( U x. V ) ) e. RR+ )
97		1red	|- ( ph -> 1 e. RR )
98	3	recnd	|- ( ph -> U e. CC )
99	98	abscld	|- ( ph -> ( abs ` U ) e. RR )
100	4	recnd	|- ( ph -> V e. CC )
101	100	abscld	|- ( ph -> ( abs ` V ) e. RR )
102	99 101	readdcld	|- ( ph -> ( ( abs ` U ) + ( abs ` V ) ) e. RR )
103	97 102	readdcld	|- ( ph -> ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) e. RR )
104		0re	|- 0 e. RR
105	104	a1i	|- ( ph -> 0 e. RR )
106	91	rpgt0d	|- ( ph -> 0 < 1 )
107	98	absge0d	|- ( ph -> 0 <_ ( abs ` U ) )
108	100	absge0d	|- ( ph -> 0 <_ ( abs ` V ) )
109	99 101	addge01d	|- ( ph -> ( 0 <_ ( abs ` V ) <-> ( abs ` U ) <_ ( ( abs ` U ) + ( abs ` V ) ) ) )
110	108 109	mpbid	|- ( ph -> ( abs ` U ) <_ ( ( abs ` U ) + ( abs ` V ) ) )
111	105 99 102 107 110	letrd	|- ( ph -> 0 <_ ( ( abs ` U ) + ( abs ` V ) ) )
112	97 102	addge01d	|- ( ph -> ( 0 <_ ( ( abs ` U ) + ( abs ` V ) ) <-> 1 <_ ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) ) )
113	111 112	mpbid	|- ( ph -> 1 <_ ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) )
114	105 97 103 106 113	ltletrd	|- ( ph -> 0 < ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) )
115	103 114	elrpd	|- ( ph -> ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) e. RR+ )
116	96 115	rpdivcld	|- ( ph -> ( ( A - ( U x. V ) ) / ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) ) e. RR+ )
117	92 116	eqeltrd	|- ( ph -> X e. RR+ )
118	91 117	ifcld	|- ( ph -> if ( 1 <_ X , 1 , X ) e. RR+ )
119	89 118	eqeltrd	|- ( ph -> Y e. RR+ )
120	119	rpred	|- ( ph -> Y e. RR )
121	3 120	resubcld	|- ( ph -> ( U - Y ) e. RR )
122	121	rexrd	|- ( ph -> ( U - Y ) e. RR* )
123	3	rexrd	|- ( ph -> U e. RR* )
124		iooltub	|- ( ( ( U - Y ) e. RR* /\ U e. RR* /\ P e. ( ( U - Y ) (,) U ) ) -> P < U )
125	122 123 10 124	syl3anc	|- ( ph -> P < U )
126	3 120	readdcld	|- ( ph -> ( U + Y ) e. RR )
127	126	rexrd	|- ( ph -> ( U + Y ) e. RR* )
128		ioogtlb	|- ( ( U e. RR* /\ ( U + Y ) e. RR* /\ R e. ( U (,) ( U + Y ) ) ) -> U < R )
129	123 127 11 128	syl3anc	|- ( ph -> U < R )
130	86 88 3 125 129	eliood	|- ( ph -> U e. ( P (,) R ) )
131	42	eqcomd	|- ( ph -> ( P (,) R ) = ( ( <" P R S Z "> ` 0 ) (,) ( <" P R S Z "> ` 1 ) ) )
132	130 131	eleqtrd	|- ( ph -> U e. ( ( <" P R S Z "> ` 0 ) (,) ( <" P R S Z "> ` 1 ) ) )
133	84 8	sseldi	|- ( ph -> S e. RR )
134	133	rexrd	|- ( ph -> S e. RR* )
135	84 9	sseldi	|- ( ph -> Z e. RR )
136	135	rexrd	|- ( ph -> Z e. RR* )
137	4 120	resubcld	|- ( ph -> ( V - Y ) e. RR )
138	137	rexrd	|- ( ph -> ( V - Y ) e. RR* )
139	4	rexrd	|- ( ph -> V e. RR* )
140		iooltub	|- ( ( ( V - Y ) e. RR* /\ V e. RR* /\ S e. ( ( V - Y ) (,) V ) ) -> S < V )
141	138 139 12 140	syl3anc	|- ( ph -> S < V )
142	4 120	readdcld	|- ( ph -> ( V + Y ) e. RR )
143	142	rexrd	|- ( ph -> ( V + Y ) e. RR* )
144		ioogtlb	|- ( ( V e. RR* /\ ( V + Y ) e. RR* /\ Z e. ( V (,) ( V + Y ) ) ) -> V < Z )
145	139 143 13 144	syl3anc	|- ( ph -> V < Z )
146	134 136 4 141 145	eliood	|- ( ph -> V e. ( S (,) Z ) )
147	50	eqcomd	|- ( ph -> ( S (,) Z ) = ( ( <" P R S Z "> ` 2 ) (,) ( <" P R S Z "> ` 3 ) ) )
148	146 147	eleqtrd	|- ( ph -> V e. ( ( <" P R S Z "> ` 2 ) (,) ( <" P R S Z "> ` 3 ) ) )
149	132 148	jca	|- ( ph -> ( U e. ( ( <" P R S Z "> ` 0 ) (,) ( <" P R S Z "> ` 1 ) ) /\ V e. ( ( <" P R S Z "> ` 2 ) (,) ( <" P R S Z "> ` 3 ) ) ) )
150		nfv	|- F/ q ( U e. ( ( <" P R S Z "> ` 0 ) (,) ( <" P R S Z "> ` 1 ) ) /\ V e. ( ( <" P R S Z "> ` 2 ) (,) ( <" P R S Z "> ` 3 ) ) )
151		nfcv	|- F/_ q <" P R S Z ">
152		nfrab1	|- F/_ q { q e. ( QQ ^m ( 0 ... 3 ) ) | A. u e. ( ( q ` 0 ) (,) ( q ` 1 ) ) A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( u x. v ) < A }
153	2 152	nfcxfr	|- F/_ q K
154	74	eleq2d	|- ( q = <" P R S Z "> -> ( U e. ( ( q ` 0 ) (,) ( q ` 1 ) ) <-> U e. ( ( <" P R S Z "> ` 0 ) (,) ( <" P R S Z "> ` 1 ) ) ) )
155	78	eleq2d	|- ( q = <" P R S Z "> -> ( V e. ( ( q ` 2 ) (,) ( q ` 3 ) ) <-> V e. ( ( <" P R S Z "> ` 2 ) (,) ( <" P R S Z "> ` 3 ) ) ) )
156	154 155	anbi12d	|- ( q = <" P R S Z "> -> ( ( U e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ V e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) <-> ( U e. ( ( <" P R S Z "> ` 0 ) (,) ( <" P R S Z "> ` 1 ) ) /\ V e. ( ( <" P R S Z "> ` 2 ) (,) ( <" P R S Z "> ` 3 ) ) ) ) )
157	150 151 153 156	rspcef	|- ( ( <" P R S Z "> e. K /\ ( U e. ( ( <" P R S Z "> ` 0 ) (,) ( <" P R S Z "> ` 1 ) ) /\ V e. ( ( <" P R S Z "> ` 2 ) (,) ( <" P R S Z "> ` 3 ) ) ) ) -> E. q e. K ( U e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ V e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) )
158	83 149 157	syl2anc	|- ( ph -> E. q e. K ( U e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ V e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) )