symgcom - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > symgcom		Structured version Visualization version GIF version

Theorem symgcom 33047

Description: Two permutations 𝑋 and 𝑌 commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 15-Oct-2023.)

**Hypotheses**
Ref	Expression
symgcom.g	⊢ 𝐺 = (SymGrp‘𝐴)
symgcom.b	⊢ 𝐵 = (Base‘𝐺)
symgcom.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)
symgcom.y	⊢ (𝜑 → 𝑌 ∈ 𝐵)
symgcom.1	⊢ (𝜑 → (𝑋 ↾ 𝐸) = ( I ↾ 𝐸))
symgcom.2	⊢ (𝜑 → (𝑌 ↾ 𝐹) = ( I ↾ 𝐹))
symgcom.3	⊢ (𝜑 → (𝐸 ∩ 𝐹) = ∅)
symgcom.4	⊢ (𝜑 → (𝐸 ∪ 𝐹) = 𝐴)

**Assertion**
Ref	Expression
symgcom	⊢ (𝜑 → (𝑋 ∘ 𝑌) = (𝑌 ∘ 𝑋))

**Proof of Theorem symgcom**
Step	Hyp	Ref	Expression
1		symgcom.4	. . . 4 ⊢ (𝜑 → (𝐸 ∪ 𝐹) = 𝐴)
2	1	reseq2d 5953	. . 3 ⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ (𝐸 ∪ 𝐹)) = ((𝑋 ∘ 𝑌) ↾ 𝐴))
3		resundi 5967	. . . 4 ⊢ ((𝑋 ∘ 𝑌) ↾ (𝐸 ∪ 𝐹)) = (((𝑋 ∘ 𝑌) ↾ 𝐸) ∪ ((𝑋 ∘ 𝑌) ↾ 𝐹))
4		resco 6226	. . . . . . 7 ⊢ ((𝑋 ∘ 𝑌) ↾ 𝐸) = (𝑋 ∘ (𝑌 ↾ 𝐸))
5		symgcom.y	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
6		symgcom.g	. . . . . . . . . . . . . . 15 ⊢ 𝐺 = (SymGrp‘𝐴)
7		symgcom.b	. . . . . . . . . . . . . . 15 ⊢ 𝐵 = (Base‘𝐺)
8	6, 7	symgbasf1o 19312	. . . . . . . . . . . . . 14 ⊢ (𝑌 ∈ 𝐵 → 𝑌:𝐴–1-1-onto→𝐴)
9	5, 8	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌:𝐴–1-1-onto→𝐴)
10		f1ocnv 6815	. . . . . . . . . . . . 13 ⊢ (𝑌:𝐴–1-1-onto→𝐴 → ^◡𝑌:𝐴–1-1-onto→𝐴)
11		f1ofun 6805	. . . . . . . . . . . . 13 ⊢ (^◡𝑌:𝐴–1-1-onto→𝐴 → Fun ^◡𝑌)
12	9, 10, 11	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → Fun ^◡𝑌)
13		f1ofn 6804	. . . . . . . . . . . . . 14 ⊢ (𝑌:𝐴–1-1-onto→𝐴 → 𝑌 Fn 𝐴)
14		fnresdm 6640	. . . . . . . . . . . . . 14 ⊢ (𝑌 Fn 𝐴 → (𝑌 ↾ 𝐴) = 𝑌)
15	9, 13, 14	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌 ↾ 𝐴) = 𝑌)
16		f1ofo 6810	. . . . . . . . . . . . . 14 ⊢ (𝑌:𝐴–1-1-onto→𝐴 → 𝑌:𝐴–onto→𝐴)
17	9, 16	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌:𝐴–onto→𝐴)
18		foeq1 6771	. . . . . . . . . . . . . 14 ⊢ ((𝑌 ↾ 𝐴) = 𝑌 → ((𝑌 ↾ 𝐴):𝐴–onto→𝐴 ↔ 𝑌:𝐴–onto→𝐴))
19	18	biimpar 477	. . . . . . . . . . . . 13 ⊢ (((𝑌 ↾ 𝐴) = 𝑌 ∧ 𝑌:𝐴–onto→𝐴) → (𝑌 ↾ 𝐴):𝐴–onto→𝐴)
20	15, 17, 19	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌 ↾ 𝐴):𝐴–onto→𝐴)
21		symgcom.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌 ↾ 𝐹) = ( I ↾ 𝐹))
22		f1oi 6841	. . . . . . . . . . . . . 14 ⊢ ( I ↾ 𝐹):𝐹–1-1-onto→𝐹
23		f1ofo 6810	. . . . . . . . . . . . . 14 ⊢ (( I ↾ 𝐹):𝐹–1-1-onto→𝐹 → ( I ↾ 𝐹):𝐹–onto→𝐹)
24	22, 23	mp1i 13	. . . . . . . . . . . . 13 ⊢ (𝜑 → ( I ↾ 𝐹):𝐹–onto→𝐹)
25		foeq1 6771	. . . . . . . . . . . . . 14 ⊢ ((𝑌 ↾ 𝐹) = ( I ↾ 𝐹) → ((𝑌 ↾ 𝐹):𝐹–onto→𝐹 ↔ ( I ↾ 𝐹):𝐹–onto→𝐹))
26	25	biimpar 477	. . . . . . . . . . . . 13 ⊢ (((𝑌 ↾ 𝐹) = ( I ↾ 𝐹) ∧ ( I ↾ 𝐹):𝐹–onto→𝐹) → (𝑌 ↾ 𝐹):𝐹–onto→𝐹)
27	21, 24, 26	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌 ↾ 𝐹):𝐹–onto→𝐹)
28		resdif 6824	. . . . . . . . . . . 12 ⊢ ((Fun ^◡𝑌 ∧ (𝑌 ↾ 𝐴):𝐴–onto→𝐴 ∧ (𝑌 ↾ 𝐹):𝐹–onto→𝐹) → (𝑌 ↾ (𝐴 ∖ 𝐹)):(𝐴 ∖ 𝐹)–1-1-onto→(𝐴 ∖ 𝐹))
29	12, 20, 27, 28	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 ↾ (𝐴 ∖ 𝐹)):(𝐴 ∖ 𝐹)–1-1-onto→(𝐴 ∖ 𝐹))
30		ssun2 4145	. . . . . . . . . . . . . . 15 ⊢ 𝐹 ⊆ (𝐸 ∪ 𝐹)
31	30, 1	sseqtrid 3992	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 ⊆ 𝐴)
32		incom 4175	. . . . . . . . . . . . . . 15 ⊢ (𝐸 ∩ 𝐹) = (𝐹 ∩ 𝐸)
33		symgcom.3	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐸 ∩ 𝐹) = ∅)
34	32, 33	eqtr3id 2779	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹 ∩ 𝐸) = ∅)
35		uncom 4124	. . . . . . . . . . . . . . 15 ⊢ (𝐸 ∪ 𝐹) = (𝐹 ∪ 𝐸)
36	35, 1	eqtr3id 2779	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹 ∪ 𝐸) = 𝐴)
37		uneqdifeq 4459	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ⊆ 𝐴 ∧ (𝐹 ∩ 𝐸) = ∅) → ((𝐹 ∪ 𝐸) = 𝐴 ↔ (𝐴 ∖ 𝐹) = 𝐸))
38	37	biimpa 476	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ⊆ 𝐴 ∧ (𝐹 ∩ 𝐸) = ∅) ∧ (𝐹 ∪ 𝐸) = 𝐴) → (𝐴 ∖ 𝐹) = 𝐸)
39	31, 34, 36, 38	syl21anc 837	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 ∖ 𝐹) = 𝐸)
40	39	reseq2d 5953	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌 ↾ (𝐴 ∖ 𝐹)) = (𝑌 ↾ 𝐸))
41	40, 39, 39	f1oeq123d 6797	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑌 ↾ (𝐴 ∖ 𝐹)):(𝐴 ∖ 𝐹)–1-1-onto→(𝐴 ∖ 𝐹) ↔ (𝑌 ↾ 𝐸):𝐸–1-1-onto→𝐸))
42	29, 41	mpbid 232	. . . . . . . . . 10 ⊢ (𝜑 → (𝑌 ↾ 𝐸):𝐸–1-1-onto→𝐸)
43		f1of 6803	. . . . . . . . . 10 ⊢ ((𝑌 ↾ 𝐸):𝐸–1-1-onto→𝐸 → (𝑌 ↾ 𝐸):𝐸⟶𝐸)
44	42, 43	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑌 ↾ 𝐸):𝐸⟶𝐸)
45	44	frnd 6699	. . . . . . . 8 ⊢ (𝜑 → ran (𝑌 ↾ 𝐸) ⊆ 𝐸)
46		cores 6225	. . . . . . . 8 ⊢ (ran (𝑌 ↾ 𝐸) ⊆ 𝐸 → ((𝑋 ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (𝑋 ∘ (𝑌 ↾ 𝐸)))
47	45, 46	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑋 ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (𝑋 ∘ (𝑌 ↾ 𝐸)))
48	4, 47	eqtr4id 2784	. . . . . 6 ⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ 𝐸) = ((𝑋 ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)))
49		symgcom.1	. . . . . . 7 ⊢ (𝜑 → (𝑋 ↾ 𝐸) = ( I ↾ 𝐸))
50	49	coeq1d 5828	. . . . . 6 ⊢ (𝜑 → ((𝑋 ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (( I ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)))
51		fcoi2 6738	. . . . . . 7 ⊢ ((𝑌 ↾ 𝐸):𝐸⟶𝐸 → (( I ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (𝑌 ↾ 𝐸))
52	44, 51	syl 17	. . . . . 6 ⊢ (𝜑 → (( I ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (𝑌 ↾ 𝐸))
53	48, 50, 52	3eqtrd 2769	. . . . 5 ⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ 𝐸) = (𝑌 ↾ 𝐸))
54		resco 6226	. . . . . 6 ⊢ ((𝑋 ∘ 𝑌) ↾ 𝐹) = (𝑋 ∘ (𝑌 ↾ 𝐹))
55	21	coeq2d 5829	. . . . . . 7 ⊢ (𝜑 → (𝑋 ∘ (𝑌 ↾ 𝐹)) = (𝑋 ∘ ( I ↾ 𝐹)))
56		coires1 6240	. . . . . . 7 ⊢ (𝑋 ∘ ( I ↾ 𝐹)) = (𝑋 ↾ 𝐹)
57	55, 56	eqtrdi 2781	. . . . . 6 ⊢ (𝜑 → (𝑋 ∘ (𝑌 ↾ 𝐹)) = (𝑋 ↾ 𝐹))
58	54, 57	eqtrid 2777	. . . . 5 ⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ 𝐹) = (𝑋 ↾ 𝐹))
59	53, 58	uneq12d 4135	. . . 4 ⊢ (𝜑 → (((𝑋 ∘ 𝑌) ↾ 𝐸) ∪ ((𝑋 ∘ 𝑌) ↾ 𝐹)) = ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)))
60	3, 59	eqtrid 2777	. . 3 ⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ (𝐸 ∪ 𝐹)) = ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)))
61		symgcom.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
62	6, 7	symgbasf1o 19312	. . . . . 6 ⊢ (𝑋 ∈ 𝐵 → 𝑋:𝐴–1-1-onto→𝐴)
63	61, 62	syl 17	. . . . 5 ⊢ (𝜑 → 𝑋:𝐴–1-1-onto→𝐴)
64		f1oco 6826	. . . . 5 ⊢ ((𝑋:𝐴–1-1-onto→𝐴 ∧ 𝑌:𝐴–1-1-onto→𝐴) → (𝑋 ∘ 𝑌):𝐴–1-1-onto→𝐴)
65	63, 9, 64	syl2anc 584	. . . 4 ⊢ (𝜑 → (𝑋 ∘ 𝑌):𝐴–1-1-onto→𝐴)
66		f1ofn 6804	. . . 4 ⊢ ((𝑋 ∘ 𝑌):𝐴–1-1-onto→𝐴 → (𝑋 ∘ 𝑌) Fn 𝐴)
67		fnresdm 6640	. . . 4 ⊢ ((𝑋 ∘ 𝑌) Fn 𝐴 → ((𝑋 ∘ 𝑌) ↾ 𝐴) = (𝑋 ∘ 𝑌))
68	65, 66, 67	3syl 18	. . 3 ⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ 𝐴) = (𝑋 ∘ 𝑌))
69	2, 60, 68	3eqtr3d 2773	. 2 ⊢ (𝜑 → ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)) = (𝑋 ∘ 𝑌))
70	1	reseq2d 5953	. . 3 ⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ (𝐸 ∪ 𝐹)) = ((𝑌 ∘ 𝑋) ↾ 𝐴))
71		resundi 5967	. . . 4 ⊢ ((𝑌 ∘ 𝑋) ↾ (𝐸 ∪ 𝐹)) = (((𝑌 ∘ 𝑋) ↾ 𝐸) ∪ ((𝑌 ∘ 𝑋) ↾ 𝐹))
72		resco 6226	. . . . . 6 ⊢ ((𝑌 ∘ 𝑋) ↾ 𝐸) = (𝑌 ∘ (𝑋 ↾ 𝐸))
73	49	coeq2d 5829	. . . . . . 7 ⊢ (𝜑 → (𝑌 ∘ (𝑋 ↾ 𝐸)) = (𝑌 ∘ ( I ↾ 𝐸)))
74		coires1 6240	. . . . . . 7 ⊢ (𝑌 ∘ ( I ↾ 𝐸)) = (𝑌 ↾ 𝐸)
75	73, 74	eqtrdi 2781	. . . . . 6 ⊢ (𝜑 → (𝑌 ∘ (𝑋 ↾ 𝐸)) = (𝑌 ↾ 𝐸))
76	72, 75	eqtrid 2777	. . . . 5 ⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ 𝐸) = (𝑌 ↾ 𝐸))
77		resco 6226	. . . . . . 7 ⊢ ((𝑌 ∘ 𝑋) ↾ 𝐹) = (𝑌 ∘ (𝑋 ↾ 𝐹))
78		f1ocnv 6815	. . . . . . . . . . . . 13 ⊢ (𝑋:𝐴–1-1-onto→𝐴 → ^◡𝑋:𝐴–1-1-onto→𝐴)
79		f1ofun 6805	. . . . . . . . . . . . 13 ⊢ (^◡𝑋:𝐴–1-1-onto→𝐴 → Fun ^◡𝑋)
80	63, 78, 79	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → Fun ^◡𝑋)
81		f1ofn 6804	. . . . . . . . . . . . . 14 ⊢ (𝑋:𝐴–1-1-onto→𝐴 → 𝑋 Fn 𝐴)
82		fnresdm 6640	. . . . . . . . . . . . . 14 ⊢ (𝑋 Fn 𝐴 → (𝑋 ↾ 𝐴) = 𝑋)
83	63, 81, 82	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 ↾ 𝐴) = 𝑋)
84		f1ofo 6810	. . . . . . . . . . . . . 14 ⊢ (𝑋:𝐴–1-1-onto→𝐴 → 𝑋:𝐴–onto→𝐴)
85	63, 84	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋:𝐴–onto→𝐴)
86		foeq1 6771	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ↾ 𝐴) = 𝑋 → ((𝑋 ↾ 𝐴):𝐴–onto→𝐴 ↔ 𝑋:𝐴–onto→𝐴))
87	86	biimpar 477	. . . . . . . . . . . . 13 ⊢ (((𝑋 ↾ 𝐴) = 𝑋 ∧ 𝑋:𝐴–onto→𝐴) → (𝑋 ↾ 𝐴):𝐴–onto→𝐴)
88	83, 85, 87	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 ↾ 𝐴):𝐴–onto→𝐴)
89		f1oi 6841	. . . . . . . . . . . . . 14 ⊢ ( I ↾ 𝐸):𝐸–1-1-onto→𝐸
90		f1ofo 6810	. . . . . . . . . . . . . 14 ⊢ (( I ↾ 𝐸):𝐸–1-1-onto→𝐸 → ( I ↾ 𝐸):𝐸–onto→𝐸)
91	89, 90	mp1i 13	. . . . . . . . . . . . 13 ⊢ (𝜑 → ( I ↾ 𝐸):𝐸–onto→𝐸)
92		foeq1 6771	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ↾ 𝐸) = ( I ↾ 𝐸) → ((𝑋 ↾ 𝐸):𝐸–onto→𝐸 ↔ ( I ↾ 𝐸):𝐸–onto→𝐸))
93	92	biimpar 477	. . . . . . . . . . . . 13 ⊢ (((𝑋 ↾ 𝐸) = ( I ↾ 𝐸) ∧ ( I ↾ 𝐸):𝐸–onto→𝐸) → (𝑋 ↾ 𝐸):𝐸–onto→𝐸)
94	49, 91, 93	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 ↾ 𝐸):𝐸–onto→𝐸)
95		resdif 6824	. . . . . . . . . . . 12 ⊢ ((Fun ^◡𝑋 ∧ (𝑋 ↾ 𝐴):𝐴–onto→𝐴 ∧ (𝑋 ↾ 𝐸):𝐸–onto→𝐸) → (𝑋 ↾ (𝐴 ∖ 𝐸)):(𝐴 ∖ 𝐸)–1-1-onto→(𝐴 ∖ 𝐸))
96	80, 88, 94, 95	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋 ↾ (𝐴 ∖ 𝐸)):(𝐴 ∖ 𝐸)–1-1-onto→(𝐴 ∖ 𝐸))
97		ssun1 4144	. . . . . . . . . . . . . . 15 ⊢ 𝐸 ⊆ (𝐸 ∪ 𝐹)
98	97, 1	sseqtrid 3992	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸 ⊆ 𝐴)
99		uneqdifeq 4459	. . . . . . . . . . . . . . 15 ⊢ ((𝐸 ⊆ 𝐴 ∧ (𝐸 ∩ 𝐹) = ∅) → ((𝐸 ∪ 𝐹) = 𝐴 ↔ (𝐴 ∖ 𝐸) = 𝐹))
100	99	biimpa 476	. . . . . . . . . . . . . 14 ⊢ (((𝐸 ⊆ 𝐴 ∧ (𝐸 ∩ 𝐹) = ∅) ∧ (𝐸 ∪ 𝐹) = 𝐴) → (𝐴 ∖ 𝐸) = 𝐹)
101	98, 33, 1, 100	syl21anc 837	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 ∖ 𝐸) = 𝐹)
102	101	reseq2d 5953	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 ↾ (𝐴 ∖ 𝐸)) = (𝑋 ↾ 𝐹))
103	102, 101, 101	f1oeq123d 6797	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑋 ↾ (𝐴 ∖ 𝐸)):(𝐴 ∖ 𝐸)–1-1-onto→(𝐴 ∖ 𝐸) ↔ (𝑋 ↾ 𝐹):𝐹–1-1-onto→𝐹))
104	96, 103	mpbid 232	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 ↾ 𝐹):𝐹–1-1-onto→𝐹)
105		f1of 6803	. . . . . . . . . 10 ⊢ ((𝑋 ↾ 𝐹):𝐹–1-1-onto→𝐹 → (𝑋 ↾ 𝐹):𝐹⟶𝐹)
106	104, 105	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 ↾ 𝐹):𝐹⟶𝐹)
107	106	frnd 6699	. . . . . . . 8 ⊢ (𝜑 → ran (𝑋 ↾ 𝐹) ⊆ 𝐹)
108		cores 6225	. . . . . . . 8 ⊢ (ran (𝑋 ↾ 𝐹) ⊆ 𝐹 → ((𝑌 ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (𝑌 ∘ (𝑋 ↾ 𝐹)))
109	107, 108	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑌 ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (𝑌 ∘ (𝑋 ↾ 𝐹)))
110	77, 109	eqtr4id 2784	. . . . . 6 ⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ 𝐹) = ((𝑌 ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)))
111	21	coeq1d 5828	. . . . . 6 ⊢ (𝜑 → ((𝑌 ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (( I ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)))
112		fcoi2 6738	. . . . . . 7 ⊢ ((𝑋 ↾ 𝐹):𝐹⟶𝐹 → (( I ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (𝑋 ↾ 𝐹))
113	106, 112	syl 17	. . . . . 6 ⊢ (𝜑 → (( I ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (𝑋 ↾ 𝐹))
114	110, 111, 113	3eqtrd 2769	. . . . 5 ⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ 𝐹) = (𝑋 ↾ 𝐹))
115	76, 114	uneq12d 4135	. . . 4 ⊢ (𝜑 → (((𝑌 ∘ 𝑋) ↾ 𝐸) ∪ ((𝑌 ∘ 𝑋) ↾ 𝐹)) = ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)))
116	71, 115	eqtrid 2777	. . 3 ⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ (𝐸 ∪ 𝐹)) = ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)))
117		f1oco 6826	. . . . 5 ⊢ ((𝑌:𝐴–1-1-onto→𝐴 ∧ 𝑋:𝐴–1-1-onto→𝐴) → (𝑌 ∘ 𝑋):𝐴–1-1-onto→𝐴)
118	9, 63, 117	syl2anc 584	. . . 4 ⊢ (𝜑 → (𝑌 ∘ 𝑋):𝐴–1-1-onto→𝐴)
119		f1ofn 6804	. . . 4 ⊢ ((𝑌 ∘ 𝑋):𝐴–1-1-onto→𝐴 → (𝑌 ∘ 𝑋) Fn 𝐴)
120		fnresdm 6640	. . . 4 ⊢ ((𝑌 ∘ 𝑋) Fn 𝐴 → ((𝑌 ∘ 𝑋) ↾ 𝐴) = (𝑌 ∘ 𝑋))
121	118, 119, 120	3syl 18	. . 3 ⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ 𝐴) = (𝑌 ∘ 𝑋))
122	70, 116, 121	3eqtr3d 2773	. 2 ⊢ (𝜑 → ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)) = (𝑌 ∘ 𝑋))
123	69, 122	eqtr3d 2767	1 ⊢ (𝜑 → (𝑋 ∘ 𝑌) = (𝑌 ∘ 𝑋))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ∖ cdif 3914 ∪ cun 3915 ∩ cin 3916 ⊆ wss 3917 ∅c0 4299 I cid 5535 ^◡ccnv 5640 ran crn 5642 ↾ cres 5643 ∘ ccom 5645 Fun wfun 6508 Fn wfn 6509 ⟶wf 6510 –onto→wfo 6512 –1-1-onto→wf1o 6513 ‘cfv 6514 Basecbs 17186 SymGrpcsymg 19306

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714 ax-cnex 11131 ax-resscn 11132 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-addrcl 11136 ax-mulcl 11137 ax-mulrcl 11138 ax-mulcom 11139 ax-addass 11140 ax-mulass 11141 ax-distr 11142 ax-i2m1 11143 ax-1ne0 11144 ax-1rid 11145 ax-rnegex 11146 ax-rrecex 11147 ax-cnre 11148 ax-pre-lttri 11149 ax-pre-lttrn 11150 ax-pre-ltadd 11151 ax-pre-mulgt0 11152

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-pss 3937 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-tp 4597 df-op 4599 df-uni 4875 df-iun 4960 df-br 5111 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5536 df-eprel 5541 df-po 5549 df-so 5550 df-fr 5594 df-we 5596 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-pred 6277 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-om 7846 df-1st 7971 df-2nd 7972 df-frecs 8263 df-wrecs 8294 df-recs 8343 df-rdg 8381 df-1o 8437 df-er 8674 df-map 8804 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-pnf 11217 df-mnf 11218 df-xr 11219 df-ltxr 11220 df-le 11221 df-sub 11414 df-neg 11415 df-nn 12194 df-2 12256 df-3 12257 df-4 12258 df-5 12259 df-6 12260 df-7 12261 df-8 12262 df-9 12263 df-n0 12450 df-z 12537 df-uz 12801 df-fz 13476 df-struct 17124 df-sets 17141 df-slot 17159 df-ndx 17171 df-base 17187 df-ress 17208 df-plusg 17240 df-tset 17246 df-efmnd 18803 df-symg 19307

This theorem is referenced by: symgcom2 33048 cyc3conja 33121

W3C validator