Metamath Proof Explorer


Theorem ltexprlem7

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 ltexprlem7 ( ( ( 𝐴P𝐵P ) ∧ 𝐴𝐵 ) → 𝐵 ⊆ ( 𝐴 +P 𝐶 ) )

Proof

Step Hyp Ref Expression
1 ltexprlem.1 𝐶 = { 𝑥 ∣ ∃ 𝑦 ( ¬ 𝑦𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) }
2 1 ltexprlem5 ( ( 𝐵P𝐴𝐵 ) → 𝐶P )
3 ltaddpr ( ( 𝐴P𝐶P ) → 𝐴 <P ( 𝐴 +P 𝐶 ) )
4 addclpr ( ( 𝐴P𝐶P ) → ( 𝐴 +P 𝐶 ) ∈ P )
5 ltprord ( ( 𝐴P ∧ ( 𝐴 +P 𝐶 ) ∈ P ) → ( 𝐴 <P ( 𝐴 +P 𝐶 ) ↔ 𝐴 ⊊ ( 𝐴 +P 𝐶 ) ) )
6 4 5 syldan ( ( 𝐴P𝐶P ) → ( 𝐴 <P ( 𝐴 +P 𝐶 ) ↔ 𝐴 ⊊ ( 𝐴 +P 𝐶 ) ) )
7 3 6 mpbid ( ( 𝐴P𝐶P ) → 𝐴 ⊊ ( 𝐴 +P 𝐶 ) )
8 7 pssssd ( ( 𝐴P𝐶P ) → 𝐴 ⊆ ( 𝐴 +P 𝐶 ) )
9 8 sseld ( ( 𝐴P𝐶P ) → ( 𝑤𝐴𝑤 ∈ ( 𝐴 +P 𝐶 ) ) )
10 9 2a1d ( ( 𝐴P𝐶P ) → ( 𝐵P → ( 𝑤𝐵 → ( 𝑤𝐴𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) )
11 10 com4r ( 𝑤𝐴 → ( ( 𝐴P𝐶P ) → ( 𝐵P → ( 𝑤𝐵𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) )
12 11 expd ( 𝑤𝐴 → ( 𝐴P → ( 𝐶P → ( 𝐵P → ( 𝑤𝐵𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) ) )
13 prnmadd ( ( 𝐵P𝑤𝐵 ) → ∃ 𝑣 ( 𝑤 +Q 𝑣 ) ∈ 𝐵 )
14 13 ex ( 𝐵P → ( 𝑤𝐵 → ∃ 𝑣 ( 𝑤 +Q 𝑣 ) ∈ 𝐵 ) )
15 elprnq ( ( 𝐵P ∧ ( 𝑤 +Q 𝑣 ) ∈ 𝐵 ) → ( 𝑤 +Q 𝑣 ) ∈ Q )
16 addnqf +Q : ( Q × Q ) ⟶ Q
17 16 fdmi dom +Q = ( Q × Q )
18 0nnq ¬ ∅ ∈ Q
19 17 18 ndmovrcl ( ( 𝑤 +Q 𝑣 ) ∈ Q → ( 𝑤Q𝑣Q ) )
20 15 19 syl ( ( 𝐵P ∧ ( 𝑤 +Q 𝑣 ) ∈ 𝐵 ) → ( 𝑤Q𝑣Q ) )
21 20 simpld ( ( 𝐵P ∧ ( 𝑤 +Q 𝑣 ) ∈ 𝐵 ) → 𝑤Q )
22 vex 𝑣 ∈ V
23 22 prlem934 ( 𝐴P → ∃ 𝑧𝐴 ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 )
24 23 adantr ( ( 𝐴P𝐶P ) → ∃ 𝑧𝐴 ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 )
25 prub ( ( ( 𝐴P𝑧𝐴 ) ∧ 𝑤Q ) → ( ¬ 𝑤𝐴𝑧 <Q 𝑤 ) )
26 ltexnq ( 𝑤Q → ( 𝑧 <Q 𝑤 ↔ ∃ 𝑥 ( 𝑧 +Q 𝑥 ) = 𝑤 ) )
27 26 adantl ( ( ( 𝐴P𝑧𝐴 ) ∧ 𝑤Q ) → ( 𝑧 <Q 𝑤 ↔ ∃ 𝑥 ( 𝑧 +Q 𝑥 ) = 𝑤 ) )
28 25 27 sylibd ( ( ( 𝐴P𝑧𝐴 ) ∧ 𝑤Q ) → ( ¬ 𝑤𝐴 → ∃ 𝑥 ( 𝑧 +Q 𝑥 ) = 𝑤 ) )
29 28 ex ( ( 𝐴P𝑧𝐴 ) → ( 𝑤Q → ( ¬ 𝑤𝐴 → ∃ 𝑥 ( 𝑧 +Q 𝑥 ) = 𝑤 ) ) )
30 29 ad2ant2r ( ( ( 𝐴P𝐶P ) ∧ ( 𝑧𝐴 ∧ ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 ) ) → ( 𝑤Q → ( ¬ 𝑤𝐴 → ∃ 𝑥 ( 𝑧 +Q 𝑥 ) = 𝑤 ) ) )
31 vex 𝑧 ∈ V
32 vex 𝑥 ∈ V
33 addcomnq ( 𝑓 +Q 𝑔 ) = ( 𝑔 +Q 𝑓 )
34 addassnq ( ( 𝑓 +Q 𝑔 ) +Q ) = ( 𝑓 +Q ( 𝑔 +Q ) )
35 31 22 32 33 34 caov32 ( ( 𝑧 +Q 𝑣 ) +Q 𝑥 ) = ( ( 𝑧 +Q 𝑥 ) +Q 𝑣 )
36 oveq1 ( ( 𝑧 +Q 𝑥 ) = 𝑤 → ( ( 𝑧 +Q 𝑥 ) +Q 𝑣 ) = ( 𝑤 +Q 𝑣 ) )
37 35 36 eqtrid ( ( 𝑧 +Q 𝑥 ) = 𝑤 → ( ( 𝑧 +Q 𝑣 ) +Q 𝑥 ) = ( 𝑤 +Q 𝑣 ) )
38 37 eleq1d ( ( 𝑧 +Q 𝑥 ) = 𝑤 → ( ( ( 𝑧 +Q 𝑣 ) +Q 𝑥 ) ∈ 𝐵 ↔ ( 𝑤 +Q 𝑣 ) ∈ 𝐵 ) )
39 38 biimpar ( ( ( 𝑧 +Q 𝑥 ) = 𝑤 ∧ ( 𝑤 +Q 𝑣 ) ∈ 𝐵 ) → ( ( 𝑧 +Q 𝑣 ) +Q 𝑥 ) ∈ 𝐵 )
40 ovex ( 𝑧 +Q 𝑣 ) ∈ V
41 eleq1 ( 𝑦 = ( 𝑧 +Q 𝑣 ) → ( 𝑦𝐴 ↔ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 ) )
42 41 notbid ( 𝑦 = ( 𝑧 +Q 𝑣 ) → ( ¬ 𝑦𝐴 ↔ ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 ) )
43 oveq1 ( 𝑦 = ( 𝑧 +Q 𝑣 ) → ( 𝑦 +Q 𝑥 ) = ( ( 𝑧 +Q 𝑣 ) +Q 𝑥 ) )
44 43 eleq1d ( 𝑦 = ( 𝑧 +Q 𝑣 ) → ( ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ↔ ( ( 𝑧 +Q 𝑣 ) +Q 𝑥 ) ∈ 𝐵 ) )
45 42 44 anbi12d ( 𝑦 = ( 𝑧 +Q 𝑣 ) → ( ( ¬ 𝑦𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) ↔ ( ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 ∧ ( ( 𝑧 +Q 𝑣 ) +Q 𝑥 ) ∈ 𝐵 ) ) )
46 40 45 spcev ( ( ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 ∧ ( ( 𝑧 +Q 𝑣 ) +Q 𝑥 ) ∈ 𝐵 ) → ∃ 𝑦 ( ¬ 𝑦𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) )
47 1 abeq2i ( 𝑥𝐶 ↔ ∃ 𝑦 ( ¬ 𝑦𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) )
48 46 47 sylibr ( ( ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 ∧ ( ( 𝑧 +Q 𝑣 ) +Q 𝑥 ) ∈ 𝐵 ) → 𝑥𝐶 )
49 39 48 sylan2 ( ( ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 ∧ ( ( 𝑧 +Q 𝑥 ) = 𝑤 ∧ ( 𝑤 +Q 𝑣 ) ∈ 𝐵 ) ) → 𝑥𝐶 )
50 df-plp +P = ( 𝑥P , 𝑤P ↦ { 𝑧 ∣ ∃ 𝑓𝑥𝑣𝑤 𝑧 = ( 𝑓 +Q 𝑣 ) } )
51 addclnq ( ( 𝑓Q𝑣Q ) → ( 𝑓 +Q 𝑣 ) ∈ Q )
52 50 51 genpprecl ( ( 𝐴P𝐶P ) → ( ( 𝑧𝐴𝑥𝐶 ) → ( 𝑧 +Q 𝑥 ) ∈ ( 𝐴 +P 𝐶 ) ) )
53 49 52 sylan2i ( ( 𝐴P𝐶P ) → ( ( 𝑧𝐴 ∧ ( ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 ∧ ( ( 𝑧 +Q 𝑥 ) = 𝑤 ∧ ( 𝑤 +Q 𝑣 ) ∈ 𝐵 ) ) ) → ( 𝑧 +Q 𝑥 ) ∈ ( 𝐴 +P 𝐶 ) ) )
54 53 exp4d ( ( 𝐴P𝐶P ) → ( 𝑧𝐴 → ( ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 → ( ( ( 𝑧 +Q 𝑥 ) = 𝑤 ∧ ( 𝑤 +Q 𝑣 ) ∈ 𝐵 ) → ( 𝑧 +Q 𝑥 ) ∈ ( 𝐴 +P 𝐶 ) ) ) ) )
55 54 imp42 ( ( ( ( 𝐴P𝐶P ) ∧ ( 𝑧𝐴 ∧ ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 ) ) ∧ ( ( 𝑧 +Q 𝑥 ) = 𝑤 ∧ ( 𝑤 +Q 𝑣 ) ∈ 𝐵 ) ) → ( 𝑧 +Q 𝑥 ) ∈ ( 𝐴 +P 𝐶 ) )
56 eleq1 ( ( 𝑧 +Q 𝑥 ) = 𝑤 → ( ( 𝑧 +Q 𝑥 ) ∈ ( 𝐴 +P 𝐶 ) ↔ 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) )
57 56 ad2antrl ( ( ( ( 𝐴P𝐶P ) ∧ ( 𝑧𝐴 ∧ ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 ) ) ∧ ( ( 𝑧 +Q 𝑥 ) = 𝑤 ∧ ( 𝑤 +Q 𝑣 ) ∈ 𝐵 ) ) → ( ( 𝑧 +Q 𝑥 ) ∈ ( 𝐴 +P 𝐶 ) ↔ 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) )
58 55 57 mpbid ( ( ( ( 𝐴P𝐶P ) ∧ ( 𝑧𝐴 ∧ ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 ) ) ∧ ( ( 𝑧 +Q 𝑥 ) = 𝑤 ∧ ( 𝑤 +Q 𝑣 ) ∈ 𝐵 ) ) → 𝑤 ∈ ( 𝐴 +P 𝐶 ) )
59 58 exp32 ( ( ( 𝐴P𝐶P ) ∧ ( 𝑧𝐴 ∧ ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 ) ) → ( ( 𝑧 +Q 𝑥 ) = 𝑤 → ( ( 𝑤 +Q 𝑣 ) ∈ 𝐵𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) )
60 59 exlimdv ( ( ( 𝐴P𝐶P ) ∧ ( 𝑧𝐴 ∧ ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 ) ) → ( ∃ 𝑥 ( 𝑧 +Q 𝑥 ) = 𝑤 → ( ( 𝑤 +Q 𝑣 ) ∈ 𝐵𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) )
61 30 60 syl6d ( ( ( 𝐴P𝐶P ) ∧ ( 𝑧𝐴 ∧ ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 ) ) → ( 𝑤Q → ( ¬ 𝑤𝐴 → ( ( 𝑤 +Q 𝑣 ) ∈ 𝐵𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) )
62 24 61 rexlimddv ( ( 𝐴P𝐶P ) → ( 𝑤Q → ( ¬ 𝑤𝐴 → ( ( 𝑤 +Q 𝑣 ) ∈ 𝐵𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) )
63 62 com14 ( ( 𝑤 +Q 𝑣 ) ∈ 𝐵 → ( 𝑤Q → ( ¬ 𝑤𝐴 → ( ( 𝐴P𝐶P ) → 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) )
64 63 adantl ( ( 𝐵P ∧ ( 𝑤 +Q 𝑣 ) ∈ 𝐵 ) → ( 𝑤Q → ( ¬ 𝑤𝐴 → ( ( 𝐴P𝐶P ) → 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) )
65 21 64 mpd ( ( 𝐵P ∧ ( 𝑤 +Q 𝑣 ) ∈ 𝐵 ) → ( ¬ 𝑤𝐴 → ( ( 𝐴P𝐶P ) → 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) )
66 65 ex ( 𝐵P → ( ( 𝑤 +Q 𝑣 ) ∈ 𝐵 → ( ¬ 𝑤𝐴 → ( ( 𝐴P𝐶P ) → 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) )
67 66 exlimdv ( 𝐵P → ( ∃ 𝑣 ( 𝑤 +Q 𝑣 ) ∈ 𝐵 → ( ¬ 𝑤𝐴 → ( ( 𝐴P𝐶P ) → 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) )
68 14 67 syld ( 𝐵P → ( 𝑤𝐵 → ( ¬ 𝑤𝐴 → ( ( 𝐴P𝐶P ) → 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) )
69 68 com4t ( ¬ 𝑤𝐴 → ( ( 𝐴P𝐶P ) → ( 𝐵P → ( 𝑤𝐵𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) )
70 69 expd ( ¬ 𝑤𝐴 → ( 𝐴P → ( 𝐶P → ( 𝐵P → ( 𝑤𝐵𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) ) )
71 12 70 pm2.61i ( 𝐴P → ( 𝐶P → ( 𝐵P → ( 𝑤𝐵𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) )
72 2 71 syl5 ( 𝐴P → ( ( 𝐵P𝐴𝐵 ) → ( 𝐵P → ( 𝑤𝐵𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) )
73 72 expd ( 𝐴P → ( 𝐵P → ( 𝐴𝐵 → ( 𝐵P → ( 𝑤𝐵𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) ) )
74 73 com34 ( 𝐴P → ( 𝐵P → ( 𝐵P → ( 𝐴𝐵 → ( 𝑤𝐵𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) ) )
75 74 pm2.43d ( 𝐴P → ( 𝐵P → ( 𝐴𝐵 → ( 𝑤𝐵𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) )
76 75 imp31 ( ( ( 𝐴P𝐵P ) ∧ 𝐴𝐵 ) → ( 𝑤𝐵𝑤 ∈ ( 𝐴 +P 𝐶 ) ) )
77 76 ssrdv ( ( ( 𝐴P𝐵P ) ∧ 𝐴𝐵 ) → 𝐵 ⊆ ( 𝐴 +P 𝐶 ) )