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 ) )