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

Metamath Proof Explorer

Theorem ecxrn2

Description: The ( R |X. S ) -coset of a set is the Cartesian product of its R -coset and S -coset. (Contributed by Peter Mazsa, 16-Oct-2020)

Ref Expression
Assertion ecxrn2 
|- ( A e. V -> [ A ] ( R |X. S ) = ( [ A ] R X. [ A ] S ) )

Proof

Step Hyp Ref Expression
1 relecxrn 
 |-  ( A e. V -> Rel [ A ] ( R |X. S ) )
2 relxp 
 |-  Rel ( [ A ] R X. [ A ] S )
3 1 2 jctir 
 |-  ( A e. V -> ( Rel [ A ] ( R |X. S ) /\ Rel ( [ A ] R X. [ A ] S ) ) )
4 brxrn 
 |-  ( ( A e. V /\ x e. _V /\ y e. _V ) -> ( A ( R |X. S ) <. x , y >. <-> ( A R x /\ A S y ) ) )
5 4 el3v23 
 |-  ( A e. V -> ( A ( R |X. S ) <. x , y >. <-> ( A R x /\ A S y ) ) )
6 opex 
 |-  <. x , y >. e. _V
7 elecALTV 
 |-  ( ( A e. V /\ <. x , y >. e. _V ) -> ( <. x , y >. e. [ A ] ( R |X. S ) <-> A ( R |X. S ) <. x , y >. ) )
8 6 7 mpan2 
 |-  ( A e. V -> ( <. x , y >. e. [ A ] ( R |X. S ) <-> A ( R |X. S ) <. x , y >. ) )
9 elecALTV 
 |-  ( ( A e. V /\ x e. _V ) -> ( x e. [ A ] R <-> A R x ) )
10 9 elvd 
 |-  ( A e. V -> ( x e. [ A ] R <-> A R x ) )
11 elecALTV 
 |-  ( ( A e. V /\ y e. _V ) -> ( y e. [ A ] S <-> A S y ) )
12 11 elvd 
 |-  ( A e. V -> ( y e. [ A ] S <-> A S y ) )
13 10 12 anbi12d 
 |-  ( A e. V -> ( ( x e. [ A ] R /\ y e. [ A ] S ) <-> ( A R x /\ A S y ) ) )
14 5 8 13 3bitr4d 
 |-  ( A e. V -> ( <. x , y >. e. [ A ] ( R |X. S ) <-> ( x e. [ A ] R /\ y e. [ A ] S ) ) )
15 opelxp 
 |-  ( <. x , y >. e. ( [ A ] R X. [ A ] S ) <-> ( x e. [ A ] R /\ y e. [ A ] S ) )
16 14 15 bitr4di 
 |-  ( A e. V -> ( <. x , y >. e. [ A ] ( R |X. S ) <-> <. x , y >. e. ( [ A ] R X. [ A ] S ) ) )
17 16 eqrelrdv2 
 |-  ( ( ( Rel [ A ] ( R |X. S ) /\ Rel ( [ A ] R X. [ A ] S ) ) /\ A e. V ) -> [ A ] ( R |X. S ) = ( [ A ] R X. [ A ] S ) )
18 3 17 mpancom 
 |-  ( A e. V -> [ A ] ( R |X. S ) = ( [ A ] R X. [ A ] S ) )