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 0 1 y 0 1 x y
Assertion vitalilem1 ˙ Er 0 1

Proof

Step Hyp Ref Expression
1 vitali.1 ˙ = x y | x 0 1 y 0 1 x y
2 1 relopabiv Rel ˙
3 simplr u 0 1 v 0 1 u v v 0 1
4 simpll u 0 1 v 0 1 u v u 0 1
5 unitssre 0 1
6 5 sseli u 0 1 u
7 6 recnd u 0 1 u
8 7 ad2antrr u 0 1 v 0 1 u v u
9 5 sseli v 0 1 v
10 9 recnd v 0 1 v
11 10 ad2antlr u 0 1 v 0 1 u v v
12 8 11 negsubdi2d u 0 1 v 0 1 u v u v = v u
13 qnegcl u v u v
14 13 adantl u 0 1 v 0 1 u v u v
15 12 14 eqeltrrd u 0 1 v 0 1 u v v u
16 3 4 15 jca31 u 0 1 v 0 1 u v v 0 1 u 0 1 v u
17 oveq12 x = u y = v x y = u v
18 17 eleq1d x = u y = v x y u v
19 18 1 brab2a u ˙ v u 0 1 v 0 1 u v
20 oveq12 x = v y = u x y = v u
21 20 eleq1d x = v y = u x y v u
22 21 1 brab2a v ˙ u v 0 1 u 0 1 v u
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 0 1 v 0 1 u v
26 25 simpld u ˙ v v ˙ w u 0 1 v 0 1
27 26 simpld u ˙ v v ˙ w u 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 v w
31 30 1 brab2a v ˙ w v 0 1 w 0 1 v w
32 28 31 sylib u ˙ v v ˙ w v 0 1 w 0 1 v w
33 32 simpld u ˙ v v ˙ w v 0 1 w 0 1
34 33 simprd u ˙ v v ˙ w w 0 1
35 27 7 syl u ˙ v v ˙ w u
36 25 11 syl u ˙ v v ˙ w v
37 5 34 sseldi u ˙ v v ˙ w w
38 37 recnd u ˙ v v ˙ w w
39 35 36 38 npncand u ˙ v v ˙ w u v + v - w = u w
40 25 simprd u ˙ v v ˙ w u v
41 32 simprd u ˙ v v ˙ w v w
42 qaddcl u v v w u v + v - w
43 40 41 42 syl2anc u ˙ v v ˙ w u v + v - w
44 39 43 eqeltrrd u ˙ v v ˙ w u w
45 oveq12 x = u y = w x y = u w
46 45 eleq1d x = u y = w x y u w
47 46 1 brab2a u ˙ w u 0 1 w 0 1 u w
48 27 34 44 47 syl21anbrc u ˙ v v ˙ w u ˙ w
49 7 subidd u 0 1 u u = 0
50 0z 0
51 zq 0 0
52 50 51 ax-mp 0
53 49 52 eqeltrdi u 0 1 u u
54 53 adantr u 0 1 u 0 1 u u
55 54 pm4.71i u 0 1 u 0 1 u 0 1 u 0 1 u u
56 pm4.24 u 0 1 u 0 1 u 0 1
57 oveq12 x = u y = u x y = u u
58 57 eleq1d x = u y = u x y u u
59 58 1 brab2a u ˙ u u 0 1 u 0 1 u u
60 55 56 59 3bitr4i u 0 1 u ˙ u
61 2 23 48 60 iseri ˙ Er 0 1