Theorem gexval

Description: Value of the exponent of a group. (Contributed by Mario Carneiro, 23-Apr-2016) (Revised by AV, 26-Sep-2020)

	Ref	Expression
Hypotheses	gexval.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
	gexval.2	⊢ · = ( .g ‘ 𝐺 )
	gexval.3	⊢ 0 = ( 0g ‘ 𝐺 )
	gexval.4	⊢ 𝐸 = ( gEx ‘ 𝐺 )
	gexval.i	⊢ 𝐼 = { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 }
Assertion	gexval	⊢ ( 𝐺 ∈ 𝑉 → 𝐸 = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) )

Proof

Step	Hyp	Ref	Expression
1		gexval.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		gexval.2	⊢ · = ( .g ‘ 𝐺 )
3		gexval.3	⊢ 0 = ( 0g ‘ 𝐺 )
4		gexval.4	⊢ 𝐸 = ( gEx ‘ 𝐺 )
5		gexval.i	⊢ 𝐼 = { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 }
6		df-gex	⊢ gEx = ( 𝑔 ∈ V ↦ ⦋ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑦 ( .g ‘ 𝑔 ) 𝑥 ) = ( 0g ‘ 𝑔 ) } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) )
7		nnex	⊢ ℕ ∈ V
8	7	rabex	⊢ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑦 ( .g ‘ 𝑔 ) 𝑥 ) = ( 0g ‘ 𝑔 ) } ∈ V
9	8	a1i	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺 ) → { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑦 ( .g ‘ 𝑔 ) 𝑥 ) = ( 0g ‘ 𝑔 ) } ∈ V )
10		simpr	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺 ) → 𝑔 = 𝐺 )
11	10	fveq2d	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺 ) → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
12	11 1	eqtr4di	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺 ) → ( Base ‘ 𝑔 ) = 𝑋 )
13	10	fveq2d	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺 ) → ( .g ‘ 𝑔 ) = ( .g ‘ 𝐺 ) )
14	13 2	eqtr4di	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺 ) → ( .g ‘ 𝑔 ) = · )
15	14	oveqd	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺 ) → ( 𝑦 ( .g ‘ 𝑔 ) 𝑥 ) = ( 𝑦 · 𝑥 ) )
16	10	fveq2d	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺 ) → ( 0g ‘ 𝑔 ) = ( 0g ‘ 𝐺 ) )
17	16 3	eqtr4di	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺 ) → ( 0g ‘ 𝑔 ) = 0 )
18	15 17	eqeq12d	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺 ) → ( ( 𝑦 ( .g ‘ 𝑔 ) 𝑥 ) = ( 0g ‘ 𝑔 ) ↔ ( 𝑦 · 𝑥 ) = 0 ) )
19	12 18	raleqbidv	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺 ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑦 ( .g ‘ 𝑔 ) 𝑥 ) = ( 0g ‘ 𝑔 ) ↔ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 ) )
20	19	rabbidv	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺 ) → { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑦 ( .g ‘ 𝑔 ) 𝑥 ) = ( 0g ‘ 𝑔 ) } = { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } )
21	20 5	eqtr4di	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺 ) → { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑦 ( .g ‘ 𝑔 ) 𝑥 ) = ( 0g ‘ 𝑔 ) } = 𝐼 )
22	21	eqeq2d	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺 ) → ( 𝑖 = { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑦 ( .g ‘ 𝑔 ) 𝑥 ) = ( 0g ‘ 𝑔 ) } ↔ 𝑖 = 𝐼 ) )
23	22	biimpa	⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺 ) ∧ 𝑖 = { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑦 ( .g ‘ 𝑔 ) 𝑥 ) = ( 0g ‘ 𝑔 ) } ) → 𝑖 = 𝐼 )
24	23	eqeq1d	⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺 ) ∧ 𝑖 = { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑦 ( .g ‘ 𝑔 ) 𝑥 ) = ( 0g ‘ 𝑔 ) } ) → ( 𝑖 = ∅ ↔ 𝐼 = ∅ ) )
25	23	infeq1d	⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺 ) ∧ 𝑖 = { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑦 ( .g ‘ 𝑔 ) 𝑥 ) = ( 0g ‘ 𝑔 ) } ) → inf ( 𝑖 , ℝ , < ) = inf ( 𝐼 , ℝ , < ) )
26	24 25	ifbieq2d	⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺 ) ∧ 𝑖 = { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑦 ( .g ‘ 𝑔 ) 𝑥 ) = ( 0g ‘ 𝑔 ) } ) → if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) )
27	9 26	csbied	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺 ) → ⦋ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑦 ( .g ‘ 𝑔 ) 𝑥 ) = ( 0g ‘ 𝑔 ) } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) )
28		elex	⊢ ( 𝐺 ∈ 𝑉 → 𝐺 ∈ V )
29		c0ex	⊢ 0 ∈ V
30		ltso	⊢ < Or ℝ
31	30	infex	⊢ inf ( 𝐼 , ℝ , < ) ∈ V
32	29 31	ifex	⊢ if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) ∈ V
33	32	a1i	⊢ ( 𝐺 ∈ 𝑉 → if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) ∈ V )
34	6 27 28 33	fvmptd2	⊢ ( 𝐺 ∈ 𝑉 → ( gEx ‘ 𝐺 ) = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) )
35	4 34	eqtrid	⊢ ( 𝐺 ∈ 𝑉 → 𝐸 = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) )