Theorem gexid

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

	Ref	Expression
Hypotheses	gexcl.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
	gexcl.2	⊢ 𝐸 = ( gEx ‘ 𝐺 )
	gexid.3	⊢ · = ( .g ‘ 𝐺 )
	gexid.4	⊢ 0 = ( 0g ‘ 𝐺 )
Assertion	gexid	⊢ ( 𝐴 ∈ 𝑋 → ( 𝐸 · 𝐴 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		gexcl.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		gexcl.2	⊢ 𝐸 = ( gEx ‘ 𝐺 )
3		gexid.3	⊢ · = ( .g ‘ 𝐺 )
4		gexid.4	⊢ 0 = ( 0g ‘ 𝐺 )
5		oveq1	⊢ ( 𝐸 = 0 → ( 𝐸 · 𝐴 ) = ( 0 · 𝐴 ) )
6	1 4 3	mulg0	⊢ ( 𝐴 ∈ 𝑋 → ( 0 · 𝐴 ) = 0 )
7	5 6	sylan9eqr	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐸 = 0 ) → ( 𝐸 · 𝐴 ) = 0 )
8	7	adantrr	⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( 𝐸 = 0 ∧ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } = ∅ ) ) → ( 𝐸 · 𝐴 ) = 0 )
9		oveq1	⊢ ( 𝑦 = 𝐸 → ( 𝑦 · 𝑥 ) = ( 𝐸 · 𝑥 ) )
10	9	eqeq1d	⊢ ( 𝑦 = 𝐸 → ( ( 𝑦 · 𝑥 ) = 0 ↔ ( 𝐸 · 𝑥 ) = 0 ) )
11	10	ralbidv	⊢ ( 𝑦 = 𝐸 → ( ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 ↔ ∀ 𝑥 ∈ 𝑋 ( 𝐸 · 𝑥 ) = 0 ) )
12	11	elrab	⊢ ( 𝐸 ∈ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } ↔ ( 𝐸 ∈ ℕ ∧ ∀ 𝑥 ∈ 𝑋 ( 𝐸 · 𝑥 ) = 0 ) )
13	12	simprbi	⊢ ( 𝐸 ∈ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } → ∀ 𝑥 ∈ 𝑋 ( 𝐸 · 𝑥 ) = 0 )
14		oveq2	⊢ ( 𝑥 = 𝐴 → ( 𝐸 · 𝑥 ) = ( 𝐸 · 𝐴 ) )
15	14	eqeq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝐸 · 𝑥 ) = 0 ↔ ( 𝐸 · 𝐴 ) = 0 ) )
16	15	rspcva	⊢ ( ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( 𝐸 · 𝑥 ) = 0 ) → ( 𝐸 · 𝐴 ) = 0 )
17	13 16	sylan2	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐸 ∈ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } ) → ( 𝐸 · 𝐴 ) = 0 )
18		elfvex	⊢ ( 𝐴 ∈ ( Base ‘ 𝐺 ) → 𝐺 ∈ V )
19	18 1	eleq2s	⊢ ( 𝐴 ∈ 𝑋 → 𝐺 ∈ V )
20		eqid	⊢ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } = { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 }
21	1 3 4 2 20	gexlem1	⊢ ( 𝐺 ∈ V → ( ( 𝐸 = 0 ∧ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } = ∅ ) ∨ 𝐸 ∈ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } ) )
22	19 21	syl	⊢ ( 𝐴 ∈ 𝑋 → ( ( 𝐸 = 0 ∧ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } = ∅ ) ∨ 𝐸 ∈ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } ) )
23	8 17 22	mpjaodan	⊢ ( 𝐴 ∈ 𝑋 → ( 𝐸 · 𝐴 ) = 0 )