This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( ( 𝐴 𝐹 𝐵 ) 𝐺 𝐶 ) = ( ( 𝐴 𝐺 𝐶 ) 𝐹 ( 𝐵 𝐺 𝐶 ) )