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 33044

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 5923	. . 3 ⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ (𝐸 ∪ 𝐹)) = ((𝑋 ∘ 𝑌) ↾ 𝐴))
3		resundi 5937	. . . 4 ⊢ ((𝑋 ∘ 𝑌) ↾ (𝐸 ∪ 𝐹)) = (((𝑋 ∘ 𝑌) ↾ 𝐸) ∪ ((𝑋 ∘ 𝑌) ↾ 𝐹))
4		resco 6192	. . . . . . 7 ⊢ ((𝑋 ∘ 𝑌) ↾ 𝐸) = (𝑋 ∘ (𝑌 ↾ 𝐸))
5		symgcom.y	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
6		symgcom.g	. . . . . . . . . . . . . . 15 ⊢ 𝐺 = (SymGrp‘𝐴)
7		symgcom.b	. . . . . . . . . . . . . . 15 ⊢ 𝐵 = (Base‘𝐺)
8	6, 7	symgbasf1o 19282	. . . . . . . . . . . . . 14 ⊢ (𝑌 ∈ 𝐵 → 𝑌:𝐴–1-1-onto→𝐴)
9	5, 8	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌:𝐴–1-1-onto→𝐴)
10		f1ocnv 6770	. . . . . . . . . . . . 13 ⊢ (𝑌:𝐴–1-1-onto→𝐴 → ^◡𝑌:𝐴–1-1-onto→𝐴)
11		f1ofun 6760	. . . . . . . . . . . . 13 ⊢ (^◡𝑌:𝐴–1-1-onto→𝐴 → Fun ^◡𝑌)
12	9, 10, 11	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → Fun ^◡𝑌)
13		f1ofn 6759	. . . . . . . . . . . . . 14 ⊢ (𝑌:𝐴–1-1-onto→𝐴 → 𝑌 Fn 𝐴)
14		fnresdm 6595	. . . . . . . . . . . . . 14 ⊢ (𝑌 Fn 𝐴 → (𝑌 ↾ 𝐴) = 𝑌)
15	9, 13, 14	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌 ↾ 𝐴) = 𝑌)
16		f1ofo 6765	. . . . . . . . . . . . . 14 ⊢ (𝑌:𝐴–1-1-onto→𝐴 → 𝑌:𝐴–onto→𝐴)
17	9, 16	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌:𝐴–onto→𝐴)
18		foeq1 6726	. . . . . . . . . . . . . 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 6796	. . . . . . . . . . . . . 14 ⊢ ( I ↾ 𝐹):𝐹–1-1-onto→𝐹
23		f1ofo 6765	. . . . . . . . . . . . . 14 ⊢ (( I ↾ 𝐹):𝐹–1-1-onto→𝐹 → ( I ↾ 𝐹):𝐹–onto→𝐹)
24	22, 23	mp1i 13	. . . . . . . . . . . . 13 ⊢ (𝜑 → ( I ↾ 𝐹):𝐹–onto→𝐹)
25		foeq1 6726	. . . . . . . . . . . . . 14 ⊢ ((𝑌 ↾ 𝐹) = ( I ↾ 𝐹) → ((𝑌 ↾ 𝐹):𝐹–onto→𝐹 ↔ ( I ↾ 𝐹):𝐹–onto→𝐹))
26	25	biimpar 477	. . . . . . . . . . . . 13 ⊢ (((𝑌 ↾ 𝐹) = ( I ↾ 𝐹) ∧ ( I ↾ 𝐹):𝐹–onto→𝐹) → (𝑌 ↾ 𝐹):𝐹–onto→𝐹)
27	21, 24, 26	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌 ↾ 𝐹):𝐹–onto→𝐹)
28		resdif 6779	. . . . . . . . . . . 12 ⊢ ((Fun ^◡𝑌 ∧ (𝑌 ↾ 𝐴):𝐴–onto→𝐴 ∧ (𝑌 ↾ 𝐹):𝐹–onto→𝐹) → (𝑌 ↾ (𝐴 ∖ 𝐹)):(𝐴 ∖ 𝐹)–1-1-onto→(𝐴 ∖ 𝐹))
29	12, 20, 27, 28	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 ↾ (𝐴 ∖ 𝐹)):(𝐴 ∖ 𝐹)–1-1-onto→(𝐴 ∖ 𝐹))
30		ssun2 4124	. . . . . . . . . . . . . . 15 ⊢ 𝐹 ⊆ (𝐸 ∪ 𝐹)
31	30, 1	sseqtrid 3972	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 ⊆ 𝐴)
32		incom 4154	. . . . . . . . . . . . . . 15 ⊢ (𝐸 ∩ 𝐹) = (𝐹 ∩ 𝐸)
33		symgcom.3	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐸 ∩ 𝐹) = ∅)
34	32, 33	eqtr3id 2780	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹 ∩ 𝐸) = ∅)
35		uncom 4103	. . . . . . . . . . . . . . 15 ⊢ (𝐸 ∪ 𝐹) = (𝐹 ∪ 𝐸)
36	35, 1	eqtr3id 2780	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹 ∪ 𝐸) = 𝐴)
37		uneqdifeq 4438	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ⊆ 𝐴 ∧ (𝐹 ∩ 𝐸) = ∅) → ((𝐹 ∪ 𝐸) = 𝐴 ↔ (𝐴 ∖ 𝐹) = 𝐸))
38	37	biimpa 476	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ⊆ 𝐴 ∧ (𝐹 ∩ 𝐸) = ∅) ∧ (𝐹 ∪ 𝐸) = 𝐴) → (𝐴 ∖ 𝐹) = 𝐸)
39	31, 34, 36, 38	syl21anc 837	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 ∖ 𝐹) = 𝐸)
40	39	reseq2d 5923	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌 ↾ (𝐴 ∖ 𝐹)) = (𝑌 ↾ 𝐸))
41	40, 39, 39	f1oeq123d 6752	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑌 ↾ (𝐴 ∖ 𝐹)):(𝐴 ∖ 𝐹)–1-1-onto→(𝐴 ∖ 𝐹) ↔ (𝑌 ↾ 𝐸):𝐸–1-1-onto→𝐸))
42	29, 41	mpbid 232	. . . . . . . . . 10 ⊢ (𝜑 → (𝑌 ↾ 𝐸):𝐸–1-1-onto→𝐸)
43		f1of 6758	. . . . . . . . . 10 ⊢ ((𝑌 ↾ 𝐸):𝐸–1-1-onto→𝐸 → (𝑌 ↾ 𝐸):𝐸⟶𝐸)
44	42, 43	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑌 ↾ 𝐸):𝐸⟶𝐸)
45	44	frnd 6654	. . . . . . . 8 ⊢ (𝜑 → ran (𝑌 ↾ 𝐸) ⊆ 𝐸)
46		cores 6191	. . . . . . . 8 ⊢ (ran (𝑌 ↾ 𝐸) ⊆ 𝐸 → ((𝑋 ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (𝑋 ∘ (𝑌 ↾ 𝐸)))
47	45, 46	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑋 ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (𝑋 ∘ (𝑌 ↾ 𝐸)))
48	4, 47	eqtr4id 2785	. . . . . 6 ⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ 𝐸) = ((𝑋 ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)))
49		symgcom.1	. . . . . . 7 ⊢ (𝜑 → (𝑋 ↾ 𝐸) = ( I ↾ 𝐸))
50	49	coeq1d 5796	. . . . . 6 ⊢ (𝜑 → ((𝑋 ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (( I ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)))
51		fcoi2 6693	. . . . . . 7 ⊢ ((𝑌 ↾ 𝐸):𝐸⟶𝐸 → (( I ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (𝑌 ↾ 𝐸))
52	44, 51	syl 17	. . . . . 6 ⊢ (𝜑 → (( I ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (𝑌 ↾ 𝐸))
53	48, 50, 52	3eqtrd 2770	. . . . 5 ⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ 𝐸) = (𝑌 ↾ 𝐸))
54		resco 6192	. . . . . 6 ⊢ ((𝑋 ∘ 𝑌) ↾ 𝐹) = (𝑋 ∘ (𝑌 ↾ 𝐹))
55	21	coeq2d 5797	. . . . . . 7 ⊢ (𝜑 → (𝑋 ∘ (𝑌 ↾ 𝐹)) = (𝑋 ∘ ( I ↾ 𝐹)))
56		coires1 6207	. . . . . . 7 ⊢ (𝑋 ∘ ( I ↾ 𝐹)) = (𝑋 ↾ 𝐹)
57	55, 56	eqtrdi 2782	. . . . . 6 ⊢ (𝜑 → (𝑋 ∘ (𝑌 ↾ 𝐹)) = (𝑋 ↾ 𝐹))
58	54, 57	eqtrid 2778	. . . . 5 ⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ 𝐹) = (𝑋 ↾ 𝐹))
59	53, 58	uneq12d 4114	. . . 4 ⊢ (𝜑 → (((𝑋 ∘ 𝑌) ↾ 𝐸) ∪ ((𝑋 ∘ 𝑌) ↾ 𝐹)) = ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)))
60	3, 59	eqtrid 2778	. . 3 ⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ (𝐸 ∪ 𝐹)) = ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)))
61		symgcom.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
62	6, 7	symgbasf1o 19282	. . . . . 6 ⊢ (𝑋 ∈ 𝐵 → 𝑋:𝐴–1-1-onto→𝐴)
63	61, 62	syl 17	. . . . 5 ⊢ (𝜑 → 𝑋:𝐴–1-1-onto→𝐴)
64		f1oco 6781	. . . . 5 ⊢ ((𝑋:𝐴–1-1-onto→𝐴 ∧ 𝑌:𝐴–1-1-onto→𝐴) → (𝑋 ∘ 𝑌):𝐴–1-1-onto→𝐴)
65	63, 9, 64	syl2anc 584	. . . 4 ⊢ (𝜑 → (𝑋 ∘ 𝑌):𝐴–1-1-onto→𝐴)
66		f1ofn 6759	. . . 4 ⊢ ((𝑋 ∘ 𝑌):𝐴–1-1-onto→𝐴 → (𝑋 ∘ 𝑌) Fn 𝐴)
67		fnresdm 6595	. . . 4 ⊢ ((𝑋 ∘ 𝑌) Fn 𝐴 → ((𝑋 ∘ 𝑌) ↾ 𝐴) = (𝑋 ∘ 𝑌))
68	65, 66, 67	3syl 18	. . 3 ⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ 𝐴) = (𝑋 ∘ 𝑌))
69	2, 60, 68	3eqtr3d 2774	. 2 ⊢ (𝜑 → ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)) = (𝑋 ∘ 𝑌))
70	1	reseq2d 5923	. . 3 ⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ (𝐸 ∪ 𝐹)) = ((𝑌 ∘ 𝑋) ↾ 𝐴))
71		resundi 5937	. . . 4 ⊢ ((𝑌 ∘ 𝑋) ↾ (𝐸 ∪ 𝐹)) = (((𝑌 ∘ 𝑋) ↾ 𝐸) ∪ ((𝑌 ∘ 𝑋) ↾ 𝐹))
72		resco 6192	. . . . . 6 ⊢ ((𝑌 ∘ 𝑋) ↾ 𝐸) = (𝑌 ∘ (𝑋 ↾ 𝐸))
73	49	coeq2d 5797	. . . . . . 7 ⊢ (𝜑 → (𝑌 ∘ (𝑋 ↾ 𝐸)) = (𝑌 ∘ ( I ↾ 𝐸)))
74		coires1 6207	. . . . . . 7 ⊢ (𝑌 ∘ ( I ↾ 𝐸)) = (𝑌 ↾ 𝐸)
75	73, 74	eqtrdi 2782	. . . . . 6 ⊢ (𝜑 → (𝑌 ∘ (𝑋 ↾ 𝐸)) = (𝑌 ↾ 𝐸))
76	72, 75	eqtrid 2778	. . . . 5 ⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ 𝐸) = (𝑌 ↾ 𝐸))
77		resco 6192	. . . . . . 7 ⊢ ((𝑌 ∘ 𝑋) ↾ 𝐹) = (𝑌 ∘ (𝑋 ↾ 𝐹))
78		f1ocnv 6770	. . . . . . . . . . . . 13 ⊢ (𝑋:𝐴–1-1-onto→𝐴 → ^◡𝑋:𝐴–1-1-onto→𝐴)
79		f1ofun 6760	. . . . . . . . . . . . 13 ⊢ (^◡𝑋:𝐴–1-1-onto→𝐴 → Fun ^◡𝑋)
80	63, 78, 79	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → Fun ^◡𝑋)
81		f1ofn 6759	. . . . . . . . . . . . . 14 ⊢ (𝑋:𝐴–1-1-onto→𝐴 → 𝑋 Fn 𝐴)
82		fnresdm 6595	. . . . . . . . . . . . . 14 ⊢ (𝑋 Fn 𝐴 → (𝑋 ↾ 𝐴) = 𝑋)
83	63, 81, 82	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 ↾ 𝐴) = 𝑋)
84		f1ofo 6765	. . . . . . . . . . . . . 14 ⊢ (𝑋:𝐴–1-1-onto→𝐴 → 𝑋:𝐴–onto→𝐴)
85	63, 84	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋:𝐴–onto→𝐴)
86		foeq1 6726	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ↾ 𝐴) = 𝑋 → ((𝑋 ↾ 𝐴):𝐴–onto→𝐴 ↔ 𝑋:𝐴–onto→𝐴))
87	86	biimpar 477	. . . . . . . . . . . . 13 ⊢ (((𝑋 ↾ 𝐴) = 𝑋 ∧ 𝑋:𝐴–onto→𝐴) → (𝑋 ↾ 𝐴):𝐴–onto→𝐴)
88	83, 85, 87	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 ↾ 𝐴):𝐴–onto→𝐴)
89		f1oi 6796	. . . . . . . . . . . . . 14 ⊢ ( I ↾ 𝐸):𝐸–1-1-onto→𝐸
90		f1ofo 6765	. . . . . . . . . . . . . 14 ⊢ (( I ↾ 𝐸):𝐸–1-1-onto→𝐸 → ( I ↾ 𝐸):𝐸–onto→𝐸)
91	89, 90	mp1i 13	. . . . . . . . . . . . 13 ⊢ (𝜑 → ( I ↾ 𝐸):𝐸–onto→𝐸)
92		foeq1 6726	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ↾ 𝐸) = ( I ↾ 𝐸) → ((𝑋 ↾ 𝐸):𝐸–onto→𝐸 ↔ ( I ↾ 𝐸):𝐸–onto→𝐸))
93	92	biimpar 477	. . . . . . . . . . . . 13 ⊢ (((𝑋 ↾ 𝐸) = ( I ↾ 𝐸) ∧ ( I ↾ 𝐸):𝐸–onto→𝐸) → (𝑋 ↾ 𝐸):𝐸–onto→𝐸)
94	49, 91, 93	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 ↾ 𝐸):𝐸–onto→𝐸)
95		resdif 6779	. . . . . . . . . . . 12 ⊢ ((Fun ^◡𝑋 ∧ (𝑋 ↾ 𝐴):𝐴–onto→𝐴 ∧ (𝑋 ↾ 𝐸):𝐸–onto→𝐸) → (𝑋 ↾ (𝐴 ∖ 𝐸)):(𝐴 ∖ 𝐸)–1-1-onto→(𝐴 ∖ 𝐸))
96	80, 88, 94, 95	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋 ↾ (𝐴 ∖ 𝐸)):(𝐴 ∖ 𝐸)–1-1-onto→(𝐴 ∖ 𝐸))
97		ssun1 4123	. . . . . . . . . . . . . . 15 ⊢ 𝐸 ⊆ (𝐸 ∪ 𝐹)
98	97, 1	sseqtrid 3972	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸 ⊆ 𝐴)
99		uneqdifeq 4438	. . . . . . . . . . . . . . 15 ⊢ ((𝐸 ⊆ 𝐴 ∧ (𝐸 ∩ 𝐹) = ∅) → ((𝐸 ∪ 𝐹) = 𝐴 ↔ (𝐴 ∖ 𝐸) = 𝐹))
100	99	biimpa 476	. . . . . . . . . . . . . 14 ⊢ (((𝐸 ⊆ 𝐴 ∧ (𝐸 ∩ 𝐹) = ∅) ∧ (𝐸 ∪ 𝐹) = 𝐴) → (𝐴 ∖ 𝐸) = 𝐹)
101	98, 33, 1, 100	syl21anc 837	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 ∖ 𝐸) = 𝐹)
102	101	reseq2d 5923	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 ↾ (𝐴 ∖ 𝐸)) = (𝑋 ↾ 𝐹))
103	102, 101, 101	f1oeq123d 6752	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑋 ↾ (𝐴 ∖ 𝐸)):(𝐴 ∖ 𝐸)–1-1-onto→(𝐴 ∖ 𝐸) ↔ (𝑋 ↾ 𝐹):𝐹–1-1-onto→𝐹))
104	96, 103	mpbid 232	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 ↾ 𝐹):𝐹–1-1-onto→𝐹)
105		f1of 6758	. . . . . . . . . 10 ⊢ ((𝑋 ↾ 𝐹):𝐹–1-1-onto→𝐹 → (𝑋 ↾ 𝐹):𝐹⟶𝐹)
106	104, 105	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 ↾ 𝐹):𝐹⟶𝐹)
107	106	frnd 6654	. . . . . . . 8 ⊢ (𝜑 → ran (𝑋 ↾ 𝐹) ⊆ 𝐹)
108		cores 6191	. . . . . . . 8 ⊢ (ran (𝑋 ↾ 𝐹) ⊆ 𝐹 → ((𝑌 ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (𝑌 ∘ (𝑋 ↾ 𝐹)))
109	107, 108	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑌 ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (𝑌 ∘ (𝑋 ↾ 𝐹)))
110	77, 109	eqtr4id 2785	. . . . . 6 ⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ 𝐹) = ((𝑌 ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)))
111	21	coeq1d 5796	. . . . . 6 ⊢ (𝜑 → ((𝑌 ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (( I ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)))
112		fcoi2 6693	. . . . . . 7 ⊢ ((𝑋 ↾ 𝐹):𝐹⟶𝐹 → (( I ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (𝑋 ↾ 𝐹))
113	106, 112	syl 17	. . . . . 6 ⊢ (𝜑 → (( I ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (𝑋 ↾ 𝐹))
114	110, 111, 113	3eqtrd 2770	. . . . 5 ⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ 𝐹) = (𝑋 ↾ 𝐹))
115	76, 114	uneq12d 4114	. . . 4 ⊢ (𝜑 → (((𝑌 ∘ 𝑋) ↾ 𝐸) ∪ ((𝑌 ∘ 𝑋) ↾ 𝐹)) = ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)))
116	71, 115	eqtrid 2778	. . 3 ⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ (𝐸 ∪ 𝐹)) = ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)))
117		f1oco 6781	. . . . 5 ⊢ ((𝑌:𝐴–1-1-onto→𝐴 ∧ 𝑋:𝐴–1-1-onto→𝐴) → (𝑌 ∘ 𝑋):𝐴–1-1-onto→𝐴)
118	9, 63, 117	syl2anc 584	. . . 4 ⊢ (𝜑 → (𝑌 ∘ 𝑋):𝐴–1-1-onto→𝐴)
119		f1ofn 6759	. . . 4 ⊢ ((𝑌 ∘ 𝑋):𝐴–1-1-onto→𝐴 → (𝑌 ∘ 𝑋) Fn 𝐴)
120		fnresdm 6595	. . . 4 ⊢ ((𝑌 ∘ 𝑋) Fn 𝐴 → ((𝑌 ∘ 𝑋) ↾ 𝐴) = (𝑌 ∘ 𝑋))
121	118, 119, 120	3syl 18	. . 3 ⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ 𝐴) = (𝑌 ∘ 𝑋))
122	70, 116, 121	3eqtr3d 2774	. 2 ⊢ (𝜑 → ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)) = (𝑌 ∘ 𝑋))
123	69, 122	eqtr3d 2768	1 ⊢ (𝜑 → (𝑋 ∘ 𝑌) = (𝑌 ∘ 𝑋))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1541 ∈ wcel 2111 ∖ cdif 3894 ∪ cun 3895 ∩ cin 3896 ⊆ wss 3897 ∅c0 4278 I cid 5505 ^◡ccnv 5610 ran crn 5612 ↾ cres 5613 ∘ ccom 5615 Fun wfun 6470 Fn wfn 6471 ⟶wf 6472 –onto→wfo 6474 –1-1-onto→wf1o 6475 ‘cfv 6476 Basecbs 17115 SymGrpcsymg 19276

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-sep 5229 ax-nul 5239 ax-pow 5298 ax-pr 5365 ax-un 7663 ax-cnex 11057 ax-resscn 11058 ax-1cn 11059 ax-icn 11060 ax-addcl 11061 ax-addrcl 11062 ax-mulcl 11063 ax-mulrcl 11064 ax-mulcom 11065 ax-addass 11066 ax-mulass 11067 ax-distr 11068 ax-i2m1 11069 ax-1ne0 11070 ax-1rid 11071 ax-rnegex 11072 ax-rrecex 11073 ax-cnre 11074 ax-pre-lttri 11075 ax-pre-lttrn 11076 ax-pre-ltadd 11077 ax-pre-mulgt0 11078

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4279 df-if 4471 df-pw 4547 df-sn 4572 df-pr 4574 df-tp 4576 df-op 4578 df-uni 4855 df-iun 4938 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5506 df-eprel 5511 df-po 5519 df-so 5520 df-fr 5564 df-we 5566 df-xp 5617 df-rel 5618 df-cnv 5619 df-co 5620 df-dm 5621 df-rn 5622 df-res 5623 df-ima 5624 df-pred 6243 df-ord 6304 df-on 6305 df-lim 6306 df-suc 6307 df-iota 6432 df-fun 6478 df-fn 6479 df-f 6480 df-f1 6481 df-fo 6482 df-f1o 6483 df-fv 6484 df-riota 7298 df-ov 7344 df-oprab 7345 df-mpo 7346 df-om 7792 df-1st 7916 df-2nd 7917 df-frecs 8206 df-wrecs 8237 df-recs 8286 df-rdg 8324 df-1o 8380 df-er 8617 df-map 8747 df-en 8865 df-dom 8866 df-sdom 8867 df-fin 8868 df-pnf 11143 df-mnf 11144 df-xr 11145 df-ltxr 11146 df-le 11147 df-sub 11341 df-neg 11342 df-nn 12121 df-2 12183 df-3 12184 df-4 12185 df-5 12186 df-6 12187 df-7 12188 df-8 12189 df-9 12190 df-n0 12377 df-z 12464 df-uz 12728 df-fz 13403 df-struct 17053 df-sets 17070 df-slot 17088 df-ndx 17100 df-base 17116 df-ress 17137 df-plusg 17169 df-tset 17175 df-efmnd 18772 df-symg 19277

This theorem is referenced by: symgcom2 33045 cyc3conja 33118

W3C validator