Theorem gexid

Description: Any element to the power of the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016)

	Ref	Expression
Hypotheses	gexcl.1	|- X = ( Base ` G )
	gexcl.2	|- E = ( gEx ` G )
	gexid.3	|- .x. = ( .g ` G )
	gexid.4	|- .0. = ( 0g ` G )
Assertion	gexid	|- ( A e. X -> ( E .x. A ) = .0. )

Proof

Step	Hyp	Ref	Expression
1		gexcl.1	|- X = ( Base ` G )
2		gexcl.2	|- E = ( gEx ` G )
3		gexid.3	|- .x. = ( .g ` G )
4		gexid.4	|- .0. = ( 0g ` G )
5		oveq1	|- ( E = 0 -> ( E .x. A ) = ( 0 .x. A ) )
6	1 4 3	mulg0	|- ( A e. X -> ( 0 .x. A ) = .0. )
7	5 6	sylan9eqr	|- ( ( A e. X /\ E = 0 ) -> ( E .x. A ) = .0. )
8	7	adantrr	|- ( ( A e. X /\ ( E = 0 /\ { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) ) ) -> ( E .x. A ) = .0. )
9		oveq1	|- ( y = E -> ( y .x. x ) = ( E .x. x ) )
10	9	eqeq1d	|- ( y = E -> ( ( y .x. x ) = .0. <-> ( E .x. x ) = .0. ) )
11	10	ralbidv	|- ( y = E -> ( A. x e. X ( y .x. x ) = .0. <-> A. x e. X ( E .x. x ) = .0. ) )
12	11	elrab	|- ( E e. { y e. NN | A. x e. X ( y .x. x ) = .0. } <-> ( E e. NN /\ A. x e. X ( E .x. x ) = .0. ) )
13	12	simprbi	|- ( E e. { y e. NN | A. x e. X ( y .x. x ) = .0. } -> A. x e. X ( E .x. x ) = .0. )
14		oveq2	|- ( x = A -> ( E .x. x ) = ( E .x. A ) )
15	14	eqeq1d	|- ( x = A -> ( ( E .x. x ) = .0. <-> ( E .x. A ) = .0. ) )
16	15	rspcva	|- ( ( A e. X /\ A. x e. X ( E .x. x ) = .0. ) -> ( E .x. A ) = .0. )
17	13 16	sylan2	|- ( ( A e. X /\ E e. { y e. NN | A. x e. X ( y .x. x ) = .0. } ) -> ( E .x. A ) = .0. )
18		elfvex	|- ( A e. ( Base ` G ) -> G e. _V )
19	18 1	eleq2s	|- ( A e. X -> G e. _V )
20		eqid	|- { y e. NN | A. x e. X ( y .x. x ) = .0. } = { y e. NN | A. x e. X ( y .x. x ) = .0. }
21	1 3 4 2 20	gexlem1	|- ( G e. _V -> ( ( E = 0 /\ { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) ) \/ E e. { y e. NN | A. x e. X ( y .x. x ) = .0. } ) )
22	19 21	syl	|- ( A e. X -> ( ( E = 0 /\ { y e. NN | A. x e. X ( y .x. x ) = .0. } = (/) ) \/ E e. { y e. NN | A. x e. X ( y .x. x ) = .0. } ) )
23	8 17 22	mpjaodan	|- ( A e. X -> ( E .x. A ) = .0. )