Metamath Proof Explorer


Theorem caovdir

Description: Reverse distributive law. (Contributed by NM, 26-Aug-1995)

Ref Expression
Hypotheses caovdir.1 𝐴 ∈ V
caovdir.2 𝐵 ∈ V
caovdir.3 𝐶 ∈ V
caovdir.com ( 𝑥 𝐺 𝑦 ) = ( 𝑦 𝐺 𝑥 )
caovdir.distr ( 𝑥 𝐺 ( 𝑦 𝐹 𝑧 ) ) = ( ( 𝑥 𝐺 𝑦 ) 𝐹 ( 𝑥 𝐺 𝑧 ) )
Assertion caovdir ( ( 𝐴 𝐹 𝐵 ) 𝐺 𝐶 ) = ( ( 𝐴 𝐺 𝐶 ) 𝐹 ( 𝐵 𝐺 𝐶 ) )

Proof

Step Hyp Ref Expression
1 caovdir.1 𝐴 ∈ V
2 caovdir.2 𝐵 ∈ V
3 caovdir.3 𝐶 ∈ V
4 caovdir.com ( 𝑥 𝐺 𝑦 ) = ( 𝑦 𝐺 𝑥 )
5 caovdir.distr ( 𝑥 𝐺 ( 𝑦 𝐹 𝑧 ) ) = ( ( 𝑥 𝐺 𝑦 ) 𝐹 ( 𝑥 𝐺 𝑧 ) )
6 3 1 2 5 caovdi ( 𝐶 𝐺 ( 𝐴 𝐹 𝐵 ) ) = ( ( 𝐶 𝐺 𝐴 ) 𝐹 ( 𝐶 𝐺 𝐵 ) )
7 ovex ( 𝐴 𝐹 𝐵 ) ∈ V
8 3 7 4 caovcom ( 𝐶 𝐺 ( 𝐴 𝐹 𝐵 ) ) = ( ( 𝐴 𝐹 𝐵 ) 𝐺 𝐶 )
9 3 1 4 caovcom ( 𝐶 𝐺 𝐴 ) = ( 𝐴 𝐺 𝐶 )
10 3 2 4 caovcom ( 𝐶 𝐺 𝐵 ) = ( 𝐵 𝐺 𝐶 )
11 9 10 oveq12i ( ( 𝐶 𝐺 𝐴 ) 𝐹 ( 𝐶 𝐺 𝐵 ) ) = ( ( 𝐴 𝐺 𝐶 ) 𝐹 ( 𝐵 𝐺 𝐶 ) )
12 6 8 11 3eqtr3i ( ( 𝐴 𝐹 𝐵 ) 𝐺 𝐶 ) = ( ( 𝐴 𝐺 𝐶 ) 𝐹 ( 𝐵 𝐺 𝐶 ) )