Step |
Hyp |
Ref |
Expression |
1 |
|
df-br |
⊢ ( 𝐺 RingOps 𝐻 ↔ ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ) |
2 |
|
relrngo |
⊢ Rel RingOps |
3 |
2
|
brrelex12i |
⊢ ( 𝐺 RingOps 𝐻 → ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) ) |
4 |
|
op1stg |
⊢ ( ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) → ( 1st ‘ ⟨ 𝐺 , 𝐻 ⟩ ) = 𝐺 ) |
5 |
3 4
|
syl |
⊢ ( 𝐺 RingOps 𝐻 → ( 1st ‘ ⟨ 𝐺 , 𝐻 ⟩ ) = 𝐺 ) |
6 |
1 5
|
sylbir |
⊢ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps → ( 1st ‘ ⟨ 𝐺 , 𝐻 ⟩ ) = 𝐺 ) |
7 |
|
eqid |
⊢ ( 1st ‘ ⟨ 𝐺 , 𝐻 ⟩ ) = ( 1st ‘ ⟨ 𝐺 , 𝐻 ⟩ ) |
8 |
7
|
rngoablo |
⊢ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps → ( 1st ‘ ⟨ 𝐺 , 𝐻 ⟩ ) ∈ AbelOp ) |
9 |
6 8
|
eqeltrrd |
⊢ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps → 𝐺 ∈ AbelOp ) |