Theorem odval

Description: Second substitution for the group order definition. (Contributed by Mario Carneiro, 13-Jul-2014) (Revised by Stefan O'Rear, 5-Sep-2015) (Revised by AV, 5-Oct-2020)

	Ref	Expression
Hypotheses	odval.1	|- X = ( Base ` G )
	odval.2	|- .x. = ( .g ` G )
	odval.3	|- .0. = ( 0g ` G )
	odval.4	|- O = ( od ` G )
	odval.i	|- I = { y e. NN | ( y .x. A ) = .0. }
Assertion	odval	|- ( A e. X -> ( O ` A ) = if ( I = (/) , 0 , inf ( I , RR , < ) ) )

Proof

Step	Hyp	Ref	Expression
1		odval.1	|- X = ( Base ` G )
2		odval.2	|- .x. = ( .g ` G )
3		odval.3	|- .0. = ( 0g ` G )
4		odval.4	|- O = ( od ` G )
5		odval.i	|- I = { y e. NN | ( y .x. A ) = .0. }
6		oveq2	|- ( x = A -> ( y .x. x ) = ( y .x. A ) )
7	6	eqeq1d	|- ( x = A -> ( ( y .x. x ) = .0. <-> ( y .x. A ) = .0. ) )
8	7	rabbidv	|- ( x = A -> { y e. NN | ( y .x. x ) = .0. } = { y e. NN | ( y .x. A ) = .0. } )
9	8 5	eqtr4di	|- ( x = A -> { y e. NN | ( y .x. x ) = .0. } = I )
10	9	csbeq1d	|- ( x = A -> [_ { y e. NN | ( y .x. x ) = .0. } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) = [_ I / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) )
11		nnex	|- NN e. _V
12	5 11	rabex2	|- I e. _V
13		eqeq1	|- ( i = I -> ( i = (/) <-> I = (/) ) )
14		infeq1	|- ( i = I -> inf ( i , RR , < ) = inf ( I , RR , < ) )
15	13 14	ifbieq2d	|- ( i = I -> if ( i = (/) , 0 , inf ( i , RR , < ) ) = if ( I = (/) , 0 , inf ( I , RR , < ) ) )
16	12 15	csbie	|- [_ I / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) = if ( I = (/) , 0 , inf ( I , RR , < ) )
17	10 16	eqtrdi	|- ( x = A -> [_ { y e. NN | ( y .x. x ) = .0. } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) = if ( I = (/) , 0 , inf ( I , RR , < ) ) )
18	1 2 3 4	odfval	|- O = ( x e. X |-> [_ { y e. NN | ( y .x. x ) = .0. } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) )
19		c0ex	|- 0 e. _V
20		ltso	|- < Or RR
21	20	infex	|- inf ( I , RR , < ) e. _V
22	19 21	ifex	|- if ( I = (/) , 0 , inf ( I , RR , < ) ) e. _V
23	17 18 22	fvmpt	|- ( A e. X -> ( O ` A ) = if ( I = (/) , 0 , inf ( I , RR , < ) ) )