Repeatedly re-proven statements

David A. Wheeler

unread,

Jul 13, 2016, 12:43:19 PM7/13/16

to metamath

Instead of just guessing, I had metamath generate every proved expression,
and then I removed everything that was a theorem or axiom.
It's a naive text comparison, so for example it will include statements
that are only true given certain hypotheses.

Still, it gives a sense of what is being repeatedly re-proved.
I've included the program that does it, and the some results.

The "winner" is "( Base ` K ) = ( Base ` K )". In general, a lot of proofs
have to insert an identity statement to make another step work.

Other statements constantly reproved (with repetition counts) are:
206 |- -u 1 e. CC
167 |- 0 e. _V
143 |- 4 e. CC
139 |- pi e. CC
111 |- ( 0 + 1 ) = 1
107 |- ( pi / 2 ) e. RR
101 |- 0 <_ 0
98 |- 2 = ( 1 + 1 )
94 |- 6 e. CC
92 |- ( 1 / 2 ) e. RR
89 |- CC C_ CC
87 |- 9 e. CC
87 |- ( B e. RR -> B e. CC )
84 |- ( ph -> 2 e. CC )
79 |- 3 = ( 2 + 1 )
78 |- 8 e. CC
76 |- ( N e. NN -> N e. CC )
75 |- 1 e. _V
73 |- 7 e. CC
71 |- ( pi / 2 ) e. CC
70 |- ( ph -> 1 e. RR )
67 |- ( 1 x. 1 ) = 1

I'll separately post the top part of the list.

--- David A. Wheeler

====================== analyze
#!/bin/sh

# Quick analysis - what statements are repeatedly proved, but
# NOT top-level theorems/axioms?

# What are the top-level proven theorems/axioms?
metamath 'read set.mm' 'set width 9999' 'show statement *' quit | \
sed -e 's/ */ /g' | grep '^[1-9].*\$[ap]' | cut -d ' ' -f 4- | \
sed -e 's/ *\$= .*$//' > ,statements

# What's been proven at any step?
metamath 'read set.mm' 'set width 9999' 'show proof *' quit | \
sed -e 's/ */ /g' | grep '^[1-9].*\$[ap]' | cut -d ' ' -f 4- | \
sed -e 's/ *\$\. *$//' > ,proven

# Show proven by any step NOT including theorems/axioms.
# "comm -23 ,proven ,statements" won't work because of duplicate lines.

grep -v -F -f ,statements < ,proven > ,embedded

sort ,embedded | uniq -c | sort -n -r > ,embedded-counts

David A. Wheeler

unread,

Jul 13, 2016, 12:51:09 PM7/13/16

to metamath, metamath

As a follow-up, here's the top repeatedly-proven statements in set.mm.
This uses text comparison, which is naive, but I could get results quickly that way.
Repetition counts are on the left.

Below are the top 1000 expressions that have the most repetition
yet are not top-level statements ($a or $p).

I'm sure this analysis can be improved!! It was a quick comparison, but it's
nice to have something to actually *analyze*.

I think this suggests areas where just a little more automation -
or addition of a few theorems - would speed proof creation.

For example, there are 167 times "0 e. _V" is proved, 143 times "4 e. CC" is proved,
and 139 times "pi e. CC" is proved. We figure out that "0 <_ 0" 101 times.
Putting some of these in set.mm directly
would make those automated and slightly shorten other proofs.

--- David A. Wheeler

===================================

2764 |- ( Base ` K ) = ( Base ` K )
651 |- y e. _V
613 |- ( Base ` R ) = ( Base ` R )
543 |- ( le ` K ) = ( le ` K )
441 |- ( Base ` G ) = ( Base ` G )
413 |- U. J = U. J
413 |- ( +g ` G ) = ( +g ` G )
392 |- ( LSubSp ` U ) = ( LSubSp ` U )
381 |- z e. _V
351 |- ( .r ` R ) = ( .r ` R )
334 |- ( 0g ` G ) = ( 0g ` G )
300 |- ( Base ` W ) = ( Base ` W )
296 |- ( Atoms ` K ) = ( Atoms ` K )
288 |- ( Base ` S ) = ( Base ` S )
286 |- ( Scalar ` W ) = ( Scalar ` W )
268 |- ( join ` K ) = ( join ` K )
252 |- ( 0. ` K ) = ( 0. ` K )
251 |- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
248 |- ( 0g ` R ) = ( 0g ` R )
240 |- ( ph -> Y e. V )
237 |- ( invg ` G ) = ( invg ` G )
210 |- ( meet ` K ) = ( meet ` K )

206 |- -u 1 e. CC

167 |- 0 e. _V

165 |- ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
164 |- f e. _V
162 |- ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
144 |- ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )

143 |- 4 e. CC

141 |- ( Base ` P ) = ( Base ` P )

139 |- pi e. CC

111 |- ( 0 + 1 ) = 1

111 |- ( <o ` K ) = ( <o ` K )
110 |- ( mulGrp ` R ) = ( mulGrp ` R )
108 |- ( P e. A -> P e. ( Base ` K ) )

107 |- ( pi / 2 ) e. RR

107 |- ( Base ` Y ) = ( Base ` Y )
105 |- ( lt ` K ) = ( lt ` K )
103 |- U. K = U. K
102 |- ( .sOLD ` U ) = ( .sOLD ` U )

101 |- 0 <_ 0

100 |- ( ph -> M e. ZZ )
100 |- ( 1. ` K ) = ( 1. ` K )
99 |- v e. _V

98 |- 2 = ( 1 + 1 )

94 |- 6 e. CC

94 |- ( ph -> M e. CC )
93 |- ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W )

92 |- ( 1 / 2 ) e. RR
89 |- CC C_ CC

88 |- ( Unit ` R ) = ( Unit ` R )
88 |- ( ph -> B e. CC )
88 |- ( Base ` T ) = ( Base ` T )

87 |- 9 e. CC
87 |- ( B e. RR -> B e. CC )

85 |- ( inv ` G ) = ( inv ` G )

84 |- ( ph -> 2 e. CC )

79 |- 3 = ( 2 + 1 )

79 |- ( oppR ` R ) = ( oppR ` R )

78 |- 8 e. CC

78 |- ( ph -> N e. ZZ )
78 |- ( J e. ( TopOn ` X ) -> X = U. J )
78 |- ( ( LCDual ` K ) ` W ) = ( ( LCDual ` K ) ` W )
77 |- g e. _V

76 |- ( N e. NN -> N e. CC )

76 |- ( LSpan ` U ) = ( LSpan ` U )
76 |- ( +g ` S ) = ( +g ` S )

75 |- 1 e. _V

73 |- 7 e. CC
71 |- ( pi / 2 ) e. CC

71 |- ( J e. ( TopOn ` X ) -> J e. Top )
70 |- ( ph -> N e. CC )

70 |- ( ph -> 1 e. RR )

68 |- c e. _V
68 |- ( ph -> B e. RR )

67 |- ( 1 x. 1 ) = 1

67 |- ( ( trL ` K ) ` W ) = ( ( trL ` K ) ` W )
66 |- ( ph -> N e. RR )
66 |- ( normCV ` U ) = ( normCV ` U )
66 |- ( CCfld |`s ZZ ) = ( CCfld |`s ZZ )
66 |- ( 0g ` S ) = ( 0g ` S )
66 |- ( 0g ` D ) = ( 0g ` D )
65 |- ( BaseSet ` U ) = ( BaseSet ` U )
64 |- ( I mPwSer R ) = ( I mPwSer R )
64 |- ( +g ` M ) = ( +g ` M )
64 |- ( .g ` G ) = ( .g ` G )
62 |- -u _i e. CC
62 |- ( TopOpen ` CCfld ) e. ( TopOn ` CC )
62 |- ( ph -> N e. NN )
62 |- ( +g ` U ) = ( +g ` U )
61 |- ( Scalar ` U ) = ( Scalar ` U )
61 |- ( ph -> M e. RR )
61 |- ( LSSum ` U ) = ( LSSum ` U )
61 |- ( dom_ ` T ) = ( dom_ ` T )
61 |- ( 1st ` R ) = ( 1st ` R )
60 |- ( R e. A -> R e. ( Base ` K ) )
60 |- ( BaseSet ` W ) = ( BaseSet ` W )
60 |- ( 1 / 2 ) e. CC
60 |- ( .s ` U ) = ( .s ` U )
60 |- ( .i ` W ) = ( .i ` W )
59 |- ( X e. ( V \ { .0. } ) -> X e. V )
59 |- ( ph -> E e. V )
59 |- ( ph -> 1 e. ZZ )
59 |- ( 1 ... N ) e. _V
58 |- t e. _V
58 |- ( ph -> J e. Top )
58 |- ( cod_ ` T ) = ( cod_ ` T )
58 |- ( Cntz ` G ) = ( Cntz ` G )
58 |- ( ( DVecH ` K ) ` W ) = ( ( DVecH ` K ) ` W )
57 |- ( N e. NN -> N e. NN0 )
57 |- ( 1 - 1 ) = 0
56 |- ran G = ran G
56 |- ( .r ` S ) = ( .r ` S )
55 |- ( Y e. ( V \ { .0. } ) -> Y e. V )
54 |- ( x e. RR+ -> x e. RR )
53 |- ( lub ` K ) = ( lub ` K )
53 |- ( 0g ` C ) = ( 0g ` C )
52 |- ( ph -> X e. RR )
52 |- ( LSubSp ` C ) = ( LSubSp ` C )
52 |- ( LSSum ` W ) = ( LSSum ` W )
52 |- ( .r ` D ) = ( .r ` D )
51 |- dom ( dom_ ` T ) = dom ( dom_ ` T )
51 |- ( ph -> A C_ RR )
51 |- ( M e. ZZ -> M e. CC )
51 |- ( 0vec ` U ) = ( 0vec ` U )
51 |- ( ( ph /\ Y = Z /\ ps ) -> K e. HL )
51 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( P =/= Q /\ S =/= T ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ -. U .<_ ( S .\/ T ) ) ) -> K e. HL )
50 |- -u 1 e. RR
50 |- ran ( 1st ` R ) = ran ( 1st ` R )
50 |- ( N e. NN -> N e. RR )
50 |- ( F ` x ) e. _V
50 |- ( 1o mPoly R ) = ( 1o mPoly R )
49 |- U. R = U. R
49 |- N e. CC
49 |- ( pmap ` K ) = ( pmap ` K )
49 |- ( ph -> 1 e. CC )
49 |- ( K e. ZZ -> K e. CC )
49 |- ( k e. NN -> k e. NN0 )
48 |- ( S e. A -> S e. ( Base ` K ) )
48 |- ( ph -> U e. RR )
48 |- ( ph -> E e. CC )
48 |- ( Base ` Z ) = ( Base ` Z )
48 |- ( .r ` F ) = ( .r ` F )
48 |- ( ( ocH ` K ) ` W ) = ( ( ocH ` K ) ` W )
47 |- Base = Slot 1
47 |- ( 0g ` P ) = ( 0g ` P )
46 |- CC = U. ( TopOpen ` CCfld )
46 |- <. <. +h , .h >. , normh >. = <. <. +h , .h >. , normh >.
46 |- ( T. -> NN e. _V )
46 |- ( ph -> w e. V )
45 |- { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
45 |- ( x = A -> x = A )
45 |- ( ph -> X e. _V )
45 |- ( Base ` K ) e. _V
45 |- ( abs o. - ) = ( abs o. - )
45 |- ( 2nd ` R ) = ( 2nd ` R )
45 |- ( 2 e. CC /\ 2 =/= 0 )
45 |- ( ( DIsoB ` K ) ` W ) = ( ( DIsoB ` K ) ` W )
44 |- (/) = ( Base ` (/) )
44 |- ( x e. ZZ -> x e. CC )
44 |- ( ph -> S C_ CC )
44 |- ( ph -> II e. ( TopOn ` ( 0 [,] 1 ) ) )
44 |- ( N e. NN0 -> N e. CC )
43 |- V e. _V
43 |- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
43 |- ( PwSer1 ` R ) = ( PwSer1 ` R )
43 |- ( ph -> R Fn I )
43 |- ( J e. Top <-> J e. ( TopOn ` U. J ) )
43 |- ( invr ` R ) = ( invr ` R )
43 |- ( deg1 ` R ) = ( deg1 ` R )
43 |- ( ( A e. CC /\ B e. CC ) -> A e. CC )
42 |- ( J e. ( TopOn ` X ) -> X e. J )
42 |- ( invg ` R ) = ( invg ` R )
42 |- ( 2 x. 1 ) = 2
42 |- ( .r ` P ) = ( .r ` P )
42 |- ( ( A e. CC /\ B e. CC ) -> B e. CC )
41 |- 1 = ; 0 1
41 |- ( Scalar ` R ) = ( Scalar ` R )
41 |- ( ph -> V e. _V )
41 |- ( ph -> K e. Top )
41 |- ( ph -> I e. _V )
41 |- ( N e. NN -> N =/= 0 )
41 |- ( 0g ` T ) = ( 0g ` T )
41 |- ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
40 |- U. S = U. S
40 |- if ( A e. ~H , A , 0h ) e. ~H
40 |- .0. e. _V
40 |- ( ph -> Y e. RR )
40 |- ( ph -> RR e. _V )
40 |- ( ph -> R e. RR )
40 |- ( ph -> N e. NN0 )
40 |- ( ph -> G e. D )
40 |- ( ph -> A. y ph )
40 |- ( ph -> 3 e. CC )
40 |- ( -g ` W ) = ( -g ` W )
40 |- ( A e. dom arctan -> A e. CC )
40 |- ( ( ph /\ Y = Z /\ ps ) -> K e. Lat )
39 |- A e. SH
39 |- ( Scalar ` C ) = ( Scalar ` C )
39 |- ( ph -> T e. CC )
39 |- ( p e. Prime -> p e. NN )
39 |- ( 1r ` F ) = ( 1r ` F )
39 |- ( +g ` H ) = ( +g ` H )
39 |- ( +g ` D ) = ( +g ` D )
38 |- ( ph -> B e. RR* )
38 |- ( mrCls ` ( SubGrp ` G ) ) = ( mrCls ` ( SubGrp ` G ) )
38 |- ( id_ ` T ) = ( id_ ` T )
38 |- ( Base ` W ) e. _V
38 |- ( Base ` L ) = ( Base ` L )
38 |- ( A e. CC -> ( _i x. A ) e. CC )
38 |- ( 2 e. RR /\ 0 < 2 )
38 |- ( ( EDRing ` K ) ` W ) = ( ( EDRing ` K ) ` W )
37 |- d e. _V
37 |- ( ph -> K e. CC )
37 |- ( Base ` G ) e. _V
37 |- ( 1r ` S ) = ( 1r ` S )
37 |- ( ( ph /\ x e. A ) -> C e. CC )
37 |- ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> K e. Lat )
36 |- ( ph -> 0 e. RR )
36 |- ( ocv ` W ) = ( ocv ` W )
36 |- ( Base ` C ) = ( Base ` C )
36 |- ( Base ` ( ( LCDual ` K ) ` W ) ) = ( Base ` ( ( LCDual ` K ) ` W ) )
36 |- ( +g ` Y ) = ( +g ` Y )
36 |- ( +g ` T ) = ( +g ` T )
36 |- ( ( LTrn ` K ) ` W ) e. _V
36 |- ( ( DIsoA ` K ) ` W ) = ( ( DIsoA ` K ) ` W )
35 |- 3 e. ZZ
35 |- 2o = suc 1o
35 |- ( ph -> X e. CC )
35 |- ( ph -> P e. CC )
35 |- ( ph -> K e. RR )
35 |- ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
35 |- ( LSAtoms ` U ) = ( LSAtoms ` U )
35 |- ( invg ` W ) = ( invg ` W )
35 |- ( glb ` K ) = ( glb ` K )
35 |- ( B e. RR -> B e. RR* )
35 |- ( B e. NN -> B e. CC )
35 |- ( A e. NN -> A e. ZZ )
35 |- ( .s ` S ) = ( .s ` S )
35 |- ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> K e. HL )
34 |- k e. _V
34 |- j e. _V
34 |- ( Z/nZ ` N ) = ( Z/nZ ` N )
34 |- ( z e. y -> A. x z e. y )
34 |- ( x e. A |-> B ) = ( x e. A |-> B )
34 |- ( Q e. A -> Q e. B )
34 |- ( ph -> R e. Grp )
34 |- ( ph -> P e. NN )
34 |- ( B e. NN -> B e. ZZ )
34 |- ( abs ` 1 ) = 1
34 |- ( A =/= B <-> -. A = B )
34 |- ( 0g ` H ) = ( 0g ` H )
34 |- ( _|_ ` B ) e. CH
34 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC )
34 |- ( ( ph /\ x e. RR+ ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
34 |- ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
34 |- ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> K e. Lat )
33 |- m e. _V
33 |- B e. SH
33 |- 4 =/= 0
33 |- ( x = y -> x = y )
33 |- ( Unit ` Z ) = ( Unit ` Z )
33 |- ( PSubSp ` K ) = ( PSubSp ` K )
33 |- ( ph -> Z e. RR+ )
33 |- ( ph -> R e. CC )
33 |- ( ph -> ( A [,] B ) C_ RR )
33 |- ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
33 |- ( M e. ZZ -> M e. RR )
33 |- ( coeff ` F ) = ( coeff ` F )
33 |- ( 1 + 0 ) = 1
32 |- N e. RR
32 |- 4 = ( 3 + 1 )
32 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
32 |- { x } e. _V
32 |- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
32 |- ( Z e. ( V \ { .0. } ) -> Z e. V )
32 |- ( ph -> T e. RR )
32 |- ( ph -> 2 =/= 0 )
32 |- ( A e. V -> A e. _V )
32 |- ( 1 / 1 ) = 1
32 |- ( 1 - 0 ) = 1
32 |- ( 0g ` Y ) = ( 0g ` Y )
32 |- ( 0 [,) +oo ) C_ RR
32 |- ( .s ` P ) = ( .s ` P )
32 |- ( ( ph /\ x e. A ) -> ( Im ` B ) e. RR )
31 |- T e. _V
31 |- H e. _V
31 |- CC = U. J
31 |- ( x e. ~H -> ( T ` x ) e. ~H )
31 |- ( TopOpen ` G ) = ( TopOpen ` G )
31 |- ( n e. NN -> n e. NN0 )
31 |- ( Base ` ( Scalar ` U ) ) = ( Base ` ( Scalar ` U ) )
31 |- ( B .ih B ) e. CC
31 |- ( 1r ` ( Scalar ` W ) ) = ( 1r ` ( Scalar ` W ) )
31 |- ( 0 [,] 1 ) C_ RR
31 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC )
31 |- ( ( K e. Lat /\ X e. B /\ W e. B ) -> ( X ./\ W ) e. B )
31 |- ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
31 |- ( ( HDMap ` K ) ` W ) = ( ( HDMap ` K ) ` W )
31 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ -. R .<_ ( P .\/ Q ) ) -> K e. HL )
30 |- Z C_ ZZ
30 |- dom ( id_ ` T ) = dom ( id_ ` T )
30 |- 1 <_ 1
30 |- (. A e. V ->. A e. V ).
30 |- (. A e. B ->. A e. B ).
30 |- ( Scalar ` D ) = ( Scalar ` D )
30 |- ( RR i^i RR ) = RR
30 |- ( Poly1 ` R ) = ( Poly1 ` R )
30 |- ( mulGrp ` Z ) = ( mulGrp ` Z )
30 |- ( log ` 2 ) e. RR
30 |- ( Base ` ( ( DVecH ` K ) ` W ) ) = ( Base ` ( ( DVecH ` K ) ` W ) )
30 |- ( 1 + 2 ) = 3
30 |- ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> A e. CC )
30 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( K e. HL /\ W e. H ) )
29 |- r e. _V
29 |- K e. CC
29 |- h e. _V
29 |- { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } = { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin }
29 |- ( x e. RR+ -> ( 1 ... ( |_ ` x ) ) e. Fin )
29 |- ( topGen ` ran (,) ) = ( topGen ` ran (,) )
29 |- ( ph -> X = U. J )
29 |- ( ph -> B e. _V )
29 |- ( M e. NN -> M e. NN0 )
29 |- ( LSHyp ` U ) = ( LSHyp ` U )
29 |- ( 2 x. pi ) e. CC
29 |- ( ( ph /\ x e. A ) -> ( Re ` B ) e. RR )
29 |- ( ( oc ` K ) ` W ) = ( ( oc ` K ) ` W )
29 |- ( ( K e. OML /\ X e. B /\ Y e. B ) -> K e. Lat )
29 |- ( ( ( K e. HL /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> K e. HL )
28 |- ZZ = ( Base ` ( CCfld |`s ZZ ) )
28 |- ( Scalar ` S ) = ( Scalar ` S )
28 |- ( ph -> M =/= 0 )
28 |- ( ph -> ( N ` { Y } ) e. ( LSubSp ` U ) )
28 |- ( NN0 ^m I ) e. _V
28 |- ( mulGrp ` S ) = ( mulGrp ` S )
28 |- ( LAut ` K ) = ( LAut ` K )
28 |- ( k e. NN -> ( k + 1 ) e. NN )
28 |- ( k e. ( 0 ... N ) -> k e. NN0 )
28 |- ( B e. NN -> B e. RR )
28 |- ( A e. dom arctan -> ( _i x. A ) e. CC )
28 |- ( 2 - 1 ) = 1
28 |- ( 0 [,] +oo ) C_ RR*
27 |- Z e. _V
27 |- -u 1 =/= 0
27 |- if ( B e. ~H , B , 0h ) e. ~H
27 |- ( x e. RR+ -> x e. CC )
27 |- ( x e. ( 2 [,) +oo ) -> x e. RR )
27 |- ( TopOpen ` CCfld ) e. Top
27 |- ( Scalar ` R ) e. _V
27 |- ( r e. RR+ -> r e. RR* )
27 |- ( ph -> Y C_ X )
27 |- ( n = N -> ( EE ` n ) = ( EE ` N ) )
27 |- ( K e. Top <-> K e. ( TopOn ` U. K ) )
27 |- ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` R ) )
27 |- ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) )
27 |- ( B e. HAtoms -> B e. CH )
27 |- ( a i^i x ) e. _V
27 |- ( A e. ZZ -> A e. RR )
27 |- ( 0 + 2 ) = 2
27 |- ( +g ` ( Scalar ` W ) ) = ( +g ` ( Scalar ` W ) )
27 |- ( _|_P ` K ) = ( _|_P ` K )
27 |- ( .s ` D ) = ( .s ` D )
27 |- ( ( N e. CC /\ 1 e. CC ) -> ( ( N - 1 ) + 1 ) = N )
27 |- ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) = ( Q .\/ P ) )
27 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> N e. NN )
27 |- ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( G ` P ) e. A /\ -. ( G ` P ) .<_ W ) )
27 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ -. R .<_ ( P .\/ Q ) ) -> K e. Lat )
27 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ R .<_ ( P .\/ Q ) ) /\ ( -. R .<_ ( S .\/ T ) /\ -. U .<_ ( S .\/ T ) ) ) ) -> K e. HL )
27 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) ) ) -> ( K e. HL /\ W e. H ) )
26 |- -u pi e. RR
26 |- dom R = dom R
26 |- B C_ B
26 |- 9 = ; 0 9
26 |- ( -v ` U ) = ( -v ` U )
26 |- ( U e. A -> U e. ( Base ` K ) )
26 |- ( Scalar ` T ) = ( Scalar ` T )
26 |- ( ph -> X C_ CC )
26 |- ( ph -> U e. ( SubGrp ` W ) )
26 |- ( ph -> S e. _V )
26 |- ( ph -> P e. ZZ )
26 |- ( ph -> 2 e. RR )
26 |- ( ph -> { X } C_ V )
26 |- ( ph -> ( LSubSp ` U ) C_ ( SubGrp ` U ) )
26 |- ( norm ` W ) = ( norm ` W )
26 |- ( N e. NN0 -> N e. RR )
26 |- ( n = N -> ( 1 ... n ) = ( 1 ... N ) )
26 |- ( M e. NN -> M e. ZZ )
26 |- ( J Om1 Y ) = ( J Om1 Y )
26 |- ( C e. RR -> C e. CC )
26 |- ( A e. ZZ -> A e. CC )
26 |- ( A e. dom arctan -> ( log ` ( 1 + ( _i x. A ) ) ) e. CC )
26 |- ( A e. ( 0 (,] 1 ) -> A e. RR )
26 |- ( 1o mPwSer R ) = ( 1o mPwSer R )
26 |- ( ||r ` R ) = ( ||r ` R )
26 |- ( _|_ ` H ) e. CH
26 |- ( .sOLD ` W ) = ( .sOLD ` W )
26 |- ( ( K e. OML /\ X e. B /\ Y e. B ) -> Y e. B )
25 |- 6 =/= 0
25 |- 0 <_ 2
25 |- ( y e. z -> A. x y e. z )
25 |- ( x = z -> ( F ` x ) = ( F ` z ) )
25 |- ( ph -> W e. NrmGrp )
25 |- ( ph -> S e. CC )
25 |- ( ph -> F e. CC )
25 |- ( ph -> E e. D )
25 |- ( ph -> 0 e. ZZ )
25 |- ( od ` G ) = ( od ` G )
25 |- ( o_ ` T ) = ( o_ ` T )
25 |- ( n e. NN -> n e. CC )
25 |- ( n e. NN -> ( Lam ` n ) e. RR )
25 |- ( MetOpen ` D ) = ( MetOpen ` D )
25 |- ( k e. NN0 -> k e. CC )
25 |- ( Base ` ( Scalar ` C ) ) = ( Base ` ( Scalar ` C ) )
25 |- ( B e. On -> Ord B )
25 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
25 |- ( 0vec ` W ) = ( 0vec ` W )
25 |- ( +v ` W ) = ( +v ` W )
25 |- ( +g ` O ) = ( +g ` O )
25 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. RR+ )
25 |- ( ( ph /\ x e. A ) -> if ( 0 <_ B , B , 0 ) e. RR )
25 |- ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( P .\/ Q ) ./\ W ) .<_ W )
25 |- ( ( DIsoC ` K ) ` W ) = ( ( DIsoC ` K ) ` W )
25 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
24 |- S : ~H --> ~H
24 |- n e. _V
24 |- K e. ( TopOn ` CC )
24 |- 2 = ; 0 2
24 |- ~H = ( BaseSet ` <. <. +h , .h >. , normh >. )
24 |- (/) = (/)
24 |- ( y e. RR -> y e. CC )
24 |- ( x = y -> ( F ` x ) = ( F ` y ) )
24 |- ( T. -> 1 e. RR )
24 |- ( Scalar ` ( ( LCDual ` K ) ` W ) ) = ( Scalar ` ( ( LCDual ` K ) ` W ) )
24 |- ( ph -> Z e. Ring )
24 |- ( ph -> S C_ ( SubGrp ` W ) )
24 |- ( ph -> ( B ^ 2 ) e. CC )
24 |- ( p e. A -> p e. B )
24 |- ( normCV ` W ) = ( normCV ` W )
24 |- ( N e. NN -> 0 < N )
24 |- ( LHyp ` K ) e. _V
24 |- ( k = K -> ( le ` k ) = .<_ )
24 |- ( -g ` R ) = ( -g ` R )
24 |- ( f = F -> ( f ` x ) = ( F ` x ) )
24 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
24 |- ( dist ` G ) = ( dist ` G )
24 |- ( 0 + 3 ) = 3
24 |- ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR )
24 |- ( ||r ` ( oppR ` R ) ) = ( ||r ` ( oppR ` R ) )
24 |- ( .r ` ( oppR ` R ) ) = ( .r ` ( oppR ` R ) )
24 |- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
24 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. RR )
24 |- ( ( ph /\ Y = Z /\ ps ) -> c e. A )
24 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
24 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> N e. NN )
24 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( P =/= Q /\ S =/= T ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ -. U .<_ ( S .\/ T ) ) ) -> K e. Lat )
23 |- -u ( pi / 2 ) e. RR
23 |- B C_ ( A u. B )
23 |- 7 = ( 6 + 1 )
23 |- ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
23 |- ( T. -> CC e. { RR , CC } )
23 |- ( T e. A -> T e. ( Base ` K ) )
23 |- ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` om ) = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` om )
23 |- ( ph -> U e. CC )
23 |- ( ph -> 0 e. CC )
23 |- ( ph -> ( Y .+ Z ) e. V )
23 |- ( norm ` T ) = ( norm ` T )
23 |- ( M e. NN -> M e. CC )
23 |- ( LSSum ` C ) = ( LSSum ` C )
23 |- ( k e. NN -> k e. RR )
23 |- ( k = K -> ( ( LTrn ` k ) ` w ) = ( ( LTrn ` K ) ` w ) )
23 |- ( I i^i I ) = I
23 |- ( A e. CC -> ( Im ` A ) e. CC )
23 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
23 |- ( ( ph /\ x e. A ) -> if ( 0 <_ -u B , -u B , 0 ) e. RR )
23 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) =/= 0 )
23 |- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> K e. Lat )
23 |- ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> K e. Lat )
23 |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. RR )
23 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ -. R .<_ ( P .\/ Q ) ) -> R e. A )
23 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( P =/= Q /\ S =/= T ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ -. U .<_ ( S .\/ T ) ) ) -> P e. A )
23 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( P =/= Q /\ S =/= T ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ -. U .<_ ( S .\/ T ) ) ) -> P =/= Q )
23 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> K e. HL )
22 |- U. L = U. L
22 |- suc A = ( A u. { A } )
22 |- D e. CC
22 |- 10 e. CC
22 |- { f e. ( LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } = { f e. ( LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
22 |- ( x e. X , y e. Y |-> `' ( { x } +c { y } ) ) = ( x e. X , y e. Y |-> `' ( { x } +c { y } ) )
22 |- ( x e. RR+ -> ( log ` x ) e. RR )
22 |- ( R maMul <. N , N , N >. ) = ( R maMul <. N , N , N >. )
22 |- ( ps -> A. y ps )
22 |- ( projh ` G ) : ~H --> ~H
22 |- ( ph -> X C_ S )
22 |- ( ph -> 3 =/= 0 )
22 |- ( LPlanes ` K ) = ( LPlanes ` K )
22 |- ( -g ` U ) = ( -g ` U )
22 |- ( a |` ( 1 ... N ) ) e. _V
22 |- ( 2nd ` A ) e. _V
22 |- ( 0g ` M ) = ( 0g ` M )
22 |- ( ~P A i^i Fin ) = ( ~P A i^i Fin )
22 |- ( .r ` Y ) = ( .r ` Y )
22 |- ( -. A. x x = y -> A. x -. A. x x = y )
22 |- ( *rf ` R ) = ( *rf ` R )
22 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
22 |- ( ( ph /\ ( i e. M /\ k e. O ) ) -> N e. Fin )
22 |- ( ( K e. OML /\ X e. B /\ Y e. B ) -> X e. B )
22 |- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> C e. ( N. X. N. ) )
22 |- ( ( 1 e. RR /\ 0 <_ 1 ) -> ( abs ` 1 ) = 1 )
22 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
21 |- -u 1 e. ZZ
21 |- M e. RR
21 |- M e. CC
21 |- dom R1 = On
21 |- 7 = ; 0 7
21 |- 5 = ( 4 + 1 )
21 |- 3 = ; 0 3
21 |- 0 e. ( 0 [,] +oo )
21 |- 0 = 0
21 |- <. A , A >. e. _V
21 |- { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V
21 |- ; 1 1 = ; 1 1
21 |- ( z e. A -> A. y z e. A )
21 |- ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
21 |- ( ph -> U. B = ( Base ` ( J Om1 Y ) ) )
21 |- ( ph -> T e. V )
21 |- ( ph -> Q e. CC )
21 |- ( ph -> F : RR --> RR )
21 |- ( ph -> E e. ( V \ { ( 0g ` U ) } ) )
21 |- ( ph -> ( B ` L ) e. Word ( I X. 2o ) )
21 |- ( p e. Prime -> p e. ZZ )
21 |- ( NN i^i NN ) = NN
21 |- ( n = k -> ( F ` n ) = ( F ` k ) )
21 |- ( M e. NN -> M e. RR )
21 |- ( LKer ` U ) = ( LKer ` U )
21 |- ( k = n -> ( F ` k ) = ( F ` n ) )
21 |- ( B e. ZZ -> B e. CC )
21 |- ( B e. CH -> ( _|_ ` B ) e. CH )
21 |- ( 1 e. RR -> 1 e. RR* )
21 |- ( 0g ` ( Scalar ` U ) ) = ( 0g ` ( Scalar ` U ) )
21 |- ( .s ` M ) = ( .s ` M )
21 |- ( ( U e. LMod /\ Y e. V ) -> ( N ` { Y } ) e. ( LSubSp ` U ) )
21 |- ( ( Q .\/ R ) .\/ P ) = ( ( Q .\/ R ) .\/ P )
21 |- ( ( mapd ` K ) ` W ) = ( ( mapd ` K ) ` W )
21 |- ( ( 0 e. RR /\ 1 e. RR ) -> ( 0 [,] 1 ) C_ RR )
21 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC )
21 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
21 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
21 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> P e. ( EE ` N ) )
21 |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( K e. HL /\ W e. H ) )
21 |- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> K e. HL )
21 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ -. R .<_ ( P .\/ Q ) ) -> Q e. A )
21 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) ) /\ -. R .<_ ( P .\/ Q ) ) -> P e. A )
21 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( ( P =/= Q /\ S =/= T ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) ) /\ R .<_ ( P .\/ Q ) ) ) -> K e. HL )
21 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( P =/= Q /\ S =/= T ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ -. U .<_ ( S .\/ T ) ) ) -> S e. A )
21 |- ( ( ( ( K e. HL /\ C e. ( Base ` K ) ) /\ ( Q e. A /\ R e. A /\ P e. A ) /\ ( T e. A /\ U e. A /\ S e. A ) ) /\ ( ( ( Q .\/ R ) .\/ P ) e. O /\ ( ( T .\/ U ) .\/ S ) e. O ) /\ ( ( -. C .<_ ( Q .\/ R ) /\ -. C .<_ ( R .\/ P ) /\ -. C .<_ ( P .\/ Q ) ) /\ ( -. C .<_ ( T .\/ U ) /\ -. C .<_ ( U .\/ S ) /\ -. C .<_ ( S .\/ T ) ) /\ ( C .<_ ( Q .\/ T ) /\ C .<_ ( R .\/ U ) /\ C .<_ ( P .\/ S ) ) ) ) <-> ( ( ( K e. HL /\ C e. ( Base ` K ) ) /\ ( Q e. A /\ R e. A /\ P e. A ) /\ ( T e. A /\ U e. A /\ S e. A ) ) /\ ( ( ( Q .\/ R ) .\/ P ) e. O /\ ( ( T .\/ U ) .\/ S ) e. O ) /\ ( ( -. C .<_ ( Q .\/ R ) /\ -. C .<_ ( R .\/ P ) /\ -. C .<_ ( P .\/ Q ) ) /\ ( -. C .<_ ( T .\/ U ) /\ -. C .<_ ( U .\/ S ) /\ -. C .<_ ( S .\/ T ) ) /\ ( C .<_ ( Q .\/ T ) /\ C .<_ ( R .\/ U ) /\ C .<_ ( P .\/ S ) ) ) ) )
20 |- D C_ CC
20 |- 6 = ( 5 + 1 )
20 |- 0p = ( CC X. { 0 } )
20 |- `' < Or RR
20 |- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
20 |- [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
20 |- ; 1 1 e. NN0
20 |- ( ZRHom ` Y ) = ( ZRHom ` Y )
20 |- ( z e. B -> A. y z e. B )
20 |- ( y e. NN -> y e. CC )
20 |- ( x e. RR+ -> x =/= 0 )
20 |- ( x e. ~P A -> x C_ A )
20 |- ( x e. ~P A <-> x C_ A )
20 |- ( x = y -> B = [_ y / x ]_ B )
20 |- ( x = y -> ( x e. A <-> y e. A ) )
20 |- ( x .N y ) = ( y .N x )
20 |- ( ph -> F Fn RR )
20 |- ( ph -> A. z ph )
20 |- ( ph -> [_ X / x ]_ B e. RR )
20 |- ( ph -> ( N ` { X } ) =/= ( N ` { Z } ) )
20 |- ( ph -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
20 |- ( ph -> ( C e. RR /\ 0 < C ) )
20 |- ( N e. NN -> N e. RR+ )
20 |- ( n e. NN -> ( n + 1 ) e. NN )
20 |- ( k e. NN -> k e. ZZ )
20 |- ( k = K -> ( LHyp ` k ) = H )
20 |- ( k = K -> ( Base ` k ) = B )
20 |- ( F : X --> Y -> dom F = X )
20 |- ( D e. ( *Met ` X ) -> X e. dom *Met )
20 |- ( Base ` ( Z/nZ ` N ) ) = ( Base ` ( Z/nZ ` N ) )
20 |- ( Base ` ( R ^s B ) ) = ( Base ` ( R ^s B ) )
20 |- ( 2 x. 0 ) = 0
20 |- ( 0 [,) +oo ) C_ RR*
20 |- ( 0 - 0 ) = 0
20 |- ( +g ` P ) = ( +g ` P )
20 |- ( .s ` T ) = ( .s ` T )
20 |- ( .s ` ( ( LCDual ` K ) ` W ) ) = ( .s ` ( ( LCDual ` K ) ` W ) )
20 |- ( .r ` W ) = ( .r ` W )
20 |- ( ( T .\/ U ) .\/ S ) = ( ( T .\/ U ) .\/ S )
20 |- ( ( ph /\ Y = Z /\ ps ) -> ( G .\/ H ) e. ( Base ` K ) )
20 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. CC )
20 |- ( ( K e. HL /\ Q e. A /\ R e. A ) -> ( Q .\/ R ) e. ( Base ` K ) )
20 |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> C e. RR )
20 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> F e. ( EE ` N ) )
20 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> d e. ( EE ` N ) )
20 |- ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) /\ ( S e. ( EE ` N ) /\ P =/= S ) ) /\ x e. ( EE ` N ) ) -> P e. ( EE ` N ) )
20 |- ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) /\ ( S e. ( EE ` N ) /\ P =/= S ) ) /\ x e. ( EE ` N ) ) -> N e. NN )
20 |- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> K e. Lat )
20 |- ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ P e. A ) -> ( G ` P ) e. A )
20 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> P =/= Q )
19 |- U. T = U. T
19 |- U. A = U. A
19 |- S C_ CC
19 |- ran H = ran H
19 |- K e. RR
19 |- A C_ ~H
19 |- 6 = ; 0 6
19 |- 4 = ; 0 4
19 |- 1o = suc (/)
19 |- +oo e. _V
19 |- { A , B } = ( { A } u. { B } )
19 |- ; 1 2 e. NN0
19 |- ( y e. ZZ -> y e. CC )
19 |- ( x e. HAtoms -> x e. CH )
19 |- ( x e. A -> A. y x e. A )
19 |- ( x e. ~H -> ( normh ` x ) e. RR )
19 |- ( w e. ( V \ { .0. } ) -> w e. V )
19 |- ( w = W -> ( ( LTrn ` K ) ` w ) = ( ( LTrn ` K ) ` W ) )
19 |- ( V e. A -> V e. ( Base ` K ) )
19 |- ( U e. LMod -> ( LSubSp ` U ) C_ ( SubGrp ` U ) )
19 |- ( U e. ( SubGrp ` G ) -> U C_ ( Base ` G ) )
19 |- ( ph -> L e. Top )
19 |- ( ph -> K e. RR+ )
19 |- ( ph -> K e. NN )
19 |- ( ph -> ( X .+ Y ) e. V )
19 |- ( n e. NN -> n e. RR+ )
19 |- ( LSubSp ` S ) = ( LSubSp ` S )
19 |- ( LSSum ` G ) = ( LSSum ` G )
19 |- ( k = K -> ( LHyp ` k ) = ( LHyp ` K ) )
19 |- ( Base ` U ) e. _V
19 |- ( Base ` N ) = ( Base ` N )
19 |- ( Base ` ( Scalar ` S ) ) = ( Base ` ( Scalar ` S ) )
19 |- ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) ) = ( Base ` ( Scalar ` ( ( LCDual ` K ) ` W ) ) )
19 |- ( B e. RR+ -> B e. RR )
19 |- ( A e. dom arctan -> ( log ` ( 1 - ( _i x. A ) ) ) e. CC )
19 |- ( a ` M ) e. _V
19 |- ( 1 x. 2 ) = 2
19 |- ( 0g ` F ) = ( 0g ` F )
19 |- ( +g ` F ) = ( +g ` F )
19 |- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` n ) / n ) e. CC )
19 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) =/= 0 )
19 |- ( ( T : ~H --> ~H /\ x e. ~H ) -> ( T ` x ) e. ~H )
19 |- ( ( Scalar ` R ) Xs_ `' ( { R } +c { S } ) ) = ( ( Scalar ` R ) Xs_ `' ( { R } +c { S } ) )
19 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. RR )
19 |- ( ( ph /\ m e. ( 1 [,) 3 ) ) -> ( ph /\ m e. RR+ ) )
19 |- ( ( K e. HL /\ S e. A /\ T e. A ) -> ( S .\/ T ) e. ( Base ` K ) )
19 |- ( ( K e. HL /\ R e. A /\ S e. A ) -> ( R .\/ S ) e. ( Base ` K ) )
19 |- ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> X e. B )
19 |- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> A e. ( N. X. N. ) )
19 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. NN0 )
19 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. CC )
19 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> G e. ( EE ` N ) )
19 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> E e. ( EE ` N ) )
19 |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> N e. Fin )
19 |- ( ( ( K e. HL /\ W e. H ) /\ ( G e. T /\ X e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( K e. HL /\ W e. H ) )
19 |- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) -> F e. A )
19 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> K e. HL )
19 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) )
19 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ P =/= Q ) /\ ( ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) /\ -. ( R ` F ) .<_ ( P .\/ Q ) /\ -. ( R ` G ) .<_ ( P .\/ Q ) ) ) -> ( K e. HL /\ W e. H ) )
18 |- ran f e. _V
18 |- dom f e. _V
18 |- <. x , y >. e. _V
18 |- ; 1 3 = ; 1 3
18 |- -. x e. (/)
18 |- ( x e. RR -> x e. CC )
18 |- ( w = W -> ( Base ` w ) = V )
18 |- ( TopOpen ` R ) = ( TopOpen ` R )
18 |- ( Scalar ` P ) = ( Scalar ` P )
18 |- ( S e. ( SubGrp ` G ) -> S C_ ( Base ` G ) )
18 |- ( ph -> U e. NrmCVec )
18 |- ( ph -> RR C_ CC )
18 |- ( ph -> P e. Prime )
18 |- ( ph -> om e. On )
18 |- ( ph -> 4 e. CC )
18 |- ( ph -> ( log ` Z ) e. CC )
18 |- ( M e. NN -> N e. CC )
18 |- ( LSpan ` C ) = ( LSpan ` C )
18 |- ( K e. ZZ -> K e. RR )
18 |- ( k = K -> ( ( DVecH ` k ) ` w ) = ( ( DVecH ` K ) ` w ) )
18 |- ( -g ` C ) = ( -g ` C )
18 |- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
18 |- ( d = D -> dom d = dom D )
18 |- ( CC \ { 0 } ) = ( Unit ` CCfld )
18 |- ( 3 e. CC /\ 3 =/= 0 )
18 |- ( 2 x. pi ) e. RR
18 |- ( 1r ` W ) = ( 1r ` W )
18 |- ( 1 e. RR -> ( 1 / 2 ) e. RR )
18 |- ( .r ` O ) = ( .r ` O )
18 |- ( ( W e. LMod /\ X e. V /\ Y e. V ) -> W e. LMod )
18 |- ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. CC )
18 |- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> X e. B )
18 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> A e. CC )
18 |- ( ( A : NN0 --> CC /\ k e. NN0 ) -> ( A ` k ) e. CC )
18 |- ( ( -. A. x x = y /\ -. A. x x = z ) -> A. x ( -. A. x x = y /\ -. A. x x = z ) )
18 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ X e. ( EE ` N ) ) ) -> N e. NN )
18 |- ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) /\ ( S e. ( EE ` N ) /\ P =/= S ) ) /\ x e. ( EE ` N ) ) -> S e. ( EE ` N ) )
18 |- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) -> Q e. A )
18 |- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ D e. T ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( F =/= ( _I |` B ) /\ D =/= ( _I |` B ) /\ ( R ` D ) =/= ( R ` F ) ) ) -> ( K e. HL /\ W e. H ) )
18 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ P =/= Q ) /\ ( ( G ` P ) =/= P /\ ( R ` G ) .<_ ( P .\/ Q ) /\ -. E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> ( K e. HL /\ W e. H ) )
18 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( P =/= Q /\ S =/= T ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ -. U .<_ ( S .\/ T ) ) ) -> ( K e. HL /\ W e. H ) )
18 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> K e. Lat )
18 |- ( ( ( ( F ` P ) e. CC /\ ( F ` P ) =/= ( F ` R ) ) /\ ( ( F ` Q ) e. CC /\ ( F ` R ) e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( F ` P ) e. CC )
17 |- R. = ( ( P. X. P. ) /. ~R )
17 |- R e. CC
17 |- Lim dom R1
17 |- K e. _V
17 |- i e. _V
17 |- G e. SH
17 |- B = ( Base ` ( mulGrp ` R ) )
17 |- 9 =/= 0
17 |- 8 = ; 0 8
17 |- ; 2 5 e. NN0
17 |- ; 2 3 = ; 2 3
17 |- ; 1 3 e. NN0
17 |- ( z e. [_ y / x ]_ B -> A. x z e. [_ y / x ]_ B )
17 |- ( x e. RR+ -> ( x e. CC /\ x =/= 0 ) )
17 |- ( x e. RR -> x e. RR* )
17 |- ( x e. On -> Ord x )
17 |- ( x e. ( 2 [,) +oo ) -> x e. RR+ )
17 |- ( x = y -> { x } = { y } )
17 |- ( x = A -> { x } = { A } )
17 |- ( U normOpOLD W ) = ( U normOpOLD W )
17 |- ( topGen ` ran (,) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
17 |- ( T. -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
17 |- ( RLReg ` R ) = ( RLReg ` R )
17 |- ( R1 Fn On -> dom R1 = On )
17 |- ( ph -> s e. D )
17 |- ( ph -> ran G = X )
17 |- ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
17 |- ( ph -> G : B --> A )
17 |- ( ph -> F Fn V )
17 |- ( ph -> E e. RR )
17 |- ( ph -> [_ X / x ]_ B e. CC )
17 |- ( ph -> ( N ` { X } ) e. ( SubGrp ` W ) )
17 |- ( ph -> ( N ` { X , Y } ) e. ( LSubSp ` U ) )
17 |- ( ph -> ( M ` ( N ` { Y } ) ) = ( J ` { G } ) )
17 |- ( ph -> ( E .+ G ) e. F )
17 |- ( ph -> ( ( P - 1 ) / 2 ) e. NN0 )
17 |- ( P e. ( Prime \ { 2 } ) -> ( ( P - 1 ) / 2 ) e. NN )
17 |- ( norm ` G ) = ( norm ` G )
17 |- ( K e. Top <-> K e. ( TopOn ` Y ) )
17 |- ( k e. NN0 -> ( k + 1 ) e. NN0 )
17 |- ( k = K -> ( Atoms ` k ) = A )
17 |- ( -g ` P ) = ( -g ` P )
17 |- ( F ` y ) e. _V
17 |- ( F : RR --> RR -> F Fn RR )
17 |- ( dist ` R ) = ( dist ` R )
17 |- ( coe1 ` G ) = ( coe1 ` G )
17 |- ( Cntz ` W ) = ( Cntz ` W )
17 |- ( C e. RR -> C e. RR* )
17 |- ( BaseSet ` U ) = ( BaseSet ` <. <. +h , .h >. , normh >. )
17 |- ( Base ` ( Scalar ` D ) ) = ( Base ` ( Scalar ` D ) )
17 |- ( A e. CH -> A e. SH )
17 |- ( A e. CC -> ( Re ` A ) e. CC )
17 |- ( A e. ( ZZ>= ` 2 ) -> A e. RR )
17 |- ( 2nd ` C ) e. _V
17 |- ( 2 x. 3 ) = 6
17 |- ( 1st ` S ) = ( 1st ` S )
17 |- ( 0g ` G ) e. _V
17 |- ( < Or RR <-> `' < Or RR )
17 |- ( +f ` G ) = ( +f ` G )
17 |- ( _i x. pi ) e. CC
17 |- ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) )
17 |- ( ( x e. CC /\ y e. CC ) -> ( x x. y ) e. CC )
17 |- ( ( x .N y ) .N z ) = ( x .N ( y .N z ) )
17 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR+ )
17 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR )
17 |- ( ( ph /\ x e. A ) -> if ( 0 <_ C , C , 0 ) e. RR )
17 |- ( ( ph /\ x e. A ) -> ( abs ` B ) e. RR )
17 |- ( ( P .\/ Q ) ./\ W ) = ( ( P .\/ Q ) ./\ W )
17 |- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> N e. NN )
17 |- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
17 |- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
17 |- ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR )
17 |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. RR )
17 |- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> B e. ( N. X. N. ) )
17 |- ( ( A e. CC /\ k e. NN0 ) -> ( A ^ k ) e. CC )
17 |- ( ( 0 e. RR /\ +oo e. RR* ) -> ( 0 [,) +oo ) C_ RR )
17 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> D e. ( EE ` N ) )
17 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
17 |- ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) /\ ( S e. ( EE ` N ) /\ P =/= S ) ) /\ x e. ( EE ` N ) ) -> Q e. ( EE ` N ) )
17 |- ( ( ( K e. HL /\ X e. S /\ Y e. S ) /\ ( Z e. S /\ W e. S ) ) -> K e. HL )
17 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( P =/= Q /\ S =/= T ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ -. U .<_ ( S .\/ T ) ) ) -> W e. H )
17 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( P =/= Q /\ S =/= T ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ -. U .<_ ( S .\/ T ) ) ) -> T e. A )
17 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( P =/= Q /\ S =/= T ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ -. U .<_ ( S .\/ T ) ) ) -> ( Q e. A /\ -. Q .<_ W ) )
17 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( P =/= Q /\ S =/= T ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ -. U .<_ ( S .\/ T ) ) ) -> ( P e. A /\ -. P .<_ W ) )
17 |- ( ( ( ( F ` P ) e. CC /\ ( F ` P ) =/= ( F ` R ) ) /\ ( ( F ` Q ) e. CC /\ ( F ` R ) e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( F ` R ) e. CC )
16 |- x e. { x }
16 |- U e. _V
16 |- RR e. { RR , CC }
16 |- Pred ( R , A , X ) = ( A i^i ( `' R " { X } ) )
16 |- if ( A e. CH , A , 0H ) e. CH
16 |- C e. SH
16 |- 8 =/= 0
16 |- 3 e. _V
16 |- 0 = ; 0 0
16 |- .x. = ( +g ` ( mulGrp ` R ) )
16 |- ( ZZ>= ` N ) = ( ZZ>= ` N )
16 |- ( z e. C -> A. x z e. C )
16 |- ( y e. RR+ -> y e. RR )
16 |- ( y e. ~H -> ( normh ` y ) e. RR )
16 |- ( y = x <-> x = y )
16 |- ( X i^i Y ) C_ Y
16 |- ( x e. ZZ -> x e. RR )
16 |- ( x e. RR -> ( psi ` x ) e. RR )
16 |- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
16 |- ( Unit ` ( Z/nZ ` N ) ) = ( Unit ` ( Z/nZ ` N ) )
16 |- ( T e. ( SubGrp ` G ) -> T C_ ( Base ` G ) )
16 |- ( S e. _V -> dom S e. _V )
16 |- ( r e. RR+ -> r e. RR )
16 |- ( pi / 2 ) e. RR*
16 |- ( ph -> W e. Abel )
16 |- ( ph -> S e. DivRing )
16 |- ( ph -> RR e. { RR , CC } )
16 |- ( ph -> ran F = B )
16 |- ( ph -> L e. ( TopOn ` U. L ) )
16 |- ( ph -> K e. ( TopOn ` U. K ) )
16 |- ( ph -> K e. ( SubGrp ` G ) )
16 |- ( ph -> E e. RR+ )
16 |- ( ph -> { Y } C_ V )
16 |- ( ph -> ( ( x e. A |-> ( Re ` B ) ) e. L^1 /\ ( x e. A |-> ( Im ` B ) ) e. L^1 ) )
16 |- ( ph -> ( ( ( M ^ 2 ) / 2 ) / 2 ) e. RR )
16 |- ( oppR ` F ) = ( oppR ` F )
16 |- ( norm ` S ) = ( norm ` S )
16 |- ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
16 |- ( n e. NN -> n e. RR )
16 |- ( n e. NN -> n =/= 0 )
16 |- ( mrCls ` C ) = ( mrCls ` C )
16 |- ( M e. NN0 -> M e. RR )
16 |- ( log ` 2 ) e. CC
16 |- ( k e. NN0 -> ( ! ` k ) e. NN )
16 |- ( k = K -> ( le ` k ) = ( le ` K ) )
16 |- ( k = j -> ( F ` k ) = ( F ` j ) )
16 |- ( J e. ( TopOn ` X ) -> F Fn X )
16 |- ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = E ) ) = ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = E ) )
16 |- ( invg ` S ) = ( invg ` S )
16 |- ( invg ` H ) = ( invg ` H )
16 |- ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) = ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) )
16 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
16 |- ( D e. ( NN \ []NN ) -> D e. NN )
16 |- ( C e. NN -> C e. CC )
16 |- ( A e. dom arctan -> _i e. CC )
16 |- ( A e. CC -> ( sqr ` ( 1 - ( A ^ 2 ) ) ) e. CC )
16 |- ( A C_ B -> ( x e. A -> x e. B ) )
16 |- ( 2nd ` S ) = ( 2nd ` S )
16 |- ( 1 e. ZZ -> -u 1 e. ZZ )
16 |- ( 0g ` R ) e. _V
16 |- ( .r ` Z ) = ( .r ` Z )
16 |- ( .r ` A ) = ( .r ` A )
16 |- ( .r ` ( Scalar ` W ) ) = ( .r ` ( Scalar ` W ) )
16 |- ( *r ` F ) = ( *r ` F )
16 |- ( ( x e. CC /\ y e. CC ) -> ( x + y ) e. CC )
16 |- ( ( U e. NrmCVec /\ k e. ( 1 ... 4 ) ) -> J e. ( TopOn ` ( BaseSet ` U ) ) )
16 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 2 e. CC )
16 |- ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) ) = ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) )
16 |- ( ( ph \/ ps ) <-> ( -. ph -> ps ) )
16 |- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> f : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
16 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> F : A --> B )
16 |- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ X e. ( EE ` N ) /\ Y e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
16 |- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
16 |- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
16 |- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> X e. B )
16 |- ( ( K e. HL /\ ( X e. B /\ P e. A /\ Q e. A ) ) -> Q e. B )
16 |- ( ( abs o. - ) o. F ) = ( ( abs o. - ) o. F )
16 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY N ) e. CC )
16 |- ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> x e. RR )
16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
16 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) ) ) -> N e. NN )
16 |- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( ( R =/= P /\ R .<_ ( P .\/ Q ) ) /\ ( P .<_ X /\ Q .<_ Y ) /\ ( ( F ` Y ) e. N /\ ( X ./\ Y ) e. A /\ -. Q .<_ X ) ) ) -> K e. Lat )
16 |- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` F ) e. ( Base ` K ) )
16 |- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ ( R e. A /\ -. R .<_ W ) ) ) -> K e. Lat )
16 |- ( ( ( K e. HL /\ P .<_ ( Q .\/ R ) /\ ( ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( R .\/ U ) ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A /\ U e. A ) ) -> K e. Lat )
16 |- ( ( ( c e. A /\ d e. A ) /\ -. c .<_ ( ( Q .\/ R ) .\/ P ) /\ ( d =/= c /\ -. d .<_ ( ( Q .\/ R ) .\/ P ) /\ C .<_ ( c .\/ d ) ) ) <-> ( ( c e. A /\ d e. A ) /\ -. c .<_ ( ( Q .\/ R ) .\/ P ) /\ ( d =/= c /\ -. d .<_ ( ( Q .\/ R ) .\/ P ) /\ C .<_ ( c .\/ d ) ) ) )
16 |- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\ ( ( A gcd B ) = 1 /\ -. 2 || A ) ) -> C e. CC )
16 |- ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> n e. NN )
16 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` X ) /\ b e. ( I ` X ) ) ) -> ( K e. HL /\ W e. H ) )
16 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> g e. T )
16 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) ) /\ ( X e. B /\ -. X .<_ W ) /\ ( S =/= T /\ ( S .\/ ( X ./\ W ) ) = X /\ ( T .\/ ( X ./\ W ) ) = X ) ) -> K e. Lat )
16 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ P =/= Q ) /\ ( ( G ` P ) =/= P /\ ( R ` G ) .<_ ( P .\/ Q ) /\ -. E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> G e. T )
16 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) /\ ( ( F ` P ) =/= P /\ ( R ` F ) = ( R ` G ) /\ ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) =/= ( P .\/ Q ) ) ) -> ( K e. HL /\ W e. H ) )
16 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( T e. A /\ -. T .<_ W ) /\ ( P =/= Q /\ S =/= T ) ) /\ ( -. S .<_ ( P .\/ Q ) /\ -. T .<_ ( P .\/ Q ) /\ -. U .<_ ( S .\/ T ) ) ) -> Q e. A )
16 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ R .<_ ( P .\/ Q ) /\ -. S .<_ ( P .\/ Q ) ) ) -> ( K e. HL /\ W e. H ) )
15 |- Z C_ RR
15 |- Y e. _V
15 |- U. y e. _V
15 |- -u -u 1 = 1
15 |- S e. SH
15 |- ran ( 1st ` S ) = ran ( 1st ` S )
15 |- p e. _V
15 |- C = ( Base ` T )
15 |- 2 e. _V
15 |- 10 = ( 9 + 1 )
15 |- 1 <_ 2
15 |- 0 <_ ( 1 / 2 )
15 |- { X } e. _V
15 |- ; A B = ( ( 10 x. A ) + B )
15 |- ; 2 5 = ; 2 5
15 |- ; 1 9 = ; 1 9
15 |- ( ZZ>= ` M ) = ( ZZ>= ` M )
15 |- ( y e. NN -> y e. ZZ )
15 |- ( X i^i Y ) C_ X
15 |- ( x e. X , y e. Y |-> `' ( { x } +c { y } ) ) : ( X X. Y ) -1-1-onto-> ran ( x e. X , y e. Y |-> `' ( { x } +c { y } ) )
15 |- ( x e. { A } -> x = A )
15 |- ( x e. ( 2 [,) +oo ) <-> ( x e. RR /\ 2 <_ x ) )
15 |- ( x = z -> x = z )
15 |- ( x = X -> x = X )
15 |- ( x = A -> ( x e. B <-> A e. B ) )
15 |- ( w = W -> ( ( DVecH ` K ) ` w ) = U )
15 |- ( var1 ` R ) = ( var1 ` R )
15 |- ( TopOpen ` K ) = ( TopOpen ` K )
15 |- ( T. -> J e. ( TopOn ` CC ) )
15 |- ( S normOp T ) = ( S normOp T )
15 |- ( R ^s B ) = ( R ^s B )
15 |- ( ph -> Y e. RR+ )
15 |- ( ph -> X e. RR+ )
15 |- ( ph -> W e. Grp )
15 |- ( ph -> P =/= 0 )
15 |- ( ph -> m e. NN )
15 |- ( ph -> K e. NN0 )
15 |- ( ph -> F e. Ring )
15 |- ( ph -> B e. Fin )
15 |- ( ph -> A. x e. S A e. RR )
15 |- ( ph -> A e. B )
15 |- ( ph -> ( x e. A |-> ( Re ` B ) ) e. L^1 )
15 |- ( ph -> ( x e. A |-> ( Im ` B ) ) e. L^1 )
15 |- ( ph -> ( log ` N ) e. CC )
15 |- ( ph -> ( I ` <. X , F , Z >. ) e. D )
15 |- ( ph -> ( dom F i^i dom G ) e. dom vol )
15 |- ( ph -> ( C ^ 2 ) e. CC )
15 |- ( ph -> ( 2 x. N ) e. RR )
15 |- ( ph -> ( ( RR _D F ) ` U ) e. RR )
15 |- ( p e. NN -> p e. RR+ )
15 |- ( p e. A -> p e. ( Base ` K ) )
15 |- ( p = K -> ( Base ` p ) = B )
15 |- ( om ~<_ A -> A e. _V )
15 |- ( n = m -> A = [_ m / n ]_ A )
15 |- ( mulGrp ` P ) = ( mulGrp ` P )
15 |- ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
15 |- ( LIdeal ` R ) = ( LIdeal ` R )
15 |- ( k e. NN0 -> k e. RR )
15 |- ( k e. A |-> B ) = ( k e. A |-> B )
15 |- ( k e. ( 0 ... 3 ) -> k e. ZZ )
15 |- ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( x ./\ W ) ) = x ) -> z = ( if ( s .<_ ( P .\/ Q ) , ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = E ) ) , [_ s / t ]_ D ) .\/ ( x ./\ W ) ) ) ) = ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( x ./\ W ) ) = x ) -> z = ( if ( s .<_ ( P .\/ Q ) , ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = E ) ) , [_ s / t ]_ D ) .\/ ( x ./\ W ) ) ) )
15 |- ( g = G -> ran g = X )
15 |- ( G ` x ) e. _V
15 |- ( -g ` S ) = ( -g ` S )
15 |- ( freeMnd ` ( I X. 2o ) ) = ( freeMnd ` ( I X. 2o ) )
15 |- ( deg ` F ) = ( deg ` F )
15 |- ( CC \ { 0 } ) C_ CC
15 |- ( C e. HAtoms -> C e. CH )
15 |- ( Base ` S ) e. _V
15 |- ( Base ` R ) = ( Base ` O )
15 |- ( Base ` P ) e. _V
15 |- ( A e. RR+ -> ( 1 / A ) e. RR )
15 |- ( A e. NN0 -> A e. ZZ )
15 |- ( A e. dom arctan -> ( 1 - ( _i x. A ) ) e. CC )
15 |- ( A e. CC -> ( _i x. ( Im ` A ) ) e. CC )
15 |- ( A e. ( ZZ>= ` 2 ) -> A e. ZZ )
15 |- ( A e. ( 0 (,] 1 ) <-> ( A e. RR /\ 0 < A /\ A <_ 1 ) )
15 |- ( 1st ` U ) = ( 1st ` U )
15 |- ( 1r ` Z ) = ( 1r ` Z )

Mario Carneiro

unread,

Jul 13, 2016, 12:56:19 PM7/13/16

to metamath

Very interesting. It would be nice to screen out those which are nominally one-step proofs, such as CC C_ CC which is not strictly one step because it is ssid[cc], but is one step ssid[] if syntax proofs are ignored. Adding a theorem specifically for CC C_ CC would seem odd because it doesn't actually decrease any step counts in the standard HTML display. The same is true for ( Base ` K ) = ( Base ` K ), which is eqid[] if you ignore the syntax proof but actually expands to eqid[cfv[cbs, cK]]. You should try searching for steps in 'show proof */lemmon' that have at least one hypothesis (because these are the only actual candidates for shrinking the proof).

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

Mario Carneiro

unread,

Jul 13, 2016, 1:28:55 PM7/13/16

to metamath

I did my own test along the lines I mention, results below. Since this doesn't keep track of the context of the theorem, there are many statements like ( ph -> U e. LMod ) which are probably not extractible into lemmas because they rely on different hypotheses (or even if they all come from the same hypotheses, there is still minimum one step needed to transform the needed hyps into the desired result). There are also some peculiarities like ( ( ph /\ ps /\ ch /\ th ) -> ta ) (which uses the four-branch AND w-bnj17 used only in JBN's mathbox) which I can only assume make their way to the top of the list because of some extreme repetition in the mathbox. (FYI I can guarantee that Norm's gigantic mathbox is the source of your (Base`K) = (Base`K); we don't usually use K for structures except for lattices, and Norm did a ton of work on lattices.)

But ignoring these, I see that 0 e. _V basically tops the list, so you are certainly on to something with your suggestion.

44 |- (/) = ( Base ` (/) )

34 |- ( Q e. A -> Q e. B )

     34 |- ( ph -> Z e. V )
     34 |- ( ph -> ( ps -> th ) )
     34 |- ( 2 e. CC /\ 2 =/= 0 )
     33 |- -. ph
     33 |- ( ph -> P e. A )
     33 |- ( ph -> A e. RR )
     32 |- V e. _V
     32 |- ( ph -> C e. LMod )

31 |- H e. _V

31 |- Fun F
 31 |- A e. _V
 31 |- 1o e. _V
 31 |- .0. e. _V
 31 |- ( ph -> N e. CC )
 31 |- ( ph -> M e. ZZ )
 31 |- ( 2 x. 1 ) = 2
 30 |- ps
 30 |- G e. _V
 30 |- 1 e. RR*
 30 |- ( ph -> Q e. A )
 30 |- ( ph -> N e. NN0 )
 30 |- ( ph -> 1 e. RR )
 30 |- ( ph -> 1 e. CC )
 30 |- ( ph -> 0 e. RR )
 30 |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
 30 |- ( abs ` 1 ) = 1
 29 |- ( ph -> N e. ZZ )
 29 |- ( J e. Top <-> J e. ( TopOn ` X ) )
 29 |- ( 1 / 1 ) = 1
 29 |- ( ( K e. Lat /\ X e. B /\ W e. B ) -> ( X ./\ W ) e. B )
 28 |- T e. _V
 28 |- ( ph -> U e. A )
 28 |- ( ph -> S e. A )
 28 |- ( ph -> K e. Top )
 28 |- ( ph -> G e. Grp )
 28 |- ( ph -> A C_ RR )
 28 |- ( 2 e. RR /\ 0 < 2 )
 28 |- ( _|_ ` A ) e. CH
 27 |- X = ran G
 27 |- 1 <_ 1
 27 |- ~H = ( BaseSet ` U )
 27 |- ( ph -> B e. CC )
 27 |- ( ph -> 2 e. CC )
 27 |- ( ph -> 1 e. ZZ )
 27 |- ( ( ph /\ ps ) -> ch )

27 |- ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) = ( Q .\/ P ) )

26 |- S e. _V
26 |- if ( B e. ~H , B , 0h ) e. ~H

26 |- ( U e. A -> U e. ( Base ` K ) )

     26 |- ( ph -> I e. _V )
     26 |- ( ph -> A = B )
     26 |- ( 1 / 2 ) e. RR
     26 |- ( 1 - 0 ) = 1

David A. Wheeler

unread,

Jul 13, 2016, 2:21:49 PM7/13/16

to metamath, metamath

On Wed, 13 Jul 2016 13:28:53 -0400, Mario Carneiro <di....@gmail.com> wrote:
> I did my own test along the lines I mention, results below.

Excellent!

I also continued in the same vein. Below is my tweaked code.
We're not analyzing exactly the same way, so there are some differences
in the list, but clearly some statements are continuously re-proved.

Using 'show proof ... /lemmon" is clearly a win.

> Since this
> doesn't keep track of the context of the theorem, there are many statements
> like ( ph -> U e. LMod ) which are probably not extractible into lemmas

> because they rely on different hypotheses...

Yes. But handling that would require more work. :-).

Below are the top repetitions (with 11 or more repeats) from my list
that seem useful to me (via a quick eyeball, some probably won't be sensible).
Tools could be modified to automate them... but perhaps it'd be better to simply
have tiny proofs for "really common cases" like these, so that the proof happens once
and people only need to see it once. They are:

80 |- 0 e. _V
70 |- -u 1 e. CC
61 |- 0 <_ 0
47 |- ( 0 + 1 ) = 1
46 |- 4 e. CC

44 |- (/) = ( Base ` (/) )

43 |- ( 1 x. 1 ) = 1
42 |- 1 e. _V
42 |- ( 1 - 1 ) = 0
29 |- pi e. CC
28 |- -u 1 e. RR
28 |- ( 2 x. 1 ) = 2
27 |- ( ph -> 0 e. RR )
27 |- ( abs ` 1 ) = 1
26 |- ( 2 e. CC /\ 2 =/= 0 )
26 |- ( 1 / 1 ) = 1
25 |- -u _i e. CC
25 |- 1 <_ 1
25 |- ( 2 e. RR /\ 0 < 2 )
24 |- ( 2 - 1 ) = 1
24 |- ( 1 - 0 ) = 1
22 |- ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
21 |- ( ph -> 1 e. RR )
20 |- ( ph -> 1 e. CC )
20 |- ( 1 + 0 ) = 1
19 |- 0 <_ 2
19 |- ( ph -> 1 e. ZZ )
19 |- ( ph -> ( C e. RR /\ 0 < C ) )
19 |- ( 2 x. 0 ) = 0
18 |- 6 e. CC
18 |- 4 =/= 0
17 |- -u pi e. RR

16 |- x e. { x }

16 |- -u 1 =/= 0

16 |- RR e. { RR , CC }

16 |- ( 0 - 0 ) = 0
15 |- -u -u 1 = 1
15 |- ( 1 + 2 ) = 3
15 |- ( _i x. 0 ) = 0
14 |- 7 e. CC
14 |- 3 e. ZZ
13 |- 5 e. CC
12 |- -u 1 e. ZZ
12 |- 9 e. CC
12 |- (/) e. { (/) }
12 |- ( U e. NrmCVec -> ( 1st ` U ) e. CVecOLD )
12 |- ( ph -> 0 e. CC )
12 |- ( 3 x. 1 ) = 3
12 |- ( 1 / 2 ) e. RR
12 |- ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* )
11 |- 8 e. CC
11 |- +oo e. _V
11 |- ( W e. LMod -> R e. Ring )
11 |- ( -u 1 x. -u 1 ) = 1
11 |- ( ph -> dom ( x e. A |-> B ) = A )
11 |- ( ph -> 2 e. CC )
11 |- ( N e. NN0 -> Z e. CRing )
11 |- ( K e. OP -> ( 0. ` K ) e. ( Base ` K ) )
11 |- ( G e. Grp -> ( 0g ` G ) e. X )
11 |- ( B X. B ) e. _V
11 |- ( 3 - 1 ) = 2
11 |- ( 1 + -u 1 ) = 0

--- David A. Wheeler

================================================

#!/bin/sh

# Quick analysis - what statements are repeatedly proved, but
# NOT top-level theorems/axioms?

# What are the top-level proven theorems/axioms?
metamath 'read set.mm' 'set width 9999' 'show statement *' quit | \
sed -e 's/ */ /g' | grep '^[1-9].*\$[ap]' | cut -d ' ' -f 4- | \
sed -e 's/ *\$= .*$//' > ,statements

# What's been proven at any step?

metamath 'read set.mm' 'set width 9999' 'show proof * /lemmon' quit | \
sed -e 's/ */ /g' | grep -E '^[0-9]+ [1-9][0-9,]* [^ ]* \$[ap] ' | \
cut -d ' ' -f 5- | \

David A. Wheeler

unread,

Jul 13, 2016, 2:26:51 PM7/13/16

to metamath

Here's my latest list, limited to the top 1000.

See my previous email for the code and the summarized
"probably more useful" list... but maybe people will disagree with what I extracted.
Again, some expressions like "0 e. _V" and "-u 1 e. CC" are repeatedly proved
inside larger proofs (80 times and 70 times respectively).

--- David A. Wheeler

======================

116 |- ( W e. H -> W e. ( Base ` K ) )
102 |- ( P e. A -> P e. ( Base ` K ) )
88 |- ( Q e. A -> Q e. ( Base ` K ) )

80 |- 0 e. _V
70 |- -u 1 e. CC

69 |- ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. ( Base ` K ) )

61 |- 0 <_ 0

58 |- ( R e. A -> R e. ( Base ` K ) )

47 |- ( 0 + 1 ) = 1
46 |- 4 e. CC

46 |- ( S e. A -> S e. ( Base ` K ) )

44 |- (/) = ( Base ` (/) )
43 |- ( 1 x. 1 ) = 1
42 |- 1 e. _V
42 |- ( 1 - 1 ) = 0

38 |- if ( A e. ~H , A , 0h ) e. ~H
34 |- ( Q e. A -> Q e. B )
34 |- ( J e. Top <-> J e. ( TopOn ` U. J ) )

31 |- H e. _V

29 |- pi e. CC

29 |- .0. e. _V
29 |- ( ph -> J e. Top )

28 |- -u 1 e. RR
28 |- ( 2 x. 1 ) = 2

28 |- ( ( K e. Lat /\ X e. B /\ W e. B ) -> ( X ./\ W ) e. B )
27 |- ( ph -> N e. NN0 )

27 |- ( ph -> 0 e. RR )
27 |- ( abs ` 1 ) = 1

27 |- ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) = ( Q .\/ P ) )
26 |- ( U e. A -> U e. ( Base ` K ) )
26 |- ( TopOpen ` CCfld ) e. ( TopOn ` CC )

26 |- ( 2 e. CC /\ 2 =/= 0 )
26 |- ( 1 / 1 ) = 1
25 |- -u _i e. CC

25 |- T e. _V
25 |- if ( B e. ~H , B , 0h ) e. ~H

25 |- 1 <_ 1
25 |- ( 2 e. RR /\ 0 < 2 )

25 |- ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( P .\/ Q ) ./\ W ) .<_ W )

25 |- ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( G ` P ) e. A /\ -. ( G ` P ) .<_ W ) )

24 |- ( 2 - 1 ) = 1
24 |- ( 1 - 0 ) = 1

23 |- ( T e. A -> T e. ( Base ` K ) )
23 |- ( ph -> I e. _V )
23 |- ( K e. Top <-> K e. ( TopOn ` U. K ) )
22 |- V e. _V

22 |- ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
21 |- ( ph -> 1 e. RR )

21 |- ( ( U e. LMod /\ Y e. V ) -> ( N ` { Y } ) e. ( LSubSp ` U ) )

20 |- ( x e. ~P A <-> x C_ A )
20 |- ( ph -> N e. CC )

20 |- ( ph -> 1 e. CC )

20 |- ( p e. A -> p e. B )
20 |- ( k = K -> ( LHyp ` k ) = H )

20 |- ( 1 + 0 ) = 1

20 |- ( ( K e. HL /\ Q e. A /\ R e. A ) -> ( Q .\/ R ) e. ( Base ` K ) )

20 |- ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ P e. A ) -> ( G ` P ) e. A )

19 |- 0 <_ 2

19 |- ( U e. LMod -> ( LSubSp ` U ) C_ ( SubGrp ` U ) )

19 |- ( U e. ( SubGrp ` G ) -> U C_ ( Base ` G ) )
19 |- ( ph -> K e. Top )

19 |- ( ph -> 1 e. ZZ )
19 |- ( ph -> ( C e. RR /\ 0 < C ) )
19 |- ( 2 x. 0 ) = 0

19 |- ( ( K e. HL /\ S e. A /\ T e. A ) -> ( S .\/ T ) e. ( Base ` K ) )
19 |- ( ( K e. HL /\ R e. A /\ S e. A ) -> ( R .\/ S ) e. ( Base ` K ) )

18 |- 6 e. CC
18 |- 4 =/= 0

18 |- ( V e. A -> V e. ( Base ` K ) )

17 |- -u pi e. RR

17 |- K e. _V

17 |- dom R1 = On

17 |- B = ( Base ` ( mulGrp ` R ) )

16 |- x e. { x }
16 |- -u 1 =/= 0
16 |- RR e. { RR , CC }

16 |- if ( A e. CH , A , 0H ) e. CH

16 |- dom f e. _V
16 |- { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V

16 |- .x. = ( +g ` ( mulGrp ` R ) )

16 |- ( ph -> Y e. V )
16 |- ( ph -> N e. ZZ )
16 |- ( ph -> { X } C_ V )

16 |- ( 0 - 0 ) = 0

16 |- ( _|_ ` B ) e. CH
16 |- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` F ) e. ( Base ` K ) )
15 |- Z e. _V

15 |- -u -u 1 = 1

15 |- N e. CC
15 |- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
15 |- ( ph -> ( N ` { Y } ) e. ( LSubSp ` U ) )

15 |- ( 1 + 2 ) = 3
15 |- ( _i x. 0 ) = 0

15 |- ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld )
15 |- ( ( K e. HL /\ T e. A /\ U e. A ) -> ( T .\/ U ) e. ( Base ` K ) )
15 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. NN0 )
15 |- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) -> F e. A )
14 |- CC = U. ( TopOpen ` CCfld )

14 |- 7 e. CC
14 |- 3 e. ZZ

14 |- `' < Or RR
14 |- ( T e. ( SubGrp ` G ) -> T C_ ( Base ` G ) )
14 |- ( S e. ( SubGrp ` G ) -> S C_ ( Base ` G ) )
14 |- ( ph -> M e. CC )
14 |- ( ph -> A C_ RR )
14 |- ( K e. Top <-> K e. ( TopOn ` Y ) )
14 |- ( ( ph /\ Y = Z /\ ps ) -> ( ( Q .\/ R ) .\/ P ) = ( ( T .\/ U ) .\/ S ) )
14 |- ( ( ph /\ Y = Z /\ ps ) -> ( ( c e. A /\ d e. A ) /\ -. c .<_ ( ( Q .\/ R ) .\/ P ) /\ ( d =/= c /\ -. d .<_ ( ( Q .\/ R ) .\/ P ) /\ C .<_ ( c .\/ d ) ) ) )
14 |- ( ( ph /\ Y = Z /\ ps ) -> ( ( ( K e. HL /\ C e. ( Base ` K ) ) /\ ( Q e. A /\ R e. A /\ P e. A ) /\ ( T e. A /\ U e. A /\ S e. A ) ) /\ ( ( ( Q .\/ R ) .\/ P ) e. O /\ ( ( T .\/ U ) .\/ S ) e. O ) /\ ( ( -. C .<_ ( Q .\/ R ) /\ -. C .<_ ( R .\/ P ) /\ -. C .<_ ( P .\/ Q ) ) /\ ( -. C .<_ ( T .\/ U ) /\ -. C .<_ ( U .\/ S ) /\ -. C .<_ ( S .\/ T ) ) /\ ( C .<_ ( Q .\/ T ) /\ C .<_ ( R .\/ U ) /\ C .<_ ( P .\/ S ) ) ) ) )
14 |- ( ( K e. Lat /\ P e. ( Base ` K ) /\ Q e. ( Base ` K ) ) -> ( P .\/ Q ) e. ( Base ` K ) )
14 |- ( ( K e. HL /\ P e. A /\ S e. A ) -> ( P .\/ S ) e. ( Base ` K ) )
13 |- U e. _V
13 |- ran f e. _V
13 |- N e. _V
13 |- if ( A e. CH , A , ~H ) e. CH

13 |- 5 e. CC

12 |- -u 1 e. ZZ

12 |- M e. _V
12 |- A e. U. ( R1 " On )

12 |- 9 e. CC
12 |- (/) e. { (/) }
12 |- ( U e. NrmCVec -> ( 1st ` U ) e. CVecOLD )

12 |- ( ph -> Y C_ X )
12 |- ( ph -> S C_ CC )
12 |- ( ph -> F Fn RR )

12 |- ( ph -> 0 e. CC )

12 |- ( ph -> ( B e. RR /\ 0 ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) )
12 |- ( Base ` R ) = ( Base ` O )

12 |- ( 3 x. 1 ) = 3
12 |- ( 1 / 2 ) e. RR
12 |- ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* )

11 |- 8 e. CC

11 |- 1o e. 2o

11 |- +oo e. _V
11 |- ( W e. LMod -> R e. Ring )
11 |- ( -u 1 x. -u 1 ) = 1

11 |- ( topGen ` ran (,) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
11 |- ( s e. _V -> [_ s / t ]_ D = ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) ) )
11 |- ( ph -> S e. _V )

11 |- ( ph -> dom ( x e. A |-> B ) = A )

11 |- ( ph -> D e. CC )

11 |- ( ph -> 2 e. CC )

11 |- ( ph -> ( I ` <. X , F , Z >. ) e. D )

11 |- ( N e. NN0 -> Z e. CRing )
11 |- ( K e. OP -> ( 0. ` K ) e. ( Base ` K ) )
11 |- ( G e. Grp -> ( 0g ` G ) e. X )
11 |- ( B X. B ) e. _V
11 |- ( 3 - 1 ) = 2
11 |- ( 1 + -u 1 ) = 0

11 |- ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. ( LSubSp ` W ) )
11 |- ( ( TopOpen ` CCfld ) e. Top -> ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld ) )
11 |- ( ( K e. OP /\ Y e. B ) -> ( ._|_ ` Y ) e. B )
11 |- ( ( K e. HL /\ Q e. A ) -> ( Q .\/ Q ) = Q )
11 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY N ) e. ZZ )
11 |- ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ `' F e. T ) -> ( G o. `' F ) e. T )
11 |- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( T e. A /\ -. T .<_ W ) ) /\ ( P =/= Q /\ -. T .<_ ( P .\/ Q ) ) ) -> G e. A )
10 |- x. = ( +g ` ( mulGrp ` CCfld ) )
10 |- X = ran ( +v ` U )
10 |- U = ( LSubSp ` ( ringLMod ` R ) )
10 |- if ( B e. CH , B , ~H ) e. CH
10 |- dom + = ( CC X. CC )
10 |- B e. SH
10 |- 1st : _V --> _V
10 |- 0 e. ( 0 [,) +oo )
10 |- 0 =/= 1
10 |- `' < Or RR*
10 |- ( x _I y <-> x = y )
10 |- ( -u 1 ^ 2 ) = ( 1 ^ 2 )
10 |- ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
10 |- ( R e. Ring -> ( 1r ` R ) e. B )
10 |- ( ph -> Z e. V )
10 |- ( ph -> R e. _V )
10 |- ( ph -> L e. Top )
10 |- ( ph -> 1o e. On )
10 |- ( ph -> ( X .- Y ) e. V )
10 |- ( p e. A -> p e. ( Base ` K ) )
10 |- ( L e. Top <-> L e. ( TopOn ` U. L ) )
10 |- ( k e. Z -> k e. ZZ )
10 |- ( k = K -> ( le ` k ) = .<_ )
10 |- ( 2 x. _i ) e. CC
10 |- ( _|_ ` H ) e. CH
10 |- ( -. ps -> A. x -. ps )
10 |- ( ( W e. LMod /\ Y e. V ) -> ( N ` { Y } ) e. ( LSubSp ` W ) )
10 |- ( ( U e. LMod /\ X e. V ) -> ( N ` { X } ) e. ( LSubSp ` U ) )
10 |- ( ( pi / 2 ) + ( pi / 2 ) ) = pi
10 |- ( ( K e. OP /\ Y e. B ) -> ( ( oc ` K ) ` Y ) e. B )
10 |- ( ( ( K e. HL /\ W e. H ) /\ G e. T ) -> ( R ` G ) e. ( Base ` K ) )
10 |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ Q e. A ) -> ( F ` ( G ` Q ) ) e. A )
9 |- -u ( _i x. _i ) = -u -u 1
9 |- -oo =/= +oo
9 |- -oo < 0
9 |- om ~~ NN
9 |- J e. _V
9 |- if ( T : ~H --> ~H , T , 0hop ) : ~H --> ~H
9 |- CC e. { RR , CC }
9 |- B C_ ( A vH B )
9 |- B = ( Base ` ( 1o mPoly R ) )
9 |- 6 = ; 0 6
9 |- 5 = ; 0 5
9 |- 3 e. _V
9 |- ; 1 2 e. NN
9 |- (/) e. 2o
9 |- (,) Fn ( RR* X. RR* )
9 |- ( x e. A -> ( ph -> ps ) )
9 |- ( W e. LMod -> ( Scalar ` W ) e. Ring )
9 |- ( W e. LMod -> ( LSubSp ` W ) C_ ( SubGrp ` W ) )
9 |- ( U e. LVec -> S e. DivRing )
9 |- ( -u 1 x. -u 1 ) = ( 1 x. 1 )
9 |- ( T. -> 1 e. CC )
9 |- ( RR X. RR ) e. _V
9 |- ( r e. A -> r e. ( Base ` K ) )
9 |- ( pi / 2 ) e. RR*
9 |- ( pi / 2 ) e. CC
9 |- ( ph -> V e. _V )
9 |- ( ph -> V .<_ W )
9 |- ( ph -> N e. RR )
9 |- ( ph -> N =/= 0 )
9 |- ( ph -> D e. _V )
9 |- ( ph -> A. x e. A B e. V )
9 |- ( ph -> { Y } C_ V )
9 |- ( ph -> { X , Y } C_ V )
9 |- ( ph -> ( Y .+ Z ) e. V )
9 |- ( K e. OP -> .0. e. ( Base ` K ) )
9 |- ( k = K -> ( Base ` k ) = B )
9 |- ( k = K -> ( ( LTrn ` k ) ` w ) = ( ( LTrn ` K ) ` w ) )
9 |- ( j e. Z -> j e. ZZ )
9 |- ( F e. ( Poly ` S ) -> ( coeff ` F ) : NN0 --> CC )
9 |- ( CC \ { 0 } ) = ( Unit ` CCfld )
9 |- ( 2 x. _i ) =/= 0
9 |- ( 2 x. ( 1 / 2 ) ) = 1
9 |- ( .r ` R ) = ( +g ` ( mulGrp ` R ) )
9 |- ( ( U e. LMod /\ X e. V /\ Y e. V ) -> ( X .- Y ) e. V )
9 |- ( ( K e. Lat /\ P e. B /\ Q e. B ) -> ( P .\/ Q ) e. B )
9 |- ( ( K e. HL /\ P e. A /\ U e. A ) -> ( P .\/ U ) e. ( Base ` K ) )
9 |- ( ( -. A. z z = x /\ -. A. z z = y ) -> ( x = y -> A. z x = y ) )
9 |- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> F : ( Base ` K ) -1-1-onto-> ( Base ` K ) )
9 |- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( R ./\ W ) = ( 0. ` K ) )
9 |- - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )

8 |- ZZ = ( Base ` ( CCfld |`s ZZ ) )

8 |- Z C_ ZZ
8 |- y e. suc y
8 |- x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
8 |- x. = ( .r ` ( CCfld |`s ZZ ) )
8 |- -u ( pi / 2 ) e. RR*
8 |- -u ( pi / 2 ) e. RR
8 |- R e. _V
8 |- P = ( ( I mPwSer R ) |`s ( Base ` P ) )
8 |- normh e. _V
8 |- N e. RR
8 |- L e. _V
8 |- if ( B e. CH , B , 0H ) e. CH
8 |- dom +h = ( ~H X. ~H )
8 |- dom ( dom_ ` T ) e. _V
8 |- D e. CC
8 |- 2 e. ( ZZ>= ` 1 )
8 |- 1 e. QQ
8 |- 1 = ( 0g ` ( mulGrp ` CCfld ) )
8 |- ~P V e. _V
8 |- [_ s / t ]_ D = ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) )
8 |- -. +oo e. RR
8 |- (/) =/= 1o
8 |- ( ZZ e. ( SubRing ` CCfld ) -> ZZ = ( Base ` ( CCfld |`s ZZ ) ) )
8 |- ( Y e. N -> Y e. ( Base ` K ) )
8 |- ( y `' R x <-> x R y )
8 |- ( x e. ~H -> ( T ` x ) e. ~H )
8 |- ( W e. LVec -> ( Scalar ` W ) e. DivRing )
8 |- ( -u 1 ^ 2 ) = 1
8 |- ( TopOpen ` CCfld ) e. Top
8 |- ( T. -> 2 e. CC )
8 |- ( T. -> 1 e. RR )
8 |- ( T. -> ( ringLMod ` R ) = ( ( subringAlg ` R ) ` ( Base ` R ) ) )
8 |- ( T. -> ( Base ` R ) C_ ( Base ` R ) )
8 |- ( S e. A -> S e. B )
8 |- ( projh ` G ) : ~H --> ~H
8 |- ( ph -> X e. _V )
8 |- ( ph -> V e. ( Base ` K ) )
8 |- ( ph -> U e. ( LSubSp ` W ) )
8 |- ( ph -> RR e. { RR , CC } )
8 |- ( ph -> ran F C_ ( ( Cntz ` G ) ` ran F ) )
8 |- ( ph -> G e. _V )
8 |- ( ph -> 0 e. ZZ )
8 |- ( ph -> ( N ` { Y } ) e. ( LSubSp ` W ) )
8 |- ( ph -> ( N ` { X } ) =/= ( N ` { Z } ) )
8 |- ( ph -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
8 |- ( ph -> ( A [,] B ) C_ RR )
8 |- ( ph -> ( `' F " ( _V \ 1o ) ) e. _V )
8 |- ( ph -> ( ( Scalar ` R ) Xs_ `' ( { R } +c { S } ) ) e. _V )
8 |- ( ph -> ( ( N ` { X } ) =/= ( N ` { Z } ) /\ -. Y e. ( N ` { X , Z } ) ) )
8 |- ( ph -> ( ( N ` { X } ) =/= ( N ` { Y } ) /\ -. Z e. ( N ` { X , Y } ) ) )
8 |- ( p e. ( Atoms ` K ) -> p e. ( Base ` K ) )
8 |- ( k e. ZZ -> ( _i ^ k ) =/= 0 )
8 |- ( k = K -> ( join ` k ) = .\/ )
8 |- ( F e. ( J Cn K ) -> F : U. J --> U. K )
8 |- ( Base ` P ) = ( Base ` ( 1o mPoly R ) )
8 |- ( B ^ 2 ) = ( B x. B )
8 |- ( abs ` -u 1 ) = 1
8 |- ( abs ` -u 1 ) = ( abs ` 1 )

8 |- ( A e. CC -> ( _i x. A ) e. CC )

8 |- ( 2 x. pi ) e. CC
8 |- ( 1 ... M ) = ( 1 ... ( N + 1 ) )
8 |- ( 0 <_ 1 -> ( abs ` 1 ) = 1 )
8 |- ( +v ` U ) = ( 1st ` ( 1st ` U ) )
8 |- ( -. R e. _V -> B = (/) )
8 |- ( ( U e. LMod /\ Y e. V /\ Z e. V ) -> ( Y .+ Z ) e. V )
8 |- ( ( ph /\ x e. A ) -> C e. CC )
8 |- ( ( K e. OL /\ ( P .\/ Q ) e. ( Base ` K ) ) -> ( ( P .\/ Q ) ./\ ( 1. ` K ) ) = ( P .\/ Q ) )
8 |- ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( P .\/ Q ) ./\ W ) e. ( Base ` K ) )
8 |- ( ( K e. HL /\ R e. A /\ U e. A ) -> ( R .\/ U ) e. ( Base ` K ) )
8 |- ( ( K e. HL /\ R e. A /\ P e. A ) -> ( R .\/ P ) e. ( Base ` K ) )
8 |- ( ( K e. HL /\ Q e. A /\ R e. A ) -> ( Q .\/ R ) = ( R .\/ Q ) )
8 |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. CC )
8 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> A e. ZZ )
8 |- ( ( ( K e. HL /\ W e. H ) /\ X e. T /\ P e. A ) -> ( X ` P ) e. A )
8 |- ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ I e. T ) -> ( G o. I ) e. T )
8 |- ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( R ` G ) = ( ( P .\/ ( G ` P ) ) ./\ W ) )
8 |- ( ( ( K e. HL /\ W e. H ) /\ G e. T ) -> ( R ` G ) .<_ W )
8 |- ( ( ( K e. HL /\ W e. H ) /\ { E } C_ V ) -> ( O ` { E } ) C_ V )
8 |- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( P .\/ W ) = ( 1. ` K ) )
7 |- ZZ = ( Base ` Z )
7 |- Z C_ CC
7 |- Y e. _V
7 |- x e. suc x
7 |- W e. _V
7 |- -u pi e. RR*
7 |- suc y e. _V
7 |- RR = U. J
7 |- ran G = ran ( 1st ` R )
7 |- pi =/= 0
7 |- Lim dom R1
7 |- if ( H e. CH , H , ~H ) e. CH
7 |- if ( A e. CC , A , 0 ) e. CC
7 |- if ( A e. _V , A , (/) ) e. _V
7 |- CC = U. J
7 |- CC = ran +
7 |- 2 e. _V
7 |- 2 e. ( ZZ>= ` 2 )
7 |- 10 e. CC
7 |- <. <. +h , .h >. , normh >. e. NrmCVec
7 |- .1. = ( 0g ` ( mulGrp ` R ) )
7 |- .~ e. _V
7 |- -. 1 <_ ( 1 / 2 )
7 |- -. 1 < 1
7 |- ( ZZ>= ` 2 ) = ( ZZ>= ` ( 1 + 1 ) )
7 |- ( ZZ e. ( SubRing ` CCfld ) -> ZZ = ( Base ` Z ) )
7 |- ( y i^i z ) e. _V
7 |- ( y e. ~P A <-> y C_ A )
7 |- ( x i^i y ) e. _V
7 |- ( x e. X , y e. Y |-> `' ( { x } +c { y } ) ) : ( X X. Y ) -1-1-onto-> ran ( x e. X , y e. Y |-> `' ( { x } +c { y } ) )
7 |- ( X e. N -> X e. ( Base ` K ) )
7 |- ( x e. dom A <-> E. y <. x , y >. e. A )
7 |- ( x e. ~P X <-> x C_ X )
7 |- ( W e. LMod -> D e. Ring )
7 |- ( W e. CMod -> 0 = ( 0g ` ( Scalar ` W ) ) )
7 |- ( w = W -> ( ( LTrn ` K ) ` w ) = T )
7 |- ( U e. LMod -> S e. Ring )
7 |- ( S e. ( SubMnd ` G ) -> S C_ ( Base ` G ) )
7 |- ( RR* X. RR* ) e. _V
7 |- ( r e. A -> r e. B )
7 |- ( q e. A -> q e. ( Base ` K ) )
7 |- ( ps -> R _FrSe A )
7 |- ( pi - ( pi / 2 ) ) = ( pi / 2 )
7 |- ( ph -> Y e. _V )
7 |- ( ph -> Y =/= .0. )
7 |- ( ph -> X e. ( N ` { X } ) )
7 |- ( ph -> U e. Grp )
7 |- ( ph -> RR C_ CC )
7 |- ( ph -> P e. NN )
7 |- ( ph -> M e. ( ZZ>= ` M ) )
7 |- ( ph -> K e. ( TopOn ` Y ) )
7 |- ( ph -> K e. ( TopOn ` U. K ) )
7 |- ( ph -> J e. ( TopOn ` U. J ) )
7 |- ( ph -> F : V --> B )
7 |- ( ph -> E e. ( V \ { ( 0g ` U ) } ) )
7 |- ( ph -> D e. RR )
7 |- ( ph -> B e. RR )
7 |- ( ph -> A. k e. A B e. CC )
7 |- ( ph -> 2 e. RR )
7 |- ( ph -> { E } C_ V )
7 |- ( ph -> `' ( x e. X , y e. Y |-> `' ( { x } +c { y } ) ) : ran ( x e. X , y e. Y |-> `' ( { x } +c { y } ) ) -onto-> ( X X. Y ) )
7 |- ( ph -> _E We ( `' F " ( _V \ 1o ) ) )
7 |- ( ph -> .0. e. V )
7 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
7 |- ( ph -> ( X .+ Y ) e. V )
7 |- ( ph -> ( S _D F ) : dom ( S _D F ) --> CC )
7 |- ( ph -> ( N ` { Y , Z } ) e. ( LSubSp ` W ) )
7 |- ( ph -> ( N ` { X , Y } ) e. ( LSubSp ` U ) )
7 |- ( ph -> ( N ` { w } ) =/= ( N ` { Y } ) )
7 |- ( ph -> ( M ` ( N ` { Y } ) ) e. ( LSubSp ` C ) )
7 |- ( ph -> ( G e. S <-> ( G : B --> A /\ ( `' G " ( _V \ 1o ) ) e. Fin ) ) )
7 |- ( ph -> ( D e. CC /\ D =/= 0 ) )
7 |- ( ph -> ( Base ` ( Scalar ` C ) ) = B )
7 |- ( ph -> ( B e. CC /\ B =/= 0 ) )
7 |- ( ph -> ( ( N ` { w } ) =/= ( N ` { X } ) /\ ( N ` { w } ) =/= ( N ` { Y } ) ) )
7 |- ( om ~<_ A -> A e. _V )
7 |- ( J |`t CC ) = J
7 |- ( I e. A -> I e. ( Base ` K ) )
7 |- ( G e. Grp -> ( ( invg ` G ) ` .0. ) = .0. )
7 |- ( G e. B -> ( coe1 ` G ) : NN0 --> ( Base ` R ) )
7 |- ( F e. ( S GrpHom T ) -> F : ( Base ` S ) --> ( Base ` T ) )
7 |- ( F e. ( S GrpHom T ) -> ( F ` ( 0g ` S ) ) = ( 0g ` T ) )
7 |- ( F e. ( C Cn J ) -> F : B --> U. J )
7 |- ( ch -> ph )
7 |- ( C e. Top <-> C e. ( TopOn ` B ) )
7 |- ( B = if ( B e. ~H , B , 0h ) -> ( normh ` ( if ( A e. ~H , A , 0h ) -h B ) ) = ( normh ` ( if ( A e. ~H , A , 0h ) -h if ( B e. ~H , B , 0h ) ) ) )
7 |- ( A e. CH /\ B e. CH /\ C e. CH )
7 |- ( A e. ~H -> ( T ` A ) e. ~H )
7 |- ( 6 + 7 ) = ; 1 3
7 |- ( 3 / 3 ) = 1
7 |- ( 2 x. 5 ) = 10
7 |- ( 2 x. 1 ) = ( 1 + 1 )
7 |- ( 2 / 2 ) = 1
7 |- ( 1 x. 6 ) = 6
7 |- ( 1 x. 2 ) = 2
7 |- ( 1 / 3 ) e. CC
7 |- ( 1 / 2 ) e. RR+
7 |- ( 1 / 2 ) e. CC
7 |- ( 1 / 2 ) <_ 1
7 |- ( 1 ... N ) C_ ( 1 ... M )
7 |- ( 0 x. 0 ) = 0
7 |- ( -. A e. _V -> { A } = (/) )
7 |- ( ( ph /\ Y = Z /\ ps ) -> K e. HL )
7 |- ( ( ph /\ Y = Z /\ ps ) -> I e. ( Base ` K ) )
7 |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
7 |- ( ( K e. Top /\ L e. Top ) -> ( L ^ko K ) e. ( TopOn ` ( K Cn L ) ) )
7 |- ( ( K e. Lat /\ X e. ( Base ` K ) /\ Y e. ( Base ` K ) ) -> ( X ./\ Y ) e. ( Base ` K ) )
7 |- ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ R e. ( Base ` K ) ) -> ( ( P .\/ Q ) .\/ R ) e. ( Base ` K ) )
7 |- ( ( K e. HL /\ W e. H ) -> K e. OP )
7 |- ( ( K e. HL /\ U e. A /\ V e. A ) -> ( U .\/ V ) e. ( Base ` K ) )
7 |- ( ( K e. HL /\ Q e. A /\ ( F ` ( G ` Q ) ) e. A ) -> ( Q .\/ ( F ` ( G ` Q ) ) ) e. ( Base ` K ) )
7 |- ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. B )
7 |- ( ( K e. HL /\ P e. A /\ ( F ` ( G ` P ) ) e. A ) -> ( P .\/ ( F ` ( G ` P ) ) ) e. ( Base ` K ) )
7 |- ( ( K e. HL /\ P e. A ) -> ( P .\/ P ) = P )
7 |- ( ( K e. HL /\ G e. A /\ H e. A ) -> ( G .\/ H ) e. ( Base ` K ) )
7 |- ( ( G e. Grp /\ A e. X ) -> ( ( invg ` G ) ` A ) e. X )

7 |- ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR )

7 |- ( ( A e. ( ZZ>= ` 2 ) /\ b e. ZZ ) -> ( A rmY b ) e. ZZ )
7 |- ( ( 1 / 2 ) < 1 <-> -. 1 <_ ( 1 / 2 ) )
7 |- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( `' I ` X ) e. ( Base ` K ) )
7 |- ( ( ( K e. HL /\ W e. H ) /\ P e. A /\ Q e. A ) -> U e. ( Base ` K ) )
7 |- ( ( ( K e. HL /\ W e. H ) /\ N e. T /\ P e. A ) -> ( N ` P ) e. A )
7 |- ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ G =/= ( _I |` B ) ) -> ( R ` G ) e. A )
7 |- ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( G ` Q ) e. A /\ -. ( G ` Q ) .<_ W ) )
7 |- ( ( ( K e. HL /\ W e. H ) /\ G e. T ) -> ( R ` G ) e. B )
7 |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ Q e. A ) -> ( F ` Q ) e. A )
7 |- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ Q e. A /\ T e. A ) ) -> G e. ( Base ` K ) )
7 |- ( ( ( K e. HL /\ W e. H ) /\ ( ( F e. T /\ F =/= ( _I |` B ) ) /\ ( I e. T /\ I =/= ( _I |` B ) ) /\ N e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) ) -> [_ I / g ]_ X e. T )
7 |- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> ( P .\/ Q ) e. ( LLines ` K ) )
6 |- U. x e. _V
6 |- -u 1 < 0
6 |- RR+ e. _V
6 |- recs ( ( f e. _V |-> ( iota_ s e. { y e. A | A. i e. ran f i R y } A. r e. { y e. A | A. i e. ran f i R y } -. r R s ) ) ) = recs ( ( h e. _V |-> ( iota_ v e. { w e. A | A. j e. ran h j R w } A. u e. { w e. A | A. j e. ran h j R w } -. u R v ) ) )
6 |- ran F e. _V
6 |- ran +w = ran ( 1st ` ( 2nd ` R ) )
6 |- P = ( ( PwSer1 ` R ) |`s ( Base ` ( 1o mPoly R ) ) )
6 |- om e. dom card
6 |- M e. CC
6 |- Lim dom F
6 |- K e. Top
6 |- K = ( LSpan ` ( ringLMod ` R ) )
6 |- if ( S : ~H --> ~H , S , 0hop ) : ~H --> ~H
6 |- if ( M e. ZZ , M , 0 ) e. ZZ
6 |- if ( C e. ~H , C , 0h ) e. ~H
6 |- if ( B e. CC , B , 0 ) e. CC
6 |- F = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
6 |- dom ZZ>= = ZZ
6 |- dom g e. _V
6 |- dom exp = CC
6 |- dom |`t = ( _V X. _V )
6 |- dom .Q = ( Q. X. Q. )
6 |- dom (,) = ( RR* X. RR* )
6 |- A = U. ~P A
6 |- 3 = ; 0 3
6 |- 2o e. _V
6 |- 1st Fn _V
6 |- 1o e. Fin
6 |- 1o e. { (/) , 1o }
6 |- 1 e. ( ZZ>= ` 0 )
6 |- 1 <_ 2
6 |- + e. GrpOp
6 |- + e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
6 |- ~P z e. _V
6 |- ~P B e. _V
6 |- _e < 3
6 |- ; 1 1 e. NN0
6 |- -. 2 || 1
6 |- (/) = ( E ` (/) )
6 |- (/) = ( +g ` (/) )
6 |- ( ZZ>= ` M ) C_ CC
6 |- ( ZZ e. _V -> x. = ( .r ` ( CCfld |`s ZZ ) ) )
6 |- ( z e. A -> z e. ( Base ` K ) )
6 |- ( z = y -> ( [ z / x ] ph <-> ps ) )
6 |- ( y e. F -> A. x y e. F )
6 |- ( y e. ~H -> ( T ` y ) e. ~H )
6 |- ( Y e. ( LSubSp ` U ) -> Y C_ X )
6 |- ( y `' < x <-> x < y )
6 |- ( x i^i B ) e. _V
6 |- ( X e. B -> ( 0 .x. X ) = ( 0g ` G ) )
6 |- ( x e. ~P B <-> x C_ B )
6 |- ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> `' ( { x } +c { y } ) ) : ( ( Base ` R ) X. ( Base ` S ) ) -1-1-onto-> ran ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> `' ( { x } +c { y } ) )
6 |- ( x e. ( 2 [,) +oo ) -> 0 e. RR )
6 |- ( x e. ( 2 [,) +oo ) -> 0 < x )
6 |- ( x e. ( 0 [,) +oo ) -> x e. ( 0 [,] +oo ) )
6 |- ( x = D -> ( A e. RR <-> N e. RR ) )
6 |- ( x = C -> ( A e. RR <-> M e. RR ) )
6 |- ( x `' R y <-> y R x )
6 |- ( W e. LMod -> ( Scalar ` W ) e. Grp )
6 |- ( W e. CPreHil -> 0 = ( 0g ` ( Scalar ` W ) ) )
6 |- ( w e. B -> A. y w e. B )
6 |- ( U e. S -> U C_ ( Base ` W ) )
6 |- ( U e. LMod -> R e. Ring )
6 |- ( U e. LMod -> .0. e. V )
6 |- ( U e. ( SubGrp ` G ) -> U C_ B )
6 |- ( TopOpen ` CCfld ) e. Haus
6 |- ( th -> ( ta -> et ) )
6 |- ( T e. Cat -> ( U e. ( SubCat ` T ) <-> ( U e. Cat /\ ( ( id_ ` U ) C_ ( id_ ` T ) /\ ( ( dom_ ` U ) C_ ( dom_ ` T ) /\ ( cod_ ` U ) C_ ( cod_ ` T ) ) /\ ( o_ ` U ) C_ ( o_ ` T ) ) ) ) )
6 |- ( R e. Ring -> ( Unit ` R ) C_ ( RLReg ` R ) )
6 |- ( R e. Ring -> ( oppR ` R ) e. Ring )
6 |- ( R e. Ring -> ( Base ` R ) e. ( SubRing ` R ) )
6 |- ( r = R -> ( 1r ` r ) = .1. )
6 |- ( r = R -> ( 0g ` r ) = .0. )
6 |- ( r = R -> ( .r ` r ) = .x. )
6 |- ( q e. A -> q e. B )
6 |- ( ps -> A. i ps )
6 |- ( ph -> Y = ( ( Q .\/ R ) .\/ P ) )
6 |- ( ph -> X e. J )
6 |- ( ph -> X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) )
6 |- ( ph -> X : D --> ( Base ` R ) )
6 |- ( ph -> U e. CC )

6 |- ( ph -> U e. ( SubGrp ` W ) )

6 |- ( ph -> L e. ( TopOn ` U. L ) )

6 |- ( ph -> K e. RR )
6 |- ( ph -> K e. AtLat )
6 |- ( ph -> H e. _V )
6 |- ( ph -> E e. CC )
6 |- ( ph -> dom ( x e. X |-> B ) = X )
6 |- ( ph -> dom ( x e. A |-> B ) C_ RR )
6 |- ( ph -> CC C_ CC )
6 |- ( ph -> C e. _V )
6 |- ( ph -> B e. Fin )
6 |- ( ph -> B C_ RR )
6 |- ( ph -> A. x ( ps <-> ch ) )
6 |- ( ph -> 2 =/= 0 )
6 |- ( ph -> ~P X e. Fin )
6 |- ( ph -> { 0 } C_ CC )
6 |- ( ph -> -. Z e. ( N ` { Y } ) )
6 |- ( ph -> ( x e. A <-> x e. B ) )
6 |- ( ph -> ( th -> ch ) )
6 |- ( ph -> ( ps -> ( th -> ta ) ) )
6 |- ( ph -> ( N ` { X } ) e. ( LSubSp ` W ) )
6 |- ( ph -> ( N ` { X } ) e. ( LSubSp ` U ) )
6 |- ( ph -> ( J ` E ) e. ( D \ { ( 0g ` C ) } ) )
6 |- ( ph -> ( G : B --> A /\ ( `' G " ( _V \ 1o ) ) e. Fin ) )
6 |- ( ph -> ( F .x. X ) e. V )
6 |- ( ph -> ( +g ` P ) = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) )
6 |- ( ph -> ( `' F " ( _V \ { .0. } ) ) C_ ( `' F " ( _V \ { .0. } ) ) )
6 |- ( ph -> ( ._|_ ` ( ( LSpan ` U ) ` { X } ) ) = ( ._|_ ` { X } ) )
6 |- ( ph -> ( ( P - 1 ) / 2 ) e. NN )
6 |- ( ph -> ( ( N + 1 ) - 1 ) = N )
6 |- ( ph -> ( ( M ` ( N ` { Y } ) ) = ( J ` { G } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R G ) } ) ) )
6 |- ( p e. ( Atoms ` K ) -> p e. B )
6 |- ( normop ` T ) e. CC
6 |- ( N e. NN0 -> M e. ( 1 ... M ) )
6 |- ( N e. NN0 -> L : ZZ -onto-> ( Base ` Z ) )
6 |- ( k e. ZZ -> ( _i ^ k ) e. CC )
6 |- ( K e. OP -> ( 1. ` K ) e. ( Base ` K ) )
6 |- ( k e. NN0 -> ( F ` k ) = ( ( A ^ k ) / ( ! ` k ) ) )
6 |- ( k = K -> ( Atoms ` k ) = A )

6 |- ( J e. ( TopOn ` X ) -> F Fn X )

6 |- ( G e. Mnd -> ( 0g ` G ) e. B )
6 |- ( G e. Grp -> ( 0g ` G ) e. B )
6 |- ( G e. Grp -> ( 0g ` G ) e. ( Base ` G ) )
6 |- ( F e. A -> F e. ( Base ` K ) )
6 |- ( F e. ( S LMHom T ) -> F : ( Base ` S ) --> ( Base ` T ) )
6 |- ( F e. ( S GrpHom T ) -> F : V --> ( Base ` T ) )
6 |- ( F e. ( Poly ` S ) -> N e. NN0 )
6 |- ( F e. ( CC ^pm RR ) <-> ( F : dom F --> CC /\ dom F C_ RR ) )
6 |- ( dom F =/= (/) <-> ran F =/= (/) )
6 |- ( ch -> n e. D )
6 |- ( ch -> ( th -> ta ) )
6 |- ( Base ` R ) = ( Base ` ( mulGrp ` R ) )
6 |- ( Base ` O ) = ( Base ` D )
6 |- ( A e. RR -> ( |_ ` A ) e. CC )
6 |- ( A e. dom cf <-> A e. On )
6 |- ( A e. CH /\ B e. CH /\ D e. CH )
6 |- ( A e. ( ZZ>= ` 2 ) -> A e. NN )
6 |- ( A e. ( ZZ>= ` 2 ) -> A e. CC )
6 |- ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. CC )
6 |- ( 2nd ` <. x , y >. ) = y
6 |- ( 2 x. 3 ) = 6
6 |- ( 2 + 7 ) = 9
6 |- ( 1 x. 8 ) = 8
6 |- ( 1 + 7 ) = 8
6 |- ( 0 + 2 ) = 2
6 |- ( 0 [,) +oo ) C_ ( 0 [,] +oo )
6 |- ( <_ i^i ( RR X. RR ) ) e. _V
6 |- ( _i x. 1 ) = _i
6 |- ( _|_ ` ( _|_ ` B ) ) = B
6 |- ( [ z / x ] ph -> A. y [ z / x ] ph )
6 |- ( .r ` Z ) = ( +g ` ( mulGrp ` Z ) )
6 |- ( -. R e. _V -> P = (/) )
6 |- ( -. ( I e. _V /\ R e. _V ) -> ( I mPwSer R ) = (/) )
6 |- ( ( x e. RR /\ 0 <_ x ) -> ( x e. RR* /\ 0 <_ x ) )
6 |- ( ( W e. LMod /\ Y e. V /\ Z e. V ) -> ( Y .+ Z ) e. V )
6 |- ( ( U e. LMod /\ Z e. V ) -> ( N ` { Z } ) e. ( LSubSp ` U ) )
6 |- ( ( U e. LMod /\ X e. V /\ Y e. V ) -> ( X .+ Y ) e. V )
6 |- ( ( U e. LMod /\ F e. B /\ X e. V ) -> ( F .x. X ) e. V )
6 |- ( ( U e. LMod /\ ( X .- Y ) e. V ) -> ( N ` { ( X .- Y ) } ) e. ( LSubSp ` U ) )
6 |- ( ( R e. Top /\ S e. Top ) -> ( U. R X. U. S ) = U. ( R tX S ) )
6 |- ( ( ph /\ x e. A ) -> ( abs ` B ) e. RR )
6 |- ( ( ph /\ x e. A ) -> ( ( x e. A |-> B ) ` x ) = B )
6 |- ( ( ph /\ ps /\ ch ) -> ( th -> ta ) )
6 |- ( ( ph /\ ps /\ ch ) <-> ( ph' /\ ps' /\ ch' ) )
6 |- ( ( ph /\ ps ) -> ta )
6 |- ( ( ph /\ k e. D ) -> R e. Ring )
6 |- ( ( ph /\ D e. S ) -> N e. RR )
6 |- ( ( ph /\ C e. S ) -> M e. RR )
6 |- ( ( ph /\ ( x e. CC /\ y e. CC ) ) -> ( x + y ) e. CC )
6 |- ( ( K e. OP /\ Y e. B ) -> ( ._|_ ` ( ._|_ ` Y ) ) = Y )
6 |- ( ( K e. Lat /\ Y e. B /\ Z e. B ) -> ( Y .\/ Z ) e. B )
6 |- ( ( K e. Lat /\ X e. ( Base ` K ) ) -> X ( le ` K ) X )
6 |- ( ( K e. Lat /\ Q e. ( Base ` K ) /\ R e. ( Base ` K ) ) -> ( Q .\/ R ) e. ( Base ` K ) )
6 |- ( ( K e. Lat /\ P e. ( Base ` K ) /\ R e. ( Base ` K ) ) -> ( P .\/ R ) e. ( Base ` K ) )
6 |- ( ( K e. Lat /\ ( R .\/ S ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( R .\/ S ) ./\ W ) .<_ W )
6 |- ( ( K e. Lat /\ ( P .\/ S ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( P .\/ S ) ./\ W ) .<_ W )
6 |- ( ( K e. Lat /\ ( P .\/ R ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( P .\/ R ) ./\ W ) e. ( Base ` K ) )
6 |- ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( P .\/ Q ) ./\ W ) .<_ ( P .\/ Q ) )
6 |- ( ( K e. HL /\ W e. H ) -> U e. LMod )
6 |- ( ( K e. HL /\ W e. H ) -> ( ( ( oc ` K ) ` W ) e. A /\ -. ( ( oc ` K ) ` W ) .<_ W ) )
6 |- ( ( K e. HL /\ U e. A /\ S e. A ) -> ( U .\/ S ) e. ( Base ` K ) )
6 |- ( ( K e. HL /\ S e. A /\ T e. A ) -> ( S .\/ T ) = ( T .\/ S ) )
6 |- ( ( K e. HL /\ R e. A /\ S e. A ) -> ( R .\/ S ) e. B )
6 |- ( ( K e. HL /\ R e. A ) -> ( R .\/ R ) = R )
6 |- ( ( K e. HL /\ Q e. A /\ T e. A ) -> ( Q .\/ T ) e. ( Base ` K ) )
6 |- ( ( K e. CLat /\ X C_ ( Base ` K ) ) -> ( ( lub ` K ) ` X ) e. ( Base ` K ) )
6 |- ( ( G e. Mnd /\ x e. B /\ y e. B ) -> ( x ( +g ` G ) y ) e. B )
6 |- ( ( G e. GrpOp /\ A e. X ) -> ( A P 0 ) = ( Id ` G ) )
6 |- ( ( G e. GrpOp /\ A e. X ) -> ( A G ( Id ` G ) ) = A )
6 |- ( ( A. x e. S A e. RR /\ D e. S ) -> N e. RR )
6 |- ( ( A. x e. S A e. RR /\ C e. S ) -> M e. RR )
6 |- ( ( A e. RR /\ 0 <_ A ) -> A e. CC )
6 |- ( ( 2 + 1 ) - 1 ) = 2
6 |- ( ( 1 x. 1 ) + ( 0 + 0 ) ) = ( 1 + 0 )
6 |- ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1
6 |- ( ( -. A. x x = z /\ -. A. x x = y ) -> ( z = y -> A. x z = y ) )
6 |- ( ( ( K e. V /\ W e. H ) /\ F e. T ) -> F e. ( LAut ` K ) )
6 |- ( ( ( K e. HL /\ W e. H ) /\ X e. T /\ `' G e. T ) -> ( X o. `' G ) e. T )
6 |- ( ( ( K e. HL /\ W e. H ) /\ G e. T ) -> `' G e. T )
6 |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. ( Base ` K ) ) -> ( F ` P ) e. ( Base ` K ) )
6 |- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( J ` Q ) e. ( LSubSp ` U ) )
6 |- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ D e. T ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( F =/= ( _I |` B ) /\ D =/= ( _I |` B ) /\ ( R ` D ) =/= ( R ` F ) ) ) -> ( O ` P ) e. A )
6 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q /\ ( s e. A /\ ( -. s .<_ W /\ s .<_ ( P .\/ Q ) ) ) ) -> N e. B )
6 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q /\ ( s e. A /\ ( -. s .<_ W /\ s .<_ ( P .\/ Q ) ) ) ) -> ( s e. A /\ -. s .<_ W ) )
6 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ -. S .<_ W ) /\ P =/= Q ) -> ( ( G ` S ) e. A /\ -. ( G ` S ) .<_ W ) )
5 |- z e. { z }
5 |- y e. { y }
5 |- X = ran ( 1st ` R )
5 |- U. J = U. ( topGen ` ran (,) )
5 |- U. { x } = x
5 |- U. { (/) } = (/)
5 |- -u -u _i = _i
5 |- -u ( pi / 2 ) e. CC
5 |- sup ( { 0 } , RR* , < ) = 0
5 |- ran t e. _V
5 |- ran (,) C_ ( topGen ` ran (,) )
5 |- ran ( x e. A |-> B ) = { y | E. x e. A y = B }
5 |- QQ e. ( SubRing ` CCfld )
5 |- P e. _V
5 |- -oo e. _V
5 |- om C_ Fin
5 |- O = dom J
5 |- NN = ( ZZ>= ` ( 0 + 1 ) )
5 |- N = ( ( 10 x. C ) + D )
5 |- M = ( ( 10 x. A ) + B )
5 |- J = ( J |`t CC )
5 |- if ( H e. CH , H , 0H ) e. CH
5 |- G = ( W toNrmGrp ( x e. ( Base ` W ) |-> ( sqr ` ( x ( .i ` W ) x ) ) ) )
5 |- Fun R1
5 |- Fun ~~>
5 |- dom cf = On
5 |- dom aleph = On
5 |- dom ( CC _D exp ) = CC
5 |- CCfld e. Grp
5 |- CC = ( Base ` ( mulGrp ` CCfld ) )
5 |- B e. U. ( R1 " On )
5 |- B = ( Base ` ( ringLMod ` R ) )
5 |- A. y e. A ph
5 |- A. x e. A B e. _V
5 |- 7 = ; 0 7
5 |- 4 e. ZZ
5 |- 2o e. Fin
5 |- 2o ~~ 2o
5 |- 2nd Fn _V
5 |- 2 < _e
5 |- 1o e. suc 1o
5 |- 1 = ( 1 x. 1 )
5 |- 0h e. _V
5 |- 0 e. { 0 }
5 |- 0 e. ( S u. { 0 } )
5 |- 0 e. ( 0 [,] +oo )
5 |- { x } =/= (/)
5 |- { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V
5 |- ; 2 3 e. NN0
5 |- ; 2 3 e. NN
5 |- ; 1 7 e. NN
5 |- ; 1 3 e. NN
5 |- .1. e. _V
5 |- .0. = ( 0g ` ( ringLMod ` R ) )
5 |- -. -oo < -oo
5 |- -. 1o e. 1o
5 |- -. 1 = 0
5 |- (/) Fn (/)
5 |- (/) e. { (/) , 1o }
5 |- (/) ~~ (/)
5 |- ( ZZ>= ` ( 1 - 1 ) ) = ( ZZ>= ` 0 )
5 |- ( ZZ C_ CC -> ZZ = ( Base ` ( CCfld |`s ZZ ) ) )
5 |- ( z e. A <-> { z } C_ A )
5 |- ( z e. ( ( x e. A |-> B ) ` y ) -> A. x z e. ( ( x e. A |-> B ) ` y ) )
5 |- ( y e. ( F ` z ) -> A. x y e. ( F ` z ) )
5 |- ( y `' A x <-> x A y )
5 |- ( x u. y ) e. _V
5 |- ( x i^i A ) e. _V
5 |- ( X e. P -> X e. ( Base ` K ) )
5 |- ( x e. D <-> ( x e. CC /\ ( x e. RR -> x e. RR+ ) ) )
5 |- ( x e. C <-> E. y ( -. y e. A /\ ( y +Q x ) e. B ) )
5 |- ( x e. A -> x e. ~H )
5 |- ( x e. A -> ( ( A X. { 0 } ) ` x ) = 0 )
5 |- ( x e. ( Base ` W ) |-> ( sqr ` ( x ( .i ` W ) x ) ) ) e. _V
5 |- ( x e. ( 2 [,) +oo ) -> 0 < 2 )
5 |- ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) -> ( X ` ( 1r ` Z ) ) = 1 )
5 |- ( x = y -> ( -. ph <-> -. ps ) )
5 |- ( x = T -> dom ( dom_ ` x ) = dom ( dom_ ` T ) )
5 |- ( x `' < y <-> y < x )
5 |- ( x _E A <-> x e. A )
5 |- ( x ( +g ` K ) y ) = ( x ( +g ` L ) y )
5 |- ( W e. TopSp <-> J e. ( TopOn ` ( Base ` W ) ) )
5 |- ( W e. CMod -> F = ( CCfld |`s ( Base ` F ) ) )
5 |- ( w e. C -> A. f w e. C )
5 |- ( w e. B -> w e. ~H )
5 |- ( w = W -> ( Scalar ` w ) = F )
5 |- ( w = W -> ( .s ` w ) = .x. )
5 |- ( U e. NrmCVec -> Z = ( Id ` G ) )
5 |- ( U e. LVec -> R e. DivRing )
5 |- ( -u _i x. _i ) = -u ( _i x. _i )
5 |- ( -u _i x. _i ) = 1
5 |- ( TopOpen ` CCfld ) = ( MetOpen ` ( abs o. - ) )
5 |- ( T x. A ) e. NN0
5 |- ( T e. NrmGrp -> ( M ` ( 0g ` T ) ) = 0 )
5 |- ( S e. States -> ( S ` A ) e. RR )
5 |- ( S e. ( SubGrp ` G ) -> ( 0g ` G ) e. S )
5 |- ( S e. ( Clsd ` J ) -> S C_ U. J )
5 |- ( RR* \ { -oo } ) e. _V
5 |- ( R e. Vec -> +w e. GrpOp )
5 |- ( R e. Top <-> R e. ( TopOn ` U. R ) )
5 |- ( R e. NzRing -> ( 1r ` R ) =/= ( 0g ` R ) )
5 |- ( R e. Fld -> ( ( G e. AbelOp /\ H : ( X X. X ) --> X ) /\ ( A. x e. X A. y e. X A. z e. X ( ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) /\ ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) ) /\ E. x e. X A. y e. X ( ( x H y ) = y /\ ( y H x ) = y ) ) /\ ( ( H |` ( ( X \ { ( Id ` G ) } ) X. ( X \ { ( Id ` G ) } ) ) ) e. GrpOp /\ A. x e. X A. y e. X ( x H y ) = ( y H x ) ) ) )
5 |- ( r = R -> U. U. r = U. U. R )
5 |- ( pi + -u ( pi / 2 ) ) = ( pi / 2 )
5 |- ( pi + -u ( pi / 2 ) ) = ( pi - ( pi / 2 ) )
5 |- ( ph -> X e. RR+ )
5 |- ( ph -> X : ( M X. N ) --> B )
5 |- ( ph -> U e. RR )
5 |- ( ph -> U C_ V )
5 |- ( ph -> sum_ k e. Z A = ( ~~> ` seq M ( + , F ) ) )
5 |- ( ph -> S = U. ( ( TopOpen ` CCfld ) |`t S ) )
5 |- ( ph -> S = ( oppR ` F ) )
5 |- ( ph -> RR e. _V )
5 |- ( ph -> ran S C_ ( SubGrp ` G ) )
5 |- ( ph -> R e. CMnd )
5 |- ( ph -> R e. CC )
5 |- ( ph -> Q e. CC )
5 |- ( ph -> Q e. ( SubGrp ` W ) )
5 |- ( ph -> P e. Ring )
5 |- ( ph -> P e. CC )
5 |- ( ph -> M e. Top )
5 |- ( ph -> M e. NN )
5 |- ( ph -> L : ZZ --> ( Base ` Z ) )
5 |- ( ph -> K e. OL )
5 |- ( ph -> K e. CC )
5 |- ( ph -> II e. ( TopOn ` ( 0 [,] 1 ) ) )
5 |- ( ph -> i e. F )
5 |- ( ph -> G Fn RR )
5 |- ( ph -> F Fn X )
5 |- ( ph -> F : RR --> ( 0 [,] +oo ) )
5 |- ( ph -> F : ( A [,] B ) --> RR )
5 |- ( ph -> dom R e. _V )
5 |- ( ph -> dom G = B )
5 |- ( ph -> C e. Top )
5 |- ( ph -> B = U. J )
5 |- ( ph -> B = ( ( Base ` R ) ^m D ) )
5 |- ( ph -> A. x e. X ( y e. Y |-> A ) e. ( K Cn L ) )
5 |- ( ph -> A =/= (/) )
5 |- ( ph -> 4 e. CC )
5 |- ( ph -> 1 e. NN )
5 |- ( ph -> 1 < K )
5 |- ( ph -> 0 <_ R )
5 |- ( ph -> 0 `' ( { R } +c { S } ) Fn 2o )
5 |- ( ph -> .~ e. _V )
5 |- ( ph -> ( z e. ( iota_ x e. A A. y e. B ( ps -> x = C ) ) -> A. y z e. ( iota_ x e. A A. y e. B ( ps -> x = C ) ) ) )
5 |- ( ph -> ( x e. X |-> ( y e. Y |-> A ) ) : X --> ( K Cn L ) )
5 |- ( ph -> ( x e. A |-> B ) : A --> CC )

5 |- ( ph -> ( x e. A |-> ( Re ` B ) ) e. L^1 )

5 |- ( ph -> ( x e. A |-> ( Im ` B ) ) e. L^1 )
5 |- ( ph -> ( X e. ( N ` { Y , Z } ) <-> ( N ` { X } ) C_ ( N ` { Y , Z } ) ) )
5 |- ( ph -> ( x e. ( A [,] B ) <-> ( x e. RR /\ A <_ x /\ x <_ B ) ) )
5 |- ( ph -> ( X ` ( 1r ` Z ) ) = 1 )
5 |- ( ph -> ( ta /\ et ) )
5 |- ( ph -> ( T .(+) U ) = ( U .(+) T ) )
5 |- ( ph -> ( RR _D F ) : dom ( RR _D F ) --> RR )
5 |- ( ph -> ( N ` { Y } ) =/= ( N ` { X } ) )
5 |- ( ph -> ( N ` { X } ) =/= ( N ` { w } ) )
5 |- ( ph -> ( mulGrp ` R ) e. Mnd )
5 |- ( ph -> ( M ` ( N ` { Y } ) ) = ( J ` { G } ) )
5 |- ( ph -> ( L ` G ) C_ V )
5 |- ( ph -> ( L ` { ( ( S ` u ) .+b s ) } ) e. ( LSubSp ` C ) )
5 |- ( ph -> ( I ` ( `' I ` X ) ) = X )
5 |- ( ph -> ( F ` C ) e. CC )
5 |- ( ph -> ( E e. ( 0 (,) 1 ) /\ 1 < K /\ ( U - E ) e. RR+ ) )
5 |- ( ph -> ( E .+ G ) e. F )
5 |- ( ph -> ( C e. RR /\ 0 <_ C ) )
5 |- ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
5 |- ( ph -> ( Base ` K ) = ( Base ` L ) )
5 |- ( ph -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) )
5 |- ( ph -> ( 1r ` R ) e. ( Base ` R ) )
5 |- ( ph -> ( +g ` U ) = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p ( +g ` R ) q ) ) >. } )
5 |- ( ph -> ( `' I ` X ) e. ( Base ` K ) )
5 |- ( ph -> ( .r ` P ) = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) )
5 |- ( ph -> ( ._|_ ` ( L ` G ) ) C_ V )
5 |- ( ph -> ( ( LCDual ` K ) ` W ) e. LMod )
5 |- ( ph -> ( ( `' F " ( _V \ { .0. } ) ) = (/) \/ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ E. f f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) )
5 |- ( ph -> ( # ` B ) e. NN )
5 |- ( p e. ( ZZ>= ` 2 ) -> 1 ( N e. CC /\ N =/= 0 ) )
5 |- ( M e. Top <-> M e. ( TopOn ` U. M ) )
5 |- ( K e. ( ZZ>= ` 2 ) -> K e. NN )
5 |- ( K e. ( SubGrp ` G ) -> K C_ X )
5 |- ( k e. ( M ... j ) -> k e. Z )
5 |- ( k = K -> ( meet ` k ) = ./\ )
5 |- ( k = K -> ( ( DVecH ` k ) ` w ) = ( ( DVecH ` K ) ` w ) )
5 |- ( J e. Top -> X e. _V )
5 |- ( J e. Top -> U. J e. J )
5 |- ( j = J -> U. j = X )
5 |- ( g e. T -> ( O ` g ) = ( _I |` B ) )
5 |- ( G e. Grp -> X =/= (/) )
5 |- ( G e. B -> ( D ` G ) e. RR* )
5 |- ( g = G -> ( ( D ` g ) = ( C ` F ) <-> ( D ` G ) = ( C ` F ) ) )
5 |- ( f e. X_ x e. A B <-> ( f Fn A /\ A. x e. A ( f ` x ) e. B ) )
5 |- ( F e. B -> ( coe1 ` F ) : NN0 --> ( Base ` R ) )
5 |- ( F e. ( Poly ` S ) -> F e. ( Poly ` CC ) )
5 |- ( F e. ( II Cn J ) -> F : ( 0 [,] 1 ) --> U. J )
5 |- ( F e. ( ( J CnP K ) ` P ) -> P e. U. J )
5 |- ( f = F -> ( ( D ` g ) = ( C ` f ) <-> ( D ` g ) = ( C ` F ) ) )
5 |- ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) -> ran f = ( `' F " ( _V \ { .0. } ) ) )
5 |- ( E. x ps <-> ps )
5 |- ( D e. ( *Met ` Y ) -> K e. ( TopOn ` Y ) )
5 |- ( ch -> R _FrSe A )
5 |- ( ch -> dom f = n )
5 |- ( Base ` R ) = ( Base ` M )
5 |- ( B e. dom R1 <-> B e. On )
5 |- ( A. y ps -> A. x A. y ps )
5 |- ( A. x e. X ( y e. Y |-> A ) e. ( K Cn L ) <-> ( x e. X |-> ( y e. Y |-> A ) ) : X --> ( K Cn L ) )
5 |- ( A. x A. z ( z = y -> ph ) <-> A. x ps )
5 |- ( A. x ( x e. ~P A -> x e. ~P B ) -> ~P A C_ ~P B )
5 |- ( A e. Z[i] -> ( Im ` A ) e. ZZ )
5 |- ( A e. RR+ -> ( log ` A ) e. CC )
5 |- ( A e. RR -> 0 e. RR )
5 |- ( A e. RR -> ( A ^ 2 ) = ( A x. A ) )
5 |- ( A e. CC -> ( -u _i x. A ) e. CC )
5 |- ( A e. CC -> ( 1 - ( A ^ 2 ) ) e. CC )
5 |- ( A e. CC -> ( ( abs ` A ) =/= 0 <-> A =/= 0 ) )
5 |- ( A e. ( SubRing ` R ) -> A C_ ( Base ` R ) )
5 |- ( A e. ( SubRing ` R ) -> ( .r ` R ) = ( .r ` S ) )
5 |- ( A C_ CH -> A C_ ~P ~H )
5 |- ( A = if ( A e. ~H , A , 0h ) -> ( normh ` ( A -h B ) ) = ( normh ` ( if ( A e. ~H , A , 0h ) -h B ) ) )
5 |- ( A = 0 -> ( abs ` A ) = 0 )
5 |- ( A ~<_ B -> B e. _V )
5 |- ( 4 x. 9 ) = ; 3 6
5 |- ( 4 + 7 ) = ; 1 1
5 |- ( 3 x. 7 ) = ; 2 1
5 |- ( 3 x. 6 ) = ; 1 8
5 |- ( 3 x. 5 ) = ; 1 5
5 |- ( 3 x. 4 ) = ; 1 2
5 |- ( 3 e. RR /\ 0 < 3 )
5 |- ( 3 e. CC /\ 3 =/= 0 )
5 |- ( 3 - 1 ) = ( ( 2 + 1 ) - 1 )
5 |- ( 2 x. 4 ) = 8
5 |- ( 2 + 0 ) = 2
5 |- ( 1st ` <. x , y >. ) = x
5 |- ( 1r ` Z ) = ( 0g ` ( mulGrp ` Z ) )
5 |- ( 1P +P. 1P ) e. P.
5 |- ( 10 + 0 ) = 10
5 |- ( 1 x. 9 ) = 9
5 |- ( 1 + 6 ) = 7
5 |- ( 1 + 3 ) = 4
5 |- ( 0 e. RR* -> sup ( { 0 } , RR* , < ) = 0 )
5 |- ( 0 e. ( S u. { 0 } ) <-> { 0 } C_ ( S u. { 0 } ) )
5 |- ( 0 < 1 <-> -u 1 < 0 )
5 |- ( 0 + 5 ) = 5
5 |- ( 0 + 4 ) = 4
5 |- ( 0 ^ 0 ) = 1
5 |- ( 0 [,] 1 ) C_ CC
5 |- ( 0 / 2 ) = 0
5 |- ( 0 ... 0 ) = { 0 }
5 |- ( _V i^i B ) = B
5 |- ( _i x. -u _i ) = -u ( _i x. _i )
5 |- ( .r ` L ) = ( +g ` ( mulGrp ` L ) )
5 |- ( -. x e. A -> 0 <_ 0 )
5 |- ( -. x `' < y <-> -. y < x )
5 |- ( -. W e. _V -> K = (/) )
5 |- ( -. ph -> A. y -. ph )
5 |- ( -. A. x x = y -> ( y = v -> A. x y = v ) )
5 |- ( -. A e. On -> ( cf ` A ) = (/) )
5 |- ( (/) +o (/) ) = (/)
5 |- ( ( W e. LMod /\ X e. V ) -> ( ( 1r ` F ) .x. X ) = X )
5 |- ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> T : X --> ( BaseSet ` W ) )
5 |- ( ( U e. NrmCVec /\ -u 1 e. CC /\ B e. X ) -> ( -u 1 S B ) e. X )
5 |- ( ( U e. NrmCVec /\ B e. X /\ A e. X ) -> ( * ` ( B P A ) ) = ( A P B ) )
5 |- ( ( U e. NrmCVec /\ B e. X ) -> ( 1 S B ) = B )
5 |- ( ( topGen ` ran (,) ) |`t ( 0 [,] ( 1 / 2 ) ) ) e. ( TopOn ` ( 0 [,] ( 1 / 2 ) ) )
5 |- ( ( topGen ` ran (,) ) |`t ( ( 1 / 2 ) [,] 1 ) ) e. ( TopOn ` ( ( 1 / 2 ) [,] 1 ) )
5 |- ( ( pi / 2 ) - pi ) = -u ( pi / 2 )
5 |- ( ( ph /\ x e. I ) -> ( S ` x ) e. ( SubGrp ` G ) )
5 |- ( ( ph /\ x e. A ) -> x e. RR )
5 |- ( ( ph /\ v e. V ) -> W e. LVec )
5 |- ( ( ph /\ k e. Z ) -> A e. CC )
5 |- ( ( ph /\ k e. A ) -> C e. CC )
5 |- ( ( ph /\ j e. Z ) -> j e. ( ZZ>= ` M ) )
5 |- ( ( ph /\ ( x e. CC /\ y e. CC ) ) -> ( x x. y ) e. CC )
5 |- ( ( ph /\ ( C e. S /\ D e. S ) ) -> N e. RR )
5 |- ( ( ph /\ ( C e. S /\ D e. S ) ) -> M e. RR )
5 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( G gsum F ) = ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) )
5 |- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( `' F " ( _V \ { .0. } ) ) C_ A )
5 |- ( ( K e. Lat /\ Y e. B /\ Z e. B ) -> ( Y ./\ Z ) e. B )
5 |- ( ( K e. Lat /\ Y e. B /\ W e. B ) -> ( Y ./\ W ) .<_ W )
5 |- ( ( K e. Lat /\ X e. B /\ Q e. B ) -> ( X .\/ Q ) e. B )
5 |- ( ( K e. Lat /\ Q e. ( Base ` K ) /\ R e. ( Base ` K ) ) -> ( Q .\/ R ) = ( R .\/ Q ) )
5 |- ( ( K e. Lat /\ P e. ( Base ` K ) /\ S e. ( Base ` K ) ) -> ( P .\/ S ) e. ( Base ` K ) )
5 |- ( ( K e. Lat /\ ( U e. ( Base ` K ) /\ V e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( U .<_ W /\ V .<_ W ) <-> ( U .\/ V ) .<_ W ) )
5 |- ( ( K e. Lat /\ ( R .\/ S ) e. B /\ W e. B ) -> ( ( R .\/ S ) ./\ W ) e. B )
5 |- ( ( K e. Lat /\ ( R .\/ P ) e. ( Base ` K ) /\ ( U .\/ S ) e. ( Base ` K ) ) -> ( ( R .\/ P ) ./\ ( U .\/ S ) ) e. ( Base ` K ) )
5 |- ( ( K e. Lat /\ ( Q .\/ R ) e. ( Base ` K ) /\ ( T .\/ U ) e. ( Base ` K ) ) -> ( ( Q .\/ R ) ./\ ( T .\/ U ) ) e. ( Base ` K ) )
5 |- ( ( K e. HL /\ X C_ A /\ Y C_ A ) -> ( X .+ Y ) C_ A )
5 |- ( ( K e. HL /\ W e. H ) -> W ( <o ` K ) ( 1. ` K ) )
5 |- ( ( K e. HL /\ W e. H ) -> Fun I )
5 |- ( ( K e. HL /\ P e. A /\ R e. A ) -> ( P .\/ R ) = ( R .\/ P ) )
5 |- ( ( K e. HL /\ ( T e. A /\ U e. A /\ S e. A ) ) -> ( ( T .\/ U ) .\/ S ) = ( ( S .\/ T ) .\/ U ) )
5 |- ( ( K e. HL /\ ( F ` ( G ` P ) ) e. A /\ ( F ` ( G ` Q ) ) e. A ) -> ( ( F ` ( G ` P ) ) .\/ ( F ` ( G ` Q ) ) ) = ( ( F ` ( G ` Q ) ) .\/ ( F ` ( G ` P ) ) ) )
5 |- ( ( J e. Top /\ S C_ U. J ) -> ( ( cls ` J ) ` S ) C_ U. J )
5 |- ( ( G e. GrpOp /\ A e. X ) -> ( ( inv ` G ) ` A ) e. X )
5 |- ( ( G e. Grp /\ y e. B ) -> ( ( invg ` G ) ` y ) e. B )
5 |- ( ( G e. Grp /\ N e. ZZ /\ A e. X ) -> ( N .x. A ) e. X )
5 |- ( ( G e. Grp /\ M e. ZZ /\ X e. B ) -> ( M .x. X ) e. B )
5 |- ( ( F e. A /\ 1 =/= 0 ) -> ( F ` 1 ) = 1 )
5 |- ( ( F e. ( Poly ` S ) /\ k e. NN0 ) -> ( ( A ` k ) =/= 0 -> k <_ N ) )
5 |- ( ( F ` A ) e. ( 0 [,] +oo ) -> 0 <_ ( F ` A ) )
5 |- ( ( C e. LMod /\ ( S ` u ) e. D /\ s e. D ) -> ( ( S ` u ) .+b s ) e. D )
5 |- ( ( C e. LMod /\ ( ( S ` u ) .+b s ) e. D ) -> ( L ` { ( ( S ` u ) .+b s ) } ) e. ( LSubSp ` C ) )
5 |- ( ( B e. RR /\ C e. RR ) -> ( B x. C ) = ( C x. B ) )
5 |- ( ( B e. RR /\ 0 B e. CC )
5 |- ( ( B e. RR /\ 0 ( B e. CC /\ B =/= 0 ) )
5 |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. CC )
5 |- ( ( A e. RR /\ 1 < A ) -> 0 < A )
5 |- ( ( A e. RR /\ 0 < A ) -> A e. CC )
5 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> C e. ZZ )
5 |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> C e. CC )

Stefan O'Rear

unread,

Jul 13, 2016, 2:30:20 PM7/13/16

to metamath list

Might be interesting to add a sed 's/ [a-z] / x /g; s/ [A-Z] / X /g'
to deal with the simplest cases of variable substitutions.

Personally, I'm interested in subtrees with depth > 1; things like 7
e. CC have a depth-1 proof, and are not terribly interesting because
(a) depth-1 searches can be automated (b) there are hundreds of
combinations in use and I don't want to add all of them.

-sorear

David A. Wheeler

unread,

Jul 13, 2016, 2:33:55 PM7/13/16

to metamath

I'd be happy to create several theorems for set.mm to prove
improbable expressions such as:

> 80 |- 0 e. _V
> 70 |- -u 1 e. CC
> 61 |- 0 <_ 0
> 47 |- ( 0 + 1 ) = 1
> 46 |- 4 e. CC
> 44 |- (/) = ( Base ` (/) )
> 43 |- ( 1 x. 1 ) = 1
> 42 |- 1 e. _V
> 42 |- ( 1 - 1 ) = 0
> 29 |- pi e. CC
> 28 |- -u 1 e. RR
> 28 |- ( 2 x. 1 ) = 2

These are repeatedly reproved.

By adding these theorems, there will be more automation with
no extra coding effort, and a lot of proofs will shorten by a step or two.

--- David A. Wheeler

Mario Carneiro

unread,

Jul 13, 2016, 2:36:06 PM7/13/16

to metamath

On Wed, Jul 13, 2016 at 2:30 PM, Stefan O'Rear <sor...@gmail.com> wrote:

Personally, I'm interested in subtrees with depth > 1; things like 7
e. CC have a depth-1 proof, and are not terribly interesting because
(a) depth-1 searches can be automated (b) there are hundreds of
combinations in use and I don't want to add all of them.

Well, this is exactly why we are screening for the most common combinations. If it's too long-tail it's better to just reprove it as you need.

Of course, if there is a very common length 5 subtree, then there will also be an even more common length 4 subtree, and length 3, and so on; so you should be able to get at these by pulling out the length 2 subtrees repeatedly to chop down the list. (It is also reasonable to do this analysis before creating the theorem, that is, look for the top length 2 subtrees, and within those uses, look for the most common extensions of the subtrees to length 3, etc.)

DAW: I agree these are worth inclusion. Would you like to make a PR?

Mario

Mario Carneiro

unread,

Jul 13, 2016, 2:38:01 PM7/13/16

to metamath

FYI: Every item on DAW's list has a depth-1 proof.

David A. Wheeler

unread,

Jul 13, 2016, 2:45:22 PM7/13/16

to metamath

Mario:

> DAW: I agree these are worth inclusion. Would you like to make a PR?

Yes indeed!

On Wed, 13 Jul 2016 11:30:19 -0700, "Stefan O'Rear" <sor...@gmail.com> wrote:
> Personally, I'm interested in subtrees with depth > 1; things like 7
> e. CC have a depth-1 proof, and are not terribly interesting because
> (a) depth-1 searches can be automated (b) there are hundreds of
> combinations in use and I don't want to add all of them.

Depth>1 is clearly more interesting, and it would absurd to add all
*all* depth=1 theorems. I'm just proposing that this be done
for extremely common cases.
That kind of automation isn't there right now,
and even if it was, adding a few of these theorems would cause
small improvements in a *lot* of proofs.
Adding up a lot of small numbers does have a positive effect :-).

--- David A. Wheeler

Stefan O'Rear

unread,

Jul 13, 2016, 2:53:35 PM7/13/16

to metamath list

On Wed, Jul 13, 2016 at 11:45 AM, David A. Wheeler
<dwhe...@dwheeler.com> wrote:
> Depth>1 is clearly more interesting, and it would absurd to add all
> *all* depth=1 theorems. I'm just proposing that this be done
> for extremely common cases.
> That kind of automation isn't there right now,

IMPROVE ALL/1

-sorear

David A. Wheeler

unread,

Jul 13, 2016, 3:52:14 PM7/13/16

to metamath, metamath list

David A. Wheeler:

> > That kind of automation isn't there right now,

On Wed, 13 Jul 2016 11:53:34 -0700, "Stefan O'Rear" <sor...@gmail.com> wrote:
> IMPROVE ALL/1

Sorry, I *meant* it isn't there right now (to my knowledge) in *mmj2*,
specifically its control-U command. Regardless of automation,
I still think it'd be useful to prove the "super-common theorems" separately;
it provides a small amount of shortening to a *lot* of places.
I'm only proposing this when it's already repeatedly used in set.mm a *lot*.

Also, you mean "IMPROVE ALL /DEPTH 1", right? "/1" is the default search algorithm.

That said: Mario, would it be plausible to modify mmj2 so that on
the equivalent of "improve all /depth 1" is automatically called?
That would be really quick. IIRC, even It wouldn't be needed for any
"super-common theorems" that are added, but there's a long tail
that I'm not proposing to add.

-- David A. Wheeler

Mario Carneiro

unread,

Jul 13, 2016, 6:17:54 PM7/13/16

to metamath

On Wed, Jul 13, 2016 at 3:52 PM, David A. Wheeler <dwhe...@dwheeler.com> wrote:

That said: Mario, would it be plausible to modify mmj2 so that on
the equivalent of "improve all /depth 1" is automatically called?
That would be really quick. IIRC, even It wouldn't be needed for any
"super-common theorems" that are added, but there's a long tail
that I'm not proposing to add.

Yes, quite probably. I've wanted IMPROVE in mmj2 for a while now, as it's pretty much the only feature that MM-PA does better than mmj2 ATM. (Also, MINIMIZE is not in mmj2.) The main problem is that I don't know how it works. (CC: Norm?)

Mario

Norman Megill

unread,

Jul 13, 2016, 6:20:15 PM7/13/16

to meta...@googlegroups.com

Since as Mario says these have depth-1 proofs that metamath.exe can
prove automatically, and maybe mmj2 in the future, I would feel better
about adding them if it can be shown for each case that it is used
frequently enough so that set.mm as a whole gets shortened when they are
added (and the proofs using them minimized).

To me they seem like a random collection that will only confuse the user
with more choices. Instead of just the single, general theorem 0+A=A
(which hopefully the user would know), the user will also see the choice
0+1=0 and then perhaps waste time searching for the non-existent 0+2=2
that he/she needs.

So to justify this inconsistency and clutter, we want a good reason like
shortening set.mm.

Norm

Mario Carneiro

unread,

Jul 13, 2016, 7:05:34 PM7/13/16

to metamath

That's exactly what this is. Although this search is not perfectly correlated with set.mm reduction, it is a pretty good approximation. These particular theorems are being suggested *because* they are likely to reduce the size of set.mm. I wouldn't be recommending them otherwise. Given that each application probably saves only one to three characters, it will be tough to fully pay for itself if there are only 20-30 uses, but above that it's probably a net reduction.

Mario

Norman Megill

unread,

Jul 13, 2016, 7:53:04 PM7/13/16

to meta...@googlegroups.com

IMPROVE ALL /DEPTH=0 (the default DEPTH) merely tries to match all
unassigned steps (with completely known expressions) against all
previous $a/$p with no $e hypotheses. If a match is found, we're done
with that step.

IMPROVE ALL ignores unassigned steps that aren't completely known (i.e.
have work variables).

IMPROVE ALL /DEPTH=1 tests unassigned steps against all previous $a/$p
with one $e hypothesis and also _no new variables_ in the $e that the
$a/$p doesn't have (i.e. no "cuts" in proof theory lingo, such as ax-mp
has). It then recursively sees if the resulting (and completely known)
$e matches any $a/$p with at most one $e hypothesis. It keeps going
until it matches a $a/$p with 0 hypotheses (and then we're done) or ends
up with a hypothesis with no $a/$p matches or exceeds the SEARCH_LIMIT
depth in SHOW SETTINGS (and then we backtrack to find the next match to
the previous $e).

I can't remember how I avoid an infinite idi chain. SEARCH_LIMIT would
catch it and continue on, but with wasted CPU time. I may do something
else, but I'd have to look that up.

IMPROVE ALL /DEPTH=2 is the same idea, including $a/$p with 2 $e's that
have no new variables. /DEPTH=2 or greater can also lead to exponential
explosions in principle, because the backtracking branches in two, but
usually not in practice, and in any case SEARCH_LIMIT will catch it.

And so on.

With DEPTH > 0, sometimes longer paths get picked when shorter ones will
do, but MINIMIZE will typically take care of it. By habit I often do
IMPROVE ALL followed by IMPROVE ALL/DEPTH = 1 then 2 etc. if the proof
didn't complete, in order to avoid unnecessary long paths, but it
probably isn't required. I think my to-do list has an item to make this
stepping automatic.

IMPROVE has some aggressive features like /2 and /3 and /SUBPROOFS, but
I rarely use them. The most aggressive ones can often prove
propositional calculus theorems from scratch. A couple of times it
found proofs even shorter than Wolf Lammen's. But anything more
advanced takes an unknown amount of time up to the age of the universe,
and currently there is no ^C abort (it is on my to-do list). If I use
/2 or /3 I save the proof and set.mm first.

Norm

David A. Wheeler

unread,

Jul 13, 2016, 8:11:22 PM7/13/16

to metamath, metamath

On Wed, 13 Jul 2016 19:05:33 -0400, Mario Carneiro <di....@gmail.com> wrote:
> That's exactly what this is. Although this search is not perfectly
> correlated with set.mm reduction, it is a pretty good approximation.

Agreed. Here's a very rough approximation. If a label averages 6 characters (rough estimate),
then replacing 2 references with one reduces a proof's compressed space by
6 + 1 (space) + 1 (compressed reference to it) + 1
(average reduction because we'll occasionally remove a line including its leading spaces
and/or reduce the number of multi-character abbreviations). Adding them up,
eliminating a single 1-depth reference reduces each occurrence by about 9 characters.

What do we add instead? Let's take this trivial proof as an example:
$( -1 is a complex number. Common special case.
(Contributed by David A. Wheeler, 7-Jul-2016.) $)
neg1v $p |- -u 1 e. CC $= ( c1 ax1cn negcli ) ABC $.

This takes 161 characters, including the comments, newlines, and spaces.
Let's assume that's reasonably representative.

Given this, stating any depth-1 expression with 18 or more references is saving space.
Since "-u 1 e. CC" (for example) reoccurs 70 times, it's a clear win, saving about
(70-18)*9 = 468 bytes in just this one case.
In addition, adding just a few of these reduces the number of *visible* proof steps
in many places (for many readers this effect may be more important).

In short, there are just a few expressions that reoccur a *lot*.

> > To me they seem like a random collection that will only confuse the user
> > with more choices.

A reasonable concern, but I think there's an easy solution.

I propose including, in each one's comment, the phrase "Common special case."
I think that briefly captures the essence of *why* they are there, and
thus eliminate the confusion. That phrase can be substituted with something
else later easily enough.

I think it'd be great if mmj2 added depth-1 auto-search as well, but this
is a reasonable thing to do regardless.

--- David A. Wheeler

Mario Carneiro

unread,

Jul 14, 2016, 1:51:25 AM7/14/16

to metamath

On Wed, Jul 13, 2016 at 7:52 PM, Norman Megill <n...@alum.mit.edu> wrote:

On 7/13/16 6:17 PM, Mario Carneiro wrote:

On Wed, Jul 13, 2016 at 3:52 PM, David A. Wheeler <dwhe...@dwheeler.com
<mailto:dwhe...@dwheeler.com>> wrote:

That said: Mario, would it be plausible to modify mmj2 so that on
the equivalent of "improve all /depth 1" is automatically called?
That would be really quick. IIRC, even It wouldn't be needed for any
"super-common theorems" that are added, but there's a long tail
that I'm not proposing to add.

Yes, quite probably. I've wanted IMPROVE in mmj2 for a while now, as
it's pretty much the only feature that MM-PA does better than mmj2 ATM.
(Also, MINIMIZE is not in mmj2.) The main problem is that I don't know
how it works. (CC: Norm?)

IMPROVE ALL /DEPTH=0 (the default DEPTH) merely tries to match all unassigned steps (with completely known expressions) against all previous $a/$p with no $e hypotheses. If a match is found, we're done with that step.

IMPROVE ALL ignores unassigned steps that aren't completely known (i.e. have work variables).

IMPROVE ALL /DEPTH=1 tests unassigned steps against all previous $a/$p with one $e hypothesis and also _no new variables_ in the $e that the $a/$p doesn't have (i.e. no "cuts" in proof theory lingo, such as ax-mp has). It then recursively sees if the resulting (and completely known) $e matches any $a/$p with at most one $e hypothesis. It keeps going until it matches a $a/$p with 0 hypotheses (and then we're done) or ends up with a hypothesis with no $a/$p matches or exceeds the SEARCH_LIMIT depth in SHOW SETTINGS (and then we backtrack to find the next match to the previous $e).

I can't remember how I avoid an infinite idi chain. SEARCH_LIMIT would catch it and continue on, but with wasted CPU time. I may do something else, but I'd have to look that up.

IMPROVE ALL /DEPTH=2 is the same idea, including $a/$p with 2 $e's that have no new variables. /DEPTH=2 or greater can also lead to exponential explosions in principle, because the backtracking branches in two, but usually not in practice, and in any case SEARCH_LIMIT will catch it.

It is interesting how this is similar (and different) to my autocomplete algorithm (triggered by ! steps in mmj2). I consider theorems with no new variables, of any arity, but such that every hypothesis is shorter than the original theorem. This ensures that it will always halt (although it could blow up exponentially in principle). There is no search limit.

If IMPROVE will not consider variables in hypotheses, it will not discover 0 e. _V, because elexi reduces it to 0 e. &C1 which has a new variable.

BTW that's not what I expected the DEPTH parameter to mean. It sounds more like the branching factor. SEARCH_LIMIT is an actual depth cap.

IMPROVE ALL /DEPTH=0 sounds like the same thing as mmj2's original unification alg, which is triggered on non-! steps. This will only guess a theorem if it has all the information (no work variables, and all hypotheses filled in).

And so on.

With DEPTH > 0, sometimes longer paths get picked when shorter ones will do, but MINIMIZE will typically take care of it. By habit I often do IMPROVE ALL followed by IMPROVE ALL/DEPTH = 1 then 2 etc. if the proof didn't complete, in order to avoid unnecessary long paths, but it probably isn't required. I think my to-do list has an item to make this stepping automatic.

IMPROVE has some aggressive features like /2 and /3 and /SUBPROOFS, but I rarely use them. The most aggressive ones can often prove propositional calculus theorems from scratch. A couple of times it found proofs even shorter than Wolf Lammen's. But anything more advanced takes an unknown amount of time up to the age of the universe, and currently there is no ^C abort (it is on my to-do list). If I use /2 or /3 I save the proof and set.mm first.

Norm

David A. Wheeler

unread,

Jul 14, 2016, 7:09:05 AM7/14/16

to meta...@googlegroups.com, Mario Carneiro

On July 14, 2016 1:51:23 AM EDT, Mario Carneiro <di....@gmail.com> wrote:
>If IMPROVE will not consider variables in hypotheses, it will not
>discover
>0 e. _V, because elexi reduces it to 0 e. &C1 which has a new variable.

That is unfortunate. As I noted, that is one of the most common repeatedly proven expressions in set.mm.

Why not allow work variables, and see if they can be resolved by a later step?

--- David A.Wheeler

Norman Megill

unread,

Jul 14, 2016, 9:09:43 AM7/14/16

to meta...@googlegroups.com

Allowing a new variable is allowing a "cut". Although perhaps not in
this case, in general this can lead to an exponential explosion of the
proof tree as it backtracks, just as if we allowed ax-mp or syl.

This feature is already available with IMPROVE .../2. Normally you
wouldn't use /2 beyond prop calc, but _if you know what you are doing_
you can apply it to proofs you know will be short like 0 e. _V. I use
it all the time for this kind of thing after the regular IMPROVE ALL has
done its job. Normally I would use /2 on specific steps rather than
IMPROVE ALL, unless all the steps that are unknown are of a form like
<number> e. _V that I know will have a short proof.

MM> prove nn0ssz
...
MM-PA> delete step 26
A 4-step subproof at step 26 was deleted. Steps 26:30 are now 23:27.
23 snss.1=? $? |- 0 e. _V
MM-PA> improve all /2
Pass 1: Trying to match cut-free statements...
Pass 2: Trying to match all statements...
A proof of length 4 was found for step 23.

I don't encourage the use of /2 except in such special cases because of
the risk of running forever. It will be safer after I put in a ^C that
aborts only the search in progress rather than the whole program. At
this point, unless you are absolutely sure of what you are doing, you
should save the proof and save set.mm before using /2 (note that WRITE
SOURCE can be used inside of MM-PA).

The qualifier name "/2" is kind of meaningless - not sure what I was
thinking except that I couldn't think of a name. I should change it to
something else. Maybe someone has a suggestion. /EFFORT=2? /EXERTION=2?
/AGGRESSION=2? /PLUCK=2? /CHUTZPAH = 2? :)

Norm

Mario Carneiro

unread,

Jul 14, 2016, 9:28:08 AM7/14/16

to metamath

How about IMPROVE ALL /CUT?

What does /3 do?

Norm

Norman Megill

unread,

Jul 14, 2016, 10:46:25 AM7/14/16

to meta...@googlegroups.com

On 7/14/16 9:28 AM, Mario Carneiro wrote:
> How about IMPROVE ALL /CUT?
>
> What does /3 do?
>

From HELP IMPROVE:

/ 2 - Try to match statements with cuts. It also tries to match
steps containing working ($nn) variables when they don't share
working variables with the rest of the proof. It runs slower
than / 1.
/ 3 - Attempt to find (cut-free) proofs of $e hypotheses that result
from a trial match, unlike / 2, which only attempts (cut-free)
proofs of $f hypotheses. It runs much slower than / 1, and you
may prefer to use it with specific steps. For example, if
step 456 is unknown, you may want to use IMPROVE 456 / 3 rather
than IMPROVE ALL / 3. Note that / 3 respects the / DEPTH
qualiifer, although the expense of additional run time.
/ SUBPROOFS - Look at each subproof that isn't completely known, and
try to see if it can be proved independently. This qualifier is
meaningful only for IMPROVE ALL / 2 or IMPROVE ALL / 3. It may
take a very long time to run, especially with / 3.

Reading this over, it isn't written well, and to be honest I'm now
confused about what these actually do. I added these experimentally in
2012 and may have forgotten some details. It may be that /2 only goes
back one level through cuts. In any case, in an effort to achieve a
practical runtime, the algorithm ended up more complicated than simply
going back through statements with cuts, and I should review it and
write a better help that reflects what it currently does.

The core algorithm is contained in replaceStatement() at line 331 of
mmpfas.c and is 700 lines long. Frankly, it ended up something of a
mess as I experimented with different fine-tuning. I gave up on
cleaning it up because I was discouraged at the long runtimes except for
special cases that only an advanced user would know how to recognize. I
was tempted to remove it from metamath.exe (or leave it undocumented) so
average users wouldn't lose their proofs when it never terminated.

Historically, the REPLACE command was enhanced to be more than a dumb
match like MINIMIZE.../ALLOW_GROWTH but also made simple proof attempts
on each of the hypotheses that didn't match something already in the
proof. Then it was extended to "replace" unknown steps as an enhanced
alternative to ASSIGN (but see caveats under HELP REPLACE). Then its
algorithms were exploited by and enhanced further for IMPROVE.

Norm

David A. Wheeler

unread,

Jul 16, 2016, 7:44:19 PM7/16/16

to metamath, metamath

On Wed, 13 Jul 2016 14:21:47 -0400 (EDT), "David A. Wheeler" <dwhe...@dwheeler.com> wrote:

I earlier mentioned that mmj2's automation couldn't determine these common patterns:

> 80 |- 0 e. _V

> 42 |- 1 e. _V

Today I looked at the expressions that occur 20..41 times. mmj2 managed to automatically
prove most of them. The following weren't proven:

> 27 |- ( abs ` 1 ) = 1

> 25 |- 1 <_ 1

> 24 |- ( 2 - 1 ) = 1

> 22 |- ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )

It seems to me that "1 <_ 1" and "( 2 - 1 ) = 1" at least should be trivially automated
as a more general pattern.

The last one isn't universal, since it depends on the definition of Z.
That said, this seems to happen often:
125 rexuz3.1 $e |- Z = ( ZZ>= ` M )
126 125 uztrn2 $p |- ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )

Mario: Are you planning to transition to an improving smm3, including automation?
Are suggestions of mmj2 improvements still sensible? Even if you're going to transition
to smm3, it might be useful to improve the automation in mmj2 so that the improvements
can be ported as a unit. The automation in mmj2 is actually more capable than I was expecting.

--- David A. Wheeler

Mario Carneiro

unread,

Jul 18, 2016, 3:03:01 AM7/18/16

to metamath

On Sat, Jul 16, 2016 at 7:44 PM, David A. Wheeler <dwhe...@dwheeler.com> wrote:

On Wed, 13 Jul 2016 14:21:47 -0400 (EDT), "David A. Wheeler" <dwhe...@dwheeler.com> wrote:

I earlier mentioned that mmj2's automation couldn't determine these common patterns:
> 80 |- 0 e. _V
> 42 |- 1 e. _V

Today I looked at the expressions that occur 20..41 times. mmj2 managed to automatically
prove most of them. The following weren't proven:
> 27 |- ( abs ` 1 ) = 1
> 25 |- 1 <_ 1
> 24 |- ( 2 - 1 ) = 1
> 22 |- ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )

It seems to me that "1 <_ 1" and "( 2 - 1 ) = 1" at least should be trivially automated
as a more general pattern.

The last one isn't universal, since it depends on the definition of Z.
That said, this seems to happen often:
125 rexuz3.1 $e |- Z = ( ZZ>= ` M )
126 125 uztrn2 $p |- ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )

Since we already have a lemma for this, it can't be shortened any more than it already is.

Mario: Are you planning to transition to an improving smm3, including automation?
Are suggestions of mmj2 improvements still sensible? Even if you're going to transition
to smm3, it might be useful to improve the automation in mmj2 so that the improvements
can be ported as a unit. The automation in mmj2 is actually more capable than I was expecting.

I am still accepting and acting on bug reports and feature requests for mmj2. But there are some basic design decisions made in mmj2 that I can't change without completely rewriting the program, so I hope to get smm3 up and running as an independent proof assistant.

Mario

fl

unread,

Jul 18, 2016, 4:15:22 AM7/18/16

to Metamath

Reading this over, it isn't written well, and to be honest I'm now
confused about what these actually do.

I take this opportunity to advocate the use of literate programming
recommended by Knuth. When I take the time to comment thoroughly
an algorithm I'm always happy, several years and sometimes several months later,
to be able to rest on a precise comment. Sometimes we think we will
remember but it's an illusion.

I think the same problems can occur with theorems and proofs and we should add
a companion to set.mm with comments about them under a TeX format (not a blog).

--
FL

David A. Wheeler

unread,

Jul 18, 2016, 1:02:35 PM7/18/16

to meta...@googlegroups.com, Mario Carneiro

>> It seems to me that "1 <_ 1" and "( 2 - 1 ) = 1" at least should be
>> trivially automated
>> as a more general pattern.

Ok, feature request: auto determine patterns like this.

>> The last one isn't universal, since it depends on the definition of
>Z.
>> That said, this seems to happen often:
>> 125 rexuz3.1 $e |- Z = ( ZZ>= ` M )
>> 126 125 uztrn2 $p |- ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
>>
>
>Since we already have a lemma for this, it can't be shortened any more
>than it already is.

It's not the shortening. It's that control-U should fill that in, because it's only 1 step.

>I am still accepting and acting on bug reports and feature requests for
>mmj2. But there are some basic design decisions made in mmj2 that I
>can't
>change without completely rewriting the program, so I hope to get smm3
>up
>and running as an independent proof assistant.

Got it. I'd like for there to be a single best automated system (it could call other systems.. I just want a single place to start.)

--- David A.Wheeler

Thierry Arnoux

unread,

Jul 18, 2016, 1:40:19 PM7/18/16

to meta...@googlegroups.com, Mario Carneiro

>> I am still accepting and acting on bug reports and feature requests for
>> mmj2. But there are some basic design decisions made in mmj2 that I
>> can't
>> change without completely rewriting the program, so I hope to get smm3
>> up
>> and running as an independent proof assistant.
> Got it. I'd like for there to be a single best automated system (it could call other systems.. I just want a single place to start.)
>
>

Then shall I continue my efforts to integrate mmj2 into Eclipse?
I've just added "bracket highlighting", which I feel will make me save
lot of time when checking grammar issues in complex formulas, and I had
more on the list.
Integrating mmj2 into Eclipse made a lot of sense, because both are java
based and I could grab directly into mmj2's structures to display
information in Eclipse.
But this is also a relevant effort.

Doing the same with smm3/rust is probably possible, even if more tricky,
if this is the way we want to go.
There are ways to call rust from java (e.g.
https://github.com/java-native-access/jna) - we would have to make sure
what we use is efficient.
Then, it would be great if we designed a clean/adapted API interface
between the IDE/GUI and the parser/verifier/proof assistant from the start.

The original idea to use Eclipse was to get easily benefit of the whole
services of the IDE (syntax highlighting, integration with configuration
management software like Git, and plenty of features like histories,
diffs, import/export tools, etc.)... would you guys be willing to use
Eclipse as "IDE of choice"?

BR,
_
Thierry

Mario Carneiro

unread,

Jul 18, 2016, 1:56:53 PM7/18/16

to Thierry Arnoux, metamath

On Mon, Jul 18, 2016 at 1:40 PM, Thierry Arnoux <thierry...@gmx.net> wrote:

Then shall I continue my efforts to integrate mmj2 into Eclipse?

Yes, it is certainly still useful, plus mmj2 has a huge lead over smm3 in its total development time, so I doubt that they will be comparable any time soon, and in the meantime mmj2 is still the de facto standard proof assistant.

I've just added "bracket highlighting", which I feel will make me save lot of time when checking grammar issues in complex formulas, and I had more on the list.

Very nice! Does this not come with Eclipse by default? Are these correct in the grammar, or just approximated using the standard delimiters ( ) [ ] etc. I have had some problems getting bracket matching correct for half-open interval expressions, i.e. ( 0 [,) 1 ) does not match the outer two brackets in most text editors.

Integrating mmj2 into Eclipse made a lot of sense, because both are java based and I could grab directly into mmj2's structures to display information in Eclipse.
But this is also a relevant effort.

Doing the same with smm3/rust is probably possible, even if more tricky, if this is the way we want to go.
There are ways to call rust from java (e.g. https://github.com/java-native-access/jna) - we would have to make sure what we use is efficient.
Then, it would be great if we designed a clean/adapted API interface between the IDE/GUI and the parser/verifier/proof assistant from the start.

The interface between smm3 and other programs will be strictly pipe-based or maybe socket-based, so it is not necessary to get into the rust internals. For the basics, like the syntax highlighting extensions proposed in this thread, this would be done via a command from eclipse to run the program like so:

> sgnvalALT.smm:
$p sgnvalALT |- ( A e. RR* ->
( sgn ` A ) = if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) )
$

$ smetamath smm-verify set.mm sgnvalALT.smm

error:proof.smm:3:1-3:2 incomplete: |- ( A e. RR* ->
( sgn ` A ) = if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) )

Eclipse would be responsible for creating the command line arguments, and parsing the errors and turning them into red squiggles under the text.

The original idea to use Eclipse was to get easily benefit of the whole services of the IDE (syntax highlighting, integration with configuration management software like Git, and plenty of features like histories, diffs, import/export tools, etc.)... would you guys be willing to use Eclipse as "IDE of choice"?

Yeah, Eclipse is a great IDE with all the bells and whistles. The main downside is that it is a bit *too* complicated for writing plugins, reflecting its long history and large user base, but it seems you've already got your foot in the door, so it should be better going forward.

Mario

fl

unread,

Jul 18, 2016, 2:02:20 PM7/18/16

to Metamath, di....@gmail.com

Then shall I continue my efforts to integrate mmj2 into Eclipse?

I can't tell you. If you had asked me when you started, I would have answered that it is better
that everybody focus their efforts on only one editor. But maybe it is good that there
are two concurrent editors.

The only problem that puzzles me is: don't you have efficiency issues with set.mm within Eclipse?

The original idea to use Eclipse was to get easily benefit of the whole
services of the IDE (syntax highlighting, integration with configuration
management software like Git, and plenty of features like histories,
diffs, import/export tools, etc.)

It was clear.

would you guys be willing to use Eclipse as "IDE of choice"?

If somebody asked me why I want in mmj2 (and in any other editor) my answer would be:
a well designed language to retrieve
interesting theorems (in the spirit of the regexps but more appropriate to set.mm). And algorithms
to manipulate the tree of statements
(removing those that are no longer referenced, selectionning a whole subtree, highlighting it,
deleting it, moving it). And I would also appreciate snippets of metamath codes that I only need
to copy and then to paste (I mean with $. after the distinct variable statements for instance.)

--
FL

Thierry Arnoux

unread,

Jul 18, 2016, 2:22:45 PM7/18/16

to Mario Carneiro, metamath

On 19/07/2016 01:56, Mario Carneiro wrote:

On Mon, Jul 18, 2016 at 1:40 PM, Thierry Arnoux <thierry...@gmx.net> wrote:

I've just added "bracket highlighting", which I feel will make me save lot of time when checking grammar issues in complex formulas, and I had more on the list.

Very nice! Does this not come with Eclipse by default? Are these correct in the grammar, or just approximated using the standard delimiters ( ) [ ] etc. I have had some problems getting bracket matching correct for half-open interval expressions, i.e. ( 0 [,) 1 ) does not match the outer two brackets in most text editors.

Yes, they shall be. This is based on MM tokens, so [,) is considered as a whole and does not match with (.
I've also added support for multi-character brackets, like <. , >. or $( ... $) or even $p ... $.

I have not integrated the macros yet, though.

Integrating mmj2 into Eclipse made a lot of sense, because both are java based and I could grab directly into mmj2's structures to display information in Eclipse.
But this is also a relevant effort.

Doing the same with smm3/rust is probably possible, even if more tricky, if this is the way we want to go.
There are ways to call rust from java (e.g. https://github.com/java-native-access/jna) - we would have to make sure what we use is efficient.
Then, it would be great if we designed a clean/adapted API interface between the IDE/GUI and the parser/verifier/proof assistant from the start.

The interface between smm3 and other programs will be strictly pipe-based or maybe socket-based, so it is not necessary to get into the rust internals. For the basics, like the syntax highlighting extensions proposed in this thread, this would be done via a command from eclipse to run the program like so:

> sgnvalALT.smm:
$p sgnvalALT |- ( A e. RR* ->
( sgn ` A ) = if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) )
$

$ smetamath smm-verify set.mm sgnvalALT.smm

error:proof.smm:3:1-3:2 incomplete: |- ( A e. RR* ->
( sgn ` A ) = if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) )

Eclipse would be responsible for creating the command line arguments, and parsing the errors and turning them into red squiggles under the text.

Yes, that would certainly be feasible, even if I would prefer directly getting the numeric value, rather than parsing a string.
Also, for example, Eclipse does not need to save the editor's content when doing the syntax checks, it's working off-memory.
I guess I would need to force the user to save his work on disk before each operation.
A nice feature would be to be able to undo proof assistant operations step by step and not the whole file - this means that SMM3 would have to provide the different positions changed in the proof, and the new contents. Is that how you see it?

The original idea to use Eclipse was to get easily benefit of the whole services of the IDE (syntax highlighting, integration with configuration management software like Git, and plenty of features like histories, diffs, import/export tools, etc.)... would you guys be willing to use Eclipse as "IDE of choice"?

Yeah, Eclipse is a great IDE with all the bells and whistles. The main downside is that it is a bit *too* complicated for writing plugins, reflecting its long history and large user base, but it seems you've already got your foot in the door, so it should be better going forward.

Yes, and a lot could be reused.
If in the mood, I could try to list the hooks I would need.

BR,
_
Thierry

Mario Carneiro

unread,

Jul 18, 2016, 2:39:53 PM7/18/16

to Thierry Arnoux, metamath

On Mon, Jul 18, 2016 at 2:22 PM, Thierry Arnoux <thierry...@gmx.net> wrote:

On 19/07/2016 01:56, Mario Carneiro wrote:

Integrating mmj2 into Eclipse made a lot of sense, because both are java based and I could grab directly into mmj2's structures to display information in Eclipse.
But this is also a relevant effort.

Doing the same with smm3/rust is probably possible, even if more tricky, if this is the way we want to go.
There are ways to call rust from java (e.g. https://github.com/java-native-access/jna) - we would have to make sure what we use is efficient.
Then, it would be great if we designed a clean/adapted API interface between the IDE/GUI and the parser/verifier/proof assistant from the start.

The interface between smm3 and other programs will be strictly pipe-based or maybe socket-based, so it is not necessary to get into the rust internals. For the basics, like the syntax highlighting extensions proposed in this thread, this would be done via a command from eclipse to run the program like so:

> sgnvalALT.smm:
$p sgnvalALT |- ( A e. RR* ->
( sgn ` A ) = if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) )
$

$ smetamath smm-verify set.mm sgnvalALT.smm

error:proof.smm:3:1-3:2 incomplete: |- ( A e. RR* ->
( sgn ` A ) = if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) )

Eclipse would be responsible for creating the command line arguments, and parsing the errors and turning them into red squiggles under the text.

Yes, that would certainly be feasible, even if I would prefer directly getting the numeric value, rather than parsing a string.
Also, for example, Eclipse does not need to save the editor's content when doing the syntax checks, it's working off-memory.
I guess I would need to force the user to save his work on disk before each operation.

There are a few options to resolve this. First, it could take the file on stdin instead of via a file specified on the command line. This would avoid the need to save the file. Also, to avoid startup costs it will probably be desirable to keep smm3 running in the background rather than starting a new process each time something is needed; but that means it will be acting like a server. You can use stdin and stdout for this, but it is probably more flexible to just open a socket connection between the processes and transmit information that way.

I would not recommend attempting to recreate the smm3 data structures exactly in eclipse; they are optimized for rust usage and you will need to map them over to Emetamath primitives (mmj2 primitives?) anyway. The advantage of the bare bones stdin/stdout approach is that it is maximally compatible with arbitrary new IDEs, and also seems to be the common mode of operation among compilers, which are the primary inspiration here.

A nice feature would be to be able to undo proof assistant operations step by step and not the whole file - this means that SMM3 would have to provide the different positions changed in the proof, and the new contents. Is that how you see it?

At least with the method described in this thread, the proof script is not changed by smm3 directly, the way mmj2 does. It only hints the user what to type in various locations. If you are dealing with this in mmj2, there's nothing you can do about it: it will erase the whole file and recreate it on each unify, using step names to track the cursor location across worksheet versions. Perhaps a diff will get close, but you would have to figure it out yourself, since the difference data isn't there to begin with.

Mario

Thierry Arnoux

unread,

Jul 18, 2016, 2:46:51 PM7/18/16

to meta...@googlegroups.com, di....@gmail.com

On 19/07/2016 02:02, 'fl' via Metamath wrote:

Then shall I continue my efforts to integrate mmj2 into Eclipse?

I can't tell you. If you had asked me when you started, I would have answered that it is better
that everybody focus their efforts on only one editor. But maybe it is good that there
are two concurrent editors.

The only problem that puzzles me is: don't you have efficiency issues with set.mm within Eclipse?

I have no issue with set.mm. I can see it with syntax highlighting.

The original idea to use Eclipse was to get easily benefit of the whole
services of the IDE (syntax highlighting, integration with configuration
management software like Git, and plenty of features like histories,
diffs, import/export tools, etc.)

It was clear.

would you guys be willing to use Eclipse as "IDE of choice"?

If somebody asked me why I want in mmj2 (and in any other editor) my answer would be:
a well designed language to retrieve
interesting theorems (in the spirit of the regexps but more appropriate to set.mm).

I see what you mean. In the sense of "there must be a theorem linking the dominance relation A ~<_ B and the sizes ( # ` A ) <_ ( # ` B ) ". What is it?

And algorithms
to manipulate the tree of statements
(removing those that are no longer referenced, selectionning a whole subtree, highlighting it,
deleting it, moving it).

In this sense, I was considering creating a special view where you can select a step, and view its antecedents and/or descendants as a tree.
This could be linked with the proof assistant and highlight the corresponding lines.

And I would also appreciate snippets of metamath codes that I only need
to copy and then to paste (I mean with $. after the distinct variable statements for instance.)

This would be content assist (autocompletion), triggered when you press CTRL-SPACE, which shows you a list of possible completions to choose from.
I was considering using it for the step selector in the proof assistant...
This could also be used in MM files for templates, i.e. to automatically create a skeleton for a proof.

Well, I would also be interested in those features... but let's have the core working well first!

--
FL

fl

unread,

Jul 19, 2016, 6:50:25 AM7/19/16

to Metamath, di....@gmail.com

I have no issue with set.mm. I can see it with syntax highlighting.

Right.

I see what you mean. In the sense of "there must be a theorem linking the dominance relation A ~<_ B and the sizes ( # ` A ) <_ ( # ` B ) ". What is it?

Exactly this.

And algorithms
to manipulate the tree of statements
(removing those that are no longer referenced, selectionning a whole subtree, highlighting it,
deleting it, moving it).

In this sense, I was considering creating a special view where you can select a step, and view its antecedents and/or descendants as a tree.
This could be linked with the proof assistant and highlight the corresponding lines.

If the lines of the subtree were highlighted it would already be a step forward.

But could we then select the subtree and move it or delete it?

--

FL

Reply all

Reply to author

Forward