Theorem 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	⊢ ( 𝐴 ∈ P → ( 𝐴 ·P 1P ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		df-rex	⊢ ( ∃ 𝑔 ∈ 1P 𝑥 = ( 𝑓 ·Q 𝑔 ) ↔ ∃ 𝑔 ( 𝑔 ∈ 1P ∧ 𝑥 = ( 𝑓 ·Q 𝑔 ) ) )
2		19.42v	⊢ ( ∃ 𝑔 ( 𝑥 <Q 𝑓 ∧ 𝑥 = ( 𝑓 ·Q 𝑔 ) ) ↔ ( 𝑥 <Q 𝑓 ∧ ∃ 𝑔 𝑥 = ( 𝑓 ·Q 𝑔 ) ) )
3		elprnq	⊢ ( ( 𝐴 ∈ P ∧ 𝑓 ∈ 𝐴 ) → 𝑓 ∈ Q )
4		breq1	⊢ ( 𝑥 = ( 𝑓 ·Q 𝑔 ) → ( 𝑥 <Q 𝑓 ↔ ( 𝑓 ·Q 𝑔 ) <Q 𝑓 ) )
5		df-1p	⊢ 1P = { 𝑔 ∣ 𝑔 <Q 1Q }
6	5	abeq2i	⊢ ( 𝑔 ∈ 1P ↔ 𝑔 <Q 1Q )
7		ltmnq	⊢ ( 𝑓 ∈ Q → ( 𝑔 <Q 1Q ↔ ( 𝑓 ·Q 𝑔 ) <Q ( 𝑓 ·Q 1Q ) ) )
8		mulidnq	⊢ ( 𝑓 ∈ Q → ( 𝑓 ·Q 1Q ) = 𝑓 )
9	8	breq2d	⊢ ( 𝑓 ∈ Q → ( ( 𝑓 ·Q 𝑔 ) <Q ( 𝑓 ·Q 1Q ) ↔ ( 𝑓 ·Q 𝑔 ) <Q 𝑓 ) )
10	7 9	bitrd	⊢ ( 𝑓 ∈ Q → ( 𝑔 <Q 1Q ↔ ( 𝑓 ·Q 𝑔 ) <Q 𝑓 ) )
11	6 10	syl5rbb	⊢ ( 𝑓 ∈ Q → ( ( 𝑓 ·Q 𝑔 ) <Q 𝑓 ↔ 𝑔 ∈ 1P ) )
12	4 11	sylan9bbr	⊢ ( ( 𝑓 ∈ Q ∧ 𝑥 = ( 𝑓 ·Q 𝑔 ) ) → ( 𝑥 <Q 𝑓 ↔ 𝑔 ∈ 1P ) )
13	3 12	sylan	⊢ ( ( ( 𝐴 ∈ P ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑥 = ( 𝑓 ·Q 𝑔 ) ) → ( 𝑥 <Q 𝑓 ↔ 𝑔 ∈ 1P ) )
14	13	ex	⊢ ( ( 𝐴 ∈ P ∧ 𝑓 ∈ 𝐴 ) → ( 𝑥 = ( 𝑓 ·Q 𝑔 ) → ( 𝑥 <Q 𝑓 ↔ 𝑔 ∈ 1P ) ) )
15	14	pm5.32rd	⊢ ( ( 𝐴 ∈ P ∧ 𝑓 ∈ 𝐴 ) → ( ( 𝑥 <Q 𝑓 ∧ 𝑥 = ( 𝑓 ·Q 𝑔 ) ) ↔ ( 𝑔 ∈ 1P ∧ 𝑥 = ( 𝑓 ·Q 𝑔 ) ) ) )
16	15	exbidv	⊢ ( ( 𝐴 ∈ P ∧ 𝑓 ∈ 𝐴 ) → ( ∃ 𝑔 ( 𝑥 <Q 𝑓 ∧ 𝑥 = ( 𝑓 ·Q 𝑔 ) ) ↔ ∃ 𝑔 ( 𝑔 ∈ 1P ∧ 𝑥 = ( 𝑓 ·Q 𝑔 ) ) ) )
17	2 16	syl5rbbr	⊢ ( ( 𝐴 ∈ P ∧ 𝑓 ∈ 𝐴 ) → ( ∃ 𝑔 ( 𝑔 ∈ 1P ∧ 𝑥 = ( 𝑓 ·Q 𝑔 ) ) ↔ ( 𝑥 <Q 𝑓 ∧ ∃ 𝑔 𝑥 = ( 𝑓 ·Q 𝑔 ) ) ) )
18	1 17	syl5bb	⊢ ( ( 𝐴 ∈ P ∧ 𝑓 ∈ 𝐴 ) → ( ∃ 𝑔 ∈ 1P 𝑥 = ( 𝑓 ·Q 𝑔 ) ↔ ( 𝑥 <Q 𝑓 ∧ ∃ 𝑔 𝑥 = ( 𝑓 ·Q 𝑔 ) ) ) )
19	18	rexbidva	⊢ ( 𝐴 ∈ P → ( ∃ 𝑓 ∈ 𝐴 ∃ 𝑔 ∈ 1P 𝑥 = ( 𝑓 ·Q 𝑔 ) ↔ ∃ 𝑓 ∈ 𝐴 ( 𝑥 <Q 𝑓 ∧ ∃ 𝑔 𝑥 = ( 𝑓 ·Q 𝑔 ) ) ) )
20		1pr	⊢ 1P ∈ P
21		df-mp	⊢ ·P = ( 𝑦 ∈ P , 𝑧 ∈ P ↦ { 𝑤 ∣ ∃ 𝑢 ∈ 𝑦 ∃ 𝑣 ∈ 𝑧 𝑤 = ( 𝑢 ·Q 𝑣 ) } )
22		mulclnq	⊢ ( ( 𝑢 ∈ Q ∧ 𝑣 ∈ Q ) → ( 𝑢 ·Q 𝑣 ) ∈ Q )
23	21 22	genpelv	⊢ ( ( 𝐴 ∈ P ∧ 1P ∈ P ) → ( 𝑥 ∈ ( 𝐴 ·P 1P ) ↔ ∃ 𝑓 ∈ 𝐴 ∃ 𝑔 ∈ 1P 𝑥 = ( 𝑓 ·Q 𝑔 ) ) )
24	20 23	mpan2	⊢ ( 𝐴 ∈ P → ( 𝑥 ∈ ( 𝐴 ·P 1P ) ↔ ∃ 𝑓 ∈ 𝐴 ∃ 𝑔 ∈ 1P 𝑥 = ( 𝑓 ·Q 𝑔 ) ) )
25		prnmax	⊢ ( ( 𝐴 ∈ P ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑓 ∈ 𝐴 𝑥 <Q 𝑓 )
26		ltrelnq	⊢ <Q ⊆ ( Q × Q )
27	26	brel	⊢ ( 𝑥 <Q 𝑓 → ( 𝑥 ∈ Q ∧ 𝑓 ∈ Q ) )
28		vex	⊢ 𝑓 ∈ V
29		vex	⊢ 𝑥 ∈ V
30		fvex	⊢ ( *Q ‘ 𝑓 ) ∈ V
31		mulcomnq	⊢ ( 𝑦 ·Q 𝑧 ) = ( 𝑧 ·Q 𝑦 )
32		mulassnq	⊢ ( ( 𝑦 ·Q 𝑧 ) ·Q 𝑤 ) = ( 𝑦 ·Q ( 𝑧 ·Q 𝑤 ) )
33	28 29 30 31 32	caov12	⊢ ( 𝑓 ·Q ( 𝑥 ·Q ( *Q ‘ 𝑓 ) ) ) = ( 𝑥 ·Q ( 𝑓 ·Q ( *Q ‘ 𝑓 ) ) )
34		recidnq	⊢ ( 𝑓 ∈ Q → ( 𝑓 ·Q ( *Q ‘ 𝑓 ) ) = 1Q )
35	34	oveq2d	⊢ ( 𝑓 ∈ Q → ( 𝑥 ·Q ( 𝑓 ·Q ( *Q ‘ 𝑓 ) ) ) = ( 𝑥 ·Q 1Q ) )
36	33 35	syl5eq	⊢ ( 𝑓 ∈ Q → ( 𝑓 ·Q ( 𝑥 ·Q ( *Q ‘ 𝑓 ) ) ) = ( 𝑥 ·Q 1Q ) )
37		mulidnq	⊢ ( 𝑥 ∈ Q → ( 𝑥 ·Q 1Q ) = 𝑥 )
38	36 37	sylan9eqr	⊢ ( ( 𝑥 ∈ Q ∧ 𝑓 ∈ Q ) → ( 𝑓 ·Q ( 𝑥 ·Q ( *Q ‘ 𝑓 ) ) ) = 𝑥 )
39	38	eqcomd	⊢ ( ( 𝑥 ∈ Q ∧ 𝑓 ∈ Q ) → 𝑥 = ( 𝑓 ·Q ( 𝑥 ·Q ( *Q ‘ 𝑓 ) ) ) )
40		ovex	⊢ ( 𝑥 ·Q ( *Q ‘ 𝑓 ) ) ∈ V
41		oveq2	⊢ ( 𝑔 = ( 𝑥 ·Q ( *Q ‘ 𝑓 ) ) → ( 𝑓 ·Q 𝑔 ) = ( 𝑓 ·Q ( 𝑥 ·Q ( *Q ‘ 𝑓 ) ) ) )
42	41	eqeq2d	⊢ ( 𝑔 = ( 𝑥 ·Q ( *Q ‘ 𝑓 ) ) → ( 𝑥 = ( 𝑓 ·Q 𝑔 ) ↔ 𝑥 = ( 𝑓 ·Q ( 𝑥 ·Q ( *Q ‘ 𝑓 ) ) ) ) )
43	40 42	spcev	⊢ ( 𝑥 = ( 𝑓 ·Q ( 𝑥 ·Q ( *Q ‘ 𝑓 ) ) ) → ∃ 𝑔 𝑥 = ( 𝑓 ·Q 𝑔 ) )
44	27 39 43	3syl	⊢ ( 𝑥 <Q 𝑓 → ∃ 𝑔 𝑥 = ( 𝑓 ·Q 𝑔 ) )
45	44	a1i	⊢ ( 𝑓 ∈ 𝐴 → ( 𝑥 <Q 𝑓 → ∃ 𝑔 𝑥 = ( 𝑓 ·Q 𝑔 ) ) )
46	45	ancld	⊢ ( 𝑓 ∈ 𝐴 → ( 𝑥 <Q 𝑓 → ( 𝑥 <Q 𝑓 ∧ ∃ 𝑔 𝑥 = ( 𝑓 ·Q 𝑔 ) ) ) )
47	46	reximia	⊢ ( ∃ 𝑓 ∈ 𝐴 𝑥 <Q 𝑓 → ∃ 𝑓 ∈ 𝐴 ( 𝑥 <Q 𝑓 ∧ ∃ 𝑔 𝑥 = ( 𝑓 ·Q 𝑔 ) ) )
48	25 47	syl	⊢ ( ( 𝐴 ∈ P ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑓 ∈ 𝐴 ( 𝑥 <Q 𝑓 ∧ ∃ 𝑔 𝑥 = ( 𝑓 ·Q 𝑔 ) ) )
49	48	ex	⊢ ( 𝐴 ∈ P → ( 𝑥 ∈ 𝐴 → ∃ 𝑓 ∈ 𝐴 ( 𝑥 <Q 𝑓 ∧ ∃ 𝑔 𝑥 = ( 𝑓 ·Q 𝑔 ) ) ) )
50		prcdnq	⊢ ( ( 𝐴 ∈ P ∧ 𝑓 ∈ 𝐴 ) → ( 𝑥 <Q 𝑓 → 𝑥 ∈ 𝐴 ) )
51	50	adantrd	⊢ ( ( 𝐴 ∈ P ∧ 𝑓 ∈ 𝐴 ) → ( ( 𝑥 <Q 𝑓 ∧ ∃ 𝑔 𝑥 = ( 𝑓 ·Q 𝑔 ) ) → 𝑥 ∈ 𝐴 ) )
52	51	rexlimdva	⊢ ( 𝐴 ∈ P → ( ∃ 𝑓 ∈ 𝐴 ( 𝑥 <Q 𝑓 ∧ ∃ 𝑔 𝑥 = ( 𝑓 ·Q 𝑔 ) ) → 𝑥 ∈ 𝐴 ) )
53	49 52	impbid	⊢ ( 𝐴 ∈ P → ( 𝑥 ∈ 𝐴 ↔ ∃ 𝑓 ∈ 𝐴 ( 𝑥 <Q 𝑓 ∧ ∃ 𝑔 𝑥 = ( 𝑓 ·Q 𝑔 ) ) ) )
54	19 24 53	3bitr4d	⊢ ( 𝐴 ∈ P → ( 𝑥 ∈ ( 𝐴 ·P 1P ) ↔ 𝑥 ∈ 𝐴 ) )
55	54	eqrdv	⊢ ( 𝐴 ∈ P → ( 𝐴 ·P 1P ) = 𝐴 )