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 33224

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 5961	. . 3 ⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ (𝐸 ∪ 𝐹)) = ((𝑋 ∘ 𝑌) ↾ 𝐴))
3		resundi 5975	. . . 4 ⊢ ((𝑋 ∘ 𝑌) ↾ (𝐸 ∪ 𝐹)) = (((𝑋 ∘ 𝑌) ↾ 𝐸) ∪ ((𝑋 ∘ 𝑌) ↾ 𝐹))
4		resco 6232	. . . . . . 7 ⊢ ((𝑋 ∘ 𝑌) ↾ 𝐸) = (𝑋 ∘ (𝑌 ↾ 𝐸))
5		symgcom.y	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
6		symgcom.g	. . . . . . . . . . . . . . 15 ⊢ 𝐺 = (SymGrp‘𝐴)
7		symgcom.b	. . . . . . . . . . . . . . 15 ⊢ 𝐵 = (Base‘𝐺)
8	6, 7	symgbasf1o 19406	. . . . . . . . . . . . . 14 ⊢ (𝑌 ∈ 𝐵 → 𝑌:𝐴–1-1-onto→𝐴)
9	5, 8	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌:𝐴–1-1-onto→𝐴)
10		f1ocnv 6814	. . . . . . . . . . . . 13 ⊢ (𝑌:𝐴–1-1-onto→𝐴 → ^◡𝑌:𝐴–1-1-onto→𝐴)
11		f1ofun 6803	. . . . . . . . . . . . 13 ⊢ (^◡𝑌:𝐴–1-1-onto→𝐴 → Fun ^◡𝑌)
12	9, 10, 11	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → Fun ^◡𝑌)
13		f1ofn 6802	. . . . . . . . . . . . . 14 ⊢ (𝑌:𝐴–1-1-onto→𝐴 → 𝑌 Fn 𝐴)
14		fnresdm 6635	. . . . . . . . . . . . . 14 ⊢ (𝑌 Fn 𝐴 → (𝑌 ↾ 𝐴) = 𝑌)
15	9, 13, 14	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌 ↾ 𝐴) = 𝑌)
16		f1ofo 6809	. . . . . . . . . . . . . 14 ⊢ (𝑌:𝐴–1-1-onto→𝐴 → 𝑌:𝐴–onto→𝐴)
17	9, 16	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌:𝐴–onto→𝐴)
18		foeq1 6769	. . . . . . . . . . . . . 14 ⊢ ((𝑌 ↾ 𝐴) = 𝑌 → ((𝑌 ↾ 𝐴):𝐴–onto→𝐴 ↔ 𝑌:𝐴–onto→𝐴))
19	18	biimpar 481	. . . . . . . . . . . . 13 ⊢ (((𝑌 ↾ 𝐴) = 𝑌 ∧ 𝑌:𝐴–onto→𝐴) → (𝑌 ↾ 𝐴):𝐴–onto→𝐴)
20	15, 17, 19	syl2anc 593	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌 ↾ 𝐴):𝐴–onto→𝐴)
21		symgcom.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌 ↾ 𝐹) = ( I ↾ 𝐹))
22		f1oi 6840	. . . . . . . . . . . . . 14 ⊢ ( I ↾ 𝐹):𝐹–1-1-onto→𝐹
23		f1ofo 6809	. . . . . . . . . . . . . 14 ⊢ (( I ↾ 𝐹):𝐹–1-1-onto→𝐹 → ( I ↾ 𝐹):𝐹–onto→𝐹)
24	22, 23	mp1i 13	. . . . . . . . . . . . 13 ⊢ (𝜑 → ( I ↾ 𝐹):𝐹–onto→𝐹)
25		foeq1 6769	. . . . . . . . . . . . . 14 ⊢ ((𝑌 ↾ 𝐹) = ( I ↾ 𝐹) → ((𝑌 ↾ 𝐹):𝐹–onto→𝐹 ↔ ( I ↾ 𝐹):𝐹–onto→𝐹))
26	25	biimpar 481	. . . . . . . . . . . . 13 ⊢ (((𝑌 ↾ 𝐹) = ( I ↾ 𝐹) ∧ ( I ↾ 𝐹):𝐹–onto→𝐹) → (𝑌 ↾ 𝐹):𝐹–onto→𝐹)
27	21, 24, 26	syl2anc 593	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌 ↾ 𝐹):𝐹–onto→𝐹)
28		resdif 6823	. . . . . . . . . . . 12 ⊢ ((Fun ^◡𝑌 ∧ (𝑌 ↾ 𝐴):𝐴–onto→𝐴 ∧ (𝑌 ↾ 𝐹):𝐹–onto→𝐹) → (𝑌 ↾ (𝐴 ∖ 𝐹)):(𝐴 ∖ 𝐹)–1-1-onto→(𝐴 ∖ 𝐹))
29	12, 20, 27, 28	syl3anc 1389	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 ↾ (𝐴 ∖ 𝐹)):(𝐴 ∖ 𝐹)–1-1-onto→(𝐴 ∖ 𝐹))
30		ssun2 4129	. . . . . . . . . . . . . . 15 ⊢ 𝐹 ⊆ (𝐸 ∪ 𝐹)
31	30, 1	sseqtrid 3976	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 ⊆ 𝐴)
32		incom 4159	. . . . . . . . . . . . . . 15 ⊢ (𝐸 ∩ 𝐹) = (𝐹 ∩ 𝐸)
33		symgcom.3	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐸 ∩ 𝐹) = ∅)
34	32, 33	eqtr3id 2810	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹 ∩ 𝐸) = ∅)
35		uncom 4109	. . . . . . . . . . . . . . 15 ⊢ (𝐸 ∪ 𝐹) = (𝐹 ∪ 𝐸)
36	35, 1	eqtr3id 2810	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹 ∪ 𝐸) = 𝐴)
37		uneqdifeq 4443	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ⊆ 𝐴 ∧ (𝐹 ∩ 𝐸) = ∅) → ((𝐹 ∪ 𝐸) = 𝐴 ↔ (𝐴 ∖ 𝐹) = 𝐸))
38	37	biimpa 480	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ⊆ 𝐴 ∧ (𝐹 ∩ 𝐸) = ∅) ∧ (𝐹 ∪ 𝐸) = 𝐴) → (𝐴 ∖ 𝐹) = 𝐸)
39	31, 34, 36, 38	syl21anc 848	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 ∖ 𝐹) = 𝐸)
40	39	reseq2d 5961	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌 ↾ (𝐴 ∖ 𝐹)) = (𝑌 ↾ 𝐸))
41	40, 39, 39	f1oeq123d 6795	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑌 ↾ (𝐴 ∖ 𝐹)):(𝐴 ∖ 𝐹)–1-1-onto→(𝐴 ∖ 𝐹) ↔ (𝑌 ↾ 𝐸):𝐸–1-1-onto→𝐸))
42	29, 41	mpbid 234	. . . . . . . . . 10 ⊢ (𝜑 → (𝑌 ↾ 𝐸):𝐸–1-1-onto→𝐸)
43		f1of 6801	. . . . . . . . . 10 ⊢ ((𝑌 ↾ 𝐸):𝐸–1-1-onto→𝐸 → (𝑌 ↾ 𝐸):𝐸⟶𝐸)
44	42, 43	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑌 ↾ 𝐸):𝐸⟶𝐸)
45	44	frnd 6695	. . . . . . . 8 ⊢ (𝜑 → ran (𝑌 ↾ 𝐸) ⊆ 𝐸)
46		cores 6231	. . . . . . . 8 ⊢ (ran (𝑌 ↾ 𝐸) ⊆ 𝐸 → ((𝑋 ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (𝑋 ∘ (𝑌 ↾ 𝐸)))
47	45, 46	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑋 ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (𝑋 ∘ (𝑌 ↾ 𝐸)))
48	4, 47	eqtr4id 2815	. . . . . 6 ⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ 𝐸) = ((𝑋 ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)))
49		symgcom.1	. . . . . . 7 ⊢ (𝜑 → (𝑋 ↾ 𝐸) = ( I ↾ 𝐸))
50	49	coeq1d 5829	. . . . . 6 ⊢ (𝜑 → ((𝑋 ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (( I ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)))
51		fcoi2 6734	. . . . . . 7 ⊢ ((𝑌 ↾ 𝐸):𝐸⟶𝐸 → (( I ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (𝑌 ↾ 𝐸))
52	44, 51	syl 17	. . . . . 6 ⊢ (𝜑 → (( I ↾ 𝐸) ∘ (𝑌 ↾ 𝐸)) = (𝑌 ↾ 𝐸))
53	48, 50, 52	3eqtrd 2800	. . . . 5 ⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ 𝐸) = (𝑌 ↾ 𝐸))
54		resco 6232	. . . . . 6 ⊢ ((𝑋 ∘ 𝑌) ↾ 𝐹) = (𝑋 ∘ (𝑌 ↾ 𝐹))
55	21	coeq2d 5830	. . . . . . 7 ⊢ (𝜑 → (𝑋 ∘ (𝑌 ↾ 𝐹)) = (𝑋 ∘ ( I ↾ 𝐹)))
56		coires1 6247	. . . . . . 7 ⊢ (𝑋 ∘ ( I ↾ 𝐹)) = (𝑋 ↾ 𝐹)
57	55, 56	eqtrdi 2812	. . . . . 6 ⊢ (𝜑 → (𝑋 ∘ (𝑌 ↾ 𝐹)) = (𝑋 ↾ 𝐹))
58	54, 57	eqtrid 2808	. . . . 5 ⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ 𝐹) = (𝑋 ↾ 𝐹))
59	53, 58	uneq12d 4120	. . . 4 ⊢ (𝜑 → (((𝑋 ∘ 𝑌) ↾ 𝐸) ∪ ((𝑋 ∘ 𝑌) ↾ 𝐹)) = ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)))
60	3, 59	eqtrid 2808	. . 3 ⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ (𝐸 ∪ 𝐹)) = ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)))
61		symgcom.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
62	6, 7	symgbasf1o 19406	. . . . . 6 ⊢ (𝑋 ∈ 𝐵 → 𝑋:𝐴–1-1-onto→𝐴)
63	61, 62	syl 17	. . . . 5 ⊢ (𝜑 → 𝑋:𝐴–1-1-onto→𝐴)
64		f1oco 6825	. . . . 5 ⊢ ((𝑋:𝐴–1-1-onto→𝐴 ∧ 𝑌:𝐴–1-1-onto→𝐴) → (𝑋 ∘ 𝑌):𝐴–1-1-onto→𝐴)
65	63, 9, 64	syl2anc 593	. . . 4 ⊢ (𝜑 → (𝑋 ∘ 𝑌):𝐴–1-1-onto→𝐴)
66		f1ofn 6802	. . . 4 ⊢ ((𝑋 ∘ 𝑌):𝐴–1-1-onto→𝐴 → (𝑋 ∘ 𝑌) Fn 𝐴)
67		fnresdm 6635	. . . 4 ⊢ ((𝑋 ∘ 𝑌) Fn 𝐴 → ((𝑋 ∘ 𝑌) ↾ 𝐴) = (𝑋 ∘ 𝑌))
68	65, 66, 67	3syl 18	. . 3 ⊢ (𝜑 → ((𝑋 ∘ 𝑌) ↾ 𝐴) = (𝑋 ∘ 𝑌))
69	2, 60, 68	3eqtr3d 2804	. 2 ⊢ (𝜑 → ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)) = (𝑋 ∘ 𝑌))
70	1	reseq2d 5961	. . 3 ⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ (𝐸 ∪ 𝐹)) = ((𝑌 ∘ 𝑋) ↾ 𝐴))
71		resundi 5975	. . . 4 ⊢ ((𝑌 ∘ 𝑋) ↾ (𝐸 ∪ 𝐹)) = (((𝑌 ∘ 𝑋) ↾ 𝐸) ∪ ((𝑌 ∘ 𝑋) ↾ 𝐹))
72		resco 6232	. . . . . 6 ⊢ ((𝑌 ∘ 𝑋) ↾ 𝐸) = (𝑌 ∘ (𝑋 ↾ 𝐸))
73	49	coeq2d 5830	. . . . . . 7 ⊢ (𝜑 → (𝑌 ∘ (𝑋 ↾ 𝐸)) = (𝑌 ∘ ( I ↾ 𝐸)))
74		coires1 6247	. . . . . . 7 ⊢ (𝑌 ∘ ( I ↾ 𝐸)) = (𝑌 ↾ 𝐸)
75	73, 74	eqtrdi 2812	. . . . . 6 ⊢ (𝜑 → (𝑌 ∘ (𝑋 ↾ 𝐸)) = (𝑌 ↾ 𝐸))
76	72, 75	eqtrid 2808	. . . . 5 ⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ 𝐸) = (𝑌 ↾ 𝐸))
77		resco 6232	. . . . . . 7 ⊢ ((𝑌 ∘ 𝑋) ↾ 𝐹) = (𝑌 ∘ (𝑋 ↾ 𝐹))
78		f1ocnv 6814	. . . . . . . . . . . . 13 ⊢ (𝑋:𝐴–1-1-onto→𝐴 → ^◡𝑋:𝐴–1-1-onto→𝐴)
79		f1ofun 6803	. . . . . . . . . . . . 13 ⊢ (^◡𝑋:𝐴–1-1-onto→𝐴 → Fun ^◡𝑋)
80	63, 78, 79	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → Fun ^◡𝑋)
81		f1ofn 6802	. . . . . . . . . . . . . 14 ⊢ (𝑋:𝐴–1-1-onto→𝐴 → 𝑋 Fn 𝐴)
82		fnresdm 6635	. . . . . . . . . . . . . 14 ⊢ (𝑋 Fn 𝐴 → (𝑋 ↾ 𝐴) = 𝑋)
83	63, 81, 82	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 ↾ 𝐴) = 𝑋)
84		f1ofo 6809	. . . . . . . . . . . . . 14 ⊢ (𝑋:𝐴–1-1-onto→𝐴 → 𝑋:𝐴–onto→𝐴)
85	63, 84	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋:𝐴–onto→𝐴)
86		foeq1 6769	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ↾ 𝐴) = 𝑋 → ((𝑋 ↾ 𝐴):𝐴–onto→𝐴 ↔ 𝑋:𝐴–onto→𝐴))
87	86	biimpar 481	. . . . . . . . . . . . 13 ⊢ (((𝑋 ↾ 𝐴) = 𝑋 ∧ 𝑋:𝐴–onto→𝐴) → (𝑋 ↾ 𝐴):𝐴–onto→𝐴)
88	83, 85, 87	syl2anc 593	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 ↾ 𝐴):𝐴–onto→𝐴)
89		f1oi 6840	. . . . . . . . . . . . . 14 ⊢ ( I ↾ 𝐸):𝐸–1-1-onto→𝐸
90		f1ofo 6809	. . . . . . . . . . . . . 14 ⊢ (( I ↾ 𝐸):𝐸–1-1-onto→𝐸 → ( I ↾ 𝐸):𝐸–onto→𝐸)
91	89, 90	mp1i 13	. . . . . . . . . . . . 13 ⊢ (𝜑 → ( I ↾ 𝐸):𝐸–onto→𝐸)
92		foeq1 6769	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ↾ 𝐸) = ( I ↾ 𝐸) → ((𝑋 ↾ 𝐸):𝐸–onto→𝐸 ↔ ( I ↾ 𝐸):𝐸–onto→𝐸))
93	92	biimpar 481	. . . . . . . . . . . . 13 ⊢ (((𝑋 ↾ 𝐸) = ( I ↾ 𝐸) ∧ ( I ↾ 𝐸):𝐸–onto→𝐸) → (𝑋 ↾ 𝐸):𝐸–onto→𝐸)
94	49, 91, 93	syl2anc 593	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 ↾ 𝐸):𝐸–onto→𝐸)
95		resdif 6823	. . . . . . . . . . . 12 ⊢ ((Fun ^◡𝑋 ∧ (𝑋 ↾ 𝐴):𝐴–onto→𝐴 ∧ (𝑋 ↾ 𝐸):𝐸–onto→𝐸) → (𝑋 ↾ (𝐴 ∖ 𝐸)):(𝐴 ∖ 𝐸)–1-1-onto→(𝐴 ∖ 𝐸))
96	80, 88, 94, 95	syl3anc 1389	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋 ↾ (𝐴 ∖ 𝐸)):(𝐴 ∖ 𝐸)–1-1-onto→(𝐴 ∖ 𝐸))
97		ssun1 4128	. . . . . . . . . . . . . . 15 ⊢ 𝐸 ⊆ (𝐸 ∪ 𝐹)
98	97, 1	sseqtrid 3976	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸 ⊆ 𝐴)
99		uneqdifeq 4443	. . . . . . . . . . . . . . 15 ⊢ ((𝐸 ⊆ 𝐴 ∧ (𝐸 ∩ 𝐹) = ∅) → ((𝐸 ∪ 𝐹) = 𝐴 ↔ (𝐴 ∖ 𝐸) = 𝐹))
100	99	biimpa 480	. . . . . . . . . . . . . 14 ⊢ (((𝐸 ⊆ 𝐴 ∧ (𝐸 ∩ 𝐹) = ∅) ∧ (𝐸 ∪ 𝐹) = 𝐴) → (𝐴 ∖ 𝐸) = 𝐹)
101	98, 33, 1, 100	syl21anc 848	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 ∖ 𝐸) = 𝐹)
102	101	reseq2d 5961	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 ↾ (𝐴 ∖ 𝐸)) = (𝑋 ↾ 𝐹))
103	102, 101, 101	f1oeq123d 6795	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑋 ↾ (𝐴 ∖ 𝐸)):(𝐴 ∖ 𝐸)–1-1-onto→(𝐴 ∖ 𝐸) ↔ (𝑋 ↾ 𝐹):𝐹–1-1-onto→𝐹))
104	96, 103	mpbid 234	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 ↾ 𝐹):𝐹–1-1-onto→𝐹)
105		f1of 6801	. . . . . . . . . 10 ⊢ ((𝑋 ↾ 𝐹):𝐹–1-1-onto→𝐹 → (𝑋 ↾ 𝐹):𝐹⟶𝐹)
106	104, 105	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 ↾ 𝐹):𝐹⟶𝐹)
107	106	frnd 6695	. . . . . . . 8 ⊢ (𝜑 → ran (𝑋 ↾ 𝐹) ⊆ 𝐹)
108		cores 6231	. . . . . . . 8 ⊢ (ran (𝑋 ↾ 𝐹) ⊆ 𝐹 → ((𝑌 ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (𝑌 ∘ (𝑋 ↾ 𝐹)))
109	107, 108	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑌 ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (𝑌 ∘ (𝑋 ↾ 𝐹)))
110	77, 109	eqtr4id 2815	. . . . . 6 ⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ 𝐹) = ((𝑌 ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)))
111	21	coeq1d 5829	. . . . . 6 ⊢ (𝜑 → ((𝑌 ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (( I ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)))
112		fcoi2 6734	. . . . . . 7 ⊢ ((𝑋 ↾ 𝐹):𝐹⟶𝐹 → (( I ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (𝑋 ↾ 𝐹))
113	106, 112	syl 17	. . . . . 6 ⊢ (𝜑 → (( I ↾ 𝐹) ∘ (𝑋 ↾ 𝐹)) = (𝑋 ↾ 𝐹))
114	110, 111, 113	3eqtrd 2800	. . . . 5 ⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ 𝐹) = (𝑋 ↾ 𝐹))
115	76, 114	uneq12d 4120	. . . 4 ⊢ (𝜑 → (((𝑌 ∘ 𝑋) ↾ 𝐸) ∪ ((𝑌 ∘ 𝑋) ↾ 𝐹)) = ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)))
116	71, 115	eqtrid 2808	. . 3 ⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ (𝐸 ∪ 𝐹)) = ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)))
117		f1oco 6825	. . . . 5 ⊢ ((𝑌:𝐴–1-1-onto→𝐴 ∧ 𝑋:𝐴–1-1-onto→𝐴) → (𝑌 ∘ 𝑋):𝐴–1-1-onto→𝐴)
118	9, 63, 117	syl2anc 593	. . . 4 ⊢ (𝜑 → (𝑌 ∘ 𝑋):𝐴–1-1-onto→𝐴)
119		f1ofn 6802	. . . 4 ⊢ ((𝑌 ∘ 𝑋):𝐴–1-1-onto→𝐴 → (𝑌 ∘ 𝑋) Fn 𝐴)
120		fnresdm 6635	. . . 4 ⊢ ((𝑌 ∘ 𝑋) Fn 𝐴 → ((𝑌 ∘ 𝑋) ↾ 𝐴) = (𝑌 ∘ 𝑋))
121	118, 119, 120	3syl 18	. . 3 ⊢ (𝜑 → ((𝑌 ∘ 𝑋) ↾ 𝐴) = (𝑌 ∘ 𝑋))
122	70, 116, 121	3eqtr3d 2804	. 2 ⊢ (𝜑 → ((𝑌 ↾ 𝐸) ∪ (𝑋 ↾ 𝐹)) = (𝑌 ∘ 𝑋))
123	69, 122	eqtr3d 2798	1 ⊢ (𝜑 → (𝑋 ∘ 𝑌) = (𝑌 ∘ 𝑋))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 = wceq 1559 ∈ wcel 2141 ∖ cdif 3899 ∪ cun 3900 ∩ cin 3901 ⊆ wss 3902 ∅c0 4283 I cid 5537 ^◡ccnv 5642 ran crn 5644 ↾ cres 5645 ∘ ccom 5647 Fun wfun 6510 Fn wfn 6511 ⟶wf 6512 –onto→wfo 6514 –1-1-onto→wf1o 6515 ‘cfv 6516 Basecbs 17236 SymGrpcsymg 19400

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7713 ax-cnex 11123 ax-resscn 11124 ax-1cn 11125 ax-icn 11126 ax-addcl 11127 ax-addrcl 11128 ax-mulcl 11129 ax-mulrcl 11130 ax-mulcom 11131 ax-addass 11132 ax-mulass 11133 ax-distr 11134 ax-i2m1 11135 ax-1ne0 11136 ax-1rid 11137 ax-rnegex 11138 ax-rrecex 11139 ax-cnre 11140 ax-pre-lttri 11141 ax-pre-lttrn 11142 ax-pre-ltadd 11143 ax-pre-mulgt0 11144

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-tp 4584 df-op 4586 df-uni 4863 df-iun 4948 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5538 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-we 5598 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6283 df-ord 6344 df-on 6345 df-lim 6346 df-suc 6347 df-iota 6472 df-fun 6518 df-fn 6519 df-f 6520 df-f1 6521 df-fo 6522 df-f1o 6523 df-fv 6524 df-riota 7348 df-ov 7394 df-oprab 7395 df-mpo 7396 df-om 7842 df-1st 7965 df-2nd 7966 df-frecs 8256 df-wrecs 8287 df-recs 8336 df-rdg 8375 df-1o 8431 df-er 8672 df-map 8804 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-pnf 11212 df-mnf 11213 df-xr 11214 df-ltxr 11215 df-le 11216 df-sub 11410 df-neg 11411 df-nn 12205 df-2 12274 df-3 12275 df-4 12276 df-5 12277 df-6 12278 df-7 12279 df-8 12280 df-9 12281 df-n0 12476 df-z 12563 df-uz 12834 df-fz 13507 df-struct 17174 df-sets 17191 df-slot 17209 df-ndx 17221 df-base 17237 df-ress 17258 df-plusg 17290 df-tset 17296 df-efmnd 18894 df-symg 19401

This theorem is referenced by: symgcom2 33225 cyc3conja 33298

W3C validator