Metamath Proof Explorer

Theorem caovdirg

Description: Convert an operation reverse distributive law to class notation. (Contributed by Mario Carneiro, 19-Oct-2014)

Ref Expression
Hypothesis caovdirg.1 ⊢ φ ∧ x ∈ S ∧ y ∈ S ∧ z ∈ K → x F y G z = x G z H y G z
Assertion caovdirg ⊢ φ ∧ A ∈ S ∧ B ∈ S ∧ C ∈ K → A F B G C = A G C H B G C

Proof

Step Hyp Ref Expression
1 caovdirg.1 ⊢ φ ∧ x ∈ S ∧ y ∈ S ∧ z ∈ K → x F y G z = x G z H y G z
2 1 ralrimivvva ⊢ φ → ∀ x ∈ S ∀ y ∈ S ∀ z ∈ K x F y G z = x G z H y G z
3 oveq1 ⊢ x = A → x F y = A F y
4 3 oveq1d ⊢ x = A → x F y G z = A F y G z
5 oveq1 ⊢ x = A → x G z = A G z
6 5 oveq1d ⊢ x = A → x G z H y G z = A G z H y G z
7 4 6 eqeq12d ⊢ x = A → x F y G z = x G z H y G z ↔ A F y G z = A G z H y G z
8 oveq2 ⊢ y = B → A F y = A F B
9 8 oveq1d ⊢ y = B → A F y G z = A F B G z
10 oveq1 ⊢ y = B → y G z = B G z
11 10 oveq2d ⊢ y = B → A G z H y G z = A G z H B G z
12 9 11 eqeq12d ⊢ y = B → A F y G z = A G z H y G z ↔ A F B G z = A G z H B G z
13 oveq2 ⊢ z = C → A F B G z = A F B G C
14 oveq2 ⊢ z = C → A G z = A G C
15 oveq2 ⊢ z = C → B G z = B G C
16 14 15 oveq12d ⊢ z = C → A G z H B G z = A G C H B G C
17 13 16 eqeq12d ⊢ z = C → A F B G z = A G z H B G z ↔ A F B G C = A G C H B G C
18 7 12 17 rspc3v ⊢ A ∈ S ∧ B ∈ S ∧ C ∈ K → ∀ x ∈ S ∀ y ∈ S ∀ z ∈ K x F y G z = x G z H y G z → A F B G C = A G C H B G C
19 2 18 mpan9 ⊢ φ ∧ A ∈ S ∧ B ∈ S ∧ C ∈ K → A F B G C = A G C H B G C