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 5934	. . 3 ⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ (𝐸 ∪ 𝐹)) = ((𝑋 ∘ 𝑌) ↾ 𝐴))
3		resundi 5948	. . . 4 ⊢ ((𝑋 ∘ 𝑌) ↾ (𝐸 ∪ 𝐹)) = (((𝑋 ∘ 𝑌) ↾ 𝐸) ∪ ((𝑋 ∘ 𝑌) ↾ 𝐹))
4		resco 6203	. . . . . . 7 ⊢ ((𝑋 ∘ 𝑌) ↾ 𝐸) = (𝑋 ∘ (𝑌 ↾ 𝐸))
5		symgcom.y	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
6		symgcom.g	. . . . . . . . . . . . . . 15 ⊢ 𝐺 = (SymGrp‘𝐴)
7		symgcom.b	. . . . . . . . . . . . . . 15 ⊢ 𝐵 = (Base‘𝐺)
8	6, 7	symgbasf1o 19273	. . . . . . . . . . . . . 14 ⊢ (𝑌 ∈ 𝐵 → 𝑌:𝐴–1-1-onto→𝐴)
9	5, 8	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌:𝐴–1-1-onto→𝐴)
10		f1ocnv 6780	. . . . . . . . . . . . 13 ⊢ (𝑌:𝐴–1-1-onto→𝐴 → ^◡𝑌:𝐴–1-1-onto→𝐴)
11		f1ofun 6770	. . . . . . . . . . . . 13 ⊢ (^◡𝑌:𝐴–1-1-onto→𝐴 → Fun ^◡𝑌)
12	9, 10, 11	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → Fun ^◡𝑌)
13		f1ofn 6769	. . . . . . . . . . . . . 14 ⊢ (𝑌:𝐴–1-1-onto→𝐴 → 𝑌 Fn 𝐴)
14		fnresdm 6605	. . . . . . . . . . . . . 14 ⊢ (𝑌 Fn 𝐴 → (𝑌 ↾ 𝐴) = 𝑌)
15	9, 13, 14	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌 ↾ 𝐴) = 𝑌)
16		f1ofo 6775	. . . . . . . . . . . . . 14 ⊢ (𝑌:𝐴–1-1-onto→𝐴 → 𝑌:𝐴–onto→𝐴)
17	9, 16	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌:𝐴–onto→𝐴)
18		foeq1 6736	. . . . . . . . . . . . . 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 6806	. . . . . . . . . . . . . 14 ⊢ ( I ↾ 𝐹):𝐹–1-1-onto→𝐹
23		f1ofo 6775	. . . . . . . . . . . . . 14 ⊢ (( I ↾ 𝐹):𝐹–1-1-onto→𝐹 → ( I ↾ 𝐹):𝐹–onto→𝐹)
24	22, 23	mp1i 13	. . . . . . . . . . . . 13 ⊢ (𝜑 → ( I ↾ 𝐹):𝐹–onto→𝐹)
25		foeq1 6736	. . . . . . . . . . . . . 14 ⊢ ((𝑌 ↾ 𝐹) = ( I ↾ 𝐹) → ((𝑌 ↾ 𝐹):𝐹–onto→𝐹 ↔ ( I ↾ 𝐹):𝐹–onto→𝐹))
26	25	biimpar 477	. . . . . . . . . . . . 13 ⊢ (((𝑌 ↾ 𝐹) = ( I ↾ 𝐹) ∧ ( I ↾ 𝐹):𝐹–onto→𝐹) → (𝑌 ↾ 𝐹):𝐹–onto→𝐹)
27	21, 24, 26	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌 ↾ 𝐹):𝐹–onto→𝐹)
28		resdif 6789	. . . . . . . . . . . 12 ⊢ ((Fun ^◡𝑌 ∧ (𝑌 ↾ 𝐴):𝐴–onto→𝐴 ∧ (𝑌 ↾ 𝐹):𝐹–onto→𝐹) → (𝑌 ↾ (𝐴 ∖ 𝐹)):(𝐴 ∖ 𝐹)–1-1-onto→(𝐴 ∖ 𝐹))
29	12, 20, 27, 28	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 ↾ (𝐴 ∖ 𝐹)):(𝐴 ∖ 𝐹)–1-1-onto→(𝐴 ∖ 𝐹))
30		ssun2 4132	. . . . . . . . . . . . . . 15 ⊢ 𝐹 ⊆ (𝐸 ∪ 𝐹)
31	30, 1	sseqtrid 3980	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 ⊆ 𝐴)
32		incom 4162	. . . . . . . . . . . . . . 15 ⊢ (𝐸 ∩ 𝐹) = (𝐹 ∩ 𝐸)
33		symgcom.3	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐸 ∩ 𝐹) = ∅)
34	32, 33	eqtr3id 2778	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹 ∩ 𝐸) = ∅)
35		uncom 4111	. . . . . . . . . . . . . . 15 ⊢ (𝐸 ∪ 𝐹) = (𝐹 ∪ 𝐸)
36	35, 1	eqtr3id 2778	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹 ∪ 𝐸) = 𝐴)
37		uneqdifeq 4446	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ⊆ 𝐴 ∧ (𝐹 ∩ 𝐸) = ∅) → ((𝐹 ∪ 𝐸) = 𝐴 ↔ (𝐴 ∖ 𝐹) = 𝐸))
38	37	biimpa 476	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ⊆ 𝐴 ∧ (𝐹 ∩ 𝐸) = ∅) ∧ (𝐹 ∪ 𝐸) = 𝐴) → (𝐴 ∖ 𝐹) = 𝐸)
39	31, 34, 36, 38	syl21anc 837	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 ∖ 𝐹) = 𝐸)
40	39	reseq2d 5934	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌 ↾ (𝐴 ∖ 𝐹)) = (𝑌 ↾ 𝐸))
41	40, 39, 39	f1oeq123d 6762	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑌 ↾ (𝐴 ∖ 𝐹)):(𝐴 ∖ 𝐹)–1-1-onto→(𝐴 ∖ 𝐹) ↔ (𝑌 ↾ 𝐸):𝐸–1-1-onto→𝐸))
42	29, 41	mpbid 232	. . . . . . . . . 10 ⊢ (𝜑 → (𝑌 ↾ 𝐸):𝐸–1-1-onto→𝐸)
43		f1of 6768	. . . . . . . . . 10 ⊢ ((𝑌 ↾ 𝐸):𝐸–1-1-onto→𝐸 → (𝑌 ↾ 𝐸):𝐸⟶𝐸)
44	42, 43	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑌 ↾ 𝐸):𝐸⟶𝐸)
45	44	frnd 6664	. . . . . . . 8 ⊢ (𝜑 → ran (𝑌 ↾ 𝐸) ⊆ 𝐸)
46		cores 6202	. . . . . . . 8 ⊢ (ran (𝑌 ↾ 𝐸) ⊆ 𝐸 → ((𝑋 ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (𝑋 ∘ (𝑌 ↾ 𝐸)))
47	45, 46	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑋 ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (𝑋 ∘ (𝑌 ↾ 𝐸)))
48	4, 47	eqtr4id 2783	. . . . . 6 ⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ 𝐸) = ((𝑋 ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)))
49		symgcom.1	. . . . . . 7 ⊢ (𝜑 → (𝑋 ↾ 𝐸) = ( I ↾ 𝐸))
50	49	coeq1d 5808	. . . . . 6 ⊢ (𝜑 → ((𝑋 ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (( I ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)))
51		fcoi2 6703	. . . . . . 7 ⊢ ((𝑌 ↾ 𝐸):𝐸⟶𝐸 → (( I ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (𝑌 ↾ 𝐸))
52	44, 51	syl 17	. . . . . 6 ⊢ (𝜑 → (( I ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (𝑌 ↾ 𝐸))
53	48, 50, 52	3eqtrd 2768	. . . . 5 ⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ 𝐸) = (𝑌 ↾ 𝐸))
54		resco 6203	. . . . . 6 ⊢ ((𝑋 ∘ 𝑌) ↾ 𝐹) = (𝑋 ∘ (𝑌 ↾ 𝐹))
55	21	coeq2d 5809	. . . . . . 7 ⊢ (𝜑 → (𝑋 ∘ (𝑌 ↾ 𝐹)) = (𝑋 ∘ ( I ↾ 𝐹)))
56		coires1 6217	. . . . . . 7 ⊢ (𝑋 ∘ ( I ↾ 𝐹)) = (𝑋 ↾ 𝐹)
57	55, 56	eqtrdi 2780	. . . . . 6 ⊢ (𝜑 → (𝑋 ∘ (𝑌 ↾ 𝐹)) = (𝑋 ↾ 𝐹))
58	54, 57	eqtrid 2776	. . . . 5 ⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ 𝐹) = (𝑋 ↾ 𝐹))
59	53, 58	uneq12d 4122	. . . 4 ⊢ (𝜑 → (((𝑋 ∘ 𝑌) ↾ 𝐸) ∪ ((𝑋 ∘ 𝑌) ↾ 𝐹)) = ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)))
60	3, 59	eqtrid 2776	. . 3 ⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ (𝐸 ∪ 𝐹)) = ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)))
61		symgcom.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
62	6, 7	symgbasf1o 19273	. . . . . 6 ⊢ (𝑋 ∈ 𝐵 → 𝑋:𝐴–1-1-onto→𝐴)
63	61, 62	syl 17	. . . . 5 ⊢ (𝜑 → 𝑋:𝐴–1-1-onto→𝐴)
64		f1oco 6791	. . . . 5 ⊢ ((𝑋:𝐴–1-1-onto→𝐴 ∧ 𝑌:𝐴–1-1-onto→𝐴) → (𝑋 ∘ 𝑌):𝐴–1-1-onto→𝐴)
65	63, 9, 64	syl2anc 584	. . . 4 ⊢ (𝜑 → (𝑋 ∘ 𝑌):𝐴–1-1-onto→𝐴)
66		f1ofn 6769	. . . 4 ⊢ ((𝑋 ∘ 𝑌):𝐴–1-1-onto→𝐴 → (𝑋 ∘ 𝑌) Fn 𝐴)
67		fnresdm 6605	. . . 4 ⊢ ((𝑋 ∘ 𝑌) Fn 𝐴 → ((𝑋 ∘ 𝑌) ↾ 𝐴) = (𝑋 ∘ 𝑌))
68	65, 66, 67	3syl 18	. . 3 ⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ 𝐴) = (𝑋 ∘ 𝑌))
69	2, 60, 68	3eqtr3d 2772	. 2 ⊢ (𝜑 → ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)) = (𝑋 ∘ 𝑌))
70	1	reseq2d 5934	. . 3 ⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ (𝐸 ∪ 𝐹)) = ((𝑌 ∘ 𝑋) ↾ 𝐴))
71		resundi 5948	. . . 4 ⊢ ((𝑌 ∘ 𝑋) ↾ (𝐸 ∪ 𝐹)) = (((𝑌 ∘ 𝑋) ↾ 𝐸) ∪ ((𝑌 ∘ 𝑋) ↾ 𝐹))
72		resco 6203	. . . . . 6 ⊢ ((𝑌 ∘ 𝑋) ↾ 𝐸) = (𝑌 ∘ (𝑋 ↾ 𝐸))
73	49	coeq2d 5809	. . . . . . 7 ⊢ (𝜑 → (𝑌 ∘ (𝑋 ↾ 𝐸)) = (𝑌 ∘ ( I ↾ 𝐸)))
74		coires1 6217	. . . . . . 7 ⊢ (𝑌 ∘ ( I ↾ 𝐸)) = (𝑌 ↾ 𝐸)
75	73, 74	eqtrdi 2780	. . . . . 6 ⊢ (𝜑 → (𝑌 ∘ (𝑋 ↾ 𝐸)) = (𝑌 ↾ 𝐸))
76	72, 75	eqtrid 2776	. . . . 5 ⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ 𝐸) = (𝑌 ↾ 𝐸))
77		resco 6203	. . . . . . 7 ⊢ ((𝑌 ∘ 𝑋) ↾ 𝐹) = (𝑌 ∘ (𝑋 ↾ 𝐹))
78		f1ocnv 6780	. . . . . . . . . . . . 13 ⊢ (𝑋:𝐴–1-1-onto→𝐴 → ^◡𝑋:𝐴–1-1-onto→𝐴)
79		f1ofun 6770	. . . . . . . . . . . . 13 ⊢ (^◡𝑋:𝐴–1-1-onto→𝐴 → Fun ^◡𝑋)
80	63, 78, 79	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → Fun ^◡𝑋)
81		f1ofn 6769	. . . . . . . . . . . . . 14 ⊢ (𝑋:𝐴–1-1-onto→𝐴 → 𝑋 Fn 𝐴)
82		fnresdm 6605	. . . . . . . . . . . . . 14 ⊢ (𝑋 Fn 𝐴 → (𝑋 ↾ 𝐴) = 𝑋)
83	63, 81, 82	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 ↾ 𝐴) = 𝑋)
84		f1ofo 6775	. . . . . . . . . . . . . 14 ⊢ (𝑋:𝐴–1-1-onto→𝐴 → 𝑋:𝐴–onto→𝐴)
85	63, 84	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋:𝐴–onto→𝐴)
86		foeq1 6736	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ↾ 𝐴) = 𝑋 → ((𝑋 ↾ 𝐴):𝐴–onto→𝐴 ↔ 𝑋:𝐴–onto→𝐴))
87	86	biimpar 477	. . . . . . . . . . . . 13 ⊢ (((𝑋 ↾ 𝐴) = 𝑋 ∧ 𝑋:𝐴–onto→𝐴) → (𝑋 ↾ 𝐴):𝐴–onto→𝐴)
88	83, 85, 87	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 ↾ 𝐴):𝐴–onto→𝐴)
89		f1oi 6806	. . . . . . . . . . . . . 14 ⊢ ( I ↾ 𝐸):𝐸–1-1-onto→𝐸
90		f1ofo 6775	. . . . . . . . . . . . . 14 ⊢ (( I ↾ 𝐸):𝐸–1-1-onto→𝐸 → ( I ↾ 𝐸):𝐸–onto→𝐸)
91	89, 90	mp1i 13	. . . . . . . . . . . . 13 ⊢ (𝜑 → ( I ↾ 𝐸):𝐸–onto→𝐸)
92		foeq1 6736	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ↾ 𝐸) = ( I ↾ 𝐸) → ((𝑋 ↾ 𝐸):𝐸–onto→𝐸 ↔ ( I ↾ 𝐸):𝐸–onto→𝐸))
93	92	biimpar 477	. . . . . . . . . . . . 13 ⊢ (((𝑋 ↾ 𝐸) = ( I ↾ 𝐸) ∧ ( I ↾ 𝐸):𝐸–onto→𝐸) → (𝑋 ↾ 𝐸):𝐸–onto→𝐸)
94	49, 91, 93	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 ↾ 𝐸):𝐸–onto→𝐸)
95		resdif 6789	. . . . . . . . . . . 12 ⊢ ((Fun ^◡𝑋 ∧ (𝑋 ↾ 𝐴):𝐴–onto→𝐴 ∧ (𝑋 ↾ 𝐸):𝐸–onto→𝐸) → (𝑋 ↾ (𝐴 ∖ 𝐸)):(𝐴 ∖ 𝐸)–1-1-onto→(𝐴 ∖ 𝐸))
96	80, 88, 94, 95	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋 ↾ (𝐴 ∖ 𝐸)):(𝐴 ∖ 𝐸)–1-1-onto→(𝐴 ∖ 𝐸))
97		ssun1 4131	. . . . . . . . . . . . . . 15 ⊢ 𝐸 ⊆ (𝐸 ∪ 𝐹)
98	97, 1	sseqtrid 3980	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸 ⊆ 𝐴)
99		uneqdifeq 4446	. . . . . . . . . . . . . . 15 ⊢ ((𝐸 ⊆ 𝐴 ∧ (𝐸 ∩ 𝐹) = ∅) → ((𝐸 ∪ 𝐹) = 𝐴 ↔ (𝐴 ∖ 𝐸) = 𝐹))
100	99	biimpa 476	. . . . . . . . . . . . . 14 ⊢ (((𝐸 ⊆ 𝐴 ∧ (𝐸 ∩ 𝐹) = ∅) ∧ (𝐸 ∪ 𝐹) = 𝐴) → (𝐴 ∖ 𝐸) = 𝐹)
101	98, 33, 1, 100	syl21anc 837	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 ∖ 𝐸) = 𝐹)
102	101	reseq2d 5934	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 ↾ (𝐴 ∖ 𝐸)) = (𝑋 ↾ 𝐹))
103	102, 101, 101	f1oeq123d 6762	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑋 ↾ (𝐴 ∖ 𝐸)):(𝐴 ∖ 𝐸)–1-1-onto→(𝐴 ∖ 𝐸) ↔ (𝑋 ↾ 𝐹):𝐹–1-1-onto→𝐹))
104	96, 103	mpbid 232	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 ↾ 𝐹):𝐹–1-1-onto→𝐹)
105		f1of 6768	. . . . . . . . . 10 ⊢ ((𝑋 ↾ 𝐹):𝐹–1-1-onto→𝐹 → (𝑋 ↾ 𝐹):𝐹⟶𝐹)
106	104, 105	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 ↾ 𝐹):𝐹⟶𝐹)
107	106	frnd 6664	. . . . . . . 8 ⊢ (𝜑 → ran (𝑋 ↾ 𝐹) ⊆ 𝐹)
108		cores 6202	. . . . . . . 8 ⊢ (ran (𝑋 ↾ 𝐹) ⊆ 𝐹 → ((𝑌 ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (𝑌 ∘ (𝑋 ↾ 𝐹)))
109	107, 108	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑌 ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (𝑌 ∘ (𝑋 ↾ 𝐹)))
110	77, 109	eqtr4id 2783	. . . . . 6 ⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ 𝐹) = ((𝑌 ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)))
111	21	coeq1d 5808	. . . . . 6 ⊢ (𝜑 → ((𝑌 ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (( I ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)))
112		fcoi2 6703	. . . . . . 7 ⊢ ((𝑋 ↾ 𝐹):𝐹⟶𝐹 → (( I ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (𝑋 ↾ 𝐹))
113	106, 112	syl 17	. . . . . 6 ⊢ (𝜑 → (( I ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (𝑋 ↾ 𝐹))
114	110, 111, 113	3eqtrd 2768	. . . . 5 ⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ 𝐹) = (𝑋 ↾ 𝐹))
115	76, 114	uneq12d 4122	. . . 4 ⊢ (𝜑 → (((𝑌 ∘ 𝑋) ↾ 𝐸) ∪ ((𝑌 ∘ 𝑋) ↾ 𝐹)) = ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)))
116	71, 115	eqtrid 2776	. . 3 ⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ (𝐸 ∪ 𝐹)) = ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)))
117		f1oco 6791	. . . . 5 ⊢ ((𝑌:𝐴–1-1-onto→𝐴 ∧ 𝑋:𝐴–1-1-onto→𝐴) → (𝑌 ∘ 𝑋):𝐴–1-1-onto→𝐴)
118	9, 63, 117	syl2anc 584	. . . 4 ⊢ (𝜑 → (𝑌 ∘ 𝑋):𝐴–1-1-onto→𝐴)
119		f1ofn 6769	. . . 4 ⊢ ((𝑌 ∘ 𝑋):𝐴–1-1-onto→𝐴 → (𝑌 ∘ 𝑋) Fn 𝐴)
120		fnresdm 6605	. . . 4 ⊢ ((𝑌 ∘ 𝑋) Fn 𝐴 → ((𝑌 ∘ 𝑋) ↾ 𝐴) = (𝑌 ∘ 𝑋))
121	118, 119, 120	3syl 18	. . 3 ⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ 𝐴) = (𝑌 ∘ 𝑋))
122	70, 116, 121	3eqtr3d 2772	. 2 ⊢ (𝜑 → ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)) = (𝑌 ∘ 𝑋))
123	69, 122	eqtr3d 2766	1 ⊢ (𝜑 → (𝑋 ∘ 𝑌) = (𝑌 ∘ 𝑋))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ∖ cdif 3902 ∪ cun 3903 ∩ cin 3904 ⊆ wss 3905 ∅c0 4286 I cid 5517 ^◡ccnv 5622 ran crn 5624 ↾ cres 5625 ∘ ccom 5627 Fun wfun 6480 Fn wfn 6481 ⟶wf 6482 –onto→wfo 6484 –1-1-onto→wf1o 6485 ‘cfv 6486 Basecbs 17139 SymGrpcsymg 19267

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 2701 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105

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 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-reu 3346 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-tp 4584 df-op 4586 df-uni 4862 df-iun 4946 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-riota 7310 df-ov 7356 df-oprab 7357 df-mpo 7358 df-om 7807 df-1st 7931 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-er 8632 df-map 8762 df-en 8880 df-dom 8881 df-sdom 8882 df-fin 8883 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11368 df-neg 11369 df-nn 12148 df-2 12210 df-3 12211 df-4 12212 df-5 12213 df-6 12214 df-7 12215 df-8 12216 df-9 12217 df-n0 12404 df-z 12491 df-uz 12755 df-fz 13430 df-struct 17077 df-sets 17094 df-slot 17112 df-ndx 17124 df-base 17140 df-ress 17161 df-plusg 17193 df-tset 17199 df-efmnd 18762 df-symg 19268

This theorem is referenced by: symgcom2 33045 cyc3conja 33118

W3C validator