Theorem odval

Description: Second substitution for the group order definition. (Contributed by Mario Carneiro, 13-Jul-2014) (Revised by Stefan O'Rear, 5-Sep-2015) (Revised by AV, 5-Oct-2020)

	Ref	Expression
Hypotheses	odval.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
	odval.2	⊢ · = ( .g ‘ 𝐺 )
	odval.3	⊢ 0 = ( 0g ‘ 𝐺 )
	odval.4	⊢ 𝑂 = ( od ‘ 𝐺 )
	odval.i	⊢ 𝐼 = { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 }
Assertion	odval	⊢ ( 𝐴 ∈ 𝑋 → ( 𝑂 ‘ 𝐴 ) = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) )

Proof

Step	Hyp	Ref	Expression
1		odval.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		odval.2	⊢ · = ( .g ‘ 𝐺 )
3		odval.3	⊢ 0 = ( 0g ‘ 𝐺 )
4		odval.4	⊢ 𝑂 = ( od ‘ 𝐺 )
5		odval.i	⊢ 𝐼 = { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 }
6		oveq2	⊢ ( 𝑥 = 𝐴 → ( 𝑦 · 𝑥 ) = ( 𝑦 · 𝐴 ) )
7	6	eqeq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑦 · 𝑥 ) = 0 ↔ ( 𝑦 · 𝐴 ) = 0 ) )
8	7	rabbidv	⊢ ( 𝑥 = 𝐴 → { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } = { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } )
9	8 5	eqtr4di	⊢ ( 𝑥 = 𝐴 → { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } = 𝐼 )
10	9	csbeq1d	⊢ ( 𝑥 = 𝐴 → ⦋ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) = ⦋ 𝐼 / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) )
11		nnex	⊢ ℕ ∈ V
12	5 11	rabex2	⊢ 𝐼 ∈ V
13		eqeq1	⊢ ( 𝑖 = 𝐼 → ( 𝑖 = ∅ ↔ 𝐼 = ∅ ) )
14		infeq1	⊢ ( 𝑖 = 𝐼 → inf ( 𝑖 , ℝ , < ) = inf ( 𝐼 , ℝ , < ) )
15	13 14	ifbieq2d	⊢ ( 𝑖 = 𝐼 → if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) )
16	12 15	csbie	⊢ ⦋ 𝐼 / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) )
17	10 16	eqtrdi	⊢ ( 𝑥 = 𝐴 → ⦋ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) )
18	1 2 3 4	odfval	⊢ 𝑂 = ( 𝑥 ∈ 𝑋 ↦ ⦋ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝑥 ) = 0 } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) )
19		c0ex	⊢ 0 ∈ V
20		ltso	⊢ < Or ℝ
21	20	infex	⊢ inf ( 𝐼 , ℝ , < ) ∈ V
22	19 21	ifex	⊢ if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) ∈ V
23	17 18 22	fvmpt	⊢ ( 𝐴 ∈ 𝑋 → ( 𝑂 ‘ 𝐴 ) = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) )