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 simpl 
 |-  ( ( u .~ v /\ v .~ w ) -> u .~ v )
25 24 19 sylib 
 |-  ( ( u .~ v /\ v .~ w ) -> ( ( u e. ( 0 [,] 1 ) /\ v e. ( 0 [,] 1 ) ) /\ ( u - v ) e. QQ ) )
26 25 simpld 
 |-  ( ( u .~ v /\ v .~ w ) -> ( u e. ( 0 [,] 1 ) /\ v e. ( 0 [,] 1 ) ) )
27 26 simpld 
 |-  ( ( u .~ v /\ v .~ w ) -> u e. ( 0 [,] 1 ) )
28 simpr 
 |-  ( ( u .~ v /\ v .~ w ) -> v .~ w )
29 oveq12 
 |-  ( ( x = v /\ y = w ) -> ( x - y ) = ( v - w ) )
30 29 eleq1d 
 |-  ( ( x = v /\ y = w ) -> ( ( x - y ) e. QQ <-> ( v - w ) e. QQ ) )
31 30 1 brab2a 
 |-  ( v .~ w <-> ( ( v e. ( 0 [,] 1 ) /\ w e. ( 0 [,] 1 ) ) /\ ( v - w ) e. QQ ) )
32 28 31 sylib 
 |-  ( ( u .~ v /\ v .~ w ) -> ( ( v e. ( 0 [,] 1 ) /\ w e. ( 0 [,] 1 ) ) /\ ( v - w ) e. QQ ) )
33 32 simpld 
 |-  ( ( u .~ v /\ v .~ w ) -> ( v e. ( 0 [,] 1 ) /\ w e. ( 0 [,] 1 ) ) )
34 33 simprd 
 |-  ( ( u .~ v /\ v .~ w ) -> w e. ( 0 [,] 1 ) )
35 27 7 syl 
 |-  ( ( u .~ v /\ v .~ w ) -> u e. CC )
36 25 11 syl 
 |-  ( ( u .~ v /\ v .~ w ) -> v e. CC )
37 5 34 sselid 
 |-  ( ( u .~ v /\ v .~ w ) -> w e. RR )
38 37 recnd 
 |-  ( ( u .~ v /\ v .~ w ) -> w e. CC )
39 35 36 38 npncand 
 |-  ( ( u .~ v /\ v .~ w ) -> ( ( u - v ) + ( v - w ) ) = ( u - w ) )
40 25 simprd 
 |-  ( ( u .~ v /\ v .~ w ) -> ( u - v ) e. QQ )
41 32 simprd 
 |-  ( ( u .~ v /\ v .~ w ) -> ( v - w ) e. QQ )
42 qaddcl 
 |-  ( ( ( u - v ) e. QQ /\ ( v - w ) e. QQ ) -> ( ( u - v ) + ( v - w ) ) e. QQ )
43 40 41 42 syl2anc 
 |-  ( ( u .~ v /\ v .~ w ) -> ( ( u - v ) + ( v - w ) ) e. QQ )
44 39 43 eqeltrrd 
 |-  ( ( u .~ v /\ v .~ w ) -> ( u - w ) e. QQ )
45 oveq12 
 |-  ( ( x = u /\ y = w ) -> ( x - y ) = ( u - w ) )
46 45 eleq1d 
 |-  ( ( x = u /\ y = w ) -> ( ( x - y ) e. QQ <-> ( u - w ) e. QQ ) )
47 46 1 brab2a 
 |-  ( u .~ w <-> ( ( u e. ( 0 [,] 1 ) /\ w e. ( 0 [,] 1 ) ) /\ ( u - w ) e. QQ ) )
48 27 34 44 47 syl21anbrc 
 |-  ( ( u .~ v /\ v .~ w ) -> u .~ w )
49 7 subidd 
 |-  ( u e. ( 0 [,] 1 ) -> ( u - u ) = 0 )
50 0z 
 |-  0 e. ZZ
51 zq 
 |-  ( 0 e. ZZ -> 0 e. QQ )
52 50 51 ax-mp 
 |-  0 e. QQ
53 49 52 eqeltrdi 
 |-  ( u e. ( 0 [,] 1 ) -> ( u - u ) e. QQ )
54 53 adantr 
 |-  ( ( u e. ( 0 [,] 1 ) /\ u e. ( 0 [,] 1 ) ) -> ( u - u ) e. QQ )
55 54 pm4.71i 
 |-  ( ( u e. ( 0 [,] 1 ) /\ u e. ( 0 [,] 1 ) ) <-> ( ( u e. ( 0 [,] 1 ) /\ u e. ( 0 [,] 1 ) ) /\ ( u - u ) e. QQ ) )
56 pm4.24 
 |-  ( u e. ( 0 [,] 1 ) <-> ( u e. ( 0 [,] 1 ) /\ u e. ( 0 [,] 1 ) ) )
57 oveq12 
 |-  ( ( x = u /\ y = u ) -> ( x - y ) = ( u - u ) )
58 57 eleq1d 
 |-  ( ( x = u /\ y = u ) -> ( ( x - y ) e. QQ <-> ( u - u ) e. QQ ) )
59 58 1 brab2a 
 |-  ( u .~ u <-> ( ( u e. ( 0 [,] 1 ) /\ u e. ( 0 [,] 1 ) ) /\ ( u - u ) e. QQ ) )
60 55 56 59 3bitr4i 
 |-  ( u e. ( 0 [,] 1 ) <-> u .~ u )
61 2 23 48 60 iseri 
 |-  .~ Er ( 0 [,] 1 )