Metamath Proof Explorer

Theorem vitalilem1

Description: Lemma for vitali . (Contributed by Mario Carneiro, 16-Jun-2014) (Proof shortened by AV, 1-May-2021)

Ref Expression
Hypothesis vitali.1 
|- .~ = { <. x , y >. | ( ( x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) /\ ( x - y ) e. QQ ) }
Assertion vitalilem1 
|- .~ Er ( 0 [,] 1 )

Proof

Step Hyp Ref Expression
1 vitali.1 
 |-  .~ = { <. x , y >. | ( ( x e. ( 0 [,] 1 ) /\ y e. ( 0 [,] 1 ) ) /\ ( x - y ) e. QQ ) }
2 1 relopabiv 
 |-  Rel .~
3 simplr 
 |-  ( ( ( u e. ( 0 [,] 1 ) /\ v e. ( 0 [,] 1 ) ) /\ ( u - v ) e. QQ ) -> v e. ( 0 [,] 1 ) )
4 simpll 
 |-  ( ( ( u e. ( 0 [,] 1 ) /\ v e. ( 0 [,] 1 ) ) /\ ( u - v ) e. QQ ) -> u e. ( 0 [,] 1 ) )
5 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
6 5 sseli 
 |-  ( u e. ( 0 [,] 1 ) -> u e. RR )
7 6 recnd 
 |-  ( u e. ( 0 [,] 1 ) -> u e. CC )
8 7 ad2antrr 
 |-  ( ( ( u e. ( 0 [,] 1 ) /\ v e. ( 0 [,] 1 ) ) /\ ( u - v ) e. QQ ) -> u e. CC )
9 5 sseli 
 |-  ( v e. ( 0 [,] 1 ) -> v e. RR )
10 9 recnd 
 |-  ( v e. ( 0 [,] 1 ) -> v e. CC )
11 10 ad2antlr 
 |-  ( ( ( u e. ( 0 [,] 1 ) /\ v e. ( 0 [,] 1 ) ) /\ ( u - v ) e. QQ ) -> v e. CC )
12 8 11 negsubdi2d 
 |-  ( ( ( u e. ( 0 [,] 1 ) /\ v e. ( 0 [,] 1 ) ) /\ ( u - v ) e. QQ ) -> -u ( u - v ) = ( v - u ) )
13 qnegcl 
 |-  ( ( u - v ) e. QQ -> -u ( u - v ) e. QQ )
14 13 adantl 
 |-  ( ( ( u e. ( 0 [,] 1 ) /\ v e. ( 0 [,] 1 ) ) /\ ( u - v ) e. QQ ) -> -u ( u - v ) e. QQ )
15 12 14 eqeltrrd 
 |-  ( ( ( u e. ( 0 [,] 1 ) /\ v e. ( 0 [,] 1 ) ) /\ ( u - v ) e. QQ ) -> ( v - u ) e. QQ )
16 3 4 15 jca31 
 |-  ( ( ( u e. ( 0 [,] 1 ) /\ v e. ( 0 [,] 1 ) ) /\ ( u - v ) e. QQ ) -> ( ( v e. ( 0 [,] 1 ) /\ u e. ( 0 [,] 1 ) ) /\ ( v - u ) e. QQ ) )
17 oveq12 
 |-  ( ( x = u /\ y = v ) -> ( x - y ) = ( u - v ) )
18 17 eleq1d 
 |-  ( ( x = u /\ y = v ) -> ( ( x - y ) e. QQ <-> ( u - v ) e. QQ ) )
19 18 1 brab2a 
 |-  ( u .~ v <-> ( ( u e. ( 0 [,] 1 ) /\ v e. ( 0 [,] 1 ) ) /\ ( u - v ) e. QQ ) )
20 oveq12 
 |-  ( ( x = v /\ y = u ) -> ( x - y ) = ( v - u ) )
21 20 eleq1d 
 |-  ( ( x = v /\ y = u ) -> ( ( x - y ) e. QQ <-> ( v - u ) e. QQ ) )
22 21 1 brab2a 
 |-  ( v .~ u <-> ( ( v e. ( 0 [,] 1 ) /\ u e. ( 0 [,] 1 ) ) /\ ( v - u ) e. QQ ) )
23 16 19 22 3imtr4i 
 |-  ( u .~ v -> v .~ u )
24 19 birani 
 |-  ( ( u .~ v /\ v .~ w ) -> ( ( u e. ( 0 [,] 1 ) /\ v e. ( 0 [,] 1 ) ) /\ ( u - v ) e. QQ ) )
25 24 simpld 
 |-  ( ( u .~ v /\ v .~ w ) -> ( u e. ( 0 [,] 1 ) /\ v e. ( 0 [,] 1 ) ) )
26 25 simpld 
 |-  ( ( u .~ v /\ v .~ w ) -> u e. ( 0 [,] 1 ) )
27 oveq12 
 |-  ( ( x = v /\ y = w ) -> ( x - y ) = ( v - w ) )
28 27 eleq1d 
 |-  ( ( x = v /\ y = w ) -> ( ( x - y ) e. QQ <-> ( v - w ) e. QQ ) )
29 28 1 brab2a 
 |-  ( v .~ w <-> ( ( v e. ( 0 [,] 1 ) /\ w e. ( 0 [,] 1 ) ) /\ ( v - w ) e. QQ ) )
30 29 bilani 
 |-  ( ( u .~ v /\ v .~ w ) -> ( ( v e. ( 0 [,] 1 ) /\ w e. ( 0 [,] 1 ) ) /\ ( v - w ) e. QQ ) )
31 30 simpld 
 |-  ( ( u .~ v /\ v .~ w ) -> ( v e. ( 0 [,] 1 ) /\ w e. ( 0 [,] 1 ) ) )
32 31 simprd 
 |-  ( ( u .~ v /\ v .~ w ) -> w e. ( 0 [,] 1 ) )
33 26 7 syl 
 |-  ( ( u .~ v /\ v .~ w ) -> u e. CC )
34 24 11 syl 
 |-  ( ( u .~ v /\ v .~ w ) -> v e. CC )
35 5 32 sselid 
 |-  ( ( u .~ v /\ v .~ w ) -> w e. RR )
36 35 recnd 
 |-  ( ( u .~ v /\ v .~ w ) -> w e. CC )
37 33 34 36 npncand 
 |-  ( ( u .~ v /\ v .~ w ) -> ( ( u - v ) + ( v - w ) ) = ( u - w ) )
38 24 simprd 
 |-  ( ( u .~ v /\ v .~ w ) -> ( u - v ) e. QQ )
39 30 simprd 
 |-  ( ( u .~ v /\ v .~ w ) -> ( v - w ) e. QQ )
40 qaddcl 
 |-  ( ( ( u - v ) e. QQ /\ ( v - w ) e. QQ ) -> ( ( u - v ) + ( v - w ) ) e. QQ )
41 38 39 40 syl2anc 
 |-  ( ( u .~ v /\ v .~ w ) -> ( ( u - v ) + ( v - w ) ) e. QQ )
42 37 41 eqeltrrd 
 |-  ( ( u .~ v /\ v .~ w ) -> ( u - w ) e. QQ )
43 oveq12 
 |-  ( ( x = u /\ y = w ) -> ( x - y ) = ( u - w ) )
44 43 eleq1d 
 |-  ( ( x = u /\ y = w ) -> ( ( x - y ) e. QQ <-> ( u - w ) e. QQ ) )
45 44 1 brab2a 
 |-  ( u .~ w <-> ( ( u e. ( 0 [,] 1 ) /\ w e. ( 0 [,] 1 ) ) /\ ( u - w ) e. QQ ) )
46 26 32 42 45 syl21anbrc 
 |-  ( ( u .~ v /\ v .~ w ) -> u .~ w )
47 7 subidd 
 |-  ( u e. ( 0 [,] 1 ) -> ( u - u ) = 0 )
48 0z 
 |-  0 e. ZZ
49 zq 
 |-  ( 0 e. ZZ -> 0 e. QQ )
50 48 49 ax-mp 
 |-  0 e. QQ
51 47 50 eqeltrdi 
 |-  ( u e. ( 0 [,] 1 ) -> ( u - u ) e. QQ )
52 51 adantr 
 |-  ( ( u e. ( 0 [,] 1 ) /\ u e. ( 0 [,] 1 ) ) -> ( u - u ) e. QQ )
53 52 pm4.71i 
 |-  ( ( u e. ( 0 [,] 1 ) /\ u e. ( 0 [,] 1 ) ) <-> ( ( u e. ( 0 [,] 1 ) /\ u e. ( 0 [,] 1 ) ) /\ ( u - u ) e. QQ ) )
54 pm4.24 
 |-  ( u e. ( 0 [,] 1 ) <-> ( u e. ( 0 [,] 1 ) /\ u e. ( 0 [,] 1 ) ) )
55 oveq12 
 |-  ( ( x = u /\ y = u ) -> ( x - y ) = ( u - u ) )
56 55 eleq1d 
 |-  ( ( x = u /\ y = u ) -> ( ( x - y ) e. QQ <-> ( u - u ) e. QQ ) )
57 56 1 brab2a 
 |-  ( u .~ u <-> ( ( u e. ( 0 [,] 1 ) /\ u e. ( 0 [,] 1 ) ) /\ ( u - u ) e. QQ ) )
58 53 54 57 3bitr4i 
 |-  ( u e. ( 0 [,] 1 ) <-> u .~ u )
59 2 23 46 58 iseri 
 |-  .~ Er ( 0 [,] 1 )