Metamath Proof Explorer

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 syl5eq ⊢ ( 𝐺 ∈ 𝑉 → 𝐸 = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) )