Metamath Proof Explorer

Theorem iscom2

Description: A device to add commutativity to various sorts of rings. (Contributed by FL, 6-Sep-2009) (New usage is discouraged.)

Ref Expression
Assertion iscom2 ⊢ G ∈ A ∧ H ∈ B → G H ∈ Com2 ↔ ∀ a ∈ ran ⁡ G ∀ b ∈ ran ⁡ G a H b = b H a

Proof

Step Hyp Ref Expression
1 df-com2 ⊢ Com2 = x y | ∀ a ∈ ran ⁡ x ∀ b ∈ ran ⁡ x a y b = b y a
2 1 a1i ⊢ G ∈ A ∧ H ∈ B → Com2 = x y | ∀ a ∈ ran ⁡ x ∀ b ∈ ran ⁡ x a y b = b y a
3 2 eleq2d ⊢ G ∈ A ∧ H ∈ B → G H ∈ Com2 ↔ G H ∈ x y | ∀ a ∈ ran ⁡ x ∀ b ∈ ran ⁡ x a y b = b y a
4 rneq ⊢ x = G → ran ⁡ x = ran ⁡ G
5 4 raleqdv ⊢ x = G → ∀ b ∈ ran ⁡ x a y b = b y a ↔ ∀ b ∈ ran ⁡ G a y b = b y a
6 4 5 raleqbidv ⊢ x = G → ∀ a ∈ ran ⁡ x ∀ b ∈ ran ⁡ x a y b = b y a ↔ ∀ a ∈ ran ⁡ G ∀ b ∈ ran ⁡ G a y b = b y a
7 oveq ⊢ y = H → a y b = a H b
8 oveq ⊢ y = H → b y a = b H a
9 7 8 eqeq12d ⊢ y = H → a y b = b y a ↔ a H b = b H a
10 9 2ralbidv ⊢ y = H → ∀ a ∈ ran ⁡ G ∀ b ∈ ran ⁡ G a y b = b y a ↔ ∀ a ∈ ran ⁡ G ∀ b ∈ ran ⁡ G a H b = b H a
11 6 10 opelopabg ⊢ G ∈ A ∧ H ∈ B → G H ∈ x y | ∀ a ∈ ran ⁡ x ∀ b ∈ ran ⁡ x a y b = b y a ↔ ∀ a ∈ ran ⁡ G ∀ b ∈ ran ⁡ G a H b = b H a
12 3 11 bitrd ⊢ G ∈ A ∧ H ∈ B → G H ∈ Com2 ↔ ∀ a ∈ ran ⁡ G ∀ b ∈ ran ⁡ G a H b = b H a