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→GH∈Com2↔∀a∈ran⁡G∀b∈ran⁡GaHb=bHa

Proof

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