Metamath Proof Explorer


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 · ˙ = G
gexid.4 0 ˙ = 0 G
Assertion gexid A X E · ˙ A = 0 ˙

Proof

Step Hyp Ref Expression
1 gexcl.1 X = Base G
2 gexcl.2 E = gEx G
3 gexid.3 · ˙ = G
4 gexid.4 0 ˙ = 0 G
5 oveq1 E = 0 E · ˙ A = 0 · ˙ A
6 1 4 3 mulg0 A X 0 · ˙ A = 0 ˙
7 5 6 sylan9eqr A X E = 0 E · ˙ A = 0 ˙
8 7 adantrr A X E = 0 y | x X y · ˙ x = 0 ˙ = E · ˙ A = 0 ˙
9 oveq1 y = E y · ˙ x = E · ˙ x
10 9 eqeq1d y = E y · ˙ x = 0 ˙ E · ˙ x = 0 ˙
11 10 ralbidv y = E x X y · ˙ x = 0 ˙ x X E · ˙ x = 0 ˙
12 11 elrab E y | x X y · ˙ x = 0 ˙ E x X E · ˙ x = 0 ˙
13 12 simprbi E y | x X y · ˙ x = 0 ˙ x X E · ˙ x = 0 ˙
14 oveq2 x = A E · ˙ x = E · ˙ A
15 14 eqeq1d x = A E · ˙ x = 0 ˙ E · ˙ A = 0 ˙
16 15 rspcva A X x X E · ˙ x = 0 ˙ E · ˙ A = 0 ˙
17 13 16 sylan2 A X E y | x X y · ˙ x = 0 ˙ E · ˙ A = 0 ˙
18 elfvex A Base G G V
19 18 1 eleq2s A X G V
20 eqid y | x X y · ˙ x = 0 ˙ = y | x X y · ˙ x = 0 ˙
21 1 3 4 2 20 gexlem1 G V E = 0 y | x X y · ˙ x = 0 ˙ = E y | x X y · ˙ x = 0 ˙
22 19 21 syl A X E = 0 y | x X y · ˙ x = 0 ˙ = E y | x X y · ˙ x = 0 ˙
23 8 17 22 mpjaodan A X E · ˙ A = 0 ˙