Metamath Proof Explorer


Theorem prlem934

Description: Lemma 9-3.4 of Gleason p. 122. (Contributed by NM, 25-Mar-1996) (Revised by Mario Carneiro, 11-May-2013) (New usage is discouraged.)

Ref Expression
Hypothesis prlem934.1 โŠข ๐ต โˆˆ V
Assertion prlem934 ( ๐ด โˆˆ P โ†’ โˆƒ ๐‘ฅ โˆˆ ๐ด ยฌ ( ๐‘ฅ +Q ๐ต ) โˆˆ ๐ด )

Proof

Step Hyp Ref Expression
1 prlem934.1 โŠข ๐ต โˆˆ V
2 prn0 โŠข ( ๐ด โˆˆ P โ†’ ๐ด โ‰  โˆ… )
3 r19.2z โŠข ( ( ๐ด โ‰  โˆ… โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐ต ) โˆˆ ๐ด ) โ†’ โˆƒ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐ต ) โˆˆ ๐ด )
4 3 ex โŠข ( ๐ด โ‰  โˆ… โ†’ ( โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐ต ) โˆˆ ๐ด โ†’ โˆƒ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐ต ) โˆˆ ๐ด ) )
5 2 4 syl โŠข ( ๐ด โˆˆ P โ†’ ( โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐ต ) โˆˆ ๐ด โ†’ โˆƒ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐ต ) โˆˆ ๐ด ) )
6 prpssnq โŠข ( ๐ด โˆˆ P โ†’ ๐ด โŠŠ Q )
7 6 pssssd โŠข ( ๐ด โˆˆ P โ†’ ๐ด โŠ† Q )
8 7 sseld โŠข ( ๐ด โˆˆ P โ†’ ( ( ๐‘ฅ +Q ๐ต ) โˆˆ ๐ด โ†’ ( ๐‘ฅ +Q ๐ต ) โˆˆ Q ) )
9 addnqf โŠข +Q : ( Q ร— Q ) โŸถ Q
10 9 fdmi โŠข dom +Q = ( Q ร— Q )
11 0nnq โŠข ยฌ โˆ… โˆˆ Q
12 10 11 ndmovrcl โŠข ( ( ๐‘ฅ +Q ๐ต ) โˆˆ Q โ†’ ( ๐‘ฅ โˆˆ Q โˆง ๐ต โˆˆ Q ) )
13 12 simprd โŠข ( ( ๐‘ฅ +Q ๐ต ) โˆˆ Q โ†’ ๐ต โˆˆ Q )
14 8 13 syl6com โŠข ( ( ๐‘ฅ +Q ๐ต ) โˆˆ ๐ด โ†’ ( ๐ด โˆˆ P โ†’ ๐ต โˆˆ Q ) )
15 14 rexlimivw โŠข ( โˆƒ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐ต ) โˆˆ ๐ด โ†’ ( ๐ด โˆˆ P โ†’ ๐ต โˆˆ Q ) )
16 15 com12 โŠข ( ๐ด โˆˆ P โ†’ ( โˆƒ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐ต ) โˆˆ ๐ด โ†’ ๐ต โˆˆ Q ) )
17 oveq2 โŠข ( ๐‘ = ๐ต โ†’ ( ๐‘ฅ +Q ๐‘ ) = ( ๐‘ฅ +Q ๐ต ) )
18 17 eleq1d โŠข ( ๐‘ = ๐ต โ†’ ( ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด โ†” ( ๐‘ฅ +Q ๐ต ) โˆˆ ๐ด ) )
19 18 ralbidv โŠข ( ๐‘ = ๐ต โ†’ ( โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด โ†” โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐ต ) โˆˆ ๐ด ) )
20 19 notbid โŠข ( ๐‘ = ๐ต โ†’ ( ยฌ โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด โ†” ยฌ โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐ต ) โˆˆ ๐ด ) )
21 20 imbi2d โŠข ( ๐‘ = ๐ต โ†’ ( ( ๐ด โˆˆ P โ†’ ยฌ โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด ) โ†” ( ๐ด โˆˆ P โ†’ ยฌ โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐ต ) โˆˆ ๐ด ) ) )
22 dfpss2 โŠข ( ๐ด โŠŠ Q โ†” ( ๐ด โŠ† Q โˆง ยฌ ๐ด = Q ) )
23 6 22 sylib โŠข ( ๐ด โˆˆ P โ†’ ( ๐ด โŠ† Q โˆง ยฌ ๐ด = Q ) )
24 23 simprd โŠข ( ๐ด โˆˆ P โ†’ ยฌ ๐ด = Q )
25 24 adantr โŠข ( ( ๐ด โˆˆ P โˆง ๐‘ โˆˆ Q ) โ†’ ยฌ ๐ด = Q )
26 7 3ad2ant1 โŠข ( ( ๐ด โˆˆ P โˆง ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด ) โ†’ ๐ด โŠ† Q )
27 simpl1 โŠข ( ( ( ๐ด โˆˆ P โˆง ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด ) โˆง ๐‘ค โˆˆ Q ) โ†’ ๐ด โˆˆ P )
28 n0 โŠข ( ๐ด โ‰  โˆ… โ†” โˆƒ ๐‘ฆ ๐‘ฆ โˆˆ ๐ด )
29 2 28 sylib โŠข ( ๐ด โˆˆ P โ†’ โˆƒ ๐‘ฆ ๐‘ฆ โˆˆ ๐ด )
30 27 29 syl โŠข ( ( ( ๐ด โˆˆ P โˆง ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด ) โˆง ๐‘ค โˆˆ Q ) โ†’ โˆƒ ๐‘ฆ ๐‘ฆ โˆˆ ๐ด )
31 simprl โŠข ( ( ( ๐ด โˆˆ P โˆง ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด ) โˆง ( ๐‘ค โˆˆ Q โˆง ๐‘ฆ โˆˆ ๐ด ) ) โ†’ ๐‘ค โˆˆ Q )
32 simpl2 โŠข ( ( ( ๐ด โˆˆ P โˆง ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด ) โˆง ( ๐‘ค โˆˆ Q โˆง ๐‘ฆ โˆˆ ๐ด ) ) โ†’ ๐‘ โˆˆ Q )
33 recclnq โŠข ( ๐‘ โˆˆ Q โ†’ ( *Q โ€˜ ๐‘ ) โˆˆ Q )
34 mulclnq โŠข ( ( ๐‘ค โˆˆ Q โˆง ( *Q โ€˜ ๐‘ ) โˆˆ Q ) โ†’ ( ๐‘ค ยทQ ( *Q โ€˜ ๐‘ ) ) โˆˆ Q )
35 archnq โŠข ( ( ๐‘ค ยทQ ( *Q โ€˜ ๐‘ ) ) โˆˆ Q โ†’ โˆƒ ๐‘ง โˆˆ N ( ๐‘ค ยทQ ( *Q โ€˜ ๐‘ ) ) <Q โŸจ ๐‘ง , 1o โŸฉ )
36 34 35 syl โŠข ( ( ๐‘ค โˆˆ Q โˆง ( *Q โ€˜ ๐‘ ) โˆˆ Q ) โ†’ โˆƒ ๐‘ง โˆˆ N ( ๐‘ค ยทQ ( *Q โ€˜ ๐‘ ) ) <Q โŸจ ๐‘ง , 1o โŸฉ )
37 33 36 sylan2 โŠข ( ( ๐‘ค โˆˆ Q โˆง ๐‘ โˆˆ Q ) โ†’ โˆƒ ๐‘ง โˆˆ N ( ๐‘ค ยทQ ( *Q โ€˜ ๐‘ ) ) <Q โŸจ ๐‘ง , 1o โŸฉ )
38 31 32 37 syl2anc โŠข ( ( ( ๐ด โˆˆ P โˆง ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด ) โˆง ( ๐‘ค โˆˆ Q โˆง ๐‘ฆ โˆˆ ๐ด ) ) โ†’ โˆƒ ๐‘ง โˆˆ N ( ๐‘ค ยทQ ( *Q โ€˜ ๐‘ ) ) <Q โŸจ ๐‘ง , 1o โŸฉ )
39 simpll2 โŠข ( ( ( ( ๐ด โˆˆ P โˆง ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด ) โˆง ( ๐‘ค โˆˆ Q โˆง ๐‘ฆ โˆˆ ๐ด ) ) โˆง ( ๐‘ง โˆˆ N โˆง ( ๐‘ค ยทQ ( *Q โ€˜ ๐‘ ) ) <Q โŸจ ๐‘ง , 1o โŸฉ ) ) โ†’ ๐‘ โˆˆ Q )
40 simplrl โŠข ( ( ( ( ๐ด โˆˆ P โˆง ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด ) โˆง ( ๐‘ค โˆˆ Q โˆง ๐‘ฆ โˆˆ ๐ด ) ) โˆง ( ๐‘ง โˆˆ N โˆง ( ๐‘ค ยทQ ( *Q โ€˜ ๐‘ ) ) <Q โŸจ ๐‘ง , 1o โŸฉ ) ) โ†’ ๐‘ค โˆˆ Q )
41 simprr โŠข ( ( ( ( ๐ด โˆˆ P โˆง ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด ) โˆง ( ๐‘ค โˆˆ Q โˆง ๐‘ฆ โˆˆ ๐ด ) ) โˆง ( ๐‘ง โˆˆ N โˆง ( ๐‘ค ยทQ ( *Q โ€˜ ๐‘ ) ) <Q โŸจ ๐‘ง , 1o โŸฉ ) ) โ†’ ( ๐‘ค ยทQ ( *Q โ€˜ ๐‘ ) ) <Q โŸจ ๐‘ง , 1o โŸฉ )
42 ltmnq โŠข ( ๐‘ โˆˆ Q โ†’ ( ( ๐‘ค ยทQ ( *Q โ€˜ ๐‘ ) ) <Q โŸจ ๐‘ง , 1o โŸฉ โ†” ( ๐‘ ยทQ ( ๐‘ค ยทQ ( *Q โ€˜ ๐‘ ) ) ) <Q ( ๐‘ ยทQ โŸจ ๐‘ง , 1o โŸฉ ) ) )
43 vex โŠข ๐‘ โˆˆ V
44 vex โŠข ๐‘ค โˆˆ V
45 fvex โŠข ( *Q โ€˜ ๐‘ ) โˆˆ V
46 mulcomnq โŠข ( ๐‘ฃ ยทQ ๐‘ฅ ) = ( ๐‘ฅ ยทQ ๐‘ฃ )
47 mulassnq โŠข ( ( ๐‘ฃ ยทQ ๐‘ฅ ) ยทQ ๐‘ฆ ) = ( ๐‘ฃ ยทQ ( ๐‘ฅ ยทQ ๐‘ฆ ) )
48 43 44 45 46 47 caov12 โŠข ( ๐‘ ยทQ ( ๐‘ค ยทQ ( *Q โ€˜ ๐‘ ) ) ) = ( ๐‘ค ยทQ ( ๐‘ ยทQ ( *Q โ€˜ ๐‘ ) ) )
49 mulcomnq โŠข ( ๐‘ ยทQ โŸจ ๐‘ง , 1o โŸฉ ) = ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ )
50 48 49 breq12i โŠข ( ( ๐‘ ยทQ ( ๐‘ค ยทQ ( *Q โ€˜ ๐‘ ) ) ) <Q ( ๐‘ ยทQ โŸจ ๐‘ง , 1o โŸฉ ) โ†” ( ๐‘ค ยทQ ( ๐‘ ยทQ ( *Q โ€˜ ๐‘ ) ) ) <Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) )
51 42 50 bitrdi โŠข ( ๐‘ โˆˆ Q โ†’ ( ( ๐‘ค ยทQ ( *Q โ€˜ ๐‘ ) ) <Q โŸจ ๐‘ง , 1o โŸฉ โ†” ( ๐‘ค ยทQ ( ๐‘ ยทQ ( *Q โ€˜ ๐‘ ) ) ) <Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) )
52 51 adantr โŠข ( ( ๐‘ โˆˆ Q โˆง ๐‘ค โˆˆ Q ) โ†’ ( ( ๐‘ค ยทQ ( *Q โ€˜ ๐‘ ) ) <Q โŸจ ๐‘ง , 1o โŸฉ โ†” ( ๐‘ค ยทQ ( ๐‘ ยทQ ( *Q โ€˜ ๐‘ ) ) ) <Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) )
53 recidnq โŠข ( ๐‘ โˆˆ Q โ†’ ( ๐‘ ยทQ ( *Q โ€˜ ๐‘ ) ) = 1Q )
54 53 oveq2d โŠข ( ๐‘ โˆˆ Q โ†’ ( ๐‘ค ยทQ ( ๐‘ ยทQ ( *Q โ€˜ ๐‘ ) ) ) = ( ๐‘ค ยทQ 1Q ) )
55 mulidnq โŠข ( ๐‘ค โˆˆ Q โ†’ ( ๐‘ค ยทQ 1Q ) = ๐‘ค )
56 54 55 sylan9eq โŠข ( ( ๐‘ โˆˆ Q โˆง ๐‘ค โˆˆ Q ) โ†’ ( ๐‘ค ยทQ ( ๐‘ ยทQ ( *Q โ€˜ ๐‘ ) ) ) = ๐‘ค )
57 56 breq1d โŠข ( ( ๐‘ โˆˆ Q โˆง ๐‘ค โˆˆ Q ) โ†’ ( ( ๐‘ค ยทQ ( ๐‘ ยทQ ( *Q โ€˜ ๐‘ ) ) ) <Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) โ†” ๐‘ค <Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) )
58 52 57 bitrd โŠข ( ( ๐‘ โˆˆ Q โˆง ๐‘ค โˆˆ Q ) โ†’ ( ( ๐‘ค ยทQ ( *Q โ€˜ ๐‘ ) ) <Q โŸจ ๐‘ง , 1o โŸฉ โ†” ๐‘ค <Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) )
59 58 biimpa โŠข ( ( ( ๐‘ โˆˆ Q โˆง ๐‘ค โˆˆ Q ) โˆง ( ๐‘ค ยทQ ( *Q โ€˜ ๐‘ ) ) <Q โŸจ ๐‘ง , 1o โŸฉ ) โ†’ ๐‘ค <Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) )
60 39 40 41 59 syl21anc โŠข ( ( ( ( ๐ด โˆˆ P โˆง ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด ) โˆง ( ๐‘ค โˆˆ Q โˆง ๐‘ฆ โˆˆ ๐ด ) ) โˆง ( ๐‘ง โˆˆ N โˆง ( ๐‘ค ยทQ ( *Q โ€˜ ๐‘ ) ) <Q โŸจ ๐‘ง , 1o โŸฉ ) ) โ†’ ๐‘ค <Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) )
61 simprl โŠข ( ( ( ( ๐ด โˆˆ P โˆง ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด ) โˆง ( ๐‘ค โˆˆ Q โˆง ๐‘ฆ โˆˆ ๐ด ) ) โˆง ( ๐‘ง โˆˆ N โˆง ( ๐‘ค ยทQ ( *Q โ€˜ ๐‘ ) ) <Q โŸจ ๐‘ง , 1o โŸฉ ) ) โ†’ ๐‘ง โˆˆ N )
62 pinq โŠข ( ๐‘ง โˆˆ N โ†’ โŸจ ๐‘ง , 1o โŸฉ โˆˆ Q )
63 mulclnq โŠข ( ( โŸจ ๐‘ง , 1o โŸฉ โˆˆ Q โˆง ๐‘ โˆˆ Q ) โ†’ ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) โˆˆ Q )
64 62 63 sylan โŠข ( ( ๐‘ง โˆˆ N โˆง ๐‘ โˆˆ Q ) โ†’ ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) โˆˆ Q )
65 61 39 64 syl2anc โŠข ( ( ( ( ๐ด โˆˆ P โˆง ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด ) โˆง ( ๐‘ค โˆˆ Q โˆง ๐‘ฆ โˆˆ ๐ด ) ) โˆง ( ๐‘ง โˆˆ N โˆง ( ๐‘ค ยทQ ( *Q โ€˜ ๐‘ ) ) <Q โŸจ ๐‘ง , 1o โŸฉ ) ) โ†’ ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) โˆˆ Q )
66 simpll1 โŠข ( ( ( ( ๐ด โˆˆ P โˆง ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด ) โˆง ( ๐‘ค โˆˆ Q โˆง ๐‘ฆ โˆˆ ๐ด ) ) โˆง ( ๐‘ง โˆˆ N โˆง ( ๐‘ค ยทQ ( *Q โ€˜ ๐‘ ) ) <Q โŸจ ๐‘ง , 1o โŸฉ ) ) โ†’ ๐ด โˆˆ P )
67 simplrr โŠข ( ( ( ( ๐ด โˆˆ P โˆง ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด ) โˆง ( ๐‘ค โˆˆ Q โˆง ๐‘ฆ โˆˆ ๐ด ) ) โˆง ( ๐‘ง โˆˆ N โˆง ( ๐‘ค ยทQ ( *Q โ€˜ ๐‘ ) ) <Q โŸจ ๐‘ง , 1o โŸฉ ) ) โ†’ ๐‘ฆ โˆˆ ๐ด )
68 elprnq โŠข ( ( ๐ด โˆˆ P โˆง ๐‘ฆ โˆˆ ๐ด ) โ†’ ๐‘ฆ โˆˆ Q )
69 66 67 68 syl2anc โŠข ( ( ( ( ๐ด โˆˆ P โˆง ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด ) โˆง ( ๐‘ค โˆˆ Q โˆง ๐‘ฆ โˆˆ ๐ด ) ) โˆง ( ๐‘ง โˆˆ N โˆง ( ๐‘ค ยทQ ( *Q โ€˜ ๐‘ ) ) <Q โŸจ ๐‘ง , 1o โŸฉ ) ) โ†’ ๐‘ฆ โˆˆ Q )
70 ltaddnq โŠข ( ( ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q ) โ†’ ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) <Q ( ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) +Q ๐‘ฆ ) )
71 addcomnq โŠข ( ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) +Q ๐‘ฆ ) = ( ๐‘ฆ +Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) )
72 70 71 breqtrdi โŠข ( ( ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) โˆˆ Q โˆง ๐‘ฆ โˆˆ Q ) โ†’ ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) <Q ( ๐‘ฆ +Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) )
73 65 69 72 syl2anc โŠข ( ( ( ( ๐ด โˆˆ P โˆง ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด ) โˆง ( ๐‘ค โˆˆ Q โˆง ๐‘ฆ โˆˆ ๐ด ) ) โˆง ( ๐‘ง โˆˆ N โˆง ( ๐‘ค ยทQ ( *Q โ€˜ ๐‘ ) ) <Q โŸจ ๐‘ง , 1o โŸฉ ) ) โ†’ ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) <Q ( ๐‘ฆ +Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) )
74 ltsonq โŠข <Q Or Q
75 ltrelnq โŠข <Q โŠ† ( Q ร— Q )
76 74 75 sotri โŠข ( ( ๐‘ค <Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) โˆง ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) <Q ( ๐‘ฆ +Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) ) โ†’ ๐‘ค <Q ( ๐‘ฆ +Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) )
77 60 73 76 syl2anc โŠข ( ( ( ( ๐ด โˆˆ P โˆง ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด ) โˆง ( ๐‘ค โˆˆ Q โˆง ๐‘ฆ โˆˆ ๐ด ) ) โˆง ( ๐‘ง โˆˆ N โˆง ( ๐‘ค ยทQ ( *Q โ€˜ ๐‘ ) ) <Q โŸจ ๐‘ง , 1o โŸฉ ) ) โ†’ ๐‘ค <Q ( ๐‘ฆ +Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) )
78 simpll3 โŠข ( ( ( ( ๐ด โˆˆ P โˆง ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด ) โˆง ( ๐‘ค โˆˆ Q โˆง ๐‘ฆ โˆˆ ๐ด ) ) โˆง ( ๐‘ง โˆˆ N โˆง ( ๐‘ค ยทQ ( *Q โ€˜ ๐‘ ) ) <Q โŸจ ๐‘ง , 1o โŸฉ ) ) โ†’ โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด )
79 opeq1 โŠข ( ๐‘ค = 1o โ†’ โŸจ ๐‘ค , 1o โŸฉ = โŸจ 1o , 1o โŸฉ )
80 df-1nq โŠข 1Q = โŸจ 1o , 1o โŸฉ
81 79 80 eqtr4di โŠข ( ๐‘ค = 1o โ†’ โŸจ ๐‘ค , 1o โŸฉ = 1Q )
82 81 oveq1d โŠข ( ๐‘ค = 1o โ†’ ( โŸจ ๐‘ค , 1o โŸฉ ยทQ ๐‘ ) = ( 1Q ยทQ ๐‘ ) )
83 82 oveq2d โŠข ( ๐‘ค = 1o โ†’ ( ๐‘ฆ +Q ( โŸจ ๐‘ค , 1o โŸฉ ยทQ ๐‘ ) ) = ( ๐‘ฆ +Q ( 1Q ยทQ ๐‘ ) ) )
84 83 eleq1d โŠข ( ๐‘ค = 1o โ†’ ( ( ๐‘ฆ +Q ( โŸจ ๐‘ค , 1o โŸฉ ยทQ ๐‘ ) ) โˆˆ ๐ด โ†” ( ๐‘ฆ +Q ( 1Q ยทQ ๐‘ ) ) โˆˆ ๐ด ) )
85 84 imbi2d โŠข ( ๐‘ค = 1o โ†’ ( ( ( ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด โˆง ๐‘ฆ โˆˆ ๐ด ) โ†’ ( ๐‘ฆ +Q ( โŸจ ๐‘ค , 1o โŸฉ ยทQ ๐‘ ) ) โˆˆ ๐ด ) โ†” ( ( ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด โˆง ๐‘ฆ โˆˆ ๐ด ) โ†’ ( ๐‘ฆ +Q ( 1Q ยทQ ๐‘ ) ) โˆˆ ๐ด ) ) )
86 opeq1 โŠข ( ๐‘ค = ๐‘ง โ†’ โŸจ ๐‘ค , 1o โŸฉ = โŸจ ๐‘ง , 1o โŸฉ )
87 86 oveq1d โŠข ( ๐‘ค = ๐‘ง โ†’ ( โŸจ ๐‘ค , 1o โŸฉ ยทQ ๐‘ ) = ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) )
88 87 oveq2d โŠข ( ๐‘ค = ๐‘ง โ†’ ( ๐‘ฆ +Q ( โŸจ ๐‘ค , 1o โŸฉ ยทQ ๐‘ ) ) = ( ๐‘ฆ +Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) )
89 88 eleq1d โŠข ( ๐‘ค = ๐‘ง โ†’ ( ( ๐‘ฆ +Q ( โŸจ ๐‘ค , 1o โŸฉ ยทQ ๐‘ ) ) โˆˆ ๐ด โ†” ( ๐‘ฆ +Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) โˆˆ ๐ด ) )
90 89 imbi2d โŠข ( ๐‘ค = ๐‘ง โ†’ ( ( ( ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด โˆง ๐‘ฆ โˆˆ ๐ด ) โ†’ ( ๐‘ฆ +Q ( โŸจ ๐‘ค , 1o โŸฉ ยทQ ๐‘ ) ) โˆˆ ๐ด ) โ†” ( ( ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด โˆง ๐‘ฆ โˆˆ ๐ด ) โ†’ ( ๐‘ฆ +Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) โˆˆ ๐ด ) ) )
91 opeq1 โŠข ( ๐‘ค = ( ๐‘ง +N 1o ) โ†’ โŸจ ๐‘ค , 1o โŸฉ = โŸจ ( ๐‘ง +N 1o ) , 1o โŸฉ )
92 91 oveq1d โŠข ( ๐‘ค = ( ๐‘ง +N 1o ) โ†’ ( โŸจ ๐‘ค , 1o โŸฉ ยทQ ๐‘ ) = ( โŸจ ( ๐‘ง +N 1o ) , 1o โŸฉ ยทQ ๐‘ ) )
93 92 oveq2d โŠข ( ๐‘ค = ( ๐‘ง +N 1o ) โ†’ ( ๐‘ฆ +Q ( โŸจ ๐‘ค , 1o โŸฉ ยทQ ๐‘ ) ) = ( ๐‘ฆ +Q ( โŸจ ( ๐‘ง +N 1o ) , 1o โŸฉ ยทQ ๐‘ ) ) )
94 93 eleq1d โŠข ( ๐‘ค = ( ๐‘ง +N 1o ) โ†’ ( ( ๐‘ฆ +Q ( โŸจ ๐‘ค , 1o โŸฉ ยทQ ๐‘ ) ) โˆˆ ๐ด โ†” ( ๐‘ฆ +Q ( โŸจ ( ๐‘ง +N 1o ) , 1o โŸฉ ยทQ ๐‘ ) ) โˆˆ ๐ด ) )
95 94 imbi2d โŠข ( ๐‘ค = ( ๐‘ง +N 1o ) โ†’ ( ( ( ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด โˆง ๐‘ฆ โˆˆ ๐ด ) โ†’ ( ๐‘ฆ +Q ( โŸจ ๐‘ค , 1o โŸฉ ยทQ ๐‘ ) ) โˆˆ ๐ด ) โ†” ( ( ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด โˆง ๐‘ฆ โˆˆ ๐ด ) โ†’ ( ๐‘ฆ +Q ( โŸจ ( ๐‘ง +N 1o ) , 1o โŸฉ ยทQ ๐‘ ) ) โˆˆ ๐ด ) ) )
96 mulcomnq โŠข ( 1Q ยทQ ๐‘ ) = ( ๐‘ ยทQ 1Q )
97 mulidnq โŠข ( ๐‘ โˆˆ Q โ†’ ( ๐‘ ยทQ 1Q ) = ๐‘ )
98 96 97 eqtrid โŠข ( ๐‘ โˆˆ Q โ†’ ( 1Q ยทQ ๐‘ ) = ๐‘ )
99 oveq1 โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ๐‘ฅ +Q ๐‘ ) = ( ๐‘ฆ +Q ๐‘ ) )
100 99 eleq1d โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด โ†” ( ๐‘ฆ +Q ๐‘ ) โˆˆ ๐ด ) )
101 100 rspccva โŠข ( ( โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด โˆง ๐‘ฆ โˆˆ ๐ด ) โ†’ ( ๐‘ฆ +Q ๐‘ ) โˆˆ ๐ด )
102 oveq2 โŠข ( ( 1Q ยทQ ๐‘ ) = ๐‘ โ†’ ( ๐‘ฆ +Q ( 1Q ยทQ ๐‘ ) ) = ( ๐‘ฆ +Q ๐‘ ) )
103 102 eleq1d โŠข ( ( 1Q ยทQ ๐‘ ) = ๐‘ โ†’ ( ( ๐‘ฆ +Q ( 1Q ยทQ ๐‘ ) ) โˆˆ ๐ด โ†” ( ๐‘ฆ +Q ๐‘ ) โˆˆ ๐ด ) )
104 103 biimpar โŠข ( ( ( 1Q ยทQ ๐‘ ) = ๐‘ โˆง ( ๐‘ฆ +Q ๐‘ ) โˆˆ ๐ด ) โ†’ ( ๐‘ฆ +Q ( 1Q ยทQ ๐‘ ) ) โˆˆ ๐ด )
105 98 101 104 syl2an โŠข ( ( ๐‘ โˆˆ Q โˆง ( โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด โˆง ๐‘ฆ โˆˆ ๐ด ) ) โ†’ ( ๐‘ฆ +Q ( 1Q ยทQ ๐‘ ) ) โˆˆ ๐ด )
106 105 3impb โŠข ( ( ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด โˆง ๐‘ฆ โˆˆ ๐ด ) โ†’ ( ๐‘ฆ +Q ( 1Q ยทQ ๐‘ ) ) โˆˆ ๐ด )
107 3simpa โŠข ( ( ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด โˆง ๐‘ฆ โˆˆ ๐ด ) โ†’ ( ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด ) )
108 oveq1 โŠข ( ๐‘ฅ = ( ๐‘ฆ +Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) โ†’ ( ๐‘ฅ +Q ๐‘ ) = ( ( ๐‘ฆ +Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) +Q ๐‘ ) )
109 108 eleq1d โŠข ( ๐‘ฅ = ( ๐‘ฆ +Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) โ†’ ( ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด โ†” ( ( ๐‘ฆ +Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) +Q ๐‘ ) โˆˆ ๐ด ) )
110 109 rspccva โŠข ( ( โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด โˆง ( ๐‘ฆ +Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) โˆˆ ๐ด ) โ†’ ( ( ๐‘ฆ +Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) +Q ๐‘ ) โˆˆ ๐ด )
111 addassnq โŠข ( ( ๐‘ฆ +Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) +Q ๐‘ ) = ( ๐‘ฆ +Q ( ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) +Q ๐‘ ) )
112 opex โŠข โŸจ ๐‘ง , 1o โŸฉ โˆˆ V
113 1nq โŠข 1Q โˆˆ Q
114 113 elexi โŠข 1Q โˆˆ V
115 distrnq โŠข ( ๐‘ฃ ยทQ ( ๐‘ฅ +Q ๐‘ฆ ) ) = ( ( ๐‘ฃ ยทQ ๐‘ฅ ) +Q ( ๐‘ฃ ยทQ ๐‘ฆ ) )
116 112 114 43 46 115 caovdir โŠข ( ( โŸจ ๐‘ง , 1o โŸฉ +Q 1Q ) ยทQ ๐‘ ) = ( ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) +Q ( 1Q ยทQ ๐‘ ) )
117 116 a1i โŠข ( ( ๐‘ง โˆˆ N โˆง ๐‘ โˆˆ Q ) โ†’ ( ( โŸจ ๐‘ง , 1o โŸฉ +Q 1Q ) ยทQ ๐‘ ) = ( ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) +Q ( 1Q ยทQ ๐‘ ) ) )
118 addpqnq โŠข ( ( โŸจ ๐‘ง , 1o โŸฉ โˆˆ Q โˆง 1Q โˆˆ Q ) โ†’ ( โŸจ ๐‘ง , 1o โŸฉ +Q 1Q ) = ( [Q] โ€˜ ( โŸจ ๐‘ง , 1o โŸฉ +pQ 1Q ) ) )
119 62 113 118 sylancl โŠข ( ๐‘ง โˆˆ N โ†’ ( โŸจ ๐‘ง , 1o โŸฉ +Q 1Q ) = ( [Q] โ€˜ ( โŸจ ๐‘ง , 1o โŸฉ +pQ 1Q ) ) )
120 80 oveq2i โŠข ( โŸจ ๐‘ง , 1o โŸฉ +pQ 1Q ) = ( โŸจ ๐‘ง , 1o โŸฉ +pQ โŸจ 1o , 1o โŸฉ )
121 1pi โŠข 1o โˆˆ N
122 addpipq โŠข ( ( ( ๐‘ง โˆˆ N โˆง 1o โˆˆ N ) โˆง ( 1o โˆˆ N โˆง 1o โˆˆ N ) ) โ†’ ( โŸจ ๐‘ง , 1o โŸฉ +pQ โŸจ 1o , 1o โŸฉ ) = โŸจ ( ( ๐‘ง ยทN 1o ) +N ( 1o ยทN 1o ) ) , ( 1o ยทN 1o ) โŸฉ )
123 121 121 122 mpanr12 โŠข ( ( ๐‘ง โˆˆ N โˆง 1o โˆˆ N ) โ†’ ( โŸจ ๐‘ง , 1o โŸฉ +pQ โŸจ 1o , 1o โŸฉ ) = โŸจ ( ( ๐‘ง ยทN 1o ) +N ( 1o ยทN 1o ) ) , ( 1o ยทN 1o ) โŸฉ )
124 121 123 mpan2 โŠข ( ๐‘ง โˆˆ N โ†’ ( โŸจ ๐‘ง , 1o โŸฉ +pQ โŸจ 1o , 1o โŸฉ ) = โŸจ ( ( ๐‘ง ยทN 1o ) +N ( 1o ยทN 1o ) ) , ( 1o ยทN 1o ) โŸฉ )
125 120 124 eqtrid โŠข ( ๐‘ง โˆˆ N โ†’ ( โŸจ ๐‘ง , 1o โŸฉ +pQ 1Q ) = โŸจ ( ( ๐‘ง ยทN 1o ) +N ( 1o ยทN 1o ) ) , ( 1o ยทN 1o ) โŸฉ )
126 mulidpi โŠข ( ๐‘ง โˆˆ N โ†’ ( ๐‘ง ยทN 1o ) = ๐‘ง )
127 mulidpi โŠข ( 1o โˆˆ N โ†’ ( 1o ยทN 1o ) = 1o )
128 121 127 mp1i โŠข ( ๐‘ง โˆˆ N โ†’ ( 1o ยทN 1o ) = 1o )
129 126 128 oveq12d โŠข ( ๐‘ง โˆˆ N โ†’ ( ( ๐‘ง ยทN 1o ) +N ( 1o ยทN 1o ) ) = ( ๐‘ง +N 1o ) )
130 129 128 opeq12d โŠข ( ๐‘ง โˆˆ N โ†’ โŸจ ( ( ๐‘ง ยทN 1o ) +N ( 1o ยทN 1o ) ) , ( 1o ยทN 1o ) โŸฉ = โŸจ ( ๐‘ง +N 1o ) , 1o โŸฉ )
131 125 130 eqtrd โŠข ( ๐‘ง โˆˆ N โ†’ ( โŸจ ๐‘ง , 1o โŸฉ +pQ 1Q ) = โŸจ ( ๐‘ง +N 1o ) , 1o โŸฉ )
132 131 fveq2d โŠข ( ๐‘ง โˆˆ N โ†’ ( [Q] โ€˜ ( โŸจ ๐‘ง , 1o โŸฉ +pQ 1Q ) ) = ( [Q] โ€˜ โŸจ ( ๐‘ง +N 1o ) , 1o โŸฉ ) )
133 addclpi โŠข ( ( ๐‘ง โˆˆ N โˆง 1o โˆˆ N ) โ†’ ( ๐‘ง +N 1o ) โˆˆ N )
134 121 133 mpan2 โŠข ( ๐‘ง โˆˆ N โ†’ ( ๐‘ง +N 1o ) โˆˆ N )
135 pinq โŠข ( ( ๐‘ง +N 1o ) โˆˆ N โ†’ โŸจ ( ๐‘ง +N 1o ) , 1o โŸฉ โˆˆ Q )
136 nqerid โŠข ( โŸจ ( ๐‘ง +N 1o ) , 1o โŸฉ โˆˆ Q โ†’ ( [Q] โ€˜ โŸจ ( ๐‘ง +N 1o ) , 1o โŸฉ ) = โŸจ ( ๐‘ง +N 1o ) , 1o โŸฉ )
137 134 135 136 3syl โŠข ( ๐‘ง โˆˆ N โ†’ ( [Q] โ€˜ โŸจ ( ๐‘ง +N 1o ) , 1o โŸฉ ) = โŸจ ( ๐‘ง +N 1o ) , 1o โŸฉ )
138 119 132 137 3eqtrd โŠข ( ๐‘ง โˆˆ N โ†’ ( โŸจ ๐‘ง , 1o โŸฉ +Q 1Q ) = โŸจ ( ๐‘ง +N 1o ) , 1o โŸฉ )
139 138 adantr โŠข ( ( ๐‘ง โˆˆ N โˆง ๐‘ โˆˆ Q ) โ†’ ( โŸจ ๐‘ง , 1o โŸฉ +Q 1Q ) = โŸจ ( ๐‘ง +N 1o ) , 1o โŸฉ )
140 139 oveq1d โŠข ( ( ๐‘ง โˆˆ N โˆง ๐‘ โˆˆ Q ) โ†’ ( ( โŸจ ๐‘ง , 1o โŸฉ +Q 1Q ) ยทQ ๐‘ ) = ( โŸจ ( ๐‘ง +N 1o ) , 1o โŸฉ ยทQ ๐‘ ) )
141 98 adantl โŠข ( ( ๐‘ง โˆˆ N โˆง ๐‘ โˆˆ Q ) โ†’ ( 1Q ยทQ ๐‘ ) = ๐‘ )
142 141 oveq2d โŠข ( ( ๐‘ง โˆˆ N โˆง ๐‘ โˆˆ Q ) โ†’ ( ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) +Q ( 1Q ยทQ ๐‘ ) ) = ( ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) +Q ๐‘ ) )
143 117 140 142 3eqtr3rd โŠข ( ( ๐‘ง โˆˆ N โˆง ๐‘ โˆˆ Q ) โ†’ ( ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) +Q ๐‘ ) = ( โŸจ ( ๐‘ง +N 1o ) , 1o โŸฉ ยทQ ๐‘ ) )
144 143 oveq2d โŠข ( ( ๐‘ง โˆˆ N โˆง ๐‘ โˆˆ Q ) โ†’ ( ๐‘ฆ +Q ( ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) +Q ๐‘ ) ) = ( ๐‘ฆ +Q ( โŸจ ( ๐‘ง +N 1o ) , 1o โŸฉ ยทQ ๐‘ ) ) )
145 111 144 eqtrid โŠข ( ( ๐‘ง โˆˆ N โˆง ๐‘ โˆˆ Q ) โ†’ ( ( ๐‘ฆ +Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) +Q ๐‘ ) = ( ๐‘ฆ +Q ( โŸจ ( ๐‘ง +N 1o ) , 1o โŸฉ ยทQ ๐‘ ) ) )
146 145 eleq1d โŠข ( ( ๐‘ง โˆˆ N โˆง ๐‘ โˆˆ Q ) โ†’ ( ( ( ๐‘ฆ +Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) +Q ๐‘ ) โˆˆ ๐ด โ†” ( ๐‘ฆ +Q ( โŸจ ( ๐‘ง +N 1o ) , 1o โŸฉ ยทQ ๐‘ ) ) โˆˆ ๐ด ) )
147 110 146 syl5ib โŠข ( ( ๐‘ง โˆˆ N โˆง ๐‘ โˆˆ Q ) โ†’ ( ( โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด โˆง ( ๐‘ฆ +Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) โˆˆ ๐ด ) โ†’ ( ๐‘ฆ +Q ( โŸจ ( ๐‘ง +N 1o ) , 1o โŸฉ ยทQ ๐‘ ) ) โˆˆ ๐ด ) )
148 147 expd โŠข ( ( ๐‘ง โˆˆ N โˆง ๐‘ โˆˆ Q ) โ†’ ( โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด โ†’ ( ( ๐‘ฆ +Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) โˆˆ ๐ด โ†’ ( ๐‘ฆ +Q ( โŸจ ( ๐‘ง +N 1o ) , 1o โŸฉ ยทQ ๐‘ ) ) โˆˆ ๐ด ) ) )
149 148 expimpd โŠข ( ๐‘ง โˆˆ N โ†’ ( ( ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด ) โ†’ ( ( ๐‘ฆ +Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) โˆˆ ๐ด โ†’ ( ๐‘ฆ +Q ( โŸจ ( ๐‘ง +N 1o ) , 1o โŸฉ ยทQ ๐‘ ) ) โˆˆ ๐ด ) ) )
150 107 149 syl5 โŠข ( ๐‘ง โˆˆ N โ†’ ( ( ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด โˆง ๐‘ฆ โˆˆ ๐ด ) โ†’ ( ( ๐‘ฆ +Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) โˆˆ ๐ด โ†’ ( ๐‘ฆ +Q ( โŸจ ( ๐‘ง +N 1o ) , 1o โŸฉ ยทQ ๐‘ ) ) โˆˆ ๐ด ) ) )
151 150 a2d โŠข ( ๐‘ง โˆˆ N โ†’ ( ( ( ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด โˆง ๐‘ฆ โˆˆ ๐ด ) โ†’ ( ๐‘ฆ +Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) โˆˆ ๐ด ) โ†’ ( ( ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด โˆง ๐‘ฆ โˆˆ ๐ด ) โ†’ ( ๐‘ฆ +Q ( โŸจ ( ๐‘ง +N 1o ) , 1o โŸฉ ยทQ ๐‘ ) ) โˆˆ ๐ด ) ) )
152 85 90 95 90 106 151 indpi โŠข ( ๐‘ง โˆˆ N โ†’ ( ( ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด โˆง ๐‘ฆ โˆˆ ๐ด ) โ†’ ( ๐‘ฆ +Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) โˆˆ ๐ด ) )
153 152 imp โŠข ( ( ๐‘ง โˆˆ N โˆง ( ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด โˆง ๐‘ฆ โˆˆ ๐ด ) ) โ†’ ( ๐‘ฆ +Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) โˆˆ ๐ด )
154 61 39 78 67 153 syl13anc โŠข ( ( ( ( ๐ด โˆˆ P โˆง ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด ) โˆง ( ๐‘ค โˆˆ Q โˆง ๐‘ฆ โˆˆ ๐ด ) ) โˆง ( ๐‘ง โˆˆ N โˆง ( ๐‘ค ยทQ ( *Q โ€˜ ๐‘ ) ) <Q โŸจ ๐‘ง , 1o โŸฉ ) ) โ†’ ( ๐‘ฆ +Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) โˆˆ ๐ด )
155 prcdnq โŠข ( ( ๐ด โˆˆ P โˆง ( ๐‘ฆ +Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) โˆˆ ๐ด ) โ†’ ( ๐‘ค <Q ( ๐‘ฆ +Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) โ†’ ๐‘ค โˆˆ ๐ด ) )
156 66 154 155 syl2anc โŠข ( ( ( ( ๐ด โˆˆ P โˆง ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด ) โˆง ( ๐‘ค โˆˆ Q โˆง ๐‘ฆ โˆˆ ๐ด ) ) โˆง ( ๐‘ง โˆˆ N โˆง ( ๐‘ค ยทQ ( *Q โ€˜ ๐‘ ) ) <Q โŸจ ๐‘ง , 1o โŸฉ ) ) โ†’ ( ๐‘ค <Q ( ๐‘ฆ +Q ( โŸจ ๐‘ง , 1o โŸฉ ยทQ ๐‘ ) ) โ†’ ๐‘ค โˆˆ ๐ด ) )
157 77 156 mpd โŠข ( ( ( ( ๐ด โˆˆ P โˆง ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด ) โˆง ( ๐‘ค โˆˆ Q โˆง ๐‘ฆ โˆˆ ๐ด ) ) โˆง ( ๐‘ง โˆˆ N โˆง ( ๐‘ค ยทQ ( *Q โ€˜ ๐‘ ) ) <Q โŸจ ๐‘ง , 1o โŸฉ ) ) โ†’ ๐‘ค โˆˆ ๐ด )
158 38 157 rexlimddv โŠข ( ( ( ๐ด โˆˆ P โˆง ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด ) โˆง ( ๐‘ค โˆˆ Q โˆง ๐‘ฆ โˆˆ ๐ด ) ) โ†’ ๐‘ค โˆˆ ๐ด )
159 158 expr โŠข ( ( ( ๐ด โˆˆ P โˆง ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด ) โˆง ๐‘ค โˆˆ Q ) โ†’ ( ๐‘ฆ โˆˆ ๐ด โ†’ ๐‘ค โˆˆ ๐ด ) )
160 159 exlimdv โŠข ( ( ( ๐ด โˆˆ P โˆง ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด ) โˆง ๐‘ค โˆˆ Q ) โ†’ ( โˆƒ ๐‘ฆ ๐‘ฆ โˆˆ ๐ด โ†’ ๐‘ค โˆˆ ๐ด ) )
161 30 160 mpd โŠข ( ( ( ๐ด โˆˆ P โˆง ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด ) โˆง ๐‘ค โˆˆ Q ) โ†’ ๐‘ค โˆˆ ๐ด )
162 26 161 eqelssd โŠข ( ( ๐ด โˆˆ P โˆง ๐‘ โˆˆ Q โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด ) โ†’ ๐ด = Q )
163 162 3expia โŠข ( ( ๐ด โˆˆ P โˆง ๐‘ โˆˆ Q ) โ†’ ( โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด โ†’ ๐ด = Q ) )
164 25 163 mtod โŠข ( ( ๐ด โˆˆ P โˆง ๐‘ โˆˆ Q ) โ†’ ยฌ โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด )
165 164 expcom โŠข ( ๐‘ โˆˆ Q โ†’ ( ๐ด โˆˆ P โ†’ ยฌ โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐‘ ) โˆˆ ๐ด ) )
166 21 165 vtoclga โŠข ( ๐ต โˆˆ Q โ†’ ( ๐ด โˆˆ P โ†’ ยฌ โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐ต ) โˆˆ ๐ด ) )
167 166 com12 โŠข ( ๐ด โˆˆ P โ†’ ( ๐ต โˆˆ Q โ†’ ยฌ โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐ต ) โˆˆ ๐ด ) )
168 5 16 167 3syld โŠข ( ๐ด โˆˆ P โ†’ ( โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐ต ) โˆˆ ๐ด โ†’ ยฌ โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐ต ) โˆˆ ๐ด ) )
169 168 pm2.01d โŠข ( ๐ด โˆˆ P โ†’ ยฌ โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐ต ) โˆˆ ๐ด )
170 rexnal โŠข ( โˆƒ ๐‘ฅ โˆˆ ๐ด ยฌ ( ๐‘ฅ +Q ๐ต ) โˆˆ ๐ด โ†” ยฌ โˆ€ ๐‘ฅ โˆˆ ๐ด ( ๐‘ฅ +Q ๐ต ) โˆˆ ๐ด )
171 169 170 sylibr โŠข ( ๐ด โˆˆ P โ†’ โˆƒ ๐‘ฅ โˆˆ ๐ด ยฌ ( ๐‘ฅ +Q ๐ต ) โˆˆ ๐ด )