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 |
1 2 3 4 5
|
gexval |
⊢ ( 𝐺 ∈ 𝑉 → 𝐸 = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) ) |
7 |
|
eqeq2 |
⊢ ( 0 = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) → ( 𝐸 = 0 ↔ 𝐸 = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) ) ) |
8 |
7
|
imbi1d |
⊢ ( 0 = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) → ( ( 𝐸 = 0 → ( ( 𝐸 = 0 ∧ 𝐼 = ∅ ) ∨ 𝐸 ∈ 𝐼 ) ) ↔ ( 𝐸 = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) → ( ( 𝐸 = 0 ∧ 𝐼 = ∅ ) ∨ 𝐸 ∈ 𝐼 ) ) ) ) |
9 |
|
eqeq2 |
⊢ ( inf ( 𝐼 , ℝ , < ) = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) → ( 𝐸 = inf ( 𝐼 , ℝ , < ) ↔ 𝐸 = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) ) ) |
10 |
9
|
imbi1d |
⊢ ( inf ( 𝐼 , ℝ , < ) = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) → ( ( 𝐸 = inf ( 𝐼 , ℝ , < ) → ( ( 𝐸 = 0 ∧ 𝐼 = ∅ ) ∨ 𝐸 ∈ 𝐼 ) ) ↔ ( 𝐸 = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) → ( ( 𝐸 = 0 ∧ 𝐼 = ∅ ) ∨ 𝐸 ∈ 𝐼 ) ) ) ) |
11 |
|
orc |
⊢ ( ( 𝐸 = 0 ∧ 𝐼 = ∅ ) → ( ( 𝐸 = 0 ∧ 𝐼 = ∅ ) ∨ 𝐸 ∈ 𝐼 ) ) |
12 |
11
|
expcom |
⊢ ( 𝐼 = ∅ → ( 𝐸 = 0 → ( ( 𝐸 = 0 ∧ 𝐼 = ∅ ) ∨ 𝐸 ∈ 𝐼 ) ) ) |
13 |
12
|
adantl |
⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝐼 = ∅ ) → ( 𝐸 = 0 → ( ( 𝐸 = 0 ∧ 𝐼 = ∅ ) ∨ 𝐸 ∈ 𝐼 ) ) ) |
14 |
|
ssrab2 |
⊢ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } ⊆ ℕ |
15 |
|
nnuz |
⊢ ℕ = ( ℤ≥ ‘ 1 ) |
16 |
15
|
eqcomi |
⊢ ( ℤ≥ ‘ 1 ) = ℕ |
17 |
14 5 16
|
3sstr4i |
⊢ 𝐼 ⊆ ( ℤ≥ ‘ 1 ) |
18 |
|
neqne |
⊢ ( ¬ 𝐼 = ∅ → 𝐼 ≠ ∅ ) |
19 |
18
|
adantl |
⊢ ( ( 𝐺 ∈ 𝑉 ∧ ¬ 𝐼 = ∅ ) → 𝐼 ≠ ∅ ) |
20 |
|
infssuzcl |
⊢ ( ( 𝐼 ⊆ ( ℤ≥ ‘ 1 ) ∧ 𝐼 ≠ ∅ ) → inf ( 𝐼 , ℝ , < ) ∈ 𝐼 ) |
21 |
17 19 20
|
sylancr |
⊢ ( ( 𝐺 ∈ 𝑉 ∧ ¬ 𝐼 = ∅ ) → inf ( 𝐼 , ℝ , < ) ∈ 𝐼 ) |
22 |
|
eleq1a |
⊢ ( inf ( 𝐼 , ℝ , < ) ∈ 𝐼 → ( 𝐸 = inf ( 𝐼 , ℝ , < ) → 𝐸 ∈ 𝐼 ) ) |
23 |
21 22
|
syl |
⊢ ( ( 𝐺 ∈ 𝑉 ∧ ¬ 𝐼 = ∅ ) → ( 𝐸 = inf ( 𝐼 , ℝ , < ) → 𝐸 ∈ 𝐼 ) ) |
24 |
|
olc |
⊢ ( 𝐸 ∈ 𝐼 → ( ( 𝐸 = 0 ∧ 𝐼 = ∅ ) ∨ 𝐸 ∈ 𝐼 ) ) |
25 |
23 24
|
syl6 |
⊢ ( ( 𝐺 ∈ 𝑉 ∧ ¬ 𝐼 = ∅ ) → ( 𝐸 = inf ( 𝐼 , ℝ , < ) → ( ( 𝐸 = 0 ∧ 𝐼 = ∅ ) ∨ 𝐸 ∈ 𝐼 ) ) ) |
26 |
8 10 13 25
|
ifbothda |
⊢ ( 𝐺 ∈ 𝑉 → ( 𝐸 = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) → ( ( 𝐸 = 0 ∧ 𝐼 = ∅ ) ∨ 𝐸 ∈ 𝐼 ) ) ) |
27 |
6 26
|
mpd |
⊢ ( 𝐺 ∈ 𝑉 → ( ( 𝐸 = 0 ∧ 𝐼 = ∅ ) ∨ 𝐸 ∈ 𝐼 ) ) |