This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem reclem4pr

Description: Lemma for Proposition 9-3.7(v) of Gleason p. 124. (Contributed by NM, 30-Apr-1996) (New usage is discouraged.)

Ref Expression
Hypothesis reclempr.1 ⊢ 𝐵 = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) }
Assertion reclem4pr ( 𝐴 ∈ P → ( 𝐴 ·P 𝐵 ) = 1P )

Proof

Step Hyp Ref Expression
1 reclempr.1 ⊢ 𝐵 = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) }
2 1 reclem2pr ⊢ ( 𝐴 ∈ P → 𝐵 ∈ P )
3 df-mp ⊢ ·P = ( 𝑦 ∈ P , 𝑤 ∈ P ↦ { 𝑢 ∣ ∃ 𝑓 ∈ 𝑦 ∃ 𝑔 ∈ 𝑤 𝑢 = ( 𝑓 ·Q 𝑔 ) } )
4 mulclnq ⊢ ( ( 𝑓 ∈ Q ∧ 𝑔 ∈ Q ) → ( 𝑓 ·Q 𝑔 ) ∈ Q )
5 3 4 genpelv ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑤 ∈ ( 𝐴 ·P 𝐵 ) ↔ ∃ 𝑧 ∈ 𝐴 ∃ 𝑥 ∈ 𝐵 𝑤 = ( 𝑧 ·Q 𝑥 ) ) )
6 2 5 mpdan ⊢ ( 𝐴 ∈ P → ( 𝑤 ∈ ( 𝐴 ·P 𝐵 ) ↔ ∃ 𝑧 ∈ 𝐴 ∃ 𝑥 ∈ 𝐵 𝑤 = ( 𝑧 ·Q 𝑥 ) ) )
7 1 eqabri ⊢ ( 𝑥 ∈ 𝐵 ↔ ∃ 𝑦 ( 𝑥 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) )
8 ltrelnq ⊢ <Q ⊆ ( Q × Q )
9 8 brel ⊢ ( 𝑥 <Q 𝑦 → ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) )
10 9 simprd ⊢ ( 𝑥 <Q 𝑦 → 𝑦 ∈ Q )
11 elprnq ⊢ ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ Q )
12 ltmnq ⊢ ( 𝑧 ∈ Q → ( 𝑥 <Q 𝑦 ↔ ( 𝑧 ·Q 𝑥 ) <Q ( 𝑧 ·Q 𝑦 ) ) )
13 11 12 syl ⊢ ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 <Q 𝑦 ↔ ( 𝑧 ·Q 𝑥 ) <Q ( 𝑧 ·Q 𝑦 ) ) )
14 13 biimpd ⊢ ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 <Q 𝑦 → ( 𝑧 ·Q 𝑥 ) <Q ( 𝑧 ·Q 𝑦 ) ) )
15 14 adantr ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ∈ Q ) → ( 𝑥 <Q 𝑦 → ( 𝑧 ·Q 𝑥 ) <Q ( 𝑧 ·Q 𝑦 ) ) )
16 recclnq ⊢ ( 𝑦 ∈ Q → ( *Q ‘ 𝑦 ) ∈ Q )
17 prub ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) ∧ ( *Q ‘ 𝑦 ) ∈ Q ) → ( ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 → 𝑧 <Q ( *Q ‘ 𝑦 ) ) )
18 16 17 sylan2 ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ∈ Q ) → ( ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 → 𝑧 <Q ( *Q ‘ 𝑦 ) ) )
19 ltmnq ⊢ ( 𝑦 ∈ Q → ( 𝑧 <Q ( *Q ‘ 𝑦 ) ↔ ( 𝑦 ·Q 𝑧 ) <Q ( 𝑦 ·Q ( *Q ‘ 𝑦 ) ) ) )
20 mulcomnq ⊢ ( 𝑦 ·Q 𝑧 ) = ( 𝑧 ·Q 𝑦 )
21 20 a1i ⊢ ( 𝑦 ∈ Q → ( 𝑦 ·Q 𝑧 ) = ( 𝑧 ·Q 𝑦 ) )
22 recidnq ⊢ ( 𝑦 ∈ Q → ( 𝑦 ·Q ( *Q ‘ 𝑦 ) ) = 1Q )
23 21 22 breq12d ⊢ ( 𝑦 ∈ Q → ( ( 𝑦 ·Q 𝑧 ) <Q ( 𝑦 ·Q ( *Q ‘ 𝑦 ) ) ↔ ( 𝑧 ·Q 𝑦 ) <Q 1Q ) )
24 19 23 bitrd ⊢ ( 𝑦 ∈ Q → ( 𝑧 <Q ( *Q ‘ 𝑦 ) ↔ ( 𝑧 ·Q 𝑦 ) <Q 1Q ) )
25 24 adantl ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ∈ Q ) → ( 𝑧 <Q ( *Q ‘ 𝑦 ) ↔ ( 𝑧 ·Q 𝑦 ) <Q 1Q ) )
26 18 25 sylibd ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ∈ Q ) → ( ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 → ( 𝑧 ·Q 𝑦 ) <Q 1Q ) )
27 15 26 anim12d ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ∈ Q ) → ( ( 𝑥 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) → ( ( 𝑧 ·Q 𝑥 ) <Q ( 𝑧 ·Q 𝑦 ) ∧ ( 𝑧 ·Q 𝑦 ) <Q 1Q ) ) )
28 ltsonq ⊢ <Q Or Q
29 28 8 sotri ⊢ ( ( ( 𝑧 ·Q 𝑥 ) <Q ( 𝑧 ·Q 𝑦 ) ∧ ( 𝑧 ·Q 𝑦 ) <Q 1Q ) → ( 𝑧 ·Q 𝑥 ) <Q 1Q )
30 27 29 syl6 ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ∈ Q ) → ( ( 𝑥 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) → ( 𝑧 ·Q 𝑥 ) <Q 1Q ) )
31 30 exp4b ⊢ ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) → ( 𝑦 ∈ Q → ( 𝑥 <Q 𝑦 → ( ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 → ( 𝑧 ·Q 𝑥 ) <Q 1Q ) ) ) )
32 10 31 syl5 ⊢ ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 <Q 𝑦 → ( 𝑥 <Q 𝑦 → ( ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 → ( 𝑧 ·Q 𝑥 ) <Q 1Q ) ) ) )
33 32 pm2.43d ⊢ ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 <Q 𝑦 → ( ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 → ( 𝑧 ·Q 𝑥 ) <Q 1Q ) ) )
34 33 impd ⊢ ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑥 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) → ( 𝑧 ·Q 𝑥 ) <Q 1Q ) )
35 34 exlimdv ⊢ ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) → ( ∃ 𝑦 ( 𝑥 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) → ( 𝑧 ·Q 𝑥 ) <Q 1Q ) )
36 7 35 biimtrid ⊢ ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐵 → ( 𝑧 ·Q 𝑥 ) <Q 1Q ) )
37 breq1 ⊢ ( 𝑤 = ( 𝑧 ·Q 𝑥 ) → ( 𝑤 <Q 1Q ↔ ( 𝑧 ·Q 𝑥 ) <Q 1Q ) )
38 37 biimprcd ⊢ ( ( 𝑧 ·Q 𝑥 ) <Q 1Q → ( 𝑤 = ( 𝑧 ·Q 𝑥 ) → 𝑤 <Q 1Q ) )
39 36 38 syl6 ⊢ ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐵 → ( 𝑤 = ( 𝑧 ·Q 𝑥 ) → 𝑤 <Q 1Q ) ) )
40 39 expimpd ⊢ ( 𝐴 ∈ P → ( ( 𝑧 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑤 = ( 𝑧 ·Q 𝑥 ) → 𝑤 <Q 1Q ) ) )
41 40 rexlimdvv ⊢ ( 𝐴 ∈ P → ( ∃ 𝑧 ∈ 𝐴 ∃ 𝑥 ∈ 𝐵 𝑤 = ( 𝑧 ·Q 𝑥 ) → 𝑤 <Q 1Q ) )
42 6 41 sylbid ⊢ ( 𝐴 ∈ P → ( 𝑤 ∈ ( 𝐴 ·P 𝐵 ) → 𝑤 <Q 1Q ) )
43 df-1p ⊢ 1P = { 𝑤 ∣ 𝑤 <Q 1Q }
44 43 eqabri ⊢ ( 𝑤 ∈ 1P ↔ 𝑤 <Q 1Q )
45 42 44 imbitrrdi ⊢ ( 𝐴 ∈ P → ( 𝑤 ∈ ( 𝐴 ·P 𝐵 ) → 𝑤 ∈ 1P ) )
46 45 ssrdv ⊢ ( 𝐴 ∈ P → ( 𝐴 ·P 𝐵 ) ⊆ 1P )
47 1 reclem3pr ⊢ ( 𝐴 ∈ P → 1P ⊆ ( 𝐴 ·P 𝐵 ) )
48 46 47 eqssd ⊢ ( 𝐴 ∈ P → ( 𝐴 ·P 𝐵 ) = 1P )