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 31071

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 5851	. . 3 ⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ (𝐸 ∪ 𝐹)) = ((𝑋 ∘ 𝑌) ↾ 𝐴))
3		resundi 5865	. . . 4 ⊢ ((𝑋 ∘ 𝑌) ↾ (𝐸 ∪ 𝐹)) = (((𝑋 ∘ 𝑌) ↾ 𝐸) ∪ ((𝑋 ∘ 𝑌) ↾ 𝐹))
4		resco 6114	. . . . . . 7 ⊢ ((𝑋 ∘ 𝑌) ↾ 𝐸) = (𝑋 ∘ (𝑌 ↾ 𝐸))
5		symgcom.y	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
6		symgcom.g	. . . . . . . . . . . . . . 15 ⊢ 𝐺 = (SymGrp‘𝐴)
7		symgcom.b	. . . . . . . . . . . . . . 15 ⊢ 𝐵 = (Base‘𝐺)
8	6, 7	symgbasf1o 18767	. . . . . . . . . . . . . 14 ⊢ (𝑌 ∈ 𝐵 → 𝑌:𝐴–1-1-onto→𝐴)
9	5, 8	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌:𝐴–1-1-onto→𝐴)
10		f1ocnv 6673	. . . . . . . . . . . . 13 ⊢ (𝑌:𝐴–1-1-onto→𝐴 → ^◡𝑌:𝐴–1-1-onto→𝐴)
11		f1ofun 6663	. . . . . . . . . . . . 13 ⊢ (^◡𝑌:𝐴–1-1-onto→𝐴 → Fun ^◡𝑌)
12	9, 10, 11	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → Fun ^◡𝑌)
13		f1ofn 6662	. . . . . . . . . . . . . 14 ⊢ (𝑌:𝐴–1-1-onto→𝐴 → 𝑌 Fn 𝐴)
14		fnresdm 6496	. . . . . . . . . . . . . 14 ⊢ (𝑌 Fn 𝐴 → (𝑌 ↾ 𝐴) = 𝑌)
15	9, 13, 14	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌 ↾ 𝐴) = 𝑌)
16		f1ofo 6668	. . . . . . . . . . . . . 14 ⊢ (𝑌:𝐴–1-1-onto→𝐴 → 𝑌:𝐴–onto→𝐴)
17	9, 16	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌:𝐴–onto→𝐴)
18		foeq1 6629	. . . . . . . . . . . . . 14 ⊢ ((𝑌 ↾ 𝐴) = 𝑌 → ((𝑌 ↾ 𝐴):𝐴–onto→𝐴 ↔ 𝑌:𝐴–onto→𝐴))
19	18	biimpar 481	. . . . . . . . . . . . 13 ⊢ (((𝑌 ↾ 𝐴) = 𝑌 ∧ 𝑌:𝐴–onto→𝐴) → (𝑌 ↾ 𝐴):𝐴–onto→𝐴)
20	15, 17, 19	syl2anc 587	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌 ↾ 𝐴):𝐴–onto→𝐴)
21		symgcom.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌 ↾ 𝐹) = ( I ↾ 𝐹))
22		f1oi 6698	. . . . . . . . . . . . . 14 ⊢ ( I ↾ 𝐹):𝐹–1-1-onto→𝐹
23		f1ofo 6668	. . . . . . . . . . . . . 14 ⊢ (( I ↾ 𝐹):𝐹–1-1-onto→𝐹 → ( I ↾ 𝐹):𝐹–onto→𝐹)
24	22, 23	mp1i 13	. . . . . . . . . . . . 13 ⊢ (𝜑 → ( I ↾ 𝐹):𝐹–onto→𝐹)
25		foeq1 6629	. . . . . . . . . . . . . 14 ⊢ ((𝑌 ↾ 𝐹) = ( I ↾ 𝐹) → ((𝑌 ↾ 𝐹):𝐹–onto→𝐹 ↔ ( I ↾ 𝐹):𝐹–onto→𝐹))
26	25	biimpar 481	. . . . . . . . . . . . 13 ⊢ (((𝑌 ↾ 𝐹) = ( I ↾ 𝐹) ∧ ( I ↾ 𝐹):𝐹–onto→𝐹) → (𝑌 ↾ 𝐹):𝐹–onto→𝐹)
27	21, 24, 26	syl2anc 587	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌 ↾ 𝐹):𝐹–onto→𝐹)
28		resdif 6681	. . . . . . . . . . . 12 ⊢ ((Fun ^◡𝑌 ∧ (𝑌 ↾ 𝐴):𝐴–onto→𝐴 ∧ (𝑌 ↾ 𝐹):𝐹–onto→𝐹) → (𝑌 ↾ (𝐴 ∖ 𝐹)):(𝐴 ∖ 𝐹)–1-1-onto→(𝐴 ∖ 𝐹))
29	12, 20, 27, 28	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 ↾ (𝐴 ∖ 𝐹)):(𝐴 ∖ 𝐹)–1-1-onto→(𝐴 ∖ 𝐹))
30		ssun2 4087	. . . . . . . . . . . . . . 15 ⊢ 𝐹 ⊆ (𝐸 ∪ 𝐹)
31	30, 1	sseqtrid 3953	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 ⊆ 𝐴)
32		incom 4115	. . . . . . . . . . . . . . 15 ⊢ (𝐸 ∩ 𝐹) = (𝐹 ∩ 𝐸)
33		symgcom.3	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐸 ∩ 𝐹) = ∅)
34	32, 33	eqtr3id 2792	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹 ∩ 𝐸) = ∅)
35		uncom 4067	. . . . . . . . . . . . . . 15 ⊢ (𝐸 ∪ 𝐹) = (𝐹 ∪ 𝐸)
36	35, 1	eqtr3id 2792	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹 ∪ 𝐸) = 𝐴)
37		uneqdifeq 4404	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ⊆ 𝐴 ∧ (𝐹 ∩ 𝐸) = ∅) → ((𝐹 ∪ 𝐸) = 𝐴 ↔ (𝐴 ∖ 𝐹) = 𝐸))
38	37	biimpa 480	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ⊆ 𝐴 ∧ (𝐹 ∩ 𝐸) = ∅) ∧ (𝐹 ∪ 𝐸) = 𝐴) → (𝐴 ∖ 𝐹) = 𝐸)
39	31, 34, 36, 38	syl21anc 838	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 ∖ 𝐹) = 𝐸)
40	39	reseq2d 5851	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌 ↾ (𝐴 ∖ 𝐹)) = (𝑌 ↾ 𝐸))
41	40, 39, 39	f1oeq123d 6655	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑌 ↾ (𝐴 ∖ 𝐹)):(𝐴 ∖ 𝐹)–1-1-onto→(𝐴 ∖ 𝐹) ↔ (𝑌 ↾ 𝐸):𝐸–1-1-onto→𝐸))
42	29, 41	mpbid 235	. . . . . . . . . 10 ⊢ (𝜑 → (𝑌 ↾ 𝐸):𝐸–1-1-onto→𝐸)
43		f1of 6661	. . . . . . . . . 10 ⊢ ((𝑌 ↾ 𝐸):𝐸–1-1-onto→𝐸 → (𝑌 ↾ 𝐸):𝐸⟶𝐸)
44	42, 43	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑌 ↾ 𝐸):𝐸⟶𝐸)
45	44	frnd 6553	. . . . . . . 8 ⊢ (𝜑 → ran (𝑌 ↾ 𝐸) ⊆ 𝐸)
46		cores 6113	. . . . . . . 8 ⊢ (ran (𝑌 ↾ 𝐸) ⊆ 𝐸 → ((𝑋 ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (𝑋 ∘ (𝑌 ↾ 𝐸)))
47	45, 46	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑋 ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (𝑋 ∘ (𝑌 ↾ 𝐸)))
48	4, 47	eqtr4id 2797	. . . . . 6 ⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ 𝐸) = ((𝑋 ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)))
49		symgcom.1	. . . . . . 7 ⊢ (𝜑 → (𝑋 ↾ 𝐸) = ( I ↾ 𝐸))
50	49	coeq1d 5730	. . . . . 6 ⊢ (𝜑 → ((𝑋 ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (( I ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)))
51		fcoi2 6594	. . . . . . 7 ⊢ ((𝑌 ↾ 𝐸):𝐸⟶𝐸 → (( I ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (𝑌 ↾ 𝐸))
52	44, 51	syl 17	. . . . . 6 ⊢ (𝜑 → (( I ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (𝑌 ↾ 𝐸))
53	48, 50, 52	3eqtrd 2781	. . . . 5 ⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ 𝐸) = (𝑌 ↾ 𝐸))
54		resco 6114	. . . . . 6 ⊢ ((𝑋 ∘ 𝑌) ↾ 𝐹) = (𝑋 ∘ (𝑌 ↾ 𝐹))
55	21	coeq2d 5731	. . . . . . 7 ⊢ (𝜑 → (𝑋 ∘ (𝑌 ↾ 𝐹)) = (𝑋 ∘ ( I ↾ 𝐹)))
56		coires1 6128	. . . . . . 7 ⊢ (𝑋 ∘ ( I ↾ 𝐹)) = (𝑋 ↾ 𝐹)
57	55, 56	eqtrdi 2794	. . . . . 6 ⊢ (𝜑 → (𝑋 ∘ (𝑌 ↾ 𝐹)) = (𝑋 ↾ 𝐹))
58	54, 57	syl5eq 2790	. . . . 5 ⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ 𝐹) = (𝑋 ↾ 𝐹))
59	53, 58	uneq12d 4078	. . . 4 ⊢ (𝜑 → (((𝑋 ∘ 𝑌) ↾ 𝐸) ∪ ((𝑋 ∘ 𝑌) ↾ 𝐹)) = ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)))
60	3, 59	syl5eq 2790	. . 3 ⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ (𝐸 ∪ 𝐹)) = ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)))
61		symgcom.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
62	6, 7	symgbasf1o 18767	. . . . . 6 ⊢ (𝑋 ∈ 𝐵 → 𝑋:𝐴–1-1-onto→𝐴)
63	61, 62	syl 17	. . . . 5 ⊢ (𝜑 → 𝑋:𝐴–1-1-onto→𝐴)
64		f1oco 6683	. . . . 5 ⊢ ((𝑋:𝐴–1-1-onto→𝐴 ∧ 𝑌:𝐴–1-1-onto→𝐴) → (𝑋 ∘ 𝑌):𝐴–1-1-onto→𝐴)
65	63, 9, 64	syl2anc 587	. . . 4 ⊢ (𝜑 → (𝑋 ∘ 𝑌):𝐴–1-1-onto→𝐴)
66		f1ofn 6662	. . . 4 ⊢ ((𝑋 ∘ 𝑌):𝐴–1-1-onto→𝐴 → (𝑋 ∘ 𝑌) Fn 𝐴)
67		fnresdm 6496	. . . 4 ⊢ ((𝑋 ∘ 𝑌) Fn 𝐴 → ((𝑋 ∘ 𝑌) ↾ 𝐴) = (𝑋 ∘ 𝑌))
68	65, 66, 67	3syl 18	. . 3 ⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ 𝐴) = (𝑋 ∘ 𝑌))
69	2, 60, 68	3eqtr3d 2785	. 2 ⊢ (𝜑 → ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)) = (𝑋 ∘ 𝑌))
70	1	reseq2d 5851	. . 3 ⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ (𝐸 ∪ 𝐹)) = ((𝑌 ∘ 𝑋) ↾ 𝐴))
71		resundi 5865	. . . 4 ⊢ ((𝑌 ∘ 𝑋) ↾ (𝐸 ∪ 𝐹)) = (((𝑌 ∘ 𝑋) ↾ 𝐸) ∪ ((𝑌 ∘ 𝑋) ↾ 𝐹))
72		resco 6114	. . . . . 6 ⊢ ((𝑌 ∘ 𝑋) ↾ 𝐸) = (𝑌 ∘ (𝑋 ↾ 𝐸))
73	49	coeq2d 5731	. . . . . . 7 ⊢ (𝜑 → (𝑌 ∘ (𝑋 ↾ 𝐸)) = (𝑌 ∘ ( I ↾ 𝐸)))
74		coires1 6128	. . . . . . 7 ⊢ (𝑌 ∘ ( I ↾ 𝐸)) = (𝑌 ↾ 𝐸)
75	73, 74	eqtrdi 2794	. . . . . 6 ⊢ (𝜑 → (𝑌 ∘ (𝑋 ↾ 𝐸)) = (𝑌 ↾ 𝐸))
76	72, 75	syl5eq 2790	. . . . 5 ⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ 𝐸) = (𝑌 ↾ 𝐸))
77		resco 6114	. . . . . . 7 ⊢ ((𝑌 ∘ 𝑋) ↾ 𝐹) = (𝑌 ∘ (𝑋 ↾ 𝐹))
78		f1ocnv 6673	. . . . . . . . . . . . 13 ⊢ (𝑋:𝐴–1-1-onto→𝐴 → ^◡𝑋:𝐴–1-1-onto→𝐴)
79		f1ofun 6663	. . . . . . . . . . . . 13 ⊢ (^◡𝑋:𝐴–1-1-onto→𝐴 → Fun ^◡𝑋)
80	63, 78, 79	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → Fun ^◡𝑋)
81		f1ofn 6662	. . . . . . . . . . . . . 14 ⊢ (𝑋:𝐴–1-1-onto→𝐴 → 𝑋 Fn 𝐴)
82		fnresdm 6496	. . . . . . . . . . . . . 14 ⊢ (𝑋 Fn 𝐴 → (𝑋 ↾ 𝐴) = 𝑋)
83	63, 81, 82	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 ↾ 𝐴) = 𝑋)
84		f1ofo 6668	. . . . . . . . . . . . . 14 ⊢ (𝑋:𝐴–1-1-onto→𝐴 → 𝑋:𝐴–onto→𝐴)
85	63, 84	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋:𝐴–onto→𝐴)
86		foeq1 6629	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ↾ 𝐴) = 𝑋 → ((𝑋 ↾ 𝐴):𝐴–onto→𝐴 ↔ 𝑋:𝐴–onto→𝐴))
87	86	biimpar 481	. . . . . . . . . . . . 13 ⊢ (((𝑋 ↾ 𝐴) = 𝑋 ∧ 𝑋:𝐴–onto→𝐴) → (𝑋 ↾ 𝐴):𝐴–onto→𝐴)
88	83, 85, 87	syl2anc 587	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 ↾ 𝐴):𝐴–onto→𝐴)
89		f1oi 6698	. . . . . . . . . . . . . 14 ⊢ ( I ↾ 𝐸):𝐸–1-1-onto→𝐸
90		f1ofo 6668	. . . . . . . . . . . . . 14 ⊢ (( I ↾ 𝐸):𝐸–1-1-onto→𝐸 → ( I ↾ 𝐸):𝐸–onto→𝐸)
91	89, 90	mp1i 13	. . . . . . . . . . . . 13 ⊢ (𝜑 → ( I ↾ 𝐸):𝐸–onto→𝐸)
92		foeq1 6629	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ↾ 𝐸) = ( I ↾ 𝐸) → ((𝑋 ↾ 𝐸):𝐸–onto→𝐸 ↔ ( I ↾ 𝐸):𝐸–onto→𝐸))
93	92	biimpar 481	. . . . . . . . . . . . 13 ⊢ (((𝑋 ↾ 𝐸) = ( I ↾ 𝐸) ∧ ( I ↾ 𝐸):𝐸–onto→𝐸) → (𝑋 ↾ 𝐸):𝐸–onto→𝐸)
94	49, 91, 93	syl2anc 587	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 ↾ 𝐸):𝐸–onto→𝐸)
95		resdif 6681	. . . . . . . . . . . 12 ⊢ ((Fun ^◡𝑋 ∧ (𝑋 ↾ 𝐴):𝐴–onto→𝐴 ∧ (𝑋 ↾ 𝐸):𝐸–onto→𝐸) → (𝑋 ↾ (𝐴 ∖ 𝐸)):(𝐴 ∖ 𝐸)–1-1-onto→(𝐴 ∖ 𝐸))
96	80, 88, 94, 95	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋 ↾ (𝐴 ∖ 𝐸)):(𝐴 ∖ 𝐸)–1-1-onto→(𝐴 ∖ 𝐸))
97		ssun1 4086	. . . . . . . . . . . . . . 15 ⊢ 𝐸 ⊆ (𝐸 ∪ 𝐹)
98	97, 1	sseqtrid 3953	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸 ⊆ 𝐴)
99		uneqdifeq 4404	. . . . . . . . . . . . . . 15 ⊢ ((𝐸 ⊆ 𝐴 ∧ (𝐸 ∩ 𝐹) = ∅) → ((𝐸 ∪ 𝐹) = 𝐴 ↔ (𝐴 ∖ 𝐸) = 𝐹))
100	99	biimpa 480	. . . . . . . . . . . . . 14 ⊢ (((𝐸 ⊆ 𝐴 ∧ (𝐸 ∩ 𝐹) = ∅) ∧ (𝐸 ∪ 𝐹) = 𝐴) → (𝐴 ∖ 𝐸) = 𝐹)
101	98, 33, 1, 100	syl21anc 838	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 ∖ 𝐸) = 𝐹)
102	101	reseq2d 5851	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 ↾ (𝐴 ∖ 𝐸)) = (𝑋 ↾ 𝐹))
103	102, 101, 101	f1oeq123d 6655	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑋 ↾ (𝐴 ∖ 𝐸)):(𝐴 ∖ 𝐸)–1-1-onto→(𝐴 ∖ 𝐸) ↔ (𝑋 ↾ 𝐹):𝐹–1-1-onto→𝐹))
104	96, 103	mpbid 235	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 ↾ 𝐹):𝐹–1-1-onto→𝐹)
105		f1of 6661	. . . . . . . . . 10 ⊢ ((𝑋 ↾ 𝐹):𝐹–1-1-onto→𝐹 → (𝑋 ↾ 𝐹):𝐹⟶𝐹)
106	104, 105	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 ↾ 𝐹):𝐹⟶𝐹)
107	106	frnd 6553	. . . . . . . 8 ⊢ (𝜑 → ran (𝑋 ↾ 𝐹) ⊆ 𝐹)
108		cores 6113	. . . . . . . 8 ⊢ (ran (𝑋 ↾ 𝐹) ⊆ 𝐹 → ((𝑌 ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (𝑌 ∘ (𝑋 ↾ 𝐹)))
109	107, 108	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑌 ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (𝑌 ∘ (𝑋 ↾ 𝐹)))
110	77, 109	eqtr4id 2797	. . . . . 6 ⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ 𝐹) = ((𝑌 ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)))
111	21	coeq1d 5730	. . . . . 6 ⊢ (𝜑 → ((𝑌 ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (( I ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)))
112		fcoi2 6594	. . . . . . 7 ⊢ ((𝑋 ↾ 𝐹):𝐹⟶𝐹 → (( I ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (𝑋 ↾ 𝐹))
113	106, 112	syl 17	. . . . . 6 ⊢ (𝜑 → (( I ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (𝑋 ↾ 𝐹))
114	110, 111, 113	3eqtrd 2781	. . . . 5 ⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ 𝐹) = (𝑋 ↾ 𝐹))
115	76, 114	uneq12d 4078	. . . 4 ⊢ (𝜑 → (((𝑌 ∘ 𝑋) ↾ 𝐸) ∪ ((𝑌 ∘ 𝑋) ↾ 𝐹)) = ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)))
116	71, 115	syl5eq 2790	. . 3 ⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ (𝐸 ∪ 𝐹)) = ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)))
117		f1oco 6683	. . . . 5 ⊢ ((𝑌:𝐴–1-1-onto→𝐴 ∧ 𝑋:𝐴–1-1-onto→𝐴) → (𝑌 ∘ 𝑋):𝐴–1-1-onto→𝐴)
118	9, 63, 117	syl2anc 587	. . . 4 ⊢ (𝜑 → (𝑌 ∘ 𝑋):𝐴–1-1-onto→𝐴)
119		f1ofn 6662	. . . 4 ⊢ ((𝑌 ∘ 𝑋):𝐴–1-1-onto→𝐴 → (𝑌 ∘ 𝑋) Fn 𝐴)
120		fnresdm 6496	. . . 4 ⊢ ((𝑌 ∘ 𝑋) Fn 𝐴 → ((𝑌 ∘ 𝑋) ↾ 𝐴) = (𝑌 ∘ 𝑋))
121	118, 119, 120	3syl 18	. . 3 ⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ 𝐴) = (𝑌 ∘ 𝑋))
122	70, 116, 121	3eqtr3d 2785	. 2 ⊢ (𝜑 → ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)) = (𝑌 ∘ 𝑋))
123	69, 122	eqtr3d 2779	1 ⊢ (𝜑 → (𝑋 ∘ 𝑌) = (𝑌 ∘ 𝑋))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 = wceq 1543 ∈ wcel 2110 ∖ cdif 3863 ∪ cun 3864 ∩ cin 3865 ⊆ wss 3866 ∅c0 4237 I cid 5454 ^◡ccnv 5550 ran crn 5552 ↾ cres 5553 ∘ ccom 5555 Fun wfun 6374 Fn wfn 6375 ⟶wf 6376 –onto→wfo 6378 –1-1-onto→wf1o 6379 ‘cfv 6380 Basecbs 16760 SymGrpcsymg 18759

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 ax-sep 5192 ax-nul 5199 ax-pow 5258 ax-pr 5322 ax-un 7523 ax-cnex 10785 ax-resscn 10786 ax-1cn 10787 ax-icn 10788 ax-addcl 10789 ax-addrcl 10790 ax-mulcl 10791 ax-mulrcl 10792 ax-mulcom 10793 ax-addass 10794 ax-mulass 10795 ax-distr 10796 ax-i2m1 10797 ax-1ne0 10798 ax-1rid 10799 ax-rnegex 10800 ax-rrecex 10801 ax-cnre 10802 ax-pre-lttri 10803 ax-pre-lttrn 10804 ax-pre-ltadd 10805 ax-pre-mulgt0 10806

This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2886 df-ne 2941 df-nel 3047 df-ral 3066 df-rex 3067 df-reu 3068 df-rab 3070 df-v 3410 df-sbc 3695 df-csb 3812 df-dif 3869 df-un 3871 df-in 3873 df-ss 3883 df-pss 3885 df-nul 4238 df-if 4440 df-pw 4515 df-sn 4542 df-pr 4544 df-tp 4546 df-op 4548 df-uni 4820 df-iun 4906 df-br 5054 df-opab 5116 df-mpt 5136 df-tr 5162 df-id 5455 df-eprel 5460 df-po 5468 df-so 5469 df-fr 5509 df-we 5511 df-xp 5557 df-rel 5558 df-cnv 5559 df-co 5560 df-dm 5561 df-rn 5562 df-res 5563 df-ima 5564 df-pred 6160 df-ord 6216 df-on 6217 df-lim 6218 df-suc 6219 df-iota 6338 df-fun 6382 df-fn 6383 df-f 6384 df-f1 6385 df-fo 6386 df-f1o 6387 df-fv 6388 df-riota 7170 df-ov 7216 df-oprab 7217 df-mpo 7218 df-om 7645 df-1st 7761 df-2nd 7762 df-wrecs 8047 df-recs 8108 df-rdg 8146 df-1o 8202 df-er 8391 df-map 8510 df-en 8627 df-dom 8628 df-sdom 8629 df-fin 8630 df-pnf 10869 df-mnf 10870 df-xr 10871 df-ltxr 10872 df-le 10873 df-sub 11064 df-neg 11065 df-nn 11831 df-2 11893 df-3 11894 df-4 11895 df-5 11896 df-6 11897 df-7 11898 df-8 11899 df-9 11900 df-n0 12091 df-z 12177 df-uz 12439 df-fz 13096 df-struct 16700 df-sets 16717 df-slot 16735 df-ndx 16745 df-base 16761 df-ress 16785 df-plusg 16815 df-tset 16821 df-efmnd 18296 df-symg 18760

This theorem is referenced by: symgcom2 31072 cyc3conja 31143

W3C validator