Metamath Proof Explorer

Theorem ltexprlem6

Description: Lemma for Proposition 9-3.5(iv) of Gleason p. 123. (Contributed by NM, 8-Apr-1996) (Revised by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)

Ref Expression
Hypothesis ltexprlem.1 ⊢ 𝐶 = { 𝑥 ∣ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) }
Assertion ltexprlem6 ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ 𝐴 ⊊ 𝐵 ) → ( 𝐴 +P 𝐶 ) ⊆ 𝐵 )

Proof

Step Hyp Ref Expression
1 ltexprlem.1 ⊢ 𝐶 = { 𝑥 ∣ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) }
2 1 ltexprlem5 ⊢ ( ( 𝐵 ∈ P ∧ 𝐴 ⊊ 𝐵 ) → 𝐶 ∈ P )
3 df-plp ⊢ +P = ( 𝑧 ∈ P , 𝑦 ∈ P ↦ { 𝑓 ∣ ∃ 𝑔 ∈ 𝑧 ∃ ℎ ∈ 𝑦 𝑓 = ( 𝑔 +Q ℎ ) } )
4 addclnq ⊢ ( ( 𝑔 ∈ Q ∧ ℎ ∈ Q ) → ( 𝑔 +Q ℎ ) ∈ Q )
5 3 4 genpelv ⊢ ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) → ( 𝑧 ∈ ( 𝐴 +P 𝐶 ) ↔ ∃ 𝑤 ∈ 𝐴 ∃ 𝑥 ∈ 𝐶 𝑧 = ( 𝑤 +Q 𝑥 ) ) )
6 2 5 sylan2 ⊢ ( ( 𝐴 ∈ P ∧ ( 𝐵 ∈ P ∧ 𝐴 ⊊ 𝐵 ) ) → ( 𝑧 ∈ ( 𝐴 +P 𝐶 ) ↔ ∃ 𝑤 ∈ 𝐴 ∃ 𝑥 ∈ 𝐶 𝑧 = ( 𝑤 +Q 𝑥 ) ) )
7 1 abeq2i ⊢ ( 𝑥 ∈ 𝐶 ↔ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) )
8 elprnq ⊢ ( ( 𝐵 ∈ P ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) → ( 𝑦 +Q 𝑥 ) ∈ Q )
9 addnqf ⊢ +Q : ( Q × Q ) ⟶ Q
10 9 fdmi ⊢ dom +Q = ( Q × Q )
11 0nnq ⊢ ¬ ∅ ∈ Q
12 10 11 ndmovrcl ⊢ ( ( 𝑦 +Q 𝑥 ) ∈ Q → ( 𝑦 ∈ Q ∧ 𝑥 ∈ Q ) )
13 12 simpld ⊢ ( ( 𝑦 +Q 𝑥 ) ∈ Q → 𝑦 ∈ Q )
14 8 13 syl ⊢ ( ( 𝐵 ∈ P ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) → 𝑦 ∈ Q )
15 prub ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑦 ∈ Q ) → ( ¬ 𝑦 ∈ 𝐴 → 𝑤 <Q 𝑦 ) )
16 14 15 sylan2 ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝐵 ∈ P ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) ) → ( ¬ 𝑦 ∈ 𝐴 → 𝑤 <Q 𝑦 ) )
17 12 simprd ⊢ ( ( 𝑦 +Q 𝑥 ) ∈ Q → 𝑥 ∈ Q )
18 vex ⊢ 𝑤 ∈ V
19 vex ⊢ 𝑦 ∈ V
20 ltanq ⊢ ( 𝑢 ∈ Q → ( 𝑧 <Q 𝑣 ↔ ( 𝑢 +Q 𝑧 ) <Q ( 𝑢 +Q 𝑣 ) ) )
21 vex ⊢ 𝑥 ∈ V
22 addcomnq ⊢ ( 𝑧 +Q 𝑣 ) = ( 𝑣 +Q 𝑧 )
23 18 19 20 21 22 caovord2 ⊢ ( 𝑥 ∈ Q → ( 𝑤 <Q 𝑦 ↔ ( 𝑤 +Q 𝑥 ) <Q ( 𝑦 +Q 𝑥 ) ) )
24 8 17 23 3syl ⊢ ( ( 𝐵 ∈ P ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) → ( 𝑤 <Q 𝑦 ↔ ( 𝑤 +Q 𝑥 ) <Q ( 𝑦 +Q 𝑥 ) ) )
25 prcdnq ⊢ ( ( 𝐵 ∈ P ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) → ( ( 𝑤 +Q 𝑥 ) <Q ( 𝑦 +Q 𝑥 ) → ( 𝑤 +Q 𝑥 ) ∈ 𝐵 ) )
26 24 25 sylbid ⊢ ( ( 𝐵 ∈ P ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) → ( 𝑤 <Q 𝑦 → ( 𝑤 +Q 𝑥 ) ∈ 𝐵 ) )
27 26 adantl ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝐵 ∈ P ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) ) → ( 𝑤 <Q 𝑦 → ( 𝑤 +Q 𝑥 ) ∈ 𝐵 ) )
28 16 27 syld ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝐵 ∈ P ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) ) → ( ¬ 𝑦 ∈ 𝐴 → ( 𝑤 +Q 𝑥 ) ∈ 𝐵 ) )
29 28 exp32 ⊢ ( ( 𝐴 ∈ P ∧ 𝑤 ∈ 𝐴 ) → ( 𝐵 ∈ P → ( ( 𝑦 +Q 𝑥 ) ∈ 𝐵 → ( ¬ 𝑦 ∈ 𝐴 → ( 𝑤 +Q 𝑥 ) ∈ 𝐵 ) ) ) )
30 29 com34 ⊢ ( ( 𝐴 ∈ P ∧ 𝑤 ∈ 𝐴 ) → ( 𝐵 ∈ P → ( ¬ 𝑦 ∈ 𝐴 → ( ( 𝑦 +Q 𝑥 ) ∈ 𝐵 → ( 𝑤 +Q 𝑥 ) ∈ 𝐵 ) ) ) )
31 30 imp4b ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑤 ∈ 𝐴 ) ∧ 𝐵 ∈ P ) → ( ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) → ( 𝑤 +Q 𝑥 ) ∈ 𝐵 ) )
32 31 exlimdv ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑤 ∈ 𝐴 ) ∧ 𝐵 ∈ P ) → ( ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) → ( 𝑤 +Q 𝑥 ) ∈ 𝐵 ) )
33 7 32 syl5bi ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑤 ∈ 𝐴 ) ∧ 𝐵 ∈ P ) → ( 𝑥 ∈ 𝐶 → ( 𝑤 +Q 𝑥 ) ∈ 𝐵 ) )
34 33 exp31 ⊢ ( 𝐴 ∈ P → ( 𝑤 ∈ 𝐴 → ( 𝐵 ∈ P → ( 𝑥 ∈ 𝐶 → ( 𝑤 +Q 𝑥 ) ∈ 𝐵 ) ) ) )
35 34 com23 ⊢ ( 𝐴 ∈ P → ( 𝐵 ∈ P → ( 𝑤 ∈ 𝐴 → ( 𝑥 ∈ 𝐶 → ( 𝑤 +Q 𝑥 ) ∈ 𝐵 ) ) ) )
36 35 imp43 ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) ) → ( 𝑤 +Q 𝑥 ) ∈ 𝐵 )
37 eleq1 ⊢ ( 𝑧 = ( 𝑤 +Q 𝑥 ) → ( 𝑧 ∈ 𝐵 ↔ ( 𝑤 +Q 𝑥 ) ∈ 𝐵 ) )
38 37 biimparc ⊢ ( ( ( 𝑤 +Q 𝑥 ) ∈ 𝐵 ∧ 𝑧 = ( 𝑤 +Q 𝑥 ) ) → 𝑧 ∈ 𝐵 )
39 36 38 sylan ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) ) ∧ 𝑧 = ( 𝑤 +Q 𝑥 ) ) → 𝑧 ∈ 𝐵 )
40 39 exp31 ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( 𝑤 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑧 = ( 𝑤 +Q 𝑥 ) → 𝑧 ∈ 𝐵 ) ) )
41 40 rexlimdvv ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ∃ 𝑤 ∈ 𝐴 ∃ 𝑥 ∈ 𝐶 𝑧 = ( 𝑤 +Q 𝑥 ) → 𝑧 ∈ 𝐵 ) )
42 41 adantrr ⊢ ( ( 𝐴 ∈ P ∧ ( 𝐵 ∈ P ∧ 𝐴 ⊊ 𝐵 ) ) → ( ∃ 𝑤 ∈ 𝐴 ∃ 𝑥 ∈ 𝐶 𝑧 = ( 𝑤 +Q 𝑥 ) → 𝑧 ∈ 𝐵 ) )
43 6 42 sylbid ⊢ ( ( 𝐴 ∈ P ∧ ( 𝐵 ∈ P ∧ 𝐴 ⊊ 𝐵 ) ) → ( 𝑧 ∈ ( 𝐴 +P 𝐶 ) → 𝑧 ∈ 𝐵 ) )
44 43 ssrdv ⊢ ( ( 𝐴 ∈ P ∧ ( 𝐵 ∈ P ∧ 𝐴 ⊊ 𝐵 ) ) → ( 𝐴 +P 𝐶 ) ⊆ 𝐵 )
45 44 anassrs ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ 𝐴 ⊊ 𝐵 ) → ( 𝐴 +P 𝐶 ) ⊆ 𝐵 )