fvcosymgeq

Description: The values of two compositions of permutations are equal if the values of the composed permutations are pairwise equal. (Contributed by AV, 26-Jan-2019)

	Ref	Expression
Hypotheses	gsmsymgrfix.s	$⊢ S = SymGrp (N)$
	gsmsymgrfix.b	$⊢ B = {Base}_{S}$
	gsmsymgreq.z	$⊢ Z = SymGrp (M)$
	gsmsymgreq.p	$⊢ P = {Base}_{Z}$
	gsmsymgreq.i	$⊢ I = N \cap M$
Assertion	fvcosymgeq	$⊢ (G \in B \land K \in P) \to ((X \in I \land G (X) = K (X) \land \forall n \in I F (n) = H (n)) \to (F \circ G) (X) = (H \circ K) (X))$

Proof

Step	Hyp	Ref	Expression
1		gsmsymgrfix.s	$⊢ S = SymGrp (N)$
2		gsmsymgrfix.b	$⊢ B = {Base}_{S}$
3		gsmsymgreq.z	$⊢ Z = SymGrp (M)$
4		gsmsymgreq.p	$⊢ P = {Base}_{Z}$
5		gsmsymgreq.i	$⊢ I = N \cap M$
6	1 2	symgbasf	$⊢ G \in B \to G : N ⟶ N$
7	6	ffnd	$⊢ G \in B \to G Fn N$
8	3 4	symgbasf	$⊢ K \in P \to K : M ⟶ M$
9	8	ffnd	$⊢ K \in P \to K Fn M$
10	7 9	anim12i	$⊢ (G \in B \land K \in P) \to (G Fn N \land K Fn M)$
11	10	adantr	$⊢ ((G \in B \land K \in P) \land (X \in I \land G (X) = K (X) \land \forall n \in I F (n) = H (n))) \to (G Fn N \land K Fn M)$
12	5	eleq2i	$⊢ X \in I \leftrightarrow X \in (N \cap M)$
13	12	biimpi	$⊢ X \in I \to X \in (N \cap M)$
14	13	3ad2ant1	$⊢ (X \in I \land G (X) = K (X) \land \forall n \in I F (n) = H (n)) \to X \in (N \cap M)$
15	14	adantl	$⊢ ((G \in B \land K \in P) \land (X \in I \land G (X) = K (X) \land \forall n \in I F (n) = H (n))) \to X \in (N \cap M)$
16		simpr2	$⊢ ((G \in B \land K \in P) \land (X \in I \land G (X) = K (X) \land \forall n \in I F (n) = H (n))) \to G (X) = K (X)$
17	1 2	symgbasf1o	$⊢ G \in B \to G : N \underset{1-1 onto}{⟶} N$
18		dff1o5	$⊢ G : N \underset{1-1 onto}{⟶} N \leftrightarrow (G : N \underset{1-1}{⟶} N \land ran G = N)$
19		eqcom	$⊢ ran G = N \leftrightarrow N = ran G$
20	19	biimpi	$⊢ ran G = N \to N = ran G$
21	18 20	simplbiim	$⊢ G : N \underset{1-1 onto}{⟶} N \to N = ran G$
22	17 21	syl	$⊢ G \in B \to N = ran G$
23	3 4	symgbasf1o	$⊢ K \in P \to K : M \underset{1-1 onto}{⟶} M$
24		dff1o5	$⊢ K : M \underset{1-1 onto}{⟶} M \leftrightarrow (K : M \underset{1-1}{⟶} M \land ran K = M)$
25		eqcom	$⊢ ran K = M \leftrightarrow M = ran K$
26	25	biimpi	$⊢ ran K = M \to M = ran K$
27	24 26	simplbiim	$⊢ K : M \underset{1-1 onto}{⟶} M \to M = ran K$
28	23 27	syl	$⊢ K \in P \to M = ran K$
29	22 28	ineqan12d	$⊢ (G \in B \land K \in P) \to N \cap M = ran G \cap ran K$
30	5 29	syl5eq	$⊢ (G \in B \land K \in P) \to I = ran G \cap ran K$
31	30	raleqdv	$⊢ (G \in B \land K \in P) \to (\forall n \in I F (n) = H (n) \leftrightarrow \forall n \in (ran G \cap ran K) F (n) = H (n))$
32	31	biimpcd	$⊢ \forall n \in I F (n) = H (n) \to ((G \in B \land K \in P) \to \forall n \in (ran G \cap ran K) F (n) = H (n))$
33	32	3ad2ant3	$⊢ (X \in I \land G (X) = K (X) \land \forall n \in I F (n) = H (n)) \to ((G \in B \land K \in P) \to \forall n \in (ran G \cap ran K) F (n) = H (n))$
34	33	impcom	$⊢ ((G \in B \land K \in P) \land (X \in I \land G (X) = K (X) \land \forall n \in I F (n) = H (n))) \to \forall n \in (ran G \cap ran K) F (n) = H (n)$
35	15 16 34	3jca	$⊢ ((G \in B \land K \in P) \land (X \in I \land G (X) = K (X) \land \forall n \in I F (n) = H (n))) \to (X \in (N \cap M) \land G (X) = K (X) \land \forall n \in (ran G \cap ran K) F (n) = H (n))$
36		fvcofneq	$⊢ (G Fn N \land K Fn M) \to ((X \in (N \cap M) \land G (X) = K (X) \land \forall n \in (ran G \cap ran K) F (n) = H (n)) \to (F \circ G) (X) = (H \circ K) (X))$
37	11 35 36	sylc	$⊢ ((G \in B \land K \in P) \land (X \in I \land G (X) = K (X) \land \forall n \in I F (n) = H (n))) \to (F \circ G) (X) = (H \circ K) (X)$
38	37	ex	$⊢ (G \in B \land K \in P) \to ((X \in I \land G (X) = K (X) \land \forall n \in I F (n) = H (n)) \to (F \circ G) (X) = (H \circ K) (X))$

Metamath Proof Explorer

Theorem fvcosymgeq

Proof