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 ( 𝑅 , 𝑆 ) = ( ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ ( 𝑅 ∘ ( 1^st ↾ ( V × V ) ) ) ) ∩ ( ^◡ ( 2^nd ↾ ( V × V ) ) ∘ ( 𝑆 ∘ ( 2^nd ↾ ( V × V ) ) ) ) )
2		dfpprod2	⊢ pprod ( ^◡ 𝑅 , ^◡ 𝑆 ) = ( ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ ( ^◡ 𝑅 ∘ ( 1^st ↾ ( V × V ) ) ) ) ∩ ( ^◡ ( 2^nd ↾ ( V × V ) ) ∘ ( ^◡ 𝑆 ∘ ( 2^nd ↾ ( V × V ) ) ) ) )
3	2	cnveqi	⊢ ^◡ pprod ( ^◡ 𝑅 , ^◡ 𝑆 ) = ^◡ ( ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ ( ^◡ 𝑅 ∘ ( 1^st ↾ ( V × V ) ) ) ) ∩ ( ^◡ ( 2^nd ↾ ( V × V ) ) ∘ ( ^◡ 𝑆 ∘ ( 2^nd ↾ ( V × V ) ) ) ) )
4		cnvin	⊢ ^◡ ( ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ ( ^◡ 𝑅 ∘ ( 1^st ↾ ( V × V ) ) ) ) ∩ ( ^◡ ( 2^nd ↾ ( V × V ) ) ∘ ( ^◡ 𝑆 ∘ ( 2^nd ↾ ( V × V ) ) ) ) ) = ( ^◡ ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ ( ^◡ 𝑅 ∘ ( 1^st ↾ ( V × V ) ) ) ) ∩ ^◡ ( ^◡ ( 2^nd ↾ ( V × V ) ) ∘ ( ^◡ 𝑆 ∘ ( 2^nd ↾ ( V × V ) ) ) ) )
5		cnvco1	⊢ ^◡ ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ ( ^◡ 𝑅 ∘ ( 1^st ↾ ( V × V ) ) ) ) = ( ^◡ ( ^◡ 𝑅 ∘ ( 1^st ↾ ( V × V ) ) ) ∘ ( 1^st ↾ ( V × V ) ) )
6		cnvco1	⊢ ^◡ ( ^◡ 𝑅 ∘ ( 1^st ↾ ( V × V ) ) ) = ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ 𝑅 )
7	6	coeq1i	⊢ ( ^◡ ( ^◡ 𝑅 ∘ ( 1^st ↾ ( V × V ) ) ) ∘ ( 1^st ↾ ( V × V ) ) ) = ( ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ 𝑅 ) ∘ ( 1^st ↾ ( V × V ) ) )
8		coass	⊢ ( ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ 𝑅 ) ∘ ( 1^st ↾ ( V × V ) ) ) = ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ ( 𝑅 ∘ ( 1^st ↾ ( V × V ) ) ) )
9	5 7 8	3eqtri	⊢ ^◡ ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ ( ^◡ 𝑅 ∘ ( 1^st ↾ ( V × V ) ) ) ) = ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ ( 𝑅 ∘ ( 1^st ↾ ( V × V ) ) ) )
10		cnvco1	⊢ ^◡ ( ^◡ ( 2^nd ↾ ( V × V ) ) ∘ ( ^◡ 𝑆 ∘ ( 2^nd ↾ ( V × V ) ) ) ) = ( ^◡ ( ^◡ 𝑆 ∘ ( 2^nd ↾ ( V × V ) ) ) ∘ ( 2^nd ↾ ( V × V ) ) )
11		cnvco1	⊢ ^◡ ( ^◡ 𝑆 ∘ ( 2^nd ↾ ( V × V ) ) ) = ( ^◡ ( 2^nd ↾ ( V × V ) ) ∘ 𝑆 )
12	11	coeq1i	⊢ ( ^◡ ( ^◡ 𝑆 ∘ ( 2^nd ↾ ( V × V ) ) ) ∘ ( 2^nd ↾ ( V × V ) ) ) = ( ( ^◡ ( 2^nd ↾ ( V × V ) ) ∘ 𝑆 ) ∘ ( 2^nd ↾ ( V × V ) ) )
13		coass	⊢ ( ( ^◡ ( 2^nd ↾ ( V × V ) ) ∘ 𝑆 ) ∘ ( 2^nd ↾ ( V × V ) ) ) = ( ^◡ ( 2^nd ↾ ( V × V ) ) ∘ ( 𝑆 ∘ ( 2^nd ↾ ( V × V ) ) ) )
14	10 12 13	3eqtri	⊢ ^◡ ( ^◡ ( 2^nd ↾ ( V × V ) ) ∘ ( ^◡ 𝑆 ∘ ( 2^nd ↾ ( V × V ) ) ) ) = ( ^◡ ( 2^nd ↾ ( V × V ) ) ∘ ( 𝑆 ∘ ( 2^nd ↾ ( V × V ) ) ) )
15	9 14	ineq12i	⊢ ( ^◡ ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ ( ^◡ 𝑅 ∘ ( 1^st ↾ ( V × V ) ) ) ) ∩ ^◡ ( ^◡ ( 2^nd ↾ ( V × V ) ) ∘ ( ^◡ 𝑆 ∘ ( 2^nd ↾ ( V × V ) ) ) ) ) = ( ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ ( 𝑅 ∘ ( 1^st ↾ ( V × V ) ) ) ) ∩ ( ^◡ ( 2^nd ↾ ( V × V ) ) ∘ ( 𝑆 ∘ ( 2^nd ↾ ( V × V ) ) ) ) )
16	3 4 15	3eqtri	⊢ ^◡ pprod ( ^◡ 𝑅 , ^◡ 𝑆 ) = ( ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ ( 𝑅 ∘ ( 1^st ↾ ( V × V ) ) ) ) ∩ ( ^◡ ( 2^nd ↾ ( V × V ) ) ∘ ( 𝑆 ∘ ( 2^nd ↾ ( V × V ) ) ) ) )
17	1 16	eqtr4i	⊢ pprod ( 𝑅 , 𝑆 ) = ^◡ pprod ( ^◡ 𝑅 , ^◡ 𝑆 )