1idpr

Description: 1 is an identity element for positive real multiplication. Theorem 9-3.7(iv) of Gleason p. 124. (Contributed by NM, 2-Apr-1996) (New usage is discouraged.)

		Ref	Expression
	Assertion	1idpr	$⊢ A \in 𝑷 \to A \cdot_{𝑷} 1_{𝑷} = A$

Proof

Step	Hyp	Ref	Expression
1		df-rex	$⊢ \exists g \in 1_{𝑷} x = f \cdot_{𝑸} g \leftrightarrow \exists g (g \in 1_{𝑷} \land x = f \cdot_{𝑸} g)$
2		elprnq	$⊢ (A \in 𝑷 \land f \in A) \to f \in 𝑸$
3		breq1	$⊢ x = f \cdot_{𝑸} g \to (x <_{𝑸} f \leftrightarrow (f \cdot_{𝑸} g) <_{𝑸} f)$
4		df-1p	$⊢ 1_{𝑷} = \{g \| g <_{𝑸} 1_{𝑸}\}$
5	4	abeq2i	$⊢ g \in 1_{𝑷} \leftrightarrow g <_{𝑸} 1_{𝑸}$
6		ltmnq	$⊢ f \in 𝑸 \to (g <_{𝑸} 1_{𝑸} \leftrightarrow (f \cdot_{𝑸} g) <_{𝑸} (f \cdot_{𝑸} 1_{𝑸}))$
7		mulidnq	$⊢ f \in 𝑸 \to f \cdot_{𝑸} 1_{𝑸} = f$
8	7	breq2d	$⊢ f \in 𝑸 \to ((f \cdot_{𝑸} g) <_{𝑸} (f \cdot_{𝑸} 1_{𝑸}) \leftrightarrow (f \cdot_{𝑸} g) <_{𝑸} f)$
9	6 8	bitrd	$⊢ f \in 𝑸 \to (g <_{𝑸} 1_{𝑸} \leftrightarrow (f \cdot_{𝑸} g) <_{𝑸} f)$
10	5 9	syl5rbb	$⊢ f \in 𝑸 \to ((f \cdot_{𝑸} g) <_{𝑸} f \leftrightarrow g \in 1_{𝑷})$
11	3 10	sylan9bbr	$⊢ (f \in 𝑸 \land x = f \cdot_{𝑸} g) \to (x <_{𝑸} f \leftrightarrow g \in 1_{𝑷})$
12	2 11	sylan	$⊢ ((A \in 𝑷 \land f \in A) \land x = f \cdot_{𝑸} g) \to (x <_{𝑸} f \leftrightarrow g \in 1_{𝑷})$
13	12	ex	$⊢ (A \in 𝑷 \land f \in A) \to (x = f \cdot_{𝑸} g \to (x <_{𝑸} f \leftrightarrow g \in 1_{𝑷}))$
14	13	pm5.32rd	$⊢ (A \in 𝑷 \land f \in A) \to ((x <_{𝑸} f \land x = f \cdot_{𝑸} g) \leftrightarrow (g \in 1_{𝑷} \land x = f \cdot_{𝑸} g))$
15	14	exbidv	$⊢ (A \in 𝑷 \land f \in A) \to (\exists g (x <_{𝑸} f \land x = f \cdot_{𝑸} g) \leftrightarrow \exists g (g \in 1_{𝑷} \land x = f \cdot_{𝑸} g))$
16		19.42v	$⊢ \exists g (x <_{𝑸} f \land x = f \cdot_{𝑸} g) \leftrightarrow (x <_{𝑸} f \land \exists g x = f \cdot_{𝑸} g)$
17	15 16	bitr3di	$⊢ (A \in 𝑷 \land f \in A) \to (\exists g (g \in 1_{𝑷} \land x = f \cdot_{𝑸} g) \leftrightarrow (x <_{𝑸} f \land \exists g x = f \cdot_{𝑸} g))$
18	1 17	syl5bb	$⊢ (A \in 𝑷 \land f \in A) \to (\exists g \in 1_{𝑷} x = f \cdot_{𝑸} g \leftrightarrow (x <_{𝑸} f \land \exists g x = f \cdot_{𝑸} g))$
19	18	rexbidva	$⊢ A \in 𝑷 \to (\exists f \in A \exists g \in 1_{𝑷} x = f \cdot_{𝑸} g \leftrightarrow \exists f \in A (x <_{𝑸} f \land \exists g x = f \cdot_{𝑸} g))$
20		1pr	$⊢ 1_{𝑷} \in 𝑷$
21		df-mp	$⊢ \cdot_{𝑷} = (y \in 𝑷, z \in 𝑷 ⟼ \{w \| \exists u \in y \exists v \in z w = u \cdot_{𝑸} v\})$
22		mulclnq	$⊢ (u \in 𝑸 \land v \in 𝑸) \to u \cdot_{𝑸} v \in 𝑸$
23	21 22	genpelv	$⊢ (A \in 𝑷 \land 1_{𝑷} \in 𝑷) \to (x \in (A \cdot_{𝑷} 1_{𝑷}) \leftrightarrow \exists f \in A \exists g \in 1_{𝑷} x = f \cdot_{𝑸} g)$
24	20 23	mpan2	$⊢ A \in 𝑷 \to (x \in (A \cdot_{𝑷} 1_{𝑷}) \leftrightarrow \exists f \in A \exists g \in 1_{𝑷} x = f \cdot_{𝑸} g)$
25		prnmax	$⊢ (A \in 𝑷 \land x \in A) \to \exists f \in A x <_{𝑸} f$
26		ltrelnq	$⊢ <_{𝑸} \subseteq 𝑸 \times 𝑸$
27	26	brel	$⊢ x <_{𝑸} f \to (x \in 𝑸 \land f \in 𝑸)$
28		vex	$⊢ f \in V$
29		vex	$⊢ x \in V$
30		fvex	$⊢ *_{𝑸} (f) \in V$
31		mulcomnq	$⊢ y \cdot_{𝑸} z = z \cdot_{𝑸} y$
32		mulassnq	$⊢ (y \cdot_{𝑸} z) \cdot_{𝑸} w = y \cdot_{𝑸} (z \cdot_{𝑸} w)$
33	28 29 30 31 32	caov12	$⊢ f \cdot_{𝑸} (x \cdot_{𝑸} _{𝑸} (f)) = x \cdot_{𝑸} (f \cdot_{𝑸} _{𝑸} (f))$
34		recidnq	$⊢ f \in 𝑸 \to f \cdot_{𝑸} *_{𝑸} (f) = 1_{𝑸}$
35	34	oveq2d	$⊢ f \in 𝑸 \to x \cdot_{𝑸} (f \cdot_{𝑸} *_{𝑸} (f)) = x \cdot_{𝑸} 1_{𝑸}$
36	33 35	syl5eq	$⊢ f \in 𝑸 \to f \cdot_{𝑸} (x \cdot_{𝑸} *_{𝑸} (f)) = x \cdot_{𝑸} 1_{𝑸}$
37		mulidnq	$⊢ x \in 𝑸 \to x \cdot_{𝑸} 1_{𝑸} = x$
38	36 37	sylan9eqr	$⊢ (x \in 𝑸 \land f \in 𝑸) \to f \cdot_{𝑸} (x \cdot_{𝑸} *_{𝑸} (f)) = x$
39	38	eqcomd	$⊢ (x \in 𝑸 \land f \in 𝑸) \to x = f \cdot_{𝑸} (x \cdot_{𝑸} *_{𝑸} (f))$
40		ovex	$⊢ x \cdot_{𝑸} *_{𝑸} (f) \in V$
41		oveq2	$⊢ g = x \cdot_{𝑸} _{𝑸} (f) \to f \cdot_{𝑸} g = f \cdot_{𝑸} (x \cdot_{𝑸} _{𝑸} (f))$
42	41	eqeq2d	$⊢ g = x \cdot_{𝑸} _{𝑸} (f) \to (x = f \cdot_{𝑸} g \leftrightarrow x = f \cdot_{𝑸} (x \cdot_{𝑸} _{𝑸} (f)))$
43	40 42	spcev	$⊢ x = f \cdot_{𝑸} (x \cdot_{𝑸} *_{𝑸} (f)) \to \exists g x = f \cdot_{𝑸} g$
44	27 39 43	3syl	$⊢ x <_{𝑸} f \to \exists g x = f \cdot_{𝑸} g$
45	44	a1i	$⊢ f \in A \to (x <_{𝑸} f \to \exists g x = f \cdot_{𝑸} g)$
46	45	ancld	$⊢ f \in A \to (x <_{𝑸} f \to (x <_{𝑸} f \land \exists g x = f \cdot_{𝑸} g))$
47	46	reximia	$⊢ \exists f \in A x <_{𝑸} f \to \exists f \in A (x <_{𝑸} f \land \exists g x = f \cdot_{𝑸} g)$
48	25 47	syl	$⊢ (A \in 𝑷 \land x \in A) \to \exists f \in A (x <_{𝑸} f \land \exists g x = f \cdot_{𝑸} g)$
49	48	ex	$⊢ A \in 𝑷 \to (x \in A \to \exists f \in A (x <_{𝑸} f \land \exists g x = f \cdot_{𝑸} g))$
50		prcdnq	$⊢ (A \in 𝑷 \land f \in A) \to (x <_{𝑸} f \to x \in A)$
51	50	adantrd	$⊢ (A \in 𝑷 \land f \in A) \to ((x <_{𝑸} f \land \exists g x = f \cdot_{𝑸} g) \to x \in A)$
52	51	rexlimdva	$⊢ A \in 𝑷 \to (\exists f \in A (x <_{𝑸} f \land \exists g x = f \cdot_{𝑸} g) \to x \in A)$
53	49 52	impbid	$⊢ A \in 𝑷 \to (x \in A \leftrightarrow \exists f \in A (x <_{𝑸} f \land \exists g x = f \cdot_{𝑸} g))$
54	19 24 53	3bitr4d	$⊢ A \in 𝑷 \to (x \in (A \cdot_{𝑷} 1_{𝑷}) \leftrightarrow x \in A)$
55	54	eqrdv	$⊢ A \in 𝑷 \to A \cdot_{𝑷} 1_{𝑷} = A$

Metamath Proof Explorer

Theorem 1idpr

Proof