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

Theorem prlem936 11037
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 10916 . . . . 5 <Q โІ (Q ร— Q)
21brel 5731 . . . 4 (1Q <Q ๐ต โ†’ (1Q โˆˆ Q โˆง ๐ต โˆˆ Q))
32simprd 495 . . 3 (1Q <Q ๐ต โ†’ ๐ต โˆˆ Q)
43adantl 481 . 2 ((๐ด โˆˆ P โˆง 1Q <Q ๐ต) โ†’ ๐ต โˆˆ Q)
5 breq2 5142 . . . . 5 (๐‘ = ๐ต โ†’ (1Q <Q ๐‘ โ†” 1Q <Q ๐ต))
65anbi2d 628 . . . 4 (๐‘ = ๐ต โ†’ ((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โ†” (๐ด โˆˆ P โˆง 1Q <Q ๐ต)))
7 oveq2 7409 . . . . . . 7 (๐‘ = ๐ต โ†’ (๐‘ฅ ยทQ ๐‘) = (๐‘ฅ ยทQ ๐ต))
87eleq1d 2810 . . . . . 6 (๐‘ = ๐ต โ†’ ((๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด โ†” (๐‘ฅ ยทQ ๐ต) โˆˆ ๐ด))
98notbid 318 . . . . 5 (๐‘ = ๐ต โ†’ (ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด โ†” ยฌ (๐‘ฅ ยทQ ๐ต) โˆˆ ๐ด))
109rexbidv 3170 . . . 4 (๐‘ = ๐ต โ†’ (โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด โ†” โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ ยทQ ๐ต) โˆˆ ๐ด))
116, 10imbi12d 344 . . 3 (๐‘ = ๐ต โ†’ (((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โ†’ โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด) โ†” ((๐ด โˆˆ P โˆง 1Q <Q ๐ต) โ†’ โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ ยทQ ๐ต) โˆˆ ๐ด)))
12 prn0 10979 . . . . . 6 (๐ด โˆˆ P โ†’ ๐ด โ‰  โˆ…)
13 n0 4338 . . . . . 6 (๐ด โ‰  โˆ… โ†” โˆƒ๐‘ฆ ๐‘ฆ โˆˆ ๐ด)
1412, 13sylib 217 . . . . 5 (๐ด โˆˆ P โ†’ โˆƒ๐‘ฆ ๐‘ฆ โˆˆ ๐ด)
1514adantr 480 . . . 4 ((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โ†’ โˆƒ๐‘ฆ ๐‘ฆ โˆˆ ๐ด)
16 elprnq 10981 . . . . . . . . . . 11 ((๐ด โˆˆ P โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ ๐‘ฆ โˆˆ Q)
1716ad2ant2r 744 . . . . . . . . . 10 (((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โ†’ ๐‘ฆ โˆˆ Q)
18 mulidnq 10953 . . . . . . . . . 10 (๐‘ฆ โˆˆ Q โ†’ (๐‘ฆ ยทQ 1Q) = ๐‘ฆ)
1917, 18syl 17 . . . . . . . . 9 (((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โ†’ (๐‘ฆ ยทQ 1Q) = ๐‘ฆ)
20 simplr 766 . . . . . . . . . 10 (((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โ†’ 1Q <Q ๐‘)
21 ltmnq 10962 . . . . . . . . . . 11 (๐‘ฆ โˆˆ Q โ†’ (1Q <Q ๐‘ โ†” (๐‘ฆ ยทQ 1Q) <Q (๐‘ฆ ยทQ ๐‘)))
2221biimpa 476 . . . . . . . . . 10 ((๐‘ฆ โˆˆ Q โˆง 1Q <Q ๐‘) โ†’ (๐‘ฆ ยทQ 1Q) <Q (๐‘ฆ ยทQ ๐‘))
2317, 20, 22syl2anc 583 . . . . . . . . 9 (((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โ†’ (๐‘ฆ ยทQ 1Q) <Q (๐‘ฆ ยทQ ๐‘))
2419, 23eqbrtrrd 5162 . . . . . . . 8 (((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โ†’ ๐‘ฆ <Q (๐‘ฆ ยทQ ๐‘))
251brel 5731 . . . . . . . . . . . 12 (1Q <Q ๐‘ โ†’ (1Q โˆˆ Q โˆง ๐‘ โˆˆ Q))
2625simprd 495 . . . . . . . . . . 11 (1Q <Q ๐‘ โ†’ ๐‘ โˆˆ Q)
2726ad2antlr 724 . . . . . . . . . 10 (((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โ†’ ๐‘ โˆˆ Q)
28 mulclnq 10937 . . . . . . . . . 10 ((๐‘ฆ โˆˆ Q โˆง ๐‘ โˆˆ Q) โ†’ (๐‘ฆ ยทQ ๐‘) โˆˆ Q)
2917, 27, 28syl2anc 583 . . . . . . . . 9 (((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โ†’ (๐‘ฆ ยทQ ๐‘) โˆˆ Q)
30 ltexnq 10965 . . . . . . . . 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 772 . . . . . . . . 9 ((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โ†’ ๐ด โˆˆ P)
34 vex 3470 . . . . . . . . . 10 ๐‘ง โˆˆ V
3534prlem934 11023 . . . . . . . . 9 (๐ด โˆˆ P โ†’ โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ +Q ๐‘ง) โˆˆ ๐ด)
3633, 35syl 17 . . . . . . . 8 ((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โ†’ โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ +Q ๐‘ง) โˆˆ ๐ด)
3733adantr 480 . . . . . . . . . . . 12 (((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โˆง ๐‘ฅ โˆˆ ๐ด) โ†’ ๐ด โˆˆ P)
38 simprr 770 . . . . . . . . . . . . . 14 (((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โ†’ (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)
39 eleq1 2813 . . . . . . . . . . . . . . 15 ((๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘) โ†’ ((๐‘ฆ +Q ๐‘ง) โˆˆ ๐ด โ†” (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด))
4039biimparc 479 . . . . . . . . . . . . . 14 (((๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โ†’ (๐‘ฆ +Q ๐‘ง) โˆˆ ๐ด)
4138, 40sylan 579 . . . . . . . . . . . . 13 ((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โ†’ (๐‘ฆ +Q ๐‘ง) โˆˆ ๐ด)
4241adantr 480 . . . . . . . . . . . 12 (((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โˆง ๐‘ฅ โˆˆ ๐ด) โ†’ (๐‘ฆ +Q ๐‘ง) โˆˆ ๐ด)
43 elprnq 10981 . . . . . . . . . . . . . 14 ((๐ด โˆˆ P โˆง ๐‘ฅ โˆˆ ๐ด) โ†’ ๐‘ฅ โˆˆ Q)
4433, 43sylan 579 . . . . . . . . . . . . 13 (((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โˆง ๐‘ฅ โˆˆ ๐ด) โ†’ ๐‘ฅ โˆˆ Q)
45 elprnq 10981 . . . . . . . . . . . . . . . 16 ((๐ด โˆˆ P โˆง (๐‘ฆ +Q ๐‘ง) โˆˆ ๐ด) โ†’ (๐‘ฆ +Q ๐‘ง) โˆˆ Q)
46 addnqf 10938 . . . . . . . . . . . . . . . . . . 19 +Q :(Q ร— Q)โŸถQ
4746fdmi 6719 . . . . . . . . . . . . . . . . . 18 dom +Q = (Q ร— Q)
48 0nnq 10914 . . . . . . . . . . . . . . . . . 18 ยฌ โˆ… โˆˆ Q
4947, 48ndmovrcl 7586 . . . . . . . . . . . . . . . . 17 ((๐‘ฆ +Q ๐‘ง) โˆˆ Q โ†’ (๐‘ฆ โˆˆ Q โˆง ๐‘ง โˆˆ Q))
5049simprd 495 . . . . . . . . . . . . . . . 16 ((๐‘ฆ +Q ๐‘ง) โˆˆ Q โ†’ ๐‘ง โˆˆ Q)
5145, 50syl 17 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ P โˆง (๐‘ฆ +Q ๐‘ง) โˆˆ ๐ด) โ†’ ๐‘ง โˆˆ Q)
5233, 41, 51syl2anc 583 . . . . . . . . . . . . . 14 ((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โ†’ ๐‘ง โˆˆ Q)
5352adantr 480 . . . . . . . . . . . . 13 (((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โˆง ๐‘ฅ โˆˆ ๐ด) โ†’ ๐‘ง โˆˆ Q)
54 addclnq 10935 . . . . . . . . . . . . 13 ((๐‘ฅ โˆˆ Q โˆง ๐‘ง โˆˆ Q) โ†’ (๐‘ฅ +Q ๐‘ง) โˆˆ Q)
5544, 53, 54syl2anc 583 . . . . . . . . . . . 12 (((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โˆง ๐‘ฅ โˆˆ ๐ด) โ†’ (๐‘ฅ +Q ๐‘ง) โˆˆ Q)
56 prub 10984 . . . . . . . . . . . 12 (((๐ด โˆˆ P โˆง (๐‘ฆ +Q ๐‘ง) โˆˆ ๐ด) โˆง (๐‘ฅ +Q ๐‘ง) โˆˆ Q) โ†’ (ยฌ (๐‘ฅ +Q ๐‘ง) โˆˆ ๐ด โ†’ (๐‘ฆ +Q ๐‘ง) <Q (๐‘ฅ +Q ๐‘ง)))
5737, 42, 55, 56syl21anc 835 . . . . . . . . . . 11 (((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โˆง ๐‘ฅ โˆˆ ๐ด) โ†’ (ยฌ (๐‘ฅ +Q ๐‘ง) โˆˆ ๐ด โ†’ (๐‘ฆ +Q ๐‘ง) <Q (๐‘ฅ +Q ๐‘ง)))
5827ad2antrr 723 . . . . . . . . . . . . 13 (((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โˆง ๐‘ฅ โˆˆ ๐ด) โ†’ ๐‘ โˆˆ Q)
59 mulclnq 10937 . . . . . . . . . . . . 13 ((๐‘ฅ โˆˆ Q โˆง ๐‘ โˆˆ Q) โ†’ (๐‘ฅ ยทQ ๐‘) โˆˆ Q)
6044, 58, 59syl2anc 583 . . . . . . . . . . . 12 (((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โˆง ๐‘ฅ โˆˆ ๐ด) โ†’ (๐‘ฅ ยทQ ๐‘) โˆˆ Q)
6117ad2antrr 723 . . . . . . . . . . . 12 (((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โˆง ๐‘ฅ โˆˆ ๐ด) โ†’ ๐‘ฆ โˆˆ Q)
62 simplr 766 . . . . . . . . . . . 12 (((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โˆง ๐‘ฅ โˆˆ ๐ด) โ†’ (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘))
63 recclnq 10956 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฆ โˆˆ Q โ†’ (*Qโ€˜๐‘ฆ) โˆˆ Q)
64 mulclnq 10937 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ง โˆˆ Q โˆง (*Qโ€˜๐‘ฆ) โˆˆ Q) โ†’ (๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) โˆˆ Q)
6563, 64sylan2 592 . . . . . . . . . . . . . . . . . . 19 ((๐‘ง โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โ†’ (๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) โˆˆ Q)
6665ancoms 458 . . . . . . . . . . . . . . . . . 18 ((๐‘ฆ โˆˆ Q โˆง ๐‘ง โˆˆ Q) โ†’ (๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) โˆˆ Q)
67 ltmnq 10962 . . . . . . . . . . . . . . . . . 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 10949 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฆ) = (๐‘ง ยทQ ((*Qโ€˜๐‘ฆ) ยทQ ๐‘ฆ))
70 mulcomnq 10943 . . . . . . . . . . . . . . . . . . . . 21 ((*Qโ€˜๐‘ฆ) ยทQ ๐‘ฆ) = (๐‘ฆ ยทQ (*Qโ€˜๐‘ฆ))
7170oveq2i 7412 . . . . . . . . . . . . . . . . . . . 20 (๐‘ง ยทQ ((*Qโ€˜๐‘ฆ) ยทQ ๐‘ฆ)) = (๐‘ง ยทQ (๐‘ฆ ยทQ (*Qโ€˜๐‘ฆ)))
7269, 71eqtri 2752 . . . . . . . . . . . . . . . . . . 19 ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฆ) = (๐‘ง ยทQ (๐‘ฆ ยทQ (*Qโ€˜๐‘ฆ)))
73 recidnq 10955 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฆ โˆˆ Q โ†’ (๐‘ฆ ยทQ (*Qโ€˜๐‘ฆ)) = 1Q)
7473oveq2d 7417 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฆ โˆˆ Q โ†’ (๐‘ง ยทQ (๐‘ฆ ยทQ (*Qโ€˜๐‘ฆ))) = (๐‘ง ยทQ 1Q))
75 mulidnq 10953 . . . . . . . . . . . . . . . . . . . 20 (๐‘ง โˆˆ Q โ†’ (๐‘ง ยทQ 1Q) = ๐‘ง)
7674, 75sylan9eq 2784 . . . . . . . . . . . . . . . . . . 19 ((๐‘ฆ โˆˆ Q โˆง ๐‘ง โˆˆ Q) โ†’ (๐‘ง ยทQ (๐‘ฆ ยทQ (*Qโ€˜๐‘ฆ))) = ๐‘ง)
7772, 76eqtrid 2776 . . . . . . . . . . . . . . . . . 18 ((๐‘ฆ โˆˆ Q โˆง ๐‘ง โˆˆ Q) โ†’ ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฆ) = ๐‘ง)
7877breq1d 5148 . . . . . . . . . . . . . . . . 17 ((๐‘ฆ โˆˆ Q โˆง ๐‘ง โˆˆ Q) โ†’ (((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฆ) <Q ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ) โ†” ๐‘ง <Q ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ)))
7968, 78bitrd 279 . . . . . . . . . . . . . . . 16 ((๐‘ฆ โˆˆ Q โˆง ๐‘ง โˆˆ Q) โ†’ (๐‘ฆ <Q ๐‘ฅ โ†” ๐‘ง <Q ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ)))
8079adantll 711 . . . . . . . . . . . . . . 15 ((((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โˆง ๐‘ง โˆˆ Q) โ†’ (๐‘ฆ <Q ๐‘ฅ โ†” ๐‘ง <Q ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ)))
81 mulnqf 10939 . . . . . . . . . . . . . . . . . . . . . 22 ยทQ :(Q ร— Q)โŸถQ
8281fdmi 6719 . . . . . . . . . . . . . . . . . . . . 21 dom ยทQ = (Q ร— Q)
8382, 48ndmovrcl 7586 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ฅ ยทQ ๐‘) โˆˆ Q โ†’ (๐‘ฅ โˆˆ Q โˆง ๐‘ โˆˆ Q))
8483simpld 494 . . . . . . . . . . . . . . . . . . 19 ((๐‘ฅ ยทQ ๐‘) โˆˆ Q โ†’ ๐‘ฅ โˆˆ Q)
85 ltanq 10961 . . . . . . . . . . . . . . . . . . 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 480 . . . . . . . . . . . . . . . . 17 (((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โ†’ (๐‘ง <Q ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ) โ†” (๐‘ฅ +Q ๐‘ง) <Q (๐‘ฅ +Q ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ))))
88 vex 3470 . . . . . . . . . . . . . . . . . . . 20 ๐‘ฆ โˆˆ V
89 ovex 7434 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ)) โˆˆ V
90 mulcomnq 10943 . . . . . . . . . . . . . . . . . . . 20 (๐‘ข ยทQ ๐‘ค) = (๐‘ค ยทQ ๐‘ข)
91 distrnq 10951 . . . . . . . . . . . . . . . . . . . 20 (๐‘ข ยทQ (๐‘ค +Q ๐‘ฃ)) = ((๐‘ข ยทQ ๐‘ค) +Q (๐‘ข ยทQ ๐‘ฃ))
9288, 34, 89, 90, 91caovdir 7634 . . . . . . . . . . . . . . . . . . 19 ((๐‘ฆ +Q ๐‘ง) ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) = ((๐‘ฆ ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) +Q (๐‘ง ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))))
93 vex 3470 . . . . . . . . . . . . . . . . . . . . . 22 ๐‘ฅ โˆˆ V
94 fvex 6894 . . . . . . . . . . . . . . . . . . . . . 22 (*Qโ€˜๐‘ฆ) โˆˆ V
95 mulassnq 10949 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ข ยทQ ๐‘ค) ยทQ ๐‘ฃ) = (๐‘ข ยทQ (๐‘ค ยทQ ๐‘ฃ))
9688, 93, 94, 90, 95caov12 7628 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฆ ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) = (๐‘ฅ ยทQ (๐‘ฆ ยทQ (*Qโ€˜๐‘ฆ)))
9773oveq2d 7417 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฆ โˆˆ Q โ†’ (๐‘ฅ ยทQ (๐‘ฆ ยทQ (*Qโ€˜๐‘ฆ))) = (๐‘ฅ ยทQ 1Q))
98 mulidnq 10953 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฅ โˆˆ Q โ†’ (๐‘ฅ ยทQ 1Q) = ๐‘ฅ)
9984, 98syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ฅ ยทQ ๐‘) โˆˆ Q โ†’ (๐‘ฅ ยทQ 1Q) = ๐‘ฅ)
10097, 99sylan9eqr 2786 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โ†’ (๐‘ฅ ยทQ (๐‘ฆ ยทQ (*Qโ€˜๐‘ฆ))) = ๐‘ฅ)
10196, 100eqtrid 2776 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โ†’ (๐‘ฆ ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) = ๐‘ฅ)
102 mulcomnq 10943 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ)) = ((*Qโ€˜๐‘ฆ) ยทQ ๐‘ฅ)
103102oveq2i 7412 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ง ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) = (๐‘ง ยทQ ((*Qโ€˜๐‘ฆ) ยทQ ๐‘ฅ))
104 mulassnq 10949 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ) = (๐‘ง ยทQ ((*Qโ€˜๐‘ฆ) ยทQ ๐‘ฅ))
105103, 104eqtr4i 2755 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ง ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) = ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ)
106105a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โ†’ (๐‘ง ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) = ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ))
107101, 106oveq12d 7419 . . . . . . . . . . . . . . . . . . 19 (((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โ†’ ((๐‘ฆ ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) +Q (๐‘ง ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ)))) = (๐‘ฅ +Q ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ)))
10892, 107eqtrid 2776 . . . . . . . . . . . . . . . . . 18 (((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โ†’ ((๐‘ฆ +Q ๐‘ง) ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) = (๐‘ฅ +Q ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ)))
109108breq2d 5150 . . . . . . . . . . . . . . . . 17 (((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โ†’ ((๐‘ฅ +Q ๐‘ง) <Q ((๐‘ฆ +Q ๐‘ง) ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) โ†” (๐‘ฅ +Q ๐‘ง) <Q (๐‘ฅ +Q ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ))))
11087, 109bitr4d 282 . . . . . . . . . . . . . . . 16 (((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โ†’ (๐‘ง <Q ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ) โ†” (๐‘ฅ +Q ๐‘ง) <Q ((๐‘ฆ +Q ๐‘ง) ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ)))))
111110adantr 480 . . . . . . . . . . . . . . 15 ((((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โˆง ๐‘ง โˆˆ Q) โ†’ (๐‘ง <Q ((๐‘ง ยทQ (*Qโ€˜๐‘ฆ)) ยทQ ๐‘ฅ) โ†” (๐‘ฅ +Q ๐‘ง) <Q ((๐‘ฆ +Q ๐‘ง) ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ)))))
11280, 111bitrd 279 . . . . . . . . . . . . . 14 ((((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โˆง ๐‘ง โˆˆ Q) โ†’ (๐‘ฆ <Q ๐‘ฅ โ†” (๐‘ฅ +Q ๐‘ง) <Q ((๐‘ฆ +Q ๐‘ง) ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ)))))
113112adantrr 714 . . . . . . . . . . . . 13 ((((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โˆง (๐‘ง โˆˆ Q โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘))) โ†’ (๐‘ฆ <Q ๐‘ฅ โ†” (๐‘ฅ +Q ๐‘ง) <Q ((๐‘ฆ +Q ๐‘ง) ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ)))))
114 ltanq 10961 . . . . . . . . . . . . . . 15 (๐‘ง โˆˆ Q โ†’ (๐‘ฆ <Q ๐‘ฅ โ†” (๐‘ง +Q ๐‘ฆ) <Q (๐‘ง +Q ๐‘ฅ)))
115 addcomnq 10941 . . . . . . . . . . . . . . . 16 (๐‘ง +Q ๐‘ฆ) = (๐‘ฆ +Q ๐‘ง)
116 addcomnq 10941 . . . . . . . . . . . . . . . 16 (๐‘ง +Q ๐‘ฅ) = (๐‘ฅ +Q ๐‘ง)
117115, 116breq12i 5147 . . . . . . . . . . . . . . 15 ((๐‘ง +Q ๐‘ฆ) <Q (๐‘ง +Q ๐‘ฅ) โ†” (๐‘ฆ +Q ๐‘ง) <Q (๐‘ฅ +Q ๐‘ง))
118114, 117bitrdi 287 . . . . . . . . . . . . . 14 (๐‘ง โˆˆ Q โ†’ (๐‘ฆ <Q ๐‘ฅ โ†” (๐‘ฆ +Q ๐‘ง) <Q (๐‘ฅ +Q ๐‘ง)))
119118ad2antrl 725 . . . . . . . . . . . . 13 ((((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โˆง (๐‘ง โˆˆ Q โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘))) โ†’ (๐‘ฆ <Q ๐‘ฅ โ†” (๐‘ฆ +Q ๐‘ง) <Q (๐‘ฅ +Q ๐‘ง)))
120 oveq1 7408 . . . . . . . . . . . . . . . 16 ((๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘) โ†’ ((๐‘ฆ +Q ๐‘ง) ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) = ((๐‘ฆ ยทQ ๐‘) ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))))
121 vex 3470 . . . . . . . . . . . . . . . . . 18 ๐‘ โˆˆ V
12288, 121, 93, 90, 95, 94caov411 7632 . . . . . . . . . . . . . . . . 17 ((๐‘ฆ ยทQ ๐‘) ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) = ((๐‘ฅ ยทQ ๐‘) ยทQ (๐‘ฆ ยทQ (*Qโ€˜๐‘ฆ)))
12373oveq2d 7417 . . . . . . . . . . . . . . . . . 18 (๐‘ฆ โˆˆ Q โ†’ ((๐‘ฅ ยทQ ๐‘) ยทQ (๐‘ฆ ยทQ (*Qโ€˜๐‘ฆ))) = ((๐‘ฅ ยทQ ๐‘) ยทQ 1Q))
124 mulidnq 10953 . . . . . . . . . . . . . . . . . 18 ((๐‘ฅ ยทQ ๐‘) โˆˆ Q โ†’ ((๐‘ฅ ยทQ ๐‘) ยทQ 1Q) = (๐‘ฅ ยทQ ๐‘))
125123, 124sylan9eqr 2786 . . . . . . . . . . . . . . . . 17 (((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โ†’ ((๐‘ฅ ยทQ ๐‘) ยทQ (๐‘ฆ ยทQ (*Qโ€˜๐‘ฆ))) = (๐‘ฅ ยทQ ๐‘))
126122, 125eqtrid 2776 . . . . . . . . . . . . . . . 16 (((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โ†’ ((๐‘ฆ ยทQ ๐‘) ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) = (๐‘ฅ ยทQ ๐‘))
127120, 126sylan9eqr 2786 . . . . . . . . . . . . . . 15 ((((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โ†’ ((๐‘ฆ +Q ๐‘ง) ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) = (๐‘ฅ ยทQ ๐‘))
128127breq2d 5150 . . . . . . . . . . . . . 14 ((((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โ†’ ((๐‘ฅ +Q ๐‘ง) <Q ((๐‘ฆ +Q ๐‘ง) ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) โ†” (๐‘ฅ +Q ๐‘ง) <Q (๐‘ฅ ยทQ ๐‘)))
129128adantrl 713 . . . . . . . . . . . . 13 ((((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โˆง (๐‘ง โˆˆ Q โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘))) โ†’ ((๐‘ฅ +Q ๐‘ง) <Q ((๐‘ฆ +Q ๐‘ง) ยทQ (๐‘ฅ ยทQ (*Qโ€˜๐‘ฆ))) โ†” (๐‘ฅ +Q ๐‘ง) <Q (๐‘ฅ ยทQ ๐‘)))
130113, 119, 1293bitr3d 309 . . . . . . . . . . . 12 ((((๐‘ฅ ยทQ ๐‘) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q) โˆง (๐‘ง โˆˆ Q โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘))) โ†’ ((๐‘ฆ +Q ๐‘ง) <Q (๐‘ฅ +Q ๐‘ง) โ†” (๐‘ฅ +Q ๐‘ง) <Q (๐‘ฅ ยทQ ๐‘)))
13160, 61, 53, 62, 130syl22anc 836 . . . . . . . . . . 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 10983 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ P โˆง (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด) โ†’ ((๐‘ฅ +Q ๐‘ง) <Q (๐‘ฅ ยทQ ๐‘) โ†’ (๐‘ฅ +Q ๐‘ง) โˆˆ ๐ด))
134133impancom 451 . . . . . . . . . . . . . 14 ((๐ด โˆˆ P โˆง (๐‘ฅ +Q ๐‘ง) <Q (๐‘ฅ ยทQ ๐‘)) โ†’ ((๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด โ†’ (๐‘ฅ +Q ๐‘ง) โˆˆ ๐ด))
135134con3d 152 . . . . . . . . . . . . 13 ((๐ด โˆˆ P โˆง (๐‘ฅ +Q ๐‘ง) <Q (๐‘ฅ ยทQ ๐‘)) โ†’ (ยฌ (๐‘ฅ +Q ๐‘ง) โˆˆ ๐ด โ†’ ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด))
136135ex 412 . . . . . . . . . . . 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 3160 . . . . . . . 8 ((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โ†’ (โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ +Q ๐‘ง) โˆˆ ๐ด โ†’ โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด))
14136, 140mpd 15 . . . . . . 7 ((((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โˆง (๐‘ฆ +Q ๐‘ง) = (๐‘ฆ ยทQ ๐‘)) โ†’ โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด)
14232, 141exlimddv 1930 . . . . . 6 (((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง (๐‘ฆ โˆˆ ๐ด โˆง (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด)) โ†’ โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด)
143142expr 456 . . . . 5 (((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ ((๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด โ†’ โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด))
144 oveq1 7408 . . . . . . . . . 10 (๐‘ฅ = ๐‘ฆ โ†’ (๐‘ฅ ยทQ ๐‘) = (๐‘ฆ ยทQ ๐‘))
145144eleq1d 2810 . . . . . . . . 9 (๐‘ฅ = ๐‘ฆ โ†’ ((๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด โ†” (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด))
146145notbid 318 . . . . . . . 8 (๐‘ฅ = ๐‘ฆ โ†’ (ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด โ†” ยฌ (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด))
147146rspcev 3604 . . . . . . 7 ((๐‘ฆ โˆˆ ๐ด โˆง ยฌ (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด) โ†’ โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด)
148147ex 412 . . . . . 6 (๐‘ฆ โˆˆ ๐ด โ†’ (ยฌ (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด โ†’ โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด))
149148adantl 481 . . . . 5 (((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ (ยฌ (๐‘ฆ ยทQ ๐‘) โˆˆ ๐ด โ†’ โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด))
150143, 149pm2.61d 179 . . . 4 (((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โˆง ๐‘ฆ โˆˆ ๐ด) โ†’ โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด)
15115, 150exlimddv 1930 . . 3 ((๐ด โˆˆ P โˆง 1Q <Q ๐‘) โ†’ โˆƒ๐‘ฅ โˆˆ ๐ด ยฌ (๐‘ฅ ยทQ ๐‘) โˆˆ ๐ด)
15211, 151vtoclg 3535 . 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 395   = wceq 1533  โˆƒwex 1773   โˆˆ wcel 2098   โ‰  wne 2932  โˆƒwrex 3062  โˆ…c0 4314   class class class wbr 5138   ร— cxp 5664  โ€˜cfv 6533  (class class class)co 7401  Qcnq 10842  1Qc1q 10843   +Q cplq 10845   ยทQ cmq 10846  *Qcrq 10847   <Q cltq 10848  Pcnp 10849
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pr 5417  ax-un 7718
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7404  df-oprab 7405  df-mpo 7406  df-om 7849  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-oadd 8465  df-omul 8466  df-er 8698  df-ni 10862  df-pli 10863  df-mi 10864  df-lti 10865  df-plpq 10898  df-mpq 10899  df-ltpq 10900  df-enq 10901  df-nq 10902  df-erq 10903  df-plq 10904  df-mq 10905  df-1nq 10906  df-rq 10907  df-ltnq 10908  df-np 10971
This theorem is referenced by:  reclem3pr  11039
  Copyright terms: Public domain W3C validator