prlem936

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

		Ref	Expression
	Assertion	prlem936	$⊢ (A \in 𝑷 \land 1_{𝑸} <_{𝑸} B) \to \exists x \in A \neg x \cdot_{𝑸} B \in A$

Proof

Step	Hyp	Ref	Expression
1		ltrelnq	$⊢ <_{𝑸} \subseteq 𝑸 \times 𝑸$
2	1	brel	$⊢ 1_{𝑸} <_{𝑸} B \to (1_{𝑸} \in 𝑸 \land B \in 𝑸)$
3	2	simprd	$⊢ 1_{𝑸} <_{𝑸} B \to B \in 𝑸$
4	3	adantl	$⊢ (A \in 𝑷 \land 1_{𝑸} <_{𝑸} B) \to B \in 𝑸$
5		breq2	$⊢ b = B \to (1_{𝑸} <_{𝑸} b \leftrightarrow 1_{𝑸} <_{𝑸} B)$
6	5	anbi2d	$⊢ b = B \to ((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \leftrightarrow (A \in 𝑷 \land 1_{𝑸} <_{𝑸} B))$
7		oveq2	$⊢ b = B \to x \cdot_{𝑸} b = x \cdot_{𝑸} B$
8	7	eleq1d	$⊢ b = B \to (x \cdot_{𝑸} b \in A \leftrightarrow x \cdot_{𝑸} B \in A)$
9	8	notbid	$⊢ b = B \to (\neg x \cdot_{𝑸} b \in A \leftrightarrow \neg x \cdot_{𝑸} B \in A)$
10	9	rexbidv	$⊢ b = B \to (\exists x \in A \neg x \cdot_{𝑸} b \in A \leftrightarrow \exists x \in A \neg x \cdot_{𝑸} B \in A)$
11	6 10	imbi12d	$⊢ b = B \to (((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \to \exists x \in A \neg x \cdot_{𝑸} b \in A) \leftrightarrow ((A \in 𝑷 \land 1_{𝑸} <_{𝑸} B) \to \exists x \in A \neg x \cdot_{𝑸} B \in A))$
12		prn0	$⊢ A \in 𝑷 \to A \neq \emptyset$
13		n0	$⊢ A \neq \emptyset \leftrightarrow \exists y y \in A$
14	12 13	sylib	$⊢ A \in 𝑷 \to \exists y y \in A$
15	14	adantr	$⊢ (A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \to \exists y y \in A$
16		elprnq	$⊢ (A \in 𝑷 \land y \in A) \to y \in 𝑸$
17	16	ad2ant2r	$⊢ ((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \to y \in 𝑸$
18		mulidnq	$⊢ y \in 𝑸 \to y \cdot_{𝑸} 1_{𝑸} = y$
19	17 18	syl	$⊢ ((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \to y \cdot_{𝑸} 1_{𝑸} = y$
20		simplr	$⊢ ((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \to 1_{𝑸} <_{𝑸} b$
21		ltmnq	$⊢ y \in 𝑸 \to (1_{𝑸} <_{𝑸} b \leftrightarrow (y \cdot_{𝑸} 1_{𝑸}) <_{𝑸} (y \cdot_{𝑸} b))$
22	21	biimpa	$⊢ (y \in 𝑸 \land 1_{𝑸} <_{𝑸} b) \to (y \cdot_{𝑸} 1_{𝑸}) <_{𝑸} (y \cdot_{𝑸} b)$
23	17 20 22	syl2anc	$⊢ ((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \to (y \cdot_{𝑸} 1_{𝑸}) <_{𝑸} (y \cdot_{𝑸} b)$
24	19 23	eqbrtrrd	$⊢ ((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \to y <_{𝑸} (y \cdot_{𝑸} b)$
25	1	brel	$⊢ 1_{𝑸} <_{𝑸} b \to (1_{𝑸} \in 𝑸 \land b \in 𝑸)$
26	25	simprd	$⊢ 1_{𝑸} <_{𝑸} b \to b \in 𝑸$
27	26	ad2antlr	$⊢ ((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \to b \in 𝑸$
28		mulclnq	$⊢ (y \in 𝑸 \land b \in 𝑸) \to y \cdot_{𝑸} b \in 𝑸$
29	17 27 28	syl2anc	$⊢ ((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \to y \cdot_{𝑸} b \in 𝑸$
30		ltexnq	$⊢ y \cdot_{𝑸} b \in 𝑸 \to (y <_{𝑸} (y \cdot_{𝑸} b) \leftrightarrow \exists z y +_{𝑸} z = y \cdot_{𝑸} b)$
31	29 30	syl	$⊢ ((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \to (y <_{𝑸} (y \cdot_{𝑸} b) \leftrightarrow \exists z y +_{𝑸} z = y \cdot_{𝑸} b)$
32	24 31	mpbid	$⊢ ((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \to \exists z y +_{𝑸} z = y \cdot_{𝑸} b$
33		simplll	$⊢ (((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \land y +_{𝑸} z = y \cdot_{𝑸} b) \to A \in 𝑷$
34		vex	$⊢ z \in V$
35	34	prlem934	$⊢ A \in 𝑷 \to \exists x \in A \neg x +_{𝑸} z \in A$
36	33 35	syl	$⊢ (((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \land y +_{𝑸} z = y \cdot_{𝑸} b) \to \exists x \in A \neg x +_{𝑸} z \in A$
37	33	adantr	$⊢ ((((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \land y +_{𝑸} z = y \cdot_{𝑸} b) \land x \in A) \to A \in 𝑷$
38		simprr	$⊢ ((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \to y \cdot_{𝑸} b \in A$
39		eleq1	$⊢ y +_{𝑸} z = y \cdot_{𝑸} b \to (y +_{𝑸} z \in A \leftrightarrow y \cdot_{𝑸} b \in A)$
40	39	biimparc	$⊢ (y \cdot_{𝑸} b \in A \land y +_{𝑸} z = y \cdot_{𝑸} b) \to y +_{𝑸} z \in A$
41	38 40	sylan	$⊢ (((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \land y +_{𝑸} z = y \cdot_{𝑸} b) \to y +_{𝑸} z \in A$
42	41	adantr	$⊢ ((((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \land y +_{𝑸} z = y \cdot_{𝑸} b) \land x \in A) \to y +_{𝑸} z \in A$
43		elprnq	$⊢ (A \in 𝑷 \land x \in A) \to x \in 𝑸$
44	33 43	sylan	$⊢ ((((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \land y +_{𝑸} z = y \cdot_{𝑸} b) \land x \in A) \to x \in 𝑸$
45		elprnq	$⊢ (A \in 𝑷 \land y +_{𝑸} z \in A) \to y +_{𝑸} z \in 𝑸$
46		addnqf	$⊢ +_{𝑸} : 𝑸 \times 𝑸 ⟶ 𝑸$
47	46	fdmi	$⊢ dom +_{𝑸} = 𝑸 \times 𝑸$
48		0nnq	$⊢ \neg \emptyset \in 𝑸$
49	47 48	ndmovrcl	$⊢ y +_{𝑸} z \in 𝑸 \to (y \in 𝑸 \land z \in 𝑸)$
50	49	simprd	$⊢ y +_{𝑸} z \in 𝑸 \to z \in 𝑸$
51	45 50	syl	$⊢ (A \in 𝑷 \land y +_{𝑸} z \in A) \to z \in 𝑸$
52	33 41 51	syl2anc	$⊢ (((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \land y +_{𝑸} z = y \cdot_{𝑸} b) \to z \in 𝑸$
53	52	adantr	$⊢ ((((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \land y +_{𝑸} z = y \cdot_{𝑸} b) \land x \in A) \to z \in 𝑸$
54		addclnq	$⊢ (x \in 𝑸 \land z \in 𝑸) \to x +_{𝑸} z \in 𝑸$
55	44 53 54	syl2anc	$⊢ ((((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \land y +_{𝑸} z = y \cdot_{𝑸} b) \land x \in A) \to x +_{𝑸} z \in 𝑸$
56		prub	$⊢ ((A \in 𝑷 \land y +_{𝑸} z \in A) \land x +_{𝑸} z \in 𝑸) \to (\neg x +_{𝑸} z \in A \to (y +_{𝑸} z) <_{𝑸} (x +_{𝑸} z))$
57	37 42 55 56	syl21anc	$⊢ ((((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \land y +_{𝑸} z = y \cdot_{𝑸} b) \land x \in A) \to (\neg x +_{𝑸} z \in A \to (y +_{𝑸} z) <_{𝑸} (x +_{𝑸} z))$
58	27	ad2antrr	$⊢ ((((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \land y +_{𝑸} z = y \cdot_{𝑸} b) \land x \in A) \to b \in 𝑸$
59		mulclnq	$⊢ (x \in 𝑸 \land b \in 𝑸) \to x \cdot_{𝑸} b \in 𝑸$
60	44 58 59	syl2anc	$⊢ ((((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \land y +_{𝑸} z = y \cdot_{𝑸} b) \land x \in A) \to x \cdot_{𝑸} b \in 𝑸$
61	17	ad2antrr	$⊢ ((((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \land y +_{𝑸} z = y \cdot_{𝑸} b) \land x \in A) \to y \in 𝑸$
62		simplr	$⊢ ((((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \land y +_{𝑸} z = y \cdot_{𝑸} b) \land x \in A) \to y +_{𝑸} z = y \cdot_{𝑸} b$
63		recclnq	$⊢ y \in 𝑸 \to *_{𝑸} (y) \in 𝑸$
64		mulclnq	$⊢ (z \in 𝑸 \land _{𝑸} (y) \in 𝑸) \to z \cdot_{𝑸} _{𝑸} (y) \in 𝑸$
65	63 64	sylan2	$⊢ (z \in 𝑸 \land y \in 𝑸) \to z \cdot_{𝑸} *_{𝑸} (y) \in 𝑸$
66	65	ancoms	$⊢ (y \in 𝑸 \land z \in 𝑸) \to z \cdot_{𝑸} *_{𝑸} (y) \in 𝑸$
67		ltmnq	$⊢ z \cdot_{𝑸} _{𝑸} (y) \in 𝑸 \to (y <_{𝑸} x \leftrightarrow ((z \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} y) <_{𝑸} ((z \cdot_{𝑸} *_{𝑸} (y)) \cdot_{𝑸} x))$
68	66 67	syl	$⊢ (y \in 𝑸 \land z \in 𝑸) \to (y <_{𝑸} x \leftrightarrow ((z \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} y) <_{𝑸} ((z \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} x))$
69		mulassnq	$⊢ (z \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} y = z \cdot_{𝑸} (_{𝑸} (y) \cdot_{𝑸} y)$
70		mulcomnq	$⊢ _{𝑸} (y) \cdot_{𝑸} y = y \cdot_{𝑸} _{𝑸} (y)$
71	70	oveq2i	$⊢ z \cdot_{𝑸} (_{𝑸} (y) \cdot_{𝑸} y) = z \cdot_{𝑸} (y \cdot_{𝑸} _{𝑸} (y))$
72	69 71	eqtri	$⊢ (z \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} y = z \cdot_{𝑸} (y \cdot_{𝑸} _{𝑸} (y))$
73		recidnq	$⊢ y \in 𝑸 \to y \cdot_{𝑸} *_{𝑸} (y) = 1_{𝑸}$
74	73	oveq2d	$⊢ y \in 𝑸 \to z \cdot_{𝑸} (y \cdot_{𝑸} *_{𝑸} (y)) = z \cdot_{𝑸} 1_{𝑸}$
75		mulidnq	$⊢ z \in 𝑸 \to z \cdot_{𝑸} 1_{𝑸} = z$
76	74 75	sylan9eq	$⊢ (y \in 𝑸 \land z \in 𝑸) \to z \cdot_{𝑸} (y \cdot_{𝑸} *_{𝑸} (y)) = z$
77	72 76	syl5eq	$⊢ (y \in 𝑸 \land z \in 𝑸) \to (z \cdot_{𝑸} *_{𝑸} (y)) \cdot_{𝑸} y = z$
78	77	breq1d	$⊢ (y \in 𝑸 \land z \in 𝑸) \to (((z \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} y) <_{𝑸} ((z \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} x) \leftrightarrow z <_{𝑸} ((z \cdot_{𝑸} *_{𝑸} (y)) \cdot_{𝑸} x))$
79	68 78	bitrd	$⊢ (y \in 𝑸 \land z \in 𝑸) \to (y <_{𝑸} x \leftrightarrow z <_{𝑸} ((z \cdot_{𝑸} *_{𝑸} (y)) \cdot_{𝑸} x))$
80	79	adantll	$⊢ ((x \cdot_{𝑸} b \in 𝑸 \land y \in 𝑸) \land z \in 𝑸) \to (y <_{𝑸} x \leftrightarrow z <_{𝑸} ((z \cdot_{𝑸} *_{𝑸} (y)) \cdot_{𝑸} x))$
81		mulnqf	$⊢ \cdot_{𝑸} : 𝑸 \times 𝑸 ⟶ 𝑸$
82	81	fdmi	$⊢ dom \cdot_{𝑸} = 𝑸 \times 𝑸$
83	82 48	ndmovrcl	$⊢ x \cdot_{𝑸} b \in 𝑸 \to (x \in 𝑸 \land b \in 𝑸)$
84	83	simpld	$⊢ x \cdot_{𝑸} b \in 𝑸 \to x \in 𝑸$
85		ltanq	$⊢ x \in 𝑸 \to (z <_{𝑸} ((z \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} x) \leftrightarrow (x +_{𝑸} z) <_{𝑸} (x +_{𝑸} ((z \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} x)))$
86	84 85	syl	$⊢ x \cdot_{𝑸} b \in 𝑸 \to (z <_{𝑸} ((z \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} x) \leftrightarrow (x +_{𝑸} z) <_{𝑸} (x +_{𝑸} ((z \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} x)))$
87	86	adantr	$⊢ (x \cdot_{𝑸} b \in 𝑸 \land y \in 𝑸) \to (z <_{𝑸} ((z \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} x) \leftrightarrow (x +_{𝑸} z) <_{𝑸} (x +_{𝑸} ((z \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} x)))$
88		vex	$⊢ y \in V$
89		ovex	$⊢ x \cdot_{𝑸} *_{𝑸} (y) \in V$
90		mulcomnq	$⊢ u \cdot_{𝑸} w = w \cdot_{𝑸} u$
91		distrnq	$⊢ u \cdot_{𝑸} (w +_{𝑸} v) = (u \cdot_{𝑸} w) +_{𝑸} (u \cdot_{𝑸} v)$
92	88 34 89 90 91	caovdir	$⊢ (y +_{𝑸} z) \cdot_{𝑸} (x \cdot_{𝑸} _{𝑸} (y)) = (y \cdot_{𝑸} (x \cdot_{𝑸} _{𝑸} (y))) +_{𝑸} (z \cdot_{𝑸} (x \cdot_{𝑸} *_{𝑸} (y)))$
93		vex	$⊢ x \in V$
94		fvex	$⊢ *_{𝑸} (y) \in V$
95		mulassnq	$⊢ (u \cdot_{𝑸} w) \cdot_{𝑸} v = u \cdot_{𝑸} (w \cdot_{𝑸} v)$
96	88 93 94 90 95	caov12	$⊢ y \cdot_{𝑸} (x \cdot_{𝑸} _{𝑸} (y)) = x \cdot_{𝑸} (y \cdot_{𝑸} _{𝑸} (y))$
97	73	oveq2d	$⊢ y \in 𝑸 \to x \cdot_{𝑸} (y \cdot_{𝑸} *_{𝑸} (y)) = x \cdot_{𝑸} 1_{𝑸}$
98		mulidnq	$⊢ x \in 𝑸 \to x \cdot_{𝑸} 1_{𝑸} = x$
99	84 98	syl	$⊢ x \cdot_{𝑸} b \in 𝑸 \to x \cdot_{𝑸} 1_{𝑸} = x$
100	97 99	sylan9eqr	$⊢ (x \cdot_{𝑸} b \in 𝑸 \land y \in 𝑸) \to x \cdot_{𝑸} (y \cdot_{𝑸} *_{𝑸} (y)) = x$
101	96 100	syl5eq	$⊢ (x \cdot_{𝑸} b \in 𝑸 \land y \in 𝑸) \to y \cdot_{𝑸} (x \cdot_{𝑸} *_{𝑸} (y)) = x$
102		mulcomnq	$⊢ x \cdot_{𝑸} _{𝑸} (y) = _{𝑸} (y) \cdot_{𝑸} x$
103	102	oveq2i	$⊢ z \cdot_{𝑸} (x \cdot_{𝑸} _{𝑸} (y)) = z \cdot_{𝑸} (_{𝑸} (y) \cdot_{𝑸} x)$
104		mulassnq	$⊢ (z \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} x = z \cdot_{𝑸} (_{𝑸} (y) \cdot_{𝑸} x)$
105	103 104	eqtr4i	$⊢ z \cdot_{𝑸} (x \cdot_{𝑸} _{𝑸} (y)) = (z \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} x$
106	105	a1i	$⊢ (x \cdot_{𝑸} b \in 𝑸 \land y \in 𝑸) \to z \cdot_{𝑸} (x \cdot_{𝑸} _{𝑸} (y)) = (z \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} x$
107	101 106	oveq12d	$⊢ (x \cdot_{𝑸} b \in 𝑸 \land y \in 𝑸) \to (y \cdot_{𝑸} (x \cdot_{𝑸} _{𝑸} (y))) +_{𝑸} (z \cdot_{𝑸} (x \cdot_{𝑸} _{𝑸} (y))) = x +_{𝑸} ((z \cdot_{𝑸} *_{𝑸} (y)) \cdot_{𝑸} x)$
108	92 107	syl5eq	$⊢ (x \cdot_{𝑸} b \in 𝑸 \land y \in 𝑸) \to (y +_{𝑸} z) \cdot_{𝑸} (x \cdot_{𝑸} _{𝑸} (y)) = x +_{𝑸} ((z \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} x)$
109	108	breq2d	$⊢ (x \cdot_{𝑸} b \in 𝑸 \land y \in 𝑸) \to ((x +_{𝑸} z) <_{𝑸} ((y +_{𝑸} z) \cdot_{𝑸} (x \cdot_{𝑸} _{𝑸} (y))) \leftrightarrow (x +_{𝑸} z) <_{𝑸} (x +_{𝑸} ((z \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} x)))$
110	87 109	bitr4d	$⊢ (x \cdot_{𝑸} b \in 𝑸 \land y \in 𝑸) \to (z <_{𝑸} ((z \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} x) \leftrightarrow (x +_{𝑸} z) <_{𝑸} ((y +_{𝑸} z) \cdot_{𝑸} (x \cdot_{𝑸} _{𝑸} (y))))$
111	110	adantr	$⊢ ((x \cdot_{𝑸} b \in 𝑸 \land y \in 𝑸) \land z \in 𝑸) \to (z <_{𝑸} ((z \cdot_{𝑸} _{𝑸} (y)) \cdot_{𝑸} x) \leftrightarrow (x +_{𝑸} z) <_{𝑸} ((y +_{𝑸} z) \cdot_{𝑸} (x \cdot_{𝑸} _{𝑸} (y))))$
112	80 111	bitrd	$⊢ ((x \cdot_{𝑸} b \in 𝑸 \land y \in 𝑸) \land z \in 𝑸) \to (y <_{𝑸} x \leftrightarrow (x +_{𝑸} z) <_{𝑸} ((y +_{𝑸} z) \cdot_{𝑸} (x \cdot_{𝑸} *_{𝑸} (y))))$
113	112	adantrr	$⊢ ((x \cdot_{𝑸} b \in 𝑸 \land y \in 𝑸) \land (z \in 𝑸 \land y +_{𝑸} z = y \cdot_{𝑸} b)) \to (y <_{𝑸} x \leftrightarrow (x +_{𝑸} z) <_{𝑸} ((y +_{𝑸} z) \cdot_{𝑸} (x \cdot_{𝑸} *_{𝑸} (y))))$
114		ltanq	$⊢ z \in 𝑸 \to (y <_{𝑸} x \leftrightarrow (z +_{𝑸} y) <_{𝑸} (z +_{𝑸} x))$
115		addcomnq	$⊢ z +_{𝑸} y = y +_{𝑸} z$
116		addcomnq	$⊢ z +_{𝑸} x = x +_{𝑸} z$
117	115 116	breq12i	$⊢ (z +_{𝑸} y) <_{𝑸} (z +_{𝑸} x) \leftrightarrow (y +_{𝑸} z) <_{𝑸} (x +_{𝑸} z)$
118	114 117	syl6bb	$⊢ z \in 𝑸 \to (y <_{𝑸} x \leftrightarrow (y +_{𝑸} z) <_{𝑸} (x +_{𝑸} z))$
119	118	ad2antrl	$⊢ ((x \cdot_{𝑸} b \in 𝑸 \land y \in 𝑸) \land (z \in 𝑸 \land y +_{𝑸} z = y \cdot_{𝑸} b)) \to (y <_{𝑸} x \leftrightarrow (y +_{𝑸} z) <_{𝑸} (x +_{𝑸} z))$
120		oveq1	$⊢ y +_{𝑸} z = y \cdot_{𝑸} b \to (y +_{𝑸} z) \cdot_{𝑸} (x \cdot_{𝑸} _{𝑸} (y)) = (y \cdot_{𝑸} b) \cdot_{𝑸} (x \cdot_{𝑸} _{𝑸} (y))$
121		vex	$⊢ b \in V$
122	88 121 93 90 95 94	caov411	$⊢ (y \cdot_{𝑸} b) \cdot_{𝑸} (x \cdot_{𝑸} _{𝑸} (y)) = (x \cdot_{𝑸} b) \cdot_{𝑸} (y \cdot_{𝑸} _{𝑸} (y))$
123	73	oveq2d	$⊢ y \in 𝑸 \to (x \cdot_{𝑸} b) \cdot_{𝑸} (y \cdot_{𝑸} *_{𝑸} (y)) = (x \cdot_{𝑸} b) \cdot_{𝑸} 1_{𝑸}$
124		mulidnq	$⊢ x \cdot_{𝑸} b \in 𝑸 \to (x \cdot_{𝑸} b) \cdot_{𝑸} 1_{𝑸} = x \cdot_{𝑸} b$
125	123 124	sylan9eqr	$⊢ (x \cdot_{𝑸} b \in 𝑸 \land y \in 𝑸) \to (x \cdot_{𝑸} b) \cdot_{𝑸} (y \cdot_{𝑸} *_{𝑸} (y)) = x \cdot_{𝑸} b$
126	122 125	syl5eq	$⊢ (x \cdot_{𝑸} b \in 𝑸 \land y \in 𝑸) \to (y \cdot_{𝑸} b) \cdot_{𝑸} (x \cdot_{𝑸} *_{𝑸} (y)) = x \cdot_{𝑸} b$
127	120 126	sylan9eqr	$⊢ ((x \cdot_{𝑸} b \in 𝑸 \land y \in 𝑸) \land y +_{𝑸} z = y \cdot_{𝑸} b) \to (y +_{𝑸} z) \cdot_{𝑸} (x \cdot_{𝑸} *_{𝑸} (y)) = x \cdot_{𝑸} b$
128	127	breq2d	$⊢ ((x \cdot_{𝑸} b \in 𝑸 \land y \in 𝑸) \land y +_{𝑸} z = y \cdot_{𝑸} b) \to ((x +_{𝑸} z) <_{𝑸} ((y +_{𝑸} z) \cdot_{𝑸} (x \cdot_{𝑸} *_{𝑸} (y))) \leftrightarrow (x +_{𝑸} z) <_{𝑸} (x \cdot_{𝑸} b))$
129	128	adantrl	$⊢ ((x \cdot_{𝑸} b \in 𝑸 \land y \in 𝑸) \land (z \in 𝑸 \land y +_{𝑸} z = y \cdot_{𝑸} b)) \to ((x +_{𝑸} z) <_{𝑸} ((y +_{𝑸} z) \cdot_{𝑸} (x \cdot_{𝑸} *_{𝑸} (y))) \leftrightarrow (x +_{𝑸} z) <_{𝑸} (x \cdot_{𝑸} b))$
130	113 119 129	3bitr3d	$⊢ ((x \cdot_{𝑸} b \in 𝑸 \land y \in 𝑸) \land (z \in 𝑸 \land y +_{𝑸} z = y \cdot_{𝑸} b)) \to ((y +_{𝑸} z) <_{𝑸} (x +_{𝑸} z) \leftrightarrow (x +_{𝑸} z) <_{𝑸} (x \cdot_{𝑸} b))$
131	60 61 53 62 130	syl22anc	$⊢ ((((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \land y +_{𝑸} z = y \cdot_{𝑸} b) \land x \in A) \to ((y +_{𝑸} z) <_{𝑸} (x +_{𝑸} z) \leftrightarrow (x +_{𝑸} z) <_{𝑸} (x \cdot_{𝑸} b))$
132	57 131	sylibd	$⊢ ((((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \land y +_{𝑸} z = y \cdot_{𝑸} b) \land x \in A) \to (\neg x +_{𝑸} z \in A \to (x +_{𝑸} z) <_{𝑸} (x \cdot_{𝑸} b))$
133		prcdnq	$⊢ (A \in 𝑷 \land x \cdot_{𝑸} b \in A) \to ((x +_{𝑸} z) <_{𝑸} (x \cdot_{𝑸} b) \to x +_{𝑸} z \in A)$
134	133	impancom	$⊢ (A \in 𝑷 \land (x +_{𝑸} z) <_{𝑸} (x \cdot_{𝑸} b)) \to (x \cdot_{𝑸} b \in A \to x +_{𝑸} z \in A)$
135	134	con3d	$⊢ (A \in 𝑷 \land (x +_{𝑸} z) <_{𝑸} (x \cdot_{𝑸} b)) \to (\neg x +_{𝑸} z \in A \to \neg x \cdot_{𝑸} b \in A)$
136	135	ex	$⊢ A \in 𝑷 \to ((x +_{𝑸} z) <_{𝑸} (x \cdot_{𝑸} b) \to (\neg x +_{𝑸} z \in A \to \neg x \cdot_{𝑸} b \in A))$
137	136	com23	$⊢ A \in 𝑷 \to (\neg x +_{𝑸} z \in A \to ((x +_{𝑸} z) <_{𝑸} (x \cdot_{𝑸} b) \to \neg x \cdot_{𝑸} b \in A))$
138	37 137	syl	$⊢ ((((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \land y +_{𝑸} z = y \cdot_{𝑸} b) \land x \in A) \to (\neg x +_{𝑸} z \in A \to ((x +_{𝑸} z) <_{𝑸} (x \cdot_{𝑸} b) \to \neg x \cdot_{𝑸} b \in A))$
139	132 138	mpdd	$⊢ ((((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \land y +_{𝑸} z = y \cdot_{𝑸} b) \land x \in A) \to (\neg x +_{𝑸} z \in A \to \neg x \cdot_{𝑸} b \in A)$
140	139	reximdva	$⊢ (((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \land y +_{𝑸} z = y \cdot_{𝑸} b) \to (\exists x \in A \neg x +_{𝑸} z \in A \to \exists x \in A \neg x \cdot_{𝑸} b \in A)$
141	36 140	mpd	$⊢ (((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \land y +_{𝑸} z = y \cdot_{𝑸} b) \to \exists x \in A \neg x \cdot_{𝑸} b \in A$
142	32 141	exlimddv	$⊢ ((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land (y \in A \land y \cdot_{𝑸} b \in A)) \to \exists x \in A \neg x \cdot_{𝑸} b \in A$
143	142	expr	$⊢ ((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land y \in A) \to (y \cdot_{𝑸} b \in A \to \exists x \in A \neg x \cdot_{𝑸} b \in A)$
144		oveq1	$⊢ x = y \to x \cdot_{𝑸} b = y \cdot_{𝑸} b$
145	144	eleq1d	$⊢ x = y \to (x \cdot_{𝑸} b \in A \leftrightarrow y \cdot_{𝑸} b \in A)$
146	145	notbid	$⊢ x = y \to (\neg x \cdot_{𝑸} b \in A \leftrightarrow \neg y \cdot_{𝑸} b \in A)$
147	146	rspcev	$⊢ (y \in A \land \neg y \cdot_{𝑸} b \in A) \to \exists x \in A \neg x \cdot_{𝑸} b \in A$
148	147	ex	$⊢ y \in A \to (\neg y \cdot_{𝑸} b \in A \to \exists x \in A \neg x \cdot_{𝑸} b \in A)$
149	148	adantl	$⊢ ((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land y \in A) \to (\neg y \cdot_{𝑸} b \in A \to \exists x \in A \neg x \cdot_{𝑸} b \in A)$
150	143 149	pm2.61d	$⊢ ((A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \land y \in A) \to \exists x \in A \neg x \cdot_{𝑸} b \in A$
151	15 150	exlimddv	$⊢ (A \in 𝑷 \land 1_{𝑸} <_{𝑸} b) \to \exists x \in A \neg x \cdot_{𝑸} b \in A$
152	11 151	vtoclg	$⊢ B \in 𝑸 \to ((A \in 𝑷 \land 1_{𝑸} <_{𝑸} B) \to \exists x \in A \neg x \cdot_{𝑸} B \in A)$
153	4 152	mpcom	$⊢ (A \in 𝑷 \land 1_{𝑸} <_{𝑸} B) \to \exists x \in A \neg x \cdot_{𝑸} B \in A$

Metamath Proof Explorer

Theorem prlem936

Proof