prlem934 - Metamath Proof Explorer

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

Theorem prlem934 10108

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.)

**Hypothesis**
Ref	Expression
prlem934.1	⊢ 𝐵 ∈ V

**Assertion**
Ref	Expression
prlem934	⊢ (𝐴 ∈ P → ∃𝑥 ∈ 𝐴 ¬ (𝑥 +_Q 𝐵) ∈ 𝐴)

Distinct variable groups: 𝑥,𝐴 𝑥,𝐵

Proof of Theorem prlem934 Dummy variables 𝑏 𝑤 𝑦 𝑧 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		prn0 10064	. . . . 5 ⊢ (𝐴 ∈ P → 𝐴 ≠ ∅)
2		r19.2z 4219	. . . . . 6 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴) → ∃𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴)
3	2	ex 401	. . . . 5 ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴 → ∃𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴))
4	1, 3	syl 17	. . . 4 ⊢ (𝐴 ∈ P → (∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴 → ∃𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴))
5		prpssnq 10065	. . . . . . . . 9 ⊢ (𝐴 ∈ P → 𝐴 ⊊ Q)
6	5	pssssd 3865	. . . . . . . 8 ⊢ (𝐴 ∈ P → 𝐴 ⊆ Q)
7	6	sseld 3760	. . . . . . 7 ⊢ (𝐴 ∈ P → ((𝑥 +_Q 𝐵) ∈ 𝐴 → (𝑥 +_Q 𝐵) ∈ Q))
8		addnqf 10023	. . . . . . . . . 10 ⊢ +_Q :(Q × Q)⟶Q
9	8	fdmi 6233	. . . . . . . . 9 ⊢ dom +_Q = (Q × Q)
10		0nnq 9999	. . . . . . . . 9 ⊢ ¬ ∅ ∈ Q
11	9, 10	ndmovrcl 7018	. . . . . . . 8 ⊢ ((𝑥 +_Q 𝐵) ∈ Q → (𝑥 ∈ Q ∧ 𝐵 ∈ Q))
12	11	simprd 489	. . . . . . 7 ⊢ ((𝑥 +_Q 𝐵) ∈ Q → 𝐵 ∈ Q)
13	7, 12	syl6com 37	. . . . . 6 ⊢ ((𝑥 +_Q 𝐵) ∈ 𝐴 → (𝐴 ∈ P → 𝐵 ∈ Q))
14	13	rexlimivw 3176	. . . . 5 ⊢ (∃𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴 → (𝐴 ∈ P → 𝐵 ∈ Q))
15	14	com12 32	. . . 4 ⊢ (𝐴 ∈ P → (∃𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴 → 𝐵 ∈ Q))
16		oveq2 6850	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → (𝑥 +_Q 𝑏) = (𝑥 +_Q 𝐵))
17	16	eleq1d 2829	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → ((𝑥 +_Q 𝑏) ∈ 𝐴 ↔ (𝑥 +_Q 𝐵) ∈ 𝐴))
18	17	ralbidv 3133	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → (∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ↔ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴))
19	18	notbid 309	. . . . . . 7 ⊢ (𝑏 = 𝐵 → (¬ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ↔ ¬ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴))
20	19	imbi2d 331	. . . . . 6 ⊢ (𝑏 = 𝐵 → ((𝐴 ∈ P → ¬ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ↔ (𝐴 ∈ P → ¬ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴)))
21		dfpss2 3853	. . . . . . . . . . 11 ⊢ (𝐴 ⊊ Q ↔ (𝐴 ⊆ Q ∧ ¬ 𝐴 = Q))
22	5, 21	sylib 209	. . . . . . . . . 10 ⊢ (𝐴 ∈ P → (𝐴 ⊆ Q ∧ ¬ 𝐴 = Q))
23	22	simprd 489	. . . . . . . . 9 ⊢ (𝐴 ∈ P → ¬ 𝐴 = Q)
24	23	adantr 472	. . . . . . . 8 ⊢ ((𝐴 ∈ P ∧ 𝑏 ∈ Q) → ¬ 𝐴 = Q)
25	6	3ad2ant1 1163	. . . . . . . . . 10 ⊢ ((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) → 𝐴 ⊆ Q)
26		simpl1 1242	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ 𝑤 ∈ Q) → 𝐴 ∈ P)
27		n0 4095	. . . . . . . . . . . . 13 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝐴)
28	1, 27	sylib 209	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ P → ∃𝑦 𝑦 ∈ 𝐴)
29	26, 28	syl 17	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ 𝑤 ∈ Q) → ∃𝑦 𝑦 ∈ 𝐴)
30		simprl 787	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) → 𝑤 ∈ Q)
31		simpl2 1244	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) → 𝑏 ∈ Q)
32		recclnq 10041	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ Q → (*_Q‘𝑏) ∈ Q)
33		mulclnq 10022	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 ∈ Q ∧ (_Q‘𝑏) ∈ Q) → (𝑤 ·_Q (_Q‘𝑏)) ∈ Q)
34		archnq 10055	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 ·_Q (_Q‘𝑏)) ∈ Q → ∃𝑧 ∈ N (𝑤 ·_Q (_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)
35	33, 34	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ Q ∧ (_Q‘𝑏) ∈ Q) → ∃𝑧 ∈ N (𝑤 ·_Q (_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)
36	32, 35	sylan2 586	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ Q ∧ 𝑏 ∈ Q) → ∃𝑧 ∈ N (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)
37	30, 31, 36	syl2anc 579	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) → ∃𝑧 ∈ N (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)
38		simpll2 1271	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)) → 𝑏 ∈ Q)
39		simplrl 795	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)) → 𝑤 ∈ Q)
40		simprr 789	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·_Q (_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)) → (𝑤 ·_Q (_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)
41		ltmnq 10047	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 ∈ Q → ((𝑤 ·_Q (_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩ ↔ (𝑏 ·_Q (𝑤 ·_Q (_Q‘𝑏))) <_Q (𝑏 ·_Q ⟨𝑧, 1_𝑜⟩)))
42		vex 3353	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑏 ∈ V
43		vex 3353	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑤 ∈ V
44		fvex 6388	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (*_Q‘𝑏) ∈ V
45		mulcomnq 10028	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ·_Q 𝑥) = (𝑥 ·_Q 𝑣)
46		mulassnq 10034	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑣 ·_Q 𝑥) ·_Q 𝑦) = (𝑣 ·_Q (𝑥 ·_Q 𝑦))
47	42, 43, 44, 45, 46	caov12 7060	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 ·_Q (𝑤 ·_Q (_Q‘𝑏))) = (𝑤 ·_Q (𝑏 ·_Q (_Q‘𝑏)))
48		mulcomnq 10028	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 ·_Q ⟨𝑧, 1_𝑜⟩) = (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)
49	47, 48	breq12i 4818	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏 ·_Q (𝑤 ·_Q (_Q‘𝑏))) <_Q (𝑏 ·_Q ⟨𝑧, 1_𝑜⟩) ↔ (𝑤 ·_Q (𝑏 ·_Q (_Q‘𝑏))) <_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏))
50	41, 49	syl6bb 278	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ Q → ((𝑤 ·_Q (_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩ ↔ (𝑤 ·_Q (𝑏 ·_Q (_Q‘𝑏))) <_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)))
51	50	adantr 472	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏 ∈ Q ∧ 𝑤 ∈ Q) → ((𝑤 ·_Q (_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩ ↔ (𝑤 ·_Q (𝑏 ·_Q (_Q‘𝑏))) <_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)))
52		recidnq 10040	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 ∈ Q → (𝑏 ·_Q (*_Q‘𝑏)) = 1_Q)
53	52	oveq2d 6858	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 ∈ Q → (𝑤 ·_Q (𝑏 ·_Q (*_Q‘𝑏))) = (𝑤 ·_Q 1_Q))
54		mulidnq 10038	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ Q → (𝑤 ·_Q 1_Q) = 𝑤)
55	53, 54	sylan9eq 2819	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∈ Q ∧ 𝑤 ∈ Q) → (𝑤 ·_Q (𝑏 ·_Q (*_Q‘𝑏))) = 𝑤)
56	55	breq1d 4819	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏 ∈ Q ∧ 𝑤 ∈ Q) → ((𝑤 ·_Q (𝑏 ·_Q (*_Q‘𝑏))) <_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) ↔ 𝑤 <_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)))
57	51, 56	bitrd 270	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ Q ∧ 𝑤 ∈ Q) → ((𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩ ↔ 𝑤 <_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)))
58	57	biimpa 468	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑏 ∈ Q ∧ 𝑤 ∈ Q) ∧ (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩) → 𝑤 <_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏))
59	38, 39, 40, 58	syl21anc 866	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)) → 𝑤 <_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏))
60		simprl 787	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)) → 𝑧 ∈ N)
61		pinq 10002	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ N → ⟨𝑧, 1_𝑜⟩ ∈ Q)
62		mulclnq 10022	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⟨𝑧, 1_𝑜⟩ ∈ Q ∧ 𝑏 ∈ Q) → (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) ∈ Q)
63	61, 62	sylan 575	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) ∈ Q)
64	60, 38, 63	syl2anc 579	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)) → (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) ∈ Q)
65		simpll1 1269	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)) → 𝐴 ∈ P)
66		simplrr 796	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)) → 𝑦 ∈ 𝐴)
67		elprnq 10066	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ P ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ Q)
68	65, 66, 67	syl2anc 579	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)) → 𝑦 ∈ Q)
69		ltaddnq 10049	. . . . . . . . . . . . . . . . . 18 ⊢ (((⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) ∈ Q ∧ 𝑦 ∈ Q) → (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) <_Q ((⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) +_Q 𝑦))
70		addcomnq 10026	. . . . . . . . . . . . . . . . . 18 ⊢ ((⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) +_Q 𝑦) = (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏))
71	69, 70	syl6breq 4850	. . . . . . . . . . . . . . . . 17 ⊢ (((⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) ∈ Q ∧ 𝑦 ∈ Q) → (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) <_Q (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)))
72	64, 68, 71	syl2anc 579	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)) → (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) <_Q (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)))
73		ltsonq 10044	. . . . . . . . . . . . . . . . 17 ⊢ <_Q Or Q
74		ltrelnq 10001	. . . . . . . . . . . . . . . . 17 ⊢ <_Q ⊆ (Q × Q)
75	73, 74	sotri 5706	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 <_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) ∧ (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) <_Q (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏))) → 𝑤 <_Q (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)))
76	59, 72, 75	syl2anc 579	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)) → 𝑤 <_Q (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)))
77		simpll3 1273	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)) → ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴)
78		opeq1 4559	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 1_𝑜 → ⟨𝑤, 1_𝑜⟩ = ⟨1_𝑜, 1_𝑜⟩)
79		df-1nq 9991	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1_Q = ⟨1_𝑜, 1_𝑜⟩
80	78, 79	syl6eqr 2817	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 1_𝑜 → ⟨𝑤, 1_𝑜⟩ = 1_Q)
81	80	oveq1d 6857	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 1_𝑜 → (⟨𝑤, 1_𝑜⟩ ·_Q 𝑏) = (1_Q ·_Q 𝑏))
82	81	oveq2d 6858	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 1_𝑜 → (𝑦 +_Q (⟨𝑤, 1_𝑜⟩ ·_Q 𝑏)) = (𝑦 +_Q (1_Q ·_Q 𝑏)))
83	82	eleq1d 2829	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 1_𝑜 → ((𝑦 +_Q (⟨𝑤, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴 ↔ (𝑦 +_Q (1_Q ·_Q 𝑏)) ∈ 𝐴))
84	83	imbi2d 331	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 1_𝑜 → (((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +_Q (⟨𝑤, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴) ↔ ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +_Q (1_Q ·_Q 𝑏)) ∈ 𝐴)))
85		opeq1 4559	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑧 → ⟨𝑤, 1_𝑜⟩ = ⟨𝑧, 1_𝑜⟩)
86	85	oveq1d 6857	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑧 → (⟨𝑤, 1_𝑜⟩ ·_Q 𝑏) = (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏))
87	86	oveq2d 6858	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑧 → (𝑦 +_Q (⟨𝑤, 1_𝑜⟩ ·_Q 𝑏)) = (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)))
88	87	eleq1d 2829	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑧 → ((𝑦 +_Q (⟨𝑤, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴 ↔ (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴))
89	88	imbi2d 331	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑧 → (((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +_Q (⟨𝑤, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴) ↔ ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴)))
90		opeq1 4559	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = (𝑧 +_N 1_𝑜) → ⟨𝑤, 1_𝑜⟩ = ⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩)
91	90	oveq1d 6857	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = (𝑧 +_N 1_𝑜) → (⟨𝑤, 1_𝑜⟩ ·_Q 𝑏) = (⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ·_Q 𝑏))
92	91	oveq2d 6858	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = (𝑧 +_N 1_𝑜) → (𝑦 +_Q (⟨𝑤, 1_𝑜⟩ ·_Q 𝑏)) = (𝑦 +_Q (⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ·_Q 𝑏)))
93	92	eleq1d 2829	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = (𝑧 +_N 1_𝑜) → ((𝑦 +_Q (⟨𝑤, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴 ↔ (𝑦 +_Q (⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴))
94	93	imbi2d 331	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = (𝑧 +_N 1_𝑜) → (((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +_Q (⟨𝑤, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴) ↔ ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +_Q (⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴)))
95		mulcomnq 10028	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1_Q ·_Q 𝑏) = (𝑏 ·_Q 1_Q)
96		mulidnq 10038	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 ∈ Q → (𝑏 ·_Q 1_Q) = 𝑏)
97	95, 96	syl5eq 2811	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 ∈ Q → (1_Q ·_Q 𝑏) = 𝑏)
98		oveq1 6849	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → (𝑥 +_Q 𝑏) = (𝑦 +_Q 𝑏))
99	98	eleq1d 2829	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑦 → ((𝑥 +_Q 𝑏) ∈ 𝐴 ↔ (𝑦 +_Q 𝑏) ∈ 𝐴))
100	99	rspccva 3460	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +_Q 𝑏) ∈ 𝐴)
101		oveq2 6850	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1_Q ·_Q 𝑏) = 𝑏 → (𝑦 +_Q (1_Q ·_Q 𝑏)) = (𝑦 +_Q 𝑏))
102	101	eleq1d 2829	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1_Q ·_Q 𝑏) = 𝑏 → ((𝑦 +_Q (1_Q ·_Q 𝑏)) ∈ 𝐴 ↔ (𝑦 +_Q 𝑏) ∈ 𝐴))
103	102	biimpar 469	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((1_Q ·_Q 𝑏) = 𝑏 ∧ (𝑦 +_Q 𝑏) ∈ 𝐴) → (𝑦 +_Q (1_Q ·_Q 𝑏)) ∈ 𝐴)
104	97, 100, 103	syl2an 589	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∈ Q ∧ (∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑦 +_Q (1_Q ·_Q 𝑏)) ∈ 𝐴)
105	104	3impb 1143	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +_Q (1_Q ·_Q 𝑏)) ∈ 𝐴)
106		3simpa 1178	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴))
107		oveq1 6849	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) → (𝑥 +_Q 𝑏) = ((𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) +_Q 𝑏))
108	107	eleq1d 2829	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) → ((𝑥 +_Q 𝑏) ∈ 𝐴 ↔ ((𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) +_Q 𝑏) ∈ 𝐴))
109	108	rspccva 3460	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴) → ((𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) +_Q 𝑏) ∈ 𝐴)
110		addassnq 10033	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) +_Q 𝑏) = (𝑦 +_Q ((⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) +_Q 𝑏))
111		opex 5088	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ⟨𝑧, 1_𝑜⟩ ∈ V
112		1nq 10003	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 1_Q ∈ Q
113	112	elexi 3366	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 1_Q ∈ V
114		distrnq 10036	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑣 ·_Q (𝑥 +_Q 𝑦)) = ((𝑣 ·_Q 𝑥) +_Q (𝑣 ·_Q 𝑦))
115	111, 113, 42, 45, 114	caovdir 7066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((⟨𝑧, 1_𝑜⟩ +_Q 1_Q) ·_Q 𝑏) = ((⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) +_Q (1_Q ·_Q 𝑏))
116	115	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → ((⟨𝑧, 1_𝑜⟩ +_Q 1_Q) ·_Q 𝑏) = ((⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) +_Q (1_Q ·_Q 𝑏)))
117		addpqnq 10013	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((⟨𝑧, 1_𝑜⟩ ∈ Q ∧ 1_Q ∈ Q) → (⟨𝑧, 1_𝑜⟩ +_Q 1_Q) = ([Q]‘(⟨𝑧, 1_𝑜⟩ +_pQ 1_Q)))
118	61, 112, 117	sylancl 580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 ∈ N → (⟨𝑧, 1_𝑜⟩ +_Q 1_Q) = ([Q]‘(⟨𝑧, 1_𝑜⟩ +_pQ 1_Q)))
119	79	oveq2i 6853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (⟨𝑧, 1_𝑜⟩ +_pQ 1_Q) = (⟨𝑧, 1_𝑜⟩ +_pQ ⟨1_𝑜, 1_𝑜⟩)
120		1pi 9958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ 1_𝑜 ∈ N
121		addpipq 10012	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝑧 ∈ N ∧ 1_𝑜 ∈ N) ∧ (1_𝑜 ∈ N ∧ 1_𝑜 ∈ N)) → (⟨𝑧, 1_𝑜⟩ +_pQ ⟨1_𝑜, 1_𝑜⟩) = ⟨((𝑧 ·_N 1_𝑜) +_N (1_𝑜 ·_N 1_𝑜)), (1_𝑜 ·_N 1_𝑜)⟩)
122	120, 120, 121	mpanr12 696	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑧 ∈ N ∧ 1_𝑜 ∈ N) → (⟨𝑧, 1_𝑜⟩ +_pQ ⟨1_𝑜, 1_𝑜⟩) = ⟨((𝑧 ·_N 1_𝑜) +_N (1_𝑜 ·_N 1_𝑜)), (1_𝑜 ·_N 1_𝑜)⟩)
123	120, 122	mpan2 682	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 ∈ N → (⟨𝑧, 1_𝑜⟩ +_pQ ⟨1_𝑜, 1_𝑜⟩) = ⟨((𝑧 ·_N 1_𝑜) +_N (1_𝑜 ·_N 1_𝑜)), (1_𝑜 ·_N 1_𝑜)⟩)
124	119, 123	syl5eq 2811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 ∈ N → (⟨𝑧, 1_𝑜⟩ +_pQ 1_Q) = ⟨((𝑧 ·_N 1_𝑜) +_N (1_𝑜 ·_N 1_𝑜)), (1_𝑜 ·_N 1_𝑜)⟩)
125		mulidpi 9961	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧 ∈ N → (𝑧 ·_N 1_𝑜) = 𝑧)
126		mulidpi 9961	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (1_𝑜 ∈ N → (1_𝑜 ·_N 1_𝑜) = 1_𝑜)
127	120, 126	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧 ∈ N → (1_𝑜 ·_N 1_𝑜) = 1_𝑜)
128	125, 127	oveq12d 6860	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 ∈ N → ((𝑧 ·_N 1_𝑜) +_N (1_𝑜 ·_N 1_𝑜)) = (𝑧 +_N 1_𝑜))
129	128, 127	opeq12d 4567	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 ∈ N → ⟨((𝑧 ·_N 1_𝑜) +_N (1_𝑜 ·_N 1_𝑜)), (1_𝑜 ·_N 1_𝑜)⟩ = ⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩)
130	124, 129	eqtrd 2799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧 ∈ N → (⟨𝑧, 1_𝑜⟩ +_pQ 1_Q) = ⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩)
131	130	fveq2d 6379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 ∈ N → ([Q]‘(⟨𝑧, 1_𝑜⟩ +_pQ 1_Q)) = ([Q]‘⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩))
132		addclpi 9967	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑧 ∈ N ∧ 1_𝑜 ∈ N) → (𝑧 +_N 1_𝑜) ∈ N)
133	120, 132	mpan2 682	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧 ∈ N → (𝑧 +_N 1_𝑜) ∈ N)
134		pinq 10002	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑧 +_N 1_𝑜) ∈ N → ⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ∈ Q)
135		nqerid 10008	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ∈ Q → ([Q]‘⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩) = ⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩)
136	133, 134, 135	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 ∈ N → ([Q]‘⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩) = ⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩)
137	118, 131, 136	3eqtrd 2803	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑧 ∈ N → (⟨𝑧, 1_𝑜⟩ +_Q 1_Q) = ⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩)
138	137	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → (⟨𝑧, 1_𝑜⟩ +_Q 1_Q) = ⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩)
139	138	oveq1d 6857	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → ((⟨𝑧, 1_𝑜⟩ +_Q 1_Q) ·_Q 𝑏) = (⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ·_Q 𝑏))
140	97	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → (1_Q ·_Q 𝑏) = 𝑏)
141	140	oveq2d 6858	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → ((⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) +_Q (1_Q ·_Q 𝑏)) = ((⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) +_Q 𝑏))
142	116, 139, 141	3eqtr3rd 2808	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → ((⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) +_Q 𝑏) = (⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ·_Q 𝑏))
143	142	oveq2d 6858	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → (𝑦 +_Q ((⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) +_Q 𝑏)) = (𝑦 +_Q (⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ·_Q 𝑏)))
144	110, 143	syl5eq 2811	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → ((𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) +_Q 𝑏) = (𝑦 +_Q (⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ·_Q 𝑏)))
145	144	eleq1d 2829	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → (((𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) +_Q 𝑏) ∈ 𝐴 ↔ (𝑦 +_Q (⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴))
146	109, 145	syl5ib 235	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → ((∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴) → (𝑦 +_Q (⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴))
147	146	expd 404	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → (∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 → ((𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴 → (𝑦 +_Q (⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴)))
148	147	expimpd 445	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ N → ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) → ((𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴 → (𝑦 +_Q (⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴)))
149	106, 148	syl5 34	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ N → ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴 → (𝑦 +_Q (⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴)))
150	149	a2d 29	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ N → (((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴) → ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +_Q (⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴)))
151	84, 89, 94, 89, 105, 150	indpi 9982	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ N → ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴))
152	151	imp 395	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ N ∧ (𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴)
153	60, 38, 77, 66, 152	syl13anc 1491	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)) → (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴)
154		prcdnq 10068	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ P ∧ (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴) → (𝑤 <_Q (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) → 𝑤 ∈ 𝐴))
155	65, 153, 154	syl2anc 579	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)) → (𝑤 <_Q (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) → 𝑤 ∈ 𝐴))
156	76, 155	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)) → 𝑤 ∈ 𝐴)
157	37, 156	rexlimddv 3182	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) → 𝑤 ∈ 𝐴)
158	157	expr 448	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ 𝑤 ∈ Q) → (𝑦 ∈ 𝐴 → 𝑤 ∈ 𝐴))
159	158	exlimdv 2028	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ 𝑤 ∈ Q) → (∃𝑦 𝑦 ∈ 𝐴 → 𝑤 ∈ 𝐴))
160	29, 159	mpd 15	. . . . . . . . . 10 ⊢ (((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ 𝑤 ∈ Q) → 𝑤 ∈ 𝐴)
161	25, 160	eqelssd 3782	. . . . . . . . 9 ⊢ ((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) → 𝐴 = Q)
162	161	3expia 1150	. . . . . . . 8 ⊢ ((𝐴 ∈ P ∧ 𝑏 ∈ Q) → (∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 → 𝐴 = Q))
163	24, 162	mtod 189	. . . . . . 7 ⊢ ((𝐴 ∈ P ∧ 𝑏 ∈ Q) → ¬ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴)
164	163	expcom 402	. . . . . 6 ⊢ (𝑏 ∈ Q → (𝐴 ∈ P → ¬ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴))
165	20, 164	vtoclga 3424	. . . . 5 ⊢ (𝐵 ∈ Q → (𝐴 ∈ P → ¬ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴))
166	165	com12 32	. . . 4 ⊢ (𝐴 ∈ P → (𝐵 ∈ Q → ¬ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴))
167	4, 15, 166	3syld 60	. . 3 ⊢ (𝐴 ∈ P → (∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴 → ¬ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴))
168	167	pm2.01d 181	. 2 ⊢ (𝐴 ∈ P → ¬ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴)
169		rexnal 3141	. 2 ⊢ (∃𝑥 ∈ 𝐴 ¬ (𝑥 +_Q 𝐵) ∈ 𝐴 ↔ ¬ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴)
170	168, 169	sylibr 225	1 ⊢ (𝐴 ∈ P → ∃𝑥 ∈ 𝐴 ¬ (𝑥 +_Q 𝐵) ∈ 𝐴)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 197 ∧ wa 384 ∧ w3a 1107 = wceq 1652 ∃wex 1874 ∈ wcel 2155 ≠ wne 2937 ∀wral 3055 ∃wrex 3056 Vcvv 3350 ⊆ wss 3732 ⊊ wpss 3733 ∅c0 4079 ⟨cop 4340 class class class wbr 4809 × cxp 5275 ‘cfv 6068 (class class class)co 6842 1_𝑜c1o 7757 Ncnpi 9919 +_N cpli 9920 ·_N cmi 9921 +_pQ cplpq 9923 Qcnq 9927 1_Qc1q 9928 [Q]cerq 9929 +_Q cplq 9930 ·_Q cmq 9931 *_Qcrq 9932 <_Q cltq 9933 Pcnp 9934

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1890 ax-4 1904 ax-5 2005 ax-6 2070 ax-7 2105 ax-8 2157 ax-9 2164 ax-10 2183 ax-11 2198 ax-12 2211 ax-13 2352 ax-ext 2743 ax-sep 4941 ax-nul 4949 ax-pow 5001 ax-pr 5062 ax-un 7147

This theorem depends on definitions: df-bi 198 df-an 385 df-or 874 df-3or 1108 df-3an 1109 df-tru 1656 df-ex 1875 df-nf 1879 df-sb 2063 df-mo 2565 df-eu 2582 df-clab 2752 df-cleq 2758 df-clel 2761 df-nfc 2896 df-ne 2938 df-ral 3060 df-rex 3061 df-reu 3062 df-rmo 3063 df-rab 3064 df-v 3352 df-sbc 3597 df-csb 3692 df-dif 3735 df-un 3737 df-in 3739 df-ss 3746 df-pss 3748 df-nul 4080 df-if 4244 df-pw 4317 df-sn 4335 df-pr 4337 df-tp 4339 df-op 4341 df-uni 4595 df-int 4634 df-iun 4678 df-br 4810 df-opab 4872 df-mpt 4889 df-tr 4912 df-id 5185 df-eprel 5190 df-po 5198 df-so 5199 df-fr 5236 df-we 5238 df-xp 5283 df-rel 5284 df-cnv 5285 df-co 5286 df-dm 5287 df-rn 5288 df-res 5289 df-ima 5290 df-pred 5865 df-ord 5911 df-on 5912 df-lim 5913 df-suc 5914 df-iota 6031 df-fun 6070 df-fn 6071 df-f 6072 df-f1 6073 df-fo 6074 df-f1o 6075 df-fv 6076 df-ov 6845 df-oprab 6846 df-mpt2 6847 df-om 7264 df-1st 7366 df-2nd 7367 df-wrecs 7610 df-recs 7672 df-rdg 7710 df-1o 7764 df-oadd 7768 df-omul 7769 df-er 7947 df-ni 9947 df-pli 9948 df-mi 9949 df-lti 9950 df-plpq 9983 df-mpq 9984 df-ltpq 9985 df-enq 9986 df-nq 9987 df-erq 9988 df-plq 9989 df-mq 9990 df-1nq 9991 df-rq 9992 df-ltnq 9993 df-np 10056

This theorem is referenced by: ltaddpr 10109 ltexprlem7 10117 prlem936 10122

W3C validator