pmtrcnel2

	Ref	Expression
Hypotheses	pmtrcnel.s	$⊢ S = SymGrp (D)$
	pmtrcnel.t	$⊢ T = pmTrsp (D)$
	pmtrcnel.b	$⊢ B = {Base}_{S}$
	pmtrcnel.j	$⊢ J = F (I)$
	pmtrcnel.d	$⊢ φ \to D \in V$
	pmtrcnel.f	$⊢ φ \to F \in B$
	pmtrcnel.i	$⊢ φ \to I \in dom (F ∖ I)$
Assertion	pmtrcnel2	$⊢ φ \to dom (F ∖ I) ∖ \{I, J\} \subseteq dom ((T (\{I, J\}) \circ F) ∖ I)$

Proof

Step	Hyp	Ref	Expression
1		pmtrcnel.s	$⊢ S = SymGrp (D)$
2		pmtrcnel.t	$⊢ T = pmTrsp (D)$
3		pmtrcnel.b	$⊢ B = {Base}_{S}$
4		pmtrcnel.j	$⊢ J = F (I)$
5		pmtrcnel.d	$⊢ φ \to D \in V$
6		pmtrcnel.f	$⊢ φ \to F \in B$
7		pmtrcnel.i	$⊢ φ \to I \in dom (F ∖ I)$
8		mvdco	$⊢ dom (({T (\{I, J\})}^{-1} \circ (T (\{I, J\}) \circ F)) ∖ I) \subseteq dom ({T (\{I, J\})}^{-1} ∖ I) \cup dom ((T (\{I, J\}) \circ F) ∖ I)$
9	8	a1i	$⊢ φ \to dom (({T (\{I, J\})}^{-1} \circ (T (\{I, J\}) \circ F)) ∖ I) \subseteq dom ({T (\{I, J\})}^{-1} ∖ I) \cup dom ((T (\{I, J\}) \circ F) ∖ I)$
10		coass	$⊢ ({T (\{I, J\})}^{-1} \circ T (\{I, J\})) \circ F = {T (\{I, J\})}^{-1} \circ (T (\{I, J\}) \circ F)$
11		difss	$⊢ F ∖ I \subseteq F$
12		dmss	$⊢ F ∖ I \subseteq F \to dom (F ∖ I) \subseteq dom F$
13	11 12	ax-mp	$⊢ dom (F ∖ I) \subseteq dom F$
14	13 7	sselid	$⊢ φ \to I \in dom F$
15	1 3	symgbasf1o	$⊢ F \in B \to F : D \underset{1-1 onto}{⟶} D$
16		f1of	$⊢ F : D \underset{1-1 onto}{⟶} D \to F : D ⟶ D$
17	6 15 16	3syl	$⊢ φ \to F : D ⟶ D$
18	17	fdmd	$⊢ φ \to dom F = D$
19	14 18	eleqtrd	$⊢ φ \to I \in D$
20	17 19	ffvelcdmd	$⊢ φ \to F (I) \in D$
21	4 20	eqeltrid	$⊢ φ \to J \in D$
22	19 21	prssd	$⊢ φ \to \{I, J\} \subseteq D$
23	17	ffnd	$⊢ φ \to F Fn D$
24		fnelnfp	$⊢ (F Fn D \land I \in D) \to (I \in dom (F ∖ I) \leftrightarrow F (I) \neq I)$
25	24	biimpa	$⊢ ((F Fn D \land I \in D) \land I \in dom (F ∖ I)) \to F (I) \neq I$
26	23 19 7 25	syl21anc	$⊢ φ \to F (I) \neq I$
27	26	necomd	$⊢ φ \to I \neq F (I)$
28	4	a1i	$⊢ φ \to J = F (I)$
29	27 28	neeqtrrd	$⊢ φ \to I \neq J$
30		enpr2	$⊢ (I \in D \land J \in D \land I \neq J) \to \{I, J\} \approx 2_{𝑜}$
31	19 21 29 30	syl3anc	$⊢ φ \to \{I, J\} \approx 2_{𝑜}$
32		eqid	$⊢ ran T = ran T$
33	2 32	pmtrrn	$⊢ (D \in V \land \{I, J\} \subseteq D \land \{I, J\} \approx 2_{𝑜}) \to T (\{I, J\}) \in ran T$
34	5 22 31 33	syl3anc	$⊢ φ \to T (\{I, J\}) \in ran T$
35	2 32	pmtrff1o	$⊢ T (\{I, J\}) \in ran T \to T (\{I, J\}) : D \underset{1-1 onto}{⟶} D$
36		f1ococnv1	$⊢ T (\{I, J\}) : D \underset{1-1 onto}{⟶} D \to {T (\{I, J\})}^{-1} \circ T (\{I, J\}) = {I ↾}_{D}$
37	34 35 36	3syl	$⊢ φ \to {T (\{I, J\})}^{-1} \circ T (\{I, J\}) = {I ↾}_{D}$
38	37	coeq1d	$⊢ φ \to ({T (\{I, J\})}^{-1} \circ T (\{I, J\})) \circ F = ({I ↾}_{D}) \circ F$
39	10 38	eqtr3id	$⊢ φ \to {T (\{I, J\})}^{-1} \circ (T (\{I, J\}) \circ F) = ({I ↾}_{D}) \circ F$
40		fcoi2	$⊢ F : D ⟶ D \to ({I ↾}_{D}) \circ F = F$
41	17 40	syl	$⊢ φ \to ({I ↾}_{D}) \circ F = F$
42	39 41	eqtrd	$⊢ φ \to {T (\{I, J\})}^{-1} \circ (T (\{I, J\}) \circ F) = F$
43	42	difeq1d	$⊢ φ \to ({T (\{I, J\})}^{-1} \circ (T (\{I, J\}) \circ F)) ∖ I = F ∖ I$
44	43	dmeqd	$⊢ φ \to dom (({T (\{I, J\})}^{-1} \circ (T (\{I, J\}) \circ F)) ∖ I) = dom (F ∖ I)$
45	2 32	pmtrfcnv	$⊢ T (\{I, J\}) \in ran T \to {T (\{I, J\})}^{-1} = T (\{I, J\})$
46	34 45	syl	$⊢ φ \to {T (\{I, J\})}^{-1} = T (\{I, J\})$
47	46	difeq1d	$⊢ φ \to {T (\{I, J\})}^{-1} ∖ I = T (\{I, J\}) ∖ I$
48	47	dmeqd	$⊢ φ \to dom ({T (\{I, J\})}^{-1} ∖ I) = dom (T (\{I, J\}) ∖ I)$
49	2	pmtrmvd	$⊢ (D \in V \land \{I, J\} \subseteq D \land \{I, J\} \approx 2_{𝑜}) \to dom (T (\{I, J\}) ∖ I) = \{I, J\}$
50	5 22 31 49	syl3anc	$⊢ φ \to dom (T (\{I, J\}) ∖ I) = \{I, J\}$
51	48 50	eqtrd	$⊢ φ \to dom ({T (\{I, J\})}^{-1} ∖ I) = \{I, J\}$
52	51	uneq1d	$⊢ φ \to dom ({T (\{I, J\})}^{-1} ∖ I) \cup dom ((T (\{I, J\}) \circ F) ∖ I) = \{I, J\} \cup dom ((T (\{I, J\}) \circ F) ∖ I)$
53		uncom	$⊢ \{I, J\} \cup dom ((T (\{I, J\}) \circ F) ∖ I) = dom ((T (\{I, J\}) \circ F) ∖ I) \cup \{I, J\}$
54	52 53	eqtrdi	$⊢ φ \to dom ({T (\{I, J\})}^{-1} ∖ I) \cup dom ((T (\{I, J\}) \circ F) ∖ I) = dom ((T (\{I, J\}) \circ F) ∖ I) \cup \{I, J\}$
55	9 44 54	3sstr3d	$⊢ φ \to dom (F ∖ I) \subseteq dom ((T (\{I, J\}) \circ F) ∖ I) \cup \{I, J\}$
56	55	ssdifd	$⊢ φ \to dom (F ∖ I) ∖ \{I, J\} \subseteq (dom ((T (\{I, J\}) \circ F) ∖ I) \cup \{I, J\}) ∖ \{I, J\}$
57		difun2	$⊢ (dom ((T (\{I, J\}) \circ F) ∖ I) \cup \{I, J\}) ∖ \{I, J\} = dom ((T (\{I, J\}) \circ F) ∖ I) ∖ \{I, J\}$
58		difss	$⊢ dom ((T (\{I, J\}) \circ F) ∖ I) ∖ \{I, J\} \subseteq dom ((T (\{I, J\}) \circ F) ∖ I)$
59	57 58	eqsstri	$⊢ (dom ((T (\{I, J\}) \circ F) ∖ I) \cup \{I, J\}) ∖ \{I, J\} \subseteq dom ((T (\{I, J\}) \circ F) ∖ I)$
60	56 59	sstrdi	$⊢ φ \to dom (F ∖ I) ∖ \{I, J\} \subseteq dom ((T (\{I, J\}) \circ F) ∖ I)$

Metamath Proof Explorer

Theorem pmtrcnel2

Proof