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	$⊢ B \in V$
	Assertion	prlem934	$⊢ A \in 𝑷 \to \exists x \in A \neg x +_{𝑸} B \in A$

Proof

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

Metamath Proof Explorer

Theorem prlem934

Proof