MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prlem936 Structured version   Visualization version   GIF version

Theorem prlem936 11044
Description: Lemma 9-3.6 of [Gleason] p. 124. (Contributed by NM, 26-Apr-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
Assertion
Ref Expression
prlem936 ((๐ด โˆˆ P โˆง 1Q <Q ๐ต) โ†’ โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ ยทQ ๐ต) โˆˆ ๐ด)
Distinct variable groups:   ๐‘ฅ,๐ด   ๐‘ฅ,๐ต

Proof of Theorem prlem936
Dummy variables ๐‘ฆ ๐‘ง ๐‘ ๐‘ข ๐‘ฃ ๐‘ค are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ltrelnq 10923 . . . . 5 <Q โŠ† (Q ร— Q)
21brel 5740 . . . 4 (1Q <Q ๐ต โ†’ (1Q โˆˆ Q โˆง ๐ต โˆˆ Q))
32simprd 494 . . 3 (1Q <Q ๐ต โ†’ ๐ต โˆˆ Q)
43adantl 480 . 2 ((๐ด โˆˆ P โˆง 1Q <Q ๐ต) โ†’ ๐ต โˆˆ Q)
5 breq2 5151 . . . . 5 (๐‘ = ๐ต โ†’ (1Q <Q ๐‘ โ†” 1Q <Q ๐ต))
65anbi2d 627 . . . 4 (๐‘ = ๐ต โ†’ ((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โ†” (๐ด โˆˆ P โˆง 1Q <Q ๐ต)))
7 oveq2 7419 . . . . . . 7 (๐‘ = ๐ต โ†’ (๐‘ฅ ยทQ ๐‘) = (๐‘ฅ ยทQ ๐ต))
87eleq1d 2816 . . . . . 6 (๐‘ = ๐ต โ†’ ((๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด โ†” (๐‘ฅ ยทQ ๐ต) โˆˆ ๐ด))
98notbid 317 . . . . 5 (๐‘ = ๐ต โ†’ (ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด โ†” ยฌ (๐‘ฅ ยทQ ๐ต) โˆˆ ๐ด))
109rexbidv 3176 . . . 4 (๐‘ = ๐ต โ†’ (โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด โ†” โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ ยทQ ๐ต) โˆˆ ๐ด))
116, 10imbi12d 343 . . 3 (๐‘ = ๐ต โ†’ (((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โ†’ โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด) โ†” ((๐ด โˆˆ P โˆง 1Q <Q ๐ต) โ†’ โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ ยทQ ๐ต) โˆˆ ๐ด)))
12 prn0 10986 . . . . . 6 (๐ด โˆˆ P โ†’ ๐ด โ‰  โˆ…)
13 n0 4345 . . . . . 6 (๐ด โ‰  โˆ… โ†” โˆƒ๐‘ฆ ๐‘ฆ โˆˆ ๐ด)
1412, 13sylib 217 . . . . 5 (๐ด โˆˆ P โ†’ โˆƒ๐‘ฆ ๐‘ฆ โˆˆ ๐ด)
1514adantr 479 . . . 4 ((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โ†’ โˆƒ๐‘ฆ ๐‘ฆ โˆˆ ๐ด)
16 elprnq 10988 . . . . . . . . . . 11 ((๐ด โˆˆ P โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ ๐‘ฆ โˆˆ Q)
1716ad2ant2r 743 . . . . . . . . . 10 (((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โ†’ ๐‘ฆ โˆˆ Q)
18 mulidnq 10960 . . . . . . . . . 10 (๐‘ฆ โˆˆ Q โ†’ (๐‘ฆ ยทQ 1Q) = ๐‘ฆ)
1917, 18syl 17 . . . . . . . . 9 (((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โ†’ (๐‘ฆ ยทQ 1Q) = ๐‘ฆ)
20 simplr 765 . . . . . . . . . 10 (((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โ†’ 1Q <Q ๐‘)
21 ltmnq 10969 . . . . . . . . . . 11 (๐‘ฆ โˆˆ Q โ†’ (1Q <Q ๐‘ โ†” (๐‘ฆ ยทQ 1Q) <Q (๐‘ฆ ยทQ ๐‘)))
2221biimpa 475 . . . . . . . . . 10 ((๐‘ฆ โˆˆ Q โˆง 1Q <Q ๐‘) โ†’ (๐‘ฆ ยทQ 1Q) <Q (๐‘ฆ ยทQ ๐‘))
2317, 20, 22syl2anc 582 . . . . . . . . 9 (((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โ†’ (๐‘ฆ ยทQ 1Q) <Q (๐‘ฆ ยทQ ๐‘))
2419, 23eqbrtrrd 5171 . . . . . . . 8 (((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โ†’ ๐‘ฆ <Q (๐‘ฆ ยทQ ๐‘))
251brel 5740 . . . . . . . . . . . 12 (1Q <Q ๐‘ โ†’ (1Q โˆˆ Q โˆง ๐‘ โˆˆ Q))
2625simprd 494 . . . . . . . . . . 11 (1Q <Q ๐‘ โ†’ ๐‘ โˆˆ Q)
2726ad2antlr 723 . . . . . . . . . 10 (((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โ†’ ๐‘ โˆˆ Q)
28 mulclnq 10944 . . . . . . . . . 10 ((๐‘ฆ โˆˆ Q โˆง ๐‘ โˆˆ Q) โ†’ (๐‘ฆ ยทQ ๐‘) โˆˆ Q)
2917, 27, 28syl2anc 582 . . . . . . . . 9 (((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โ†’ (๐‘ฆ ยทQ ๐‘) โˆˆ Q)
30 ltexnq 10972 . . . . . . . . 9 ((๐‘ฆ ยทQ ๐‘) โˆˆ Q โ†’ (๐‘ฆ <Q (๐‘ฆ ยทQ ๐‘) โ†” โˆƒ๐‘ง(๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)))
3129, 30syl 17 . . . . . . . 8 (((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โ†’ (๐‘ฆ <Q (๐‘ฆ ยทQ ๐‘) โ†” โˆƒ๐‘ง(๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)))
3224, 31mpbid 231 . . . . . . 7 (((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โ†’ โˆƒ๐‘ง(๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘))
33 simplll 771 . . . . . . . . 9 ((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โ†’ ๐ด โˆˆ P)
34 vex 3476 . . . . . . . . . 10 ๐‘ง โˆˆ V
3534prlem934 11030 . . . . . . . . 9 (๐ด โˆˆ P โ†’ โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ +Q ๐‘ง) โˆˆ ๐ด)
3633, 35syl 17 . . . . . . . 8 ((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โ†’ โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ +Q ๐‘ง) โˆˆ ๐ด)
3733adantr 479 . . . . . . . . . . . 12 (((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โˆง ๐‘ฅ โˆˆ ๐ด) โ†’ ๐ด โˆˆ P)
38 simprr 769 . . . . . . . . . . . . . 14 (((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โ†’ (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)
39 eleq1 2819 . . . . . . . . . . . . . . 15 ((๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘) โ†’ ((๐‘ฆ +Q ๐‘ง) โˆˆ ๐ด โ†” (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด))
4039biimparc 478 . . . . . . . . . . . . . 14 (((๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โ†’ (๐‘ฆ +Q ๐‘ง) โˆˆ ๐ด)
4138, 40sylan 578 . . . . . . . . . . . . 13 ((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โ†’ (๐‘ฆ +Q ๐‘ง) โˆˆ ๐ด)
4241adantr 479 . . . . . . . . . . . 12 (((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โˆง ๐‘ฅ โˆˆ ๐ด) โ†’ (๐‘ฆ +Q ๐‘ง) โˆˆ ๐ด)
43 elprnq 10988 . . . . . . . . . . . . . 14 ((๐ด โˆˆ P โˆง ๐‘ฅ โˆˆ ๐ด) โ†’ ๐‘ฅ โˆˆ Q)
4433, 43sylan 578 . . . . . . . . . . . . 13 (((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โˆง ๐‘ฅ โˆˆ ๐ด) โ†’ ๐‘ฅ โˆˆ Q)
45 elprnq 10988 . . . . . . . . . . . . . . . 16 ((๐ด โˆˆ P โˆง (๐‘ฆ +Q ๐‘ง) โˆˆ ๐ด) โ†’ (๐‘ฆ +Q ๐‘ง) โˆˆ Q)
46 addnqf 10945 . . . . . . . . . . . . . . . . . . 19 +Q :(Q ร— Q)โŸถQ
4746fdmi 6728 . . . . . . . . . . . . . . . . . 18 dom +Q = (Q ร— Q)
48 0nnq 10921 . . . . . . . . . . . . . . . . . 18 ยฌ โˆ… โˆˆ Q
4947, 48ndmovrcl 7595 . . . . . . . . . . . . . . . . 17 ((๐‘ฆ +Q ๐‘ง) โˆˆ Q โ†’ (๐‘ฆ โˆˆ Q โˆง ๐‘ง โˆˆ Q))
5049simprd 494 . . . . . . . . . . . . . . . 16 ((๐‘ฆ +Q ๐‘ง) โˆˆ Q โ†’ ๐‘ง โˆˆ Q)
5145, 50syl 17 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ P โˆง (๐‘ฆ +Q ๐‘ง) โˆˆ ๐ด) โ†’ ๐‘ง โˆˆ Q)
5233, 41, 51syl2anc 582 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โ†’ ๐‘ง โˆˆ Q)
5352adantr 479 . . . . . . . . . . . . 13 (((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โˆง ๐‘ฅ โˆˆ ๐ด) โ†’ ๐‘ง โˆˆ Q)
54 addclnq 10942 . . . . . . . . . . . . 13 ((๐‘ฅ โˆˆ Q โˆง ๐‘ง โˆˆ Q) โ†’ (๐‘ฅ +Q ๐‘ง) โˆˆ Q)
5544, 53, 54syl2anc 582 . . . . . . . . . . . 12 (((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โˆง ๐‘ฅ โˆˆ ๐ด) โ†’ (๐‘ฅ +Q ๐‘ง) โˆˆ Q)
56 prub 10991 . . . . . . . . . . . 12 (((๐ด โˆˆ P โˆง (๐‘ฆ +Q ๐‘ง) โˆˆ ๐ด) โˆง (๐‘ฅ +Q ๐‘ง) โˆˆ Q) โ†’ (ยฌ (๐‘ฅ +Q ๐‘ง) โˆˆ ๐ด โ†’ (๐‘ฆ +Q ๐‘ง) <Q (๐‘ฅ +Q ๐‘ง)))
5737, 42, 55, 56syl21anc 834 . . . . . . . . . . 11 (((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โˆง ๐‘ฅ โˆˆ ๐ด) โ†’ (ยฌ (๐‘ฅ +Q ๐‘ง) โˆˆ ๐ด โ†’ (๐‘ฆ +Q ๐‘ง) <Q (๐‘ฅ +Q ๐‘ง)))
5827ad2antrr 722 . . . . . . . . . . . . 13 (((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โˆง ๐‘ฅ โˆˆ ๐ด) โ†’ ๐‘ โˆˆ Q)
59 mulclnq 10944 . . . . . . . . . . . . 13 ((๐‘ฅ โˆˆ Q โˆง ๐‘ โˆˆ Q) โ†’ (๐‘ฅ ยทQ ๐‘) โˆˆ Q)
6044, 58, 59syl2anc 582 . . . . . . . . . . . 12 (((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โˆง ๐‘ฅ โˆˆ ๐ด) โ†’ (๐‘ฅ ยทQ ๐‘) โˆˆ Q)
6117ad2antrr 722 . . . . . . . . . . . 12 (((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โˆง ๐‘ฅ โˆˆ ๐ด) โ†’ ๐‘ฆ โˆˆ Q)
62 simplr 765 . . . . . . . . . . . 12 (((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โˆง ๐‘ฅ โˆˆ ๐ด) โ†’ (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘))
63 recclnq 10963 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฆ โˆˆ Q โ†’ (*Qโ€˜๐‘ฆ) โˆˆ Q)
64 mulclnq 10944 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ง โˆˆ Q โˆง (*Qโ€˜๐‘ฆ) โˆˆ Q) โ†’ (๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) โˆˆ Q)
6563, 64sylan2 591 . . . . . . . . . . . . . . . . . . 19 ((๐‘ง โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โ†’ (๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) โˆˆ Q)
6665ancoms 457 . . . . . . . . . . . . . . . . . 18 ((๐‘ฆ โˆˆ Q โˆง ๐‘ง โˆˆ Q) โ†’ (๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) โˆˆ Q)
67 ltmnq 10969 . . . . . . . . . . . . . . . . . 18 ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) โˆˆ Q โ†’ (๐‘ฆ <Q ๐‘ฅ โ†” ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฆ) <Q ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ)))
6866, 67syl 17 . . . . . . . . . . . . . . . . 17 ((๐‘ฆ โˆˆ Q โˆง ๐‘ง โˆˆ Q) โ†’ (๐‘ฆ <Q ๐‘ฅ โ†” ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฆ) <Q ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ)))
69 mulassnq 10956 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฆ) = (๐‘ง ยทQ ((*Qโ€˜๐‘ฆ) ยทQ ๐‘ฆ))
70 mulcomnq 10950 . . . . . . . . . . . . . . . . . . . . 21 ((*Qโ€˜๐‘ฆ) ยทQ ๐‘ฆ) = (๐‘ฆ ยทQ (*Qโ€˜๐‘ฆ))
7170oveq2i 7422 . . . . . . . . . . . . . . . . . . . 20 (๐‘ง ยทQ ((*Qโ€˜๐‘ฆ) ยทQ ๐‘ฆ)) = (๐‘ง ยทQ (๐‘ฆ ยทQ (*Qโ€˜๐‘ฆ)))
7269, 71eqtri 2758 . . . . . . . . . . . . . . . . . . 19 ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฆ) = (๐‘ง ยทQ (๐‘ฆ ยทQ (*Qโ€˜๐‘ฆ)))
73 recidnq 10962 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฆ โˆˆ Q โ†’ (๐‘ฆ ยทQ (*Qโ€˜๐‘ฆ)) = 1Q)
7473oveq2d 7427 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฆ โˆˆ Q โ†’ (๐‘ง ยทQ (๐‘ฆ ยทQ (*Qโ€˜๐‘ฆ))) = (๐‘ง ยทQ 1Q))
75 mulidnq 10960 . . . . . . . . . . . . . . . . . . . 20 (๐‘ง โˆˆ Q โ†’ (๐‘ง ยทQ 1Q) = ๐‘ง)
7674, 75sylan9eq 2790 . . . . . . . . . . . . . . . . . . 19 ((๐‘ฆ โˆˆ Q โˆง ๐‘ง โˆˆ Q) โ†’ (๐‘ง ยทQ (๐‘ฆ ยทQ (*Qโ€˜๐‘ฆ))) = ๐‘ง)
7772, 76eqtrid 2782 . . . . . . . . . . . . . . . . . 18 ((๐‘ฆ โˆˆ Q โˆง ๐‘ง โˆˆ Q) โ†’ ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฆ) = ๐‘ง)
7877breq1d 5157 . . . . . . . . . . . . . . . . 17 ((๐‘ฆ โˆˆ Q โˆง ๐‘ง โˆˆ Q) โ†’ (((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฆ) <Q ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ) โ†” ๐‘ง <Q ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ)))
7968, 78bitrd 278 . . . . . . . . . . . . . . . 16 ((๐‘ฆ โˆˆ Q โˆง ๐‘ง โˆˆ Q) โ†’ (๐‘ฆ <Q ๐‘ฅ โ†” ๐‘ง <Q ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ)))
8079adantll 710 . . . . . . . . . . . . . . 15 ((((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โˆง ๐‘ง โˆˆ Q) โ†’ (๐‘ฆ <Q ๐‘ฅ โ†” ๐‘ง <Q ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ)))
81 mulnqf 10946 . . . . . . . . . . . . . . . . . . . . . 22 ยทQ :(Q ร— Q)โŸถQ
8281fdmi 6728 . . . . . . . . . . . . . . . . . . . . 21 dom ยทQ = (Q ร— Q)
8382, 48ndmovrcl 7595 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ฅ ยทQ ๐‘) โˆˆ Q โ†’ (๐‘ฅ โˆˆ Q โˆง ๐‘ โˆˆ Q))
8483simpld 493 . . . . . . . . . . . . . . . . . . 19 ((๐‘ฅ ยทQ ๐‘) โˆˆ Q โ†’ ๐‘ฅ โˆˆ Q)
85 ltanq 10968 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ โˆˆ Q โ†’ (๐‘ง <Q ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ) โ†” (๐‘ฅ +Q ๐‘ง) <Q (๐‘ฅ +Q ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ))))
8684, 85syl 17 . . . . . . . . . . . . . . . . . 18 ((๐‘ฅ ยทQ ๐‘) โˆˆ Q โ†’ (๐‘ง <Q ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ) โ†” (๐‘ฅ +Q ๐‘ง) <Q (๐‘ฅ +Q ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ))))
8786adantr 479 . . . . . . . . . . . . . . . . 17 (((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โ†’ (๐‘ง <Q ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ) โ†” (๐‘ฅ +Q ๐‘ง) <Q (๐‘ฅ +Q ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ))))
88 vex 3476 . . . . . . . . . . . . . . . . . . . 20 ๐‘ฆ โˆˆ V
89 ovex 7444 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ)) โˆˆ V
90 mulcomnq 10950 . . . . . . . . . . . . . . . . . . . 20 (๐‘ข ยทQ ๐‘ค) = (๐‘ค ยทQ ๐‘ข)
91 distrnq 10958 . . . . . . . . . . . . . . . . . . . 20 (๐‘ข ยทQ (๐‘ค +Q ๐‘ฃ)) = ((๐‘ข ยทQ ๐‘ค) +Q (๐‘ข ยทQ ๐‘ฃ))
9288, 34, 89, 90, 91caovdir 7643 . . . . . . . . . . . . . . . . . . 19 ((๐‘ฆ +Q ๐‘ง) ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) = ((๐‘ฆ ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) +Q (๐‘ง ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))))
93 vex 3476 . . . . . . . . . . . . . . . . . . . . . 22 ๐‘ฅ โˆˆ V
94 fvex 6903 . . . . . . . . . . . . . . . . . . . . . 22 (*Qโ€˜๐‘ฆ) โˆˆ V
95 mulassnq 10956 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ข ยทQ ๐‘ค) ยทQ ๐‘ฃ) = (๐‘ข ยทQ (๐‘ค ยทQ ๐‘ฃ))
9688, 93, 94, 90, 95caov12 7637 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฆ ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) = (๐‘ฅ ยทQ (๐‘ฆ ยทQ (*Qโ€˜๐‘ฆ)))
9773oveq2d 7427 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฆ โˆˆ Q โ†’ (๐‘ฅ ยทQ (๐‘ฆ ยทQ (*Qโ€˜๐‘ฆ))) = (๐‘ฅ ยทQ 1Q))
98 mulidnq 10960 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฅ โˆˆ Q โ†’ (๐‘ฅ ยทQ 1Q) = ๐‘ฅ)
9984, 98syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ฅ ยทQ ๐‘) โˆˆ Q โ†’ (๐‘ฅ ยทQ 1Q) = ๐‘ฅ)
10097, 99sylan9eqr 2792 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โ†’ (๐‘ฅ ยทQ (๐‘ฆ ยทQ (*Qโ€˜๐‘ฆ))) = ๐‘ฅ)
10196, 100eqtrid 2782 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โ†’ (๐‘ฆ ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) = ๐‘ฅ)
102 mulcomnq 10950 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ)) = ((*Qโ€˜๐‘ฆ) ยทQ ๐‘ฅ)
103102oveq2i 7422 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ง ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) = (๐‘ง ยทQ ((*Qโ€˜๐‘ฆ) ยทQ ๐‘ฅ))
104 mulassnq 10956 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ) = (๐‘ง ยทQ ((*Qโ€˜๐‘ฆ) ยทQ ๐‘ฅ))
105103, 104eqtr4i 2761 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ง ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) = ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ)
106105a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โ†’ (๐‘ง ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) = ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ))
107101, 106oveq12d 7429 . . . . . . . . . . . . . . . . . . 19 (((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โ†’ ((๐‘ฆ ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) +Q (๐‘ง ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ)))) = (๐‘ฅ +Q ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ)))
10892, 107eqtrid 2782 . . . . . . . . . . . . . . . . . 18 (((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โ†’ ((๐‘ฆ +Q ๐‘ง) ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) = (๐‘ฅ +Q ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ)))
109108breq2d 5159 . . . . . . . . . . . . . . . . 17 (((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โ†’ ((๐‘ฅ +Q ๐‘ง) <Q ((๐‘ฆ +Q ๐‘ง) ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) โ†” (๐‘ฅ +Q ๐‘ง) <Q (๐‘ฅ +Q ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ))))
11087, 109bitr4d 281 . . . . . . . . . . . . . . . 16 (((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โ†’ (๐‘ง <Q ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ) โ†” (๐‘ฅ +Q ๐‘ง) <Q ((๐‘ฆ +Q ๐‘ง) ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ)))))
111110adantr 479 . . . . . . . . . . . . . . 15 ((((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โˆง ๐‘ง โˆˆ Q) โ†’ (๐‘ง <Q ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ) โ†” (๐‘ฅ +Q ๐‘ง) <Q ((๐‘ฆ +Q ๐‘ง) ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ)))))
11280, 111bitrd 278 . . . . . . . . . . . . . 14 ((((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โˆง ๐‘ง โˆˆ Q) โ†’ (๐‘ฆ <Q ๐‘ฅ โ†” (๐‘ฅ +Q ๐‘ง) <Q ((๐‘ฆ +Q ๐‘ง) ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ)))))
113112adantrr 713 . . . . . . . . . . . . 13 ((((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โˆง (๐‘ง โˆˆ Q โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘))) โ†’ (๐‘ฆ <Q ๐‘ฅ โ†” (๐‘ฅ +Q ๐‘ง) <Q ((๐‘ฆ +Q ๐‘ง) ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ)))))
114 ltanq 10968 . . . . . . . . . . . . . . 15 (๐‘ง โˆˆ Q โ†’ (๐‘ฆ <Q ๐‘ฅ โ†” (๐‘ง +Q ๐‘ฆ) <Q (๐‘ง +Q ๐‘ฅ)))
115 addcomnq 10948 . . . . . . . . . . . . . . . 16 (๐‘ง +Q ๐‘ฆ) = (๐‘ฆ +Q ๐‘ง)
116 addcomnq 10948 . . . . . . . . . . . . . . . 16 (๐‘ง +Q ๐‘ฅ) = (๐‘ฅ +Q ๐‘ง)
117115, 116breq12i 5156 . . . . . . . . . . . . . . 15 ((๐‘ง +Q ๐‘ฆ) <Q (๐‘ง +Q ๐‘ฅ) โ†” (๐‘ฆ +Q ๐‘ง) <Q (๐‘ฅ +Q ๐‘ง))
118114, 117bitrdi 286 . . . . . . . . . . . . . 14 (๐‘ง โˆˆ Q โ†’ (๐‘ฆ <Q ๐‘ฅ โ†” (๐‘ฆ +Q ๐‘ง) <Q (๐‘ฅ +Q ๐‘ง)))
119118ad2antrl 724 . . . . . . . . . . . . 13 ((((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โˆง (๐‘ง โˆˆ Q โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘))) โ†’ (๐‘ฆ <Q ๐‘ฅ โ†” (๐‘ฆ +Q ๐‘ง) <Q (๐‘ฅ +Q ๐‘ง)))
120 oveq1 7418 . . . . . . . . . . . . . . . 16 ((๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘) โ†’ ((๐‘ฆ +Q ๐‘ง) ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) = ((๐‘ฆ ยทQ ๐‘) ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))))
121 vex 3476 . . . . . . . . . . . . . . . . . 18 ๐‘ โˆˆ V
12288, 121, 93, 90, 95, 94caov411 7641 . . . . . . . . . . . . . . . . 17 ((๐‘ฆ ยทQ ๐‘) ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) = ((๐‘ฅ ยทQ ๐‘) ยทQ (๐‘ฆ ยทQ (*Qโ€˜๐‘ฆ)))
12373oveq2d 7427 . . . . . . . . . . . . . . . . . 18 (๐‘ฆ โˆˆ Q โ†’ ((๐‘ฅ ยทQ ๐‘) ยทQ (๐‘ฆ ยทQ (*Qโ€˜๐‘ฆ))) = ((๐‘ฅ ยทQ ๐‘) ยทQ 1Q))
124 mulidnq 10960 . . . . . . . . . . . . . . . . . 18 ((๐‘ฅ ยทQ ๐‘) โˆˆ Q โ†’ ((๐‘ฅ ยทQ ๐‘) ยทQ 1Q) = (๐‘ฅ ยทQ ๐‘))
125123, 124sylan9eqr 2792 . . . . . . . . . . . . . . . . 17 (((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โ†’ ((๐‘ฅ ยทQ ๐‘) ยทQ (๐‘ฆ ยทQ (*Qโ€˜๐‘ฆ))) = (๐‘ฅ ยทQ ๐‘))
126122, 125eqtrid 2782 . . . . . . . . . . . . . . . 16 (((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โ†’ ((๐‘ฆ ยทQ ๐‘) ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) = (๐‘ฅ ยทQ ๐‘))
127120, 126sylan9eqr 2792 . . . . . . . . . . . . . . 15 ((((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โ†’ ((๐‘ฆ +Q ๐‘ง) ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) = (๐‘ฅ ยทQ ๐‘))
128127breq2d 5159 . . . . . . . . . . . . . 14 ((((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โ†’ ((๐‘ฅ +Q ๐‘ง) <Q ((๐‘ฆ +Q ๐‘ง) ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) โ†” (๐‘ฅ +Q ๐‘ง) <Q (๐‘ฅ ยทQ ๐‘)))
129128adantrl 712 . . . . . . . . . . . . 13 ((((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โˆง (๐‘ง โˆˆ Q โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘))) โ†’ ((๐‘ฅ +Q ๐‘ง) <Q ((๐‘ฆ +Q ๐‘ง) ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) โ†” (๐‘ฅ +Q ๐‘ง) <Q (๐‘ฅ ยทQ ๐‘)))
130113, 119, 1293bitr3d 308 . . . . . . . . . . . 12 ((((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โˆง (๐‘ง โˆˆ Q โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘))) โ†’ ((๐‘ฆ +Q ๐‘ง) <Q (๐‘ฅ +Q ๐‘ง) โ†” (๐‘ฅ +Q ๐‘ง) <Q (๐‘ฅ ยทQ ๐‘)))
13160, 61, 53, 62, 130syl22anc 835 . . . . . . . . . . 11 (((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โˆง ๐‘ฅ โˆˆ ๐ด) โ†’ ((๐‘ฆ +Q ๐‘ง) <Q (๐‘ฅ +Q ๐‘ง) โ†” (๐‘ฅ +Q ๐‘ง) <Q (๐‘ฅ ยทQ ๐‘)))
13257, 131sylibd 238 . . . . . . . . . 10 (((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โˆง ๐‘ฅ โˆˆ ๐ด) โ†’ (ยฌ (๐‘ฅ +Q ๐‘ง) โˆˆ ๐ด โ†’ (๐‘ฅ +Q ๐‘ง) <Q (๐‘ฅ ยทQ ๐‘)))
133 prcdnq 10990 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ P โˆง (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด) โ†’ ((๐‘ฅ +Q ๐‘ง) <Q (๐‘ฅ ยทQ ๐‘) โ†’ (๐‘ฅ +Q ๐‘ง) โˆˆ ๐ด))
134133impancom 450 . . . . . . . . . . . . . 14 ((๐ด โˆˆ P โˆง (๐‘ฅ +Q ๐‘ง) <Q (๐‘ฅ ยทQ ๐‘)) โ†’ ((๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด โ†’ (๐‘ฅ +Q ๐‘ง) โˆˆ ๐ด))
135134con3d 152 . . . . . . . . . . . . 13 ((๐ด โˆˆ P โˆง (๐‘ฅ +Q ๐‘ง) <Q (๐‘ฅ ยทQ ๐‘)) โ†’ (ยฌ (๐‘ฅ +Q ๐‘ง) โˆˆ ๐ด โ†’ ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด))
136135ex 411 . . . . . . . . . . . 12 (๐ด โˆˆ P โ†’ ((๐‘ฅ +Q ๐‘ง) <Q (๐‘ฅ ยทQ ๐‘) โ†’ (ยฌ (๐‘ฅ +Q ๐‘ง) โˆˆ ๐ด โ†’ ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด)))
137136com23 86 . . . . . . . . . . 11 (๐ด โˆˆ P โ†’ (ยฌ (๐‘ฅ +Q ๐‘ง) โˆˆ ๐ด โ†’ ((๐‘ฅ +Q ๐‘ง) <Q (๐‘ฅ ยทQ ๐‘) โ†’ ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด)))
13837, 137syl 17 . . . . . . . . . 10 (((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โˆง ๐‘ฅ โˆˆ ๐ด) โ†’ (ยฌ (๐‘ฅ +Q ๐‘ง) โˆˆ ๐ด โ†’ ((๐‘ฅ +Q ๐‘ง) <Q (๐‘ฅ ยทQ ๐‘) โ†’ ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด)))
139132, 138mpdd 43 . . . . . . . . 9 (((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โˆง ๐‘ฅ โˆˆ ๐ด) โ†’ (ยฌ (๐‘ฅ +Q ๐‘ง) โˆˆ ๐ด โ†’ ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด))
140139reximdva 3166 . . . . . . . 8 ((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โ†’ (โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ +Q ๐‘ง) โˆˆ ๐ด โ†’ โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด))
14136, 140mpd 15 . . . . . . 7 ((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โ†’ โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด)
14232, 141exlimddv 1936 . . . . . 6 (((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โ†’ โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด)
143142expr 455 . . . . 5 (((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ ((๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด โ†’ โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด))
144 oveq1 7418 . . . . . . . . . 10 (๐‘ฅ = ๐‘ฆ โ†’ (๐‘ฅ ยทQ ๐‘) = (๐‘ฆ ยทQ ๐‘))
145144eleq1d 2816 . . . . . . . . 9 (๐‘ฅ = ๐‘ฆ โ†’ ((๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด โ†” (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด))
146145notbid 317 . . . . . . . 8 (๐‘ฅ = ๐‘ฆ โ†’ (ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด โ†” ยฌ (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด))
147146rspcev 3611 . . . . . . 7 ((๐‘ฆ โˆˆ ๐ด โˆง ยฌ (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด) โ†’ โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด)
148147ex 411 . . . . . 6 (๐‘ฆ โˆˆ ๐ด โ†’ (ยฌ (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด โ†’ โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด))
149148adantl 480 . . . . 5 (((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ (ยฌ (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด โ†’ โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด))
150143, 149pm2.61d 179 . . . 4 (((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด)
15115, 150exlimddv 1936 . . 3 ((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โ†’ โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด)
15211, 151vtoclg 3541 . 2 (๐ต โˆˆ Q โ†’ ((๐ด โˆˆ P โˆง 1Q <Q ๐ต) โ†’ โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ ยทQ ๐ต) โˆˆ ๐ด))
1534, 152mpcom 38 1 ((๐ด โˆˆ P โˆง 1Q <Q ๐ต) โ†’ โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ ยทQ ๐ต) โˆˆ ๐ด)
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 394   = wceq 1539  โˆƒwex 1779   โˆˆ wcel 2104   โ‰  wne 2938  โˆƒwrex 3068  โˆ…c0 4321   class class class wbr 5147   ร— cxp 5673  โ€˜cfv 6542  (class class class)co 7411  Qcnq 10849  1Qc1q 10850   +Q cplq 10852   ยทQ cmq 10853  *Qcrq 10854   <Q cltq 10855  Pcnp 10856
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-oadd 8472  df-omul 8473  df-er 8705  df-ni 10869  df-pli 10870  df-mi 10871  df-lti 10872  df-plpq 10905  df-mpq 10906  df-ltpq 10907  df-enq 10908  df-nq 10909  df-erq 10910  df-plq 10911  df-mq 10912  df-1nq 10913  df-rq 10914  df-ltnq 10915  df-np 10978
This theorem is referenced by:  reclem3pr  11046
  Copyright terms: Public domain W3C validator