Theorem prlem934 9734

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 9690	. . . . 5 ⊢ (𝐴 ∈ P → 𝐴 ≠ ∅)
2		r19.2z 4012	. . . . . 6 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴) → ∃𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴)
3	2	ex 449	. . . . 5 ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴 → ∃𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴))
4	1, 3	syl 17	. . . 4 ⊢ (𝐴 ∈ P → (∀𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴 → ∃𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴))
5		prpssnq 9691	. . . . . . . . 9 ⊢ (𝐴 ∈ P → 𝐴 ⊊ Q)
6	5	pssssd 3666	. . . . . . . 8 ⊢ (𝐴 ∈ P → 𝐴 ⊆ Q)
7	6	sseld 3567	. . . . . . 7 ⊢ (𝐴 ∈ P → ((𝑥 +Q 𝐵) ∈ 𝐴 → (𝑥 +Q 𝐵) ∈ Q))
8		addnqf 9649	. . . . . . . . . 10 ⊢ +Q :(Q × Q)⟶Q
9	8	fdmi 5965	. . . . . . . . 9 ⊢ dom +Q = (Q × Q)
10		0nnq 9625	. . . . . . . . 9 ⊢ ¬ ∅ ∈ Q
11	9, 10	ndmovrcl 6718	. . . . . . . 8 ⊢ ((𝑥 +Q 𝐵) ∈ Q → (𝑥 ∈ Q ∧ 𝐵 ∈ Q))
12	11	simprd 478	. . . . . . 7 ⊢ ((𝑥 +Q 𝐵) ∈ Q → 𝐵 ∈ Q)
13	7, 12	syl6com 36	. . . . . 6 ⊢ ((𝑥 +Q 𝐵) ∈ 𝐴 → (𝐴 ∈ P → 𝐵 ∈ Q))
14	13	rexlimivw 3011	. . . . 5 ⊢ (∃𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴 → (𝐴 ∈ P → 𝐵 ∈ Q))
15	14	com12 32	. . . 4 ⊢ (𝐴 ∈ P → (∃𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴 → 𝐵 ∈ Q))
16		oveq2 6557	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → (𝑥 +Q 𝑏) = (𝑥 +Q 𝐵))
17	16	eleq1d 2672	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → ((𝑥 +Q 𝑏) ∈ 𝐴 ↔ (𝑥 +Q 𝐵) ∈ 𝐴))
18	17	ralbidv 2969	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → (∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ↔ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴))
19	18	notbid 307	. . . . . . 7 ⊢ (𝑏 = 𝐵 → (¬ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ↔ ¬ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴))
20	19	imbi2d 329	. . . . . 6 ⊢ (𝑏 = 𝐵 → ((𝐴 ∈ P → ¬ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ↔ (𝐴 ∈ P → ¬ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴)))
21		dfpss2 3654	. . . . . . . . . . 11 ⊢ (𝐴 ⊊ Q ↔ (𝐴 ⊆ Q ∧ ¬ 𝐴 = Q))
22	5, 21	sylib 207	. . . . . . . . . 10 ⊢ (𝐴 ∈ P → (𝐴 ⊆ Q ∧ ¬ 𝐴 = Q))
23	22	simprd 478	. . . . . . . . 9 ⊢ (𝐴 ∈ P → ¬ 𝐴 = Q)
24	23	adantr 480	. . . . . . . 8 ⊢ ((𝐴 ∈ P ∧ 𝑏 ∈ Q) → ¬ 𝐴 = Q)
25	6	3ad2ant1 1075	. . . . . . . . . 10 ⊢ ((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) → 𝐴 ⊆ Q)
26		simpl1 1057	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ 𝑤 ∈ Q) → 𝐴 ∈ P)
27		n0 3890	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝐴)
28	1, 27	sylib 207	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ P → ∃𝑦 𝑦 ∈ 𝐴)
29	26, 28	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ 𝑤 ∈ Q) → ∃𝑦 𝑦 ∈ 𝐴)
30		simprl 790	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) → 𝑤 ∈ Q)
31		simpl2 1058	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) → 𝑏 ∈ Q)
32		recclnq 9667	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ Q → (*Q‘𝑏) ∈ Q)
33		mulclnq 9648	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑤 ∈ Q ∧ (*Q‘𝑏) ∈ Q) → (𝑤 ·Q (*Q‘𝑏)) ∈ Q)
34		archnq 9681	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑤 ·Q (*Q‘𝑏)) ∈ Q → ∃𝑧 ∈ N (𝑤 ·Q (*Q‘𝑏)) <Q ⟨𝑧, 1𝑜⟩)
35	33, 34	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 ∈ Q ∧ (*Q‘𝑏) ∈ Q) → ∃𝑧 ∈ N (𝑤 ·Q (*Q‘𝑏)) <Q ⟨𝑧, 1𝑜⟩)
36	32, 35	sylan2 490	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 ∈ Q ∧ 𝑏 ∈ Q) → ∃𝑧 ∈ N (𝑤 ·Q (*Q‘𝑏)) <Q ⟨𝑧, 1𝑜⟩)
37	30, 31, 36	syl2anc 691	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) → ∃𝑧 ∈ N (𝑤 ·Q (*Q‘𝑏)) <Q ⟨𝑧, 1𝑜⟩)
38		simpll2 1094	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·Q (*Q‘𝑏)) <Q ⟨𝑧, 1𝑜⟩)) → 𝑏 ∈ Q)
39		simplrl 796	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·Q (*Q‘𝑏)) <Q ⟨𝑧, 1𝑜⟩)) → 𝑤 ∈ Q)
40		simprr 792	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·Q (*Q‘𝑏)) <Q ⟨𝑧, 1𝑜⟩)) → (𝑤 ·Q (*Q‘𝑏)) <Q ⟨𝑧, 1𝑜⟩)
41		ltmnq 9673	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 ∈ Q → ((𝑤 ·Q (*Q‘𝑏)) <Q ⟨𝑧, 1𝑜⟩ ↔ (𝑏 ·Q (𝑤 ·Q (*Q‘𝑏))) <Q (𝑏 ·Q ⟨𝑧, 1𝑜⟩)))
42		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑏 ∈ V
43		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑤 ∈ V
44		fvex 6113	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (*Q‘𝑏) ∈ V
45		mulcomnq 9654	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 ·Q 𝑥) = (𝑥 ·Q 𝑣)
46		mulassnq 9660	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑣 ·Q 𝑥) ·Q 𝑦) = (𝑣 ·Q (𝑥 ·Q 𝑦))
47	42, 43, 44, 45, 46	caov12 6760	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 ·Q (𝑤 ·Q (*Q‘𝑏))) = (𝑤 ·Q (𝑏 ·Q (*Q‘𝑏)))
48		mulcomnq 9654	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 ·Q ⟨𝑧, 1𝑜⟩) = (⟨𝑧, 1𝑜⟩ ·Q 𝑏)
49	47, 48	breq12i 4592	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏 ·Q (𝑤 ·Q (*Q‘𝑏))) <Q (𝑏 ·Q ⟨𝑧, 1𝑜⟩) ↔ (𝑤 ·Q (𝑏 ·Q (*Q‘𝑏))) <Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏))
50	41, 49	syl6bb 275	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 ∈ Q → ((𝑤 ·Q (*Q‘𝑏)) <Q ⟨𝑧, 1𝑜⟩ ↔ (𝑤 ·Q (𝑏 ·Q (*Q‘𝑏))) <Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)))
51	50	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏 ∈ Q ∧ 𝑤 ∈ Q) → ((𝑤 ·Q (*Q‘𝑏)) <Q ⟨𝑧, 1𝑜⟩ ↔ (𝑤 ·Q (𝑏 ·Q (*Q‘𝑏))) <Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)))
52		recidnq 9666	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 ∈ Q → (𝑏 ·Q (*Q‘𝑏)) = 1Q)
53	52	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 ∈ Q → (𝑤 ·Q (𝑏 ·Q (*Q‘𝑏))) = (𝑤 ·Q 1Q))
54		mulidnq 9664	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ Q → (𝑤 ·Q 1Q) = 𝑤)
55	53, 54	sylan9eq 2664	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑏 ∈ Q ∧ 𝑤 ∈ Q) → (𝑤 ·Q (𝑏 ·Q (*Q‘𝑏))) = 𝑤)
56	55	breq1d 4593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏 ∈ Q ∧ 𝑤 ∈ Q) → ((𝑤 ·Q (𝑏 ·Q (*Q‘𝑏))) <Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏) ↔ 𝑤 <Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)))
57	51, 56	bitrd 267	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∈ Q ∧ 𝑤 ∈ Q) → ((𝑤 ·Q (*Q‘𝑏)) <Q ⟨𝑧, 1𝑜⟩ ↔ 𝑤 <Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)))
58	57	biimpa 500	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 ∈ Q ∧ 𝑤 ∈ Q) ∧ (𝑤 ·Q (*Q‘𝑏)) <Q ⟨𝑧, 1𝑜⟩) → 𝑤 <Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏))
59	38, 39, 40, 58	syl21anc 1317	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·Q (*Q‘𝑏)) <Q ⟨𝑧, 1𝑜⟩)) → 𝑤 <Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏))
60		simprl 790	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·Q (*Q‘𝑏)) <Q ⟨𝑧, 1𝑜⟩)) → 𝑧 ∈ N)
61		pinq 9628	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ N → ⟨𝑧, 1𝑜⟩ ∈ Q)
62		mulclnq 9648	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⟨𝑧, 1𝑜⟩ ∈ Q ∧ 𝑏 ∈ Q) → (⟨𝑧, 1𝑜⟩ ·Q 𝑏) ∈ Q)
63	61, 62	sylan 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → (⟨𝑧, 1𝑜⟩ ·Q 𝑏) ∈ Q)
64	60, 38, 63	syl2anc 691	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·Q (*Q‘𝑏)) <Q ⟨𝑧, 1𝑜⟩)) → (⟨𝑧, 1𝑜⟩ ·Q 𝑏) ∈ Q)
65		simpll1 1093	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·Q (*Q‘𝑏)) <Q ⟨𝑧, 1𝑜⟩)) → 𝐴 ∈ P)
66		simplrr 797	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·Q (*Q‘𝑏)) <Q ⟨𝑧, 1𝑜⟩)) → 𝑦 ∈ 𝐴)
67		elprnq 9692	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ P ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ Q)
68	65, 66, 67	syl2anc 691	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·Q (*Q‘𝑏)) <Q ⟨𝑧, 1𝑜⟩)) → 𝑦 ∈ Q)
69		ltaddnq 9675	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((⟨𝑧, 1𝑜⟩ ·Q 𝑏) ∈ Q ∧ 𝑦 ∈ Q) → (⟨𝑧, 1𝑜⟩ ·Q 𝑏) <Q ((⟨𝑧, 1𝑜⟩ ·Q 𝑏) +Q 𝑦))
70		addcomnq 9652	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⟨𝑧, 1𝑜⟩ ·Q 𝑏) +Q 𝑦) = (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏))
71	69, 70	syl6breq 4624	. . . . . . . . . . . . . . . . . . 19 ⊢ (((⟨𝑧, 1𝑜⟩ ·Q 𝑏) ∈ Q ∧ 𝑦 ∈ Q) → (⟨𝑧, 1𝑜⟩ ·Q 𝑏) <Q (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)))
72	64, 68, 71	syl2anc 691	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·Q (*Q‘𝑏)) <Q ⟨𝑧, 1𝑜⟩)) → (⟨𝑧, 1𝑜⟩ ·Q 𝑏) <Q (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)))
73		ltsonq 9670	. . . . . . . . . . . . . . . . . . 19 ⊢ <Q Or Q
74		ltrelnq 9627	. . . . . . . . . . . . . . . . . . 19 ⊢ <Q ⊆ (Q × Q)
75	73, 74	sotri 5442	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 <Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏) ∧ (⟨𝑧, 1𝑜⟩ ·Q 𝑏) <Q (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏))) → 𝑤 <Q (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)))
76	59, 72, 75	syl2anc 691	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·Q (*Q‘𝑏)) <Q ⟨𝑧, 1𝑜⟩)) → 𝑤 <Q (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)))
77		simpll3 1095	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·Q (*Q‘𝑏)) <Q ⟨𝑧, 1𝑜⟩)) → ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴)
78		opeq1 4340	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = 1𝑜 → ⟨𝑤, 1𝑜⟩ = ⟨1𝑜, 1𝑜⟩)
79		df-1nq 9617	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 1Q = ⟨1𝑜, 1𝑜⟩
80	78, 79	syl6eqr 2662	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = 1𝑜 → ⟨𝑤, 1𝑜⟩ = 1Q)
81	80	oveq1d 6564	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 1𝑜 → (⟨𝑤, 1𝑜⟩ ·Q 𝑏) = (1Q ·Q 𝑏))
82	81	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 1𝑜 → (𝑦 +Q (⟨𝑤, 1𝑜⟩ ·Q 𝑏)) = (𝑦 +Q (1Q ·Q 𝑏)))
83	82	eleq1d 2672	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 1𝑜 → ((𝑦 +Q (⟨𝑤, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴 ↔ (𝑦 +Q (1Q ·Q 𝑏)) ∈ 𝐴))
84	83	imbi2d 329	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 1𝑜 → (((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q (⟨𝑤, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴) ↔ ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q (1Q ·Q 𝑏)) ∈ 𝐴)))
85		opeq1 4340	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = 𝑧 → ⟨𝑤, 1𝑜⟩ = ⟨𝑧, 1𝑜⟩)
86	85	oveq1d 6564	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 𝑧 → (⟨𝑤, 1𝑜⟩ ·Q 𝑏) = (⟨𝑧, 1𝑜⟩ ·Q 𝑏))
87	86	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑧 → (𝑦 +Q (⟨𝑤, 1𝑜⟩ ·Q 𝑏)) = (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)))
88	87	eleq1d 2672	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑧 → ((𝑦 +Q (⟨𝑤, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴 ↔ (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴))
89	88	imbi2d 329	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑧 → (((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q (⟨𝑤, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴) ↔ ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴)))
90		opeq1 4340	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = (𝑧 +N 1𝑜) → ⟨𝑤, 1𝑜⟩ = ⟨(𝑧 +N 1𝑜), 1𝑜⟩)
91	90	oveq1d 6564	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = (𝑧 +N 1𝑜) → (⟨𝑤, 1𝑜⟩ ·Q 𝑏) = (⟨(𝑧 +N 1𝑜), 1𝑜⟩ ·Q 𝑏))
92	91	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = (𝑧 +N 1𝑜) → (𝑦 +Q (⟨𝑤, 1𝑜⟩ ·Q 𝑏)) = (𝑦 +Q (⟨(𝑧 +N 1𝑜), 1𝑜⟩ ·Q 𝑏)))
93	92	eleq1d 2672	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = (𝑧 +N 1𝑜) → ((𝑦 +Q (⟨𝑤, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴 ↔ (𝑦 +Q (⟨(𝑧 +N 1𝑜), 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴))
94	93	imbi2d 329	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = (𝑧 +N 1𝑜) → (((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q (⟨𝑤, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴) ↔ ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q (⟨(𝑧 +N 1𝑜), 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴)))
95		mulcomnq 9654	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1Q ·Q 𝑏) = (𝑏 ·Q 1Q)
96		mulidnq 9664	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 ∈ Q → (𝑏 ·Q 1Q) = 𝑏)
97	95, 96	syl5eq 2656	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 ∈ Q → (1Q ·Q 𝑏) = 𝑏)
98		oveq1 6556	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑦 → (𝑥 +Q 𝑏) = (𝑦 +Q 𝑏))
99	98	eleq1d 2672	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑦 → ((𝑥 +Q 𝑏) ∈ 𝐴 ↔ (𝑦 +Q 𝑏) ∈ 𝐴))
100	99	rspccva 3281	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q 𝑏) ∈ 𝐴)
101		oveq2 6557	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1Q ·Q 𝑏) = 𝑏 → (𝑦 +Q (1Q ·Q 𝑏)) = (𝑦 +Q 𝑏))
102	101	eleq1d 2672	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1Q ·Q 𝑏) = 𝑏 → ((𝑦 +Q (1Q ·Q 𝑏)) ∈ 𝐴 ↔ (𝑦 +Q 𝑏) ∈ 𝐴))
103	102	biimpar 501	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1Q ·Q 𝑏) = 𝑏 ∧ (𝑦 +Q 𝑏) ∈ 𝐴) → (𝑦 +Q (1Q ·Q 𝑏)) ∈ 𝐴)
104	97, 100, 103	syl2an 493	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑏 ∈ Q ∧ (∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑦 +Q (1Q ·Q 𝑏)) ∈ 𝐴)
105	104	3impb 1252	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q (1Q ·Q 𝑏)) ∈ 𝐴)
106		3simpa 1051	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴))
107		oveq1 6556	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) → (𝑥 +Q 𝑏) = ((𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) +Q 𝑏))
108	107	eleq1d 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) → ((𝑥 +Q 𝑏) ∈ 𝐴 ↔ ((𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) +Q 𝑏) ∈ 𝐴))
109	108	rspccva 3281	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴) → ((𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) +Q 𝑏) ∈ 𝐴)
110		addassnq 9659	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) +Q 𝑏) = (𝑦 +Q ((⟨𝑧, 1𝑜⟩ ·Q 𝑏) +Q 𝑏))
111		opex 4859	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ⟨𝑧, 1𝑜⟩ ∈ V
112		1nq 9629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 1Q ∈ Q
113	112	elexi 3186	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 1Q ∈ V
114		distrnq 9662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑣 ·Q (𝑥 +Q 𝑦)) = ((𝑣 ·Q 𝑥) +Q (𝑣 ·Q 𝑦))
115	111, 113, 42, 45, 114	caovdir 6766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((⟨𝑧, 1𝑜⟩ +Q 1Q) ·Q 𝑏) = ((⟨𝑧, 1𝑜⟩ ·Q 𝑏) +Q (1Q ·Q 𝑏))
116	115	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → ((⟨𝑧, 1𝑜⟩ +Q 1Q) ·Q 𝑏) = ((⟨𝑧, 1𝑜⟩ ·Q 𝑏) +Q (1Q ·Q 𝑏)))
117		addpqnq 9639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((⟨𝑧, 1𝑜⟩ ∈ Q ∧ 1Q ∈ Q) → (⟨𝑧, 1𝑜⟩ +Q 1Q) = ([Q]‘(⟨𝑧, 1𝑜⟩ +pQ 1Q)))
118	61, 112, 117	sylancl 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 ∈ N → (⟨𝑧, 1𝑜⟩ +Q 1Q) = ([Q]‘(⟨𝑧, 1𝑜⟩ +pQ 1Q)))
119	79	oveq2i 6560	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (⟨𝑧, 1𝑜⟩ +pQ 1Q) = (⟨𝑧, 1𝑜⟩ +pQ ⟨1𝑜, 1𝑜⟩)
120		1pi 9584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ 1𝑜 ∈ N
121		addpipq 9638	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑧 ∈ 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 717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑧 ∈ N ∧ 1𝑜 ∈ N) → (⟨𝑧, 1𝑜⟩ +pQ ⟨1𝑜, 1𝑜⟩) = ⟨((𝑧 ·N 1𝑜) +N (1𝑜 ·N 1𝑜)), (1𝑜 ·N 1𝑜)⟩)
123	120, 122	mpan2 703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑧 ∈ N → (⟨𝑧, 1𝑜⟩ +pQ ⟨1𝑜, 1𝑜⟩) = ⟨((𝑧 ·N 1𝑜) +N (1𝑜 ·N 1𝑜)), (1𝑜 ·N 1𝑜)⟩)
124	119, 123	syl5eq 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧 ∈ N → (⟨𝑧, 1𝑜⟩ +pQ 1Q) = ⟨((𝑧 ·N 1𝑜) +N (1𝑜 ·N 1𝑜)), (1𝑜 ·N 1𝑜)⟩)
125		mulidpi 9587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑧 ∈ N → (𝑧 ·N 1𝑜) = 𝑧)
126		mulidpi 9587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (1𝑜 ∈ N → (1𝑜 ·N 1𝑜) = 1𝑜)
127	120, 126	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑧 ∈ N → (1𝑜 ·N 1𝑜) = 1𝑜)
128	125, 127	oveq12d 6567	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑧 ∈ N → ((𝑧 ·N 1𝑜) +N (1𝑜 ·N 1𝑜)) = (𝑧 +N 1𝑜))
129	128, 127	opeq12d 4348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧 ∈ N → ⟨((𝑧 ·N 1𝑜) +N (1𝑜 ·N 1𝑜)), (1𝑜 ·N 1𝑜)⟩ = ⟨(𝑧 +N 1𝑜), 1𝑜⟩)
130	124, 129	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 ∈ N → (⟨𝑧, 1𝑜⟩ +pQ 1Q) = ⟨(𝑧 +N 1𝑜), 1𝑜⟩)
131	130	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 ∈ N → ([Q]‘(⟨𝑧, 1𝑜⟩ +pQ 1Q)) = ([Q]‘⟨(𝑧 +N 1𝑜), 1𝑜⟩))
132		addclpi 9593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑧 ∈ N ∧ 1𝑜 ∈ N) → (𝑧 +N 1𝑜) ∈ N)
133	120, 132	mpan2 703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 ∈ N → (𝑧 +N 1𝑜) ∈ N)
134		pinq 9628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑧 +N 1𝑜) ∈ N → ⟨(𝑧 +N 1𝑜), 1𝑜⟩ ∈ Q)
135		nqerid 9634	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (⟨(𝑧 +N 1𝑜), 1𝑜⟩ ∈ Q → ([Q]‘⟨(𝑧 +N 1𝑜), 1𝑜⟩) = ⟨(𝑧 +N 1𝑜), 1𝑜⟩)
136	133, 134, 135	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 ∈ N → ([Q]‘⟨(𝑧 +N 1𝑜), 1𝑜⟩) = ⟨(𝑧 +N 1𝑜), 1𝑜⟩)
137	118, 131, 136	3eqtrd 2648	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧 ∈ N → (⟨𝑧, 1𝑜⟩ +Q 1Q) = ⟨(𝑧 +N 1𝑜), 1𝑜⟩)
138	137	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → (⟨𝑧, 1𝑜⟩ +Q 1Q) = ⟨(𝑧 +N 1𝑜), 1𝑜⟩)
139	138	oveq1d 6564	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → ((⟨𝑧, 1𝑜⟩ +Q 1Q) ·Q 𝑏) = (⟨(𝑧 +N 1𝑜), 1𝑜⟩ ·Q 𝑏))
140	97	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → (1Q ·Q 𝑏) = 𝑏)
141	140	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → ((⟨𝑧, 1𝑜⟩ ·Q 𝑏) +Q (1Q ·Q 𝑏)) = ((⟨𝑧, 1𝑜⟩ ·Q 𝑏) +Q 𝑏))
142	116, 139, 141	3eqtr3rd 2653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → ((⟨𝑧, 1𝑜⟩ ·Q 𝑏) +Q 𝑏) = (⟨(𝑧 +N 1𝑜), 1𝑜⟩ ·Q 𝑏))
143	142	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → (𝑦 +Q ((⟨𝑧, 1𝑜⟩ ·Q 𝑏) +Q 𝑏)) = (𝑦 +Q (⟨(𝑧 +N 1𝑜), 1𝑜⟩ ·Q 𝑏)))
144	110, 143	syl5eq 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → ((𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) +Q 𝑏) = (𝑦 +Q (⟨(𝑧 +N 1𝑜), 1𝑜⟩ ·Q 𝑏)))
145	144	eleq1d 2672	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → (((𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) +Q 𝑏) ∈ 𝐴 ↔ (𝑦 +Q (⟨(𝑧 +N 1𝑜), 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴))
146	109, 145	syl5ib 233	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → ((∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴) → (𝑦 +Q (⟨(𝑧 +N 1𝑜), 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴))
147	146	expd 451	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → (∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 → ((𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴 → (𝑦 +Q (⟨(𝑧 +N 1𝑜), 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴)))
148	147	expimpd 627	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ N → ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) → ((𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴 → (𝑦 +Q (⟨(𝑧 +N 1𝑜), 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴)))
149	106, 148	syl5 33	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ N → ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴 → (𝑦 +Q (⟨(𝑧 +N 1𝑜), 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴)))
150	149	a2d 29	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ N → (((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴) → ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q (⟨(𝑧 +N 1𝑜), 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴)))
151	84, 89, 94, 89, 105, 150	indpi 9608	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ N → ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴))
152	151	imp 444	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ N ∧ (𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴)
153	60, 38, 77, 66, 152	syl13anc 1320	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·Q (*Q‘𝑏)) <Q ⟨𝑧, 1𝑜⟩)) → (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴)
154		prcdnq 9694	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ P ∧ (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) ∈ 𝐴) → (𝑤 <Q (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) → 𝑤 ∈ 𝐴))
155	65, 153, 154	syl2anc 691	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·Q (*Q‘𝑏)) <Q ⟨𝑧, 1𝑜⟩)) → (𝑤 <Q (𝑦 +Q (⟨𝑧, 1𝑜⟩ ·Q 𝑏)) → 𝑤 ∈ 𝐴))
156	76, 155	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·Q (*Q‘𝑏)) <Q ⟨𝑧, 1𝑜⟩)) → 𝑤 ∈ 𝐴)
157	37, 156	rexlimddv 3017	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) → 𝑤 ∈ 𝐴)
158	157	expr 641	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ 𝑤 ∈ Q) → (𝑦 ∈ 𝐴 → 𝑤 ∈ 𝐴))
159	158	exlimdv 1848	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ 𝑤 ∈ Q) → (∃𝑦 𝑦 ∈ 𝐴 → 𝑤 ∈ 𝐴))
160	29, 159	mpd 15	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) ∧ 𝑤 ∈ Q) → 𝑤 ∈ 𝐴)
161	160	ex 449	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) → (𝑤 ∈ Q → 𝑤 ∈ 𝐴))
162	161	ssrdv 3574	. . . . . . . . . 10 ⊢ ((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) → Q ⊆ 𝐴)
163	25, 162	eqssd 3585	. . . . . . . . 9 ⊢ ((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴) → 𝐴 = Q)
164	163	3expia 1259	. . . . . . . 8 ⊢ ((𝐴 ∈ P ∧ 𝑏 ∈ Q) → (∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴 → 𝐴 = Q))
165	24, 164	mtod 188	. . . . . . 7 ⊢ ((𝐴 ∈ P ∧ 𝑏 ∈ Q) → ¬ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴)
166	165	expcom 450	. . . . . 6 ⊢ (𝑏 ∈ Q → (𝐴 ∈ P → ¬ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝑏) ∈ 𝐴))
167	20, 166	vtoclga 3245	. . . . 5 ⊢ (𝐵 ∈ Q → (𝐴 ∈ P → ¬ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴))
168	167	com12 32	. . . 4 ⊢ (𝐴 ∈ P → (𝐵 ∈ Q → ¬ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴))
169	4, 15, 168	3syld 58	. . 3 ⊢ (𝐴 ∈ P → (∀𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴 → ¬ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴))
170	169	pm2.01d 180	. 2 ⊢ (𝐴 ∈ P → ¬ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴)
171		rexnal 2978	. 2 ⊢ (∃𝑥 ∈ 𝐴 ¬ (𝑥 +Q 𝐵) ∈ 𝐴 ↔ ¬ ∀𝑥 ∈ 𝐴 (𝑥 +Q 𝐵) ∈ 𝐴)
172	170, 171	sylibr 223	1 ⊢ (𝐴 ∈ P → ∃𝑥 ∈ 𝐴 ¬ (𝑥 +Q 𝐵) ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ⊆ wss 3540   ⊊ wpss 3541  ∅c0 3874  ⟨cop 4131   class class class wbr 4583   × cxp 5036  ‘cfv 5804  (class class class)co 6549  1_𝑜c1o 7440  Ncnpi 9545   +_N cpli 9546   ·_N cmi 9547   +_pQ cplpq 9549  Qcnq 9553  1_Qc1q 9554  [Q]cerq 9555   +_Q cplq 9556   ·_Q cmq 9557  *_Qcrq 9558   <_Q cltq 9559  Pcnp 9560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-omul 7452  df-er 7629  df-ni 9573  df-pli 9574  df-mi 9575  df-lti 9576  df-plpq 9609  df-mpq 9610  df-ltpq 9611  df-enq 9612  df-nq 9613  df-erq 9614  df-plq 9615  df-mq 9616  df-1nq 9617  df-rq 9618  df-ltnq 9619  df-np 9682

This theorem is referenced by:  ltaddpr  9735  ltexprlem7  9743  prlem936  9748