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

Metamath Proof Explorer

Theorem pprodcnveq

Description: A converse law for parallel product. (Contributed by Scott Fenton, 3-May-2014)

Ref Expression
Assertion pprodcnveq pprod ( 𝑅 , 𝑆 ) = ◡ pprod ( ◡ 𝑅 , ◡ 𝑆 )

Proof

Step Hyp Ref Expression
1 dfpprod2 ⊢ pprod ( 𝑅 , 𝑆 ) = ( ( ◡ ( 1st ↾ ( V × V ) ) ∘ ( 𝑅 ∘ ( 1st ↾ ( V × V ) ) ) ) ∩ ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( 𝑆 ∘ ( 2nd ↾ ( V × V ) ) ) ) )
2 dfpprod2 ⊢ pprod ( ◡ 𝑅 , ◡ 𝑆 ) = ( ( ◡ ( 1st ↾ ( V × V ) ) ∘ ( ◡ 𝑅 ∘ ( 1st ↾ ( V × V ) ) ) ) ∩ ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( ◡ 𝑆 ∘ ( 2nd ↾ ( V × V ) ) ) ) )
3 2 cnveqi ⊢ ◡ pprod ( ◡ 𝑅 , ◡ 𝑆 ) = ◡ ( ( ◡ ( 1st ↾ ( V × V ) ) ∘ ( ◡ 𝑅 ∘ ( 1st ↾ ( V × V ) ) ) ) ∩ ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( ◡ 𝑆 ∘ ( 2nd ↾ ( V × V ) ) ) ) )
4 cnvin ⊢ ◡ ( ( ◡ ( 1st ↾ ( V × V ) ) ∘ ( ◡ 𝑅 ∘ ( 1st ↾ ( V × V ) ) ) ) ∩ ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( ◡ 𝑆 ∘ ( 2nd ↾ ( V × V ) ) ) ) ) = ( ◡ ( ◡ ( 1st ↾ ( V × V ) ) ∘ ( ◡ 𝑅 ∘ ( 1st ↾ ( V × V ) ) ) ) ∩ ◡ ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( ◡ 𝑆 ∘ ( 2nd ↾ ( V × V ) ) ) ) )
5 cnvco1 ⊢ ◡ ( ◡ ( 1st ↾ ( V × V ) ) ∘ ( ◡ 𝑅 ∘ ( 1st ↾ ( V × V ) ) ) ) = ( ◡ ( ◡ 𝑅 ∘ ( 1st ↾ ( V × V ) ) ) ∘ ( 1st ↾ ( V × V ) ) )
6 cnvco1 ⊢ ◡ ( ◡ 𝑅 ∘ ( 1st ↾ ( V × V ) ) ) = ( ◡ ( 1st ↾ ( V × V ) ) ∘ 𝑅 )
7 6 coeq1i ⊢ ( ◡ ( ◡ 𝑅 ∘ ( 1st ↾ ( V × V ) ) ) ∘ ( 1st ↾ ( V × V ) ) ) = ( ( ◡ ( 1st ↾ ( V × V ) ) ∘ 𝑅 ) ∘ ( 1st ↾ ( V × V ) ) )
8 coass ⊢ ( ( ◡ ( 1st ↾ ( V × V ) ) ∘ 𝑅 ) ∘ ( 1st ↾ ( V × V ) ) ) = ( ◡ ( 1st ↾ ( V × V ) ) ∘ ( 𝑅 ∘ ( 1st ↾ ( V × V ) ) ) )
9 5 7 8 3eqtri ⊢ ◡ ( ◡ ( 1st ↾ ( V × V ) ) ∘ ( ◡ 𝑅 ∘ ( 1st ↾ ( V × V ) ) ) ) = ( ◡ ( 1st ↾ ( V × V ) ) ∘ ( 𝑅 ∘ ( 1st ↾ ( V × V ) ) ) )
10 cnvco1 ⊢ ◡ ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( ◡ 𝑆 ∘ ( 2nd ↾ ( V × V ) ) ) ) = ( ◡ ( ◡ 𝑆 ∘ ( 2nd ↾ ( V × V ) ) ) ∘ ( 2nd ↾ ( V × V ) ) )
11 cnvco1 ⊢ ◡ ( ◡ 𝑆 ∘ ( 2nd ↾ ( V × V ) ) ) = ( ◡ ( 2nd ↾ ( V × V ) ) ∘ 𝑆 )
12 11 coeq1i ⊢ ( ◡ ( ◡ 𝑆 ∘ ( 2nd ↾ ( V × V ) ) ) ∘ ( 2nd ↾ ( V × V ) ) ) = ( ( ◡ ( 2nd ↾ ( V × V ) ) ∘ 𝑆 ) ∘ ( 2nd ↾ ( V × V ) ) )
13 coass ⊢ ( ( ◡ ( 2nd ↾ ( V × V ) ) ∘ 𝑆 ) ∘ ( 2nd ↾ ( V × V ) ) ) = ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( 𝑆 ∘ ( 2nd ↾ ( V × V ) ) ) )
14 10 12 13 3eqtri ⊢ ◡ ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( ◡ 𝑆 ∘ ( 2nd ↾ ( V × V ) ) ) ) = ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( 𝑆 ∘ ( 2nd ↾ ( V × V ) ) ) )
15 9 14 ineq12i ⊢ ( ◡ ( ◡ ( 1st ↾ ( V × V ) ) ∘ ( ◡ 𝑅 ∘ ( 1st ↾ ( V × V ) ) ) ) ∩ ◡ ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( ◡ 𝑆 ∘ ( 2nd ↾ ( V × V ) ) ) ) ) = ( ( ◡ ( 1st ↾ ( V × V ) ) ∘ ( 𝑅 ∘ ( 1st ↾ ( V × V ) ) ) ) ∩ ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( 𝑆 ∘ ( 2nd ↾ ( V × V ) ) ) ) )
16 3 4 15 3eqtri ⊢ ◡ pprod ( ◡ 𝑅 , ◡ 𝑆 ) = ( ( ◡ ( 1st ↾ ( V × V ) ) ∘ ( 𝑅 ∘ ( 1st ↾ ( V × V ) ) ) ) ∩ ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( 𝑆 ∘ ( 2nd ↾ ( V × V ) ) ) ) )
17 1 16 eqtr4i ⊢ pprod ( 𝑅 , 𝑆 ) = ◡ pprod ( ◡ 𝑅 , ◡ 𝑆 )