Metamath Proof Explorer

Theorem cycpmconjvlem

Description: Lemma for cycpmconjv . (Contributed by Thierry Arnoux, 9-Oct-2023)

Ref Expression
Hypotheses cycpmconjvlem.f ⊢ ( 𝜑 → 𝐹 : 𝐷 –1-1-onto→ 𝐷 )
cycpmconjvlem.b ⊢ ( 𝜑 → 𝐵 ⊆ 𝐷 )
Assertion cycpmconjvlem ( 𝜑 → ( ( 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) ∘ ◡ 𝐹 ) = ( I ↾ ( 𝐷 ∖ ran ( 𝐹 ↾ 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 cycpmconjvlem.f ⊢ ( 𝜑 → 𝐹 : 𝐷 –1-1-onto→ 𝐷 )
2 cycpmconjvlem.b ⊢ ( 𝜑 → 𝐵 ⊆ 𝐷 )
3 f1ofun ⊢ ( 𝐹 : 𝐷 –1-1-onto→ 𝐷 → Fun 𝐹 )
4 1 3 syl ⊢ ( 𝜑 → Fun 𝐹 )
5 funrel ⊢ ( Fun 𝐹 → Rel 𝐹 )
6 dfrel2 ⊢ ( Rel 𝐹 ↔ ◡ ◡ 𝐹 = 𝐹 )
7 5 6 sylib ⊢ ( Fun 𝐹 → ◡ ◡ 𝐹 = 𝐹 )
8 7 reseq1d ⊢ ( Fun 𝐹 → ( ◡ ◡ 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) = ( 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) )
9 8 cnveqd ⊢ ( Fun 𝐹 → ◡ ( ◡ ◡ 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) = ◡ ( 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) )
10 9 coeq2d ⊢ ( Fun 𝐹 → ( ( 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) ∘ ◡ ( ◡ ◡ 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) ) = ( ( 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) ∘ ◡ ( 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) ) )
11 4 10 syl ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) ∘ ◡ ( ◡ ◡ 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) ) = ( ( 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) ∘ ◡ ( 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) ) )
12 difssd ⊢ ( 𝜑 → ( 𝐷 ∖ 𝐵 ) ⊆ 𝐷 )
13 f1odm ⊢ ( 𝐹 : 𝐷 –1-1-onto→ 𝐷 → dom 𝐹 = 𝐷 )
14 1 13 syl ⊢ ( 𝜑 → dom 𝐹 = 𝐷 )
15 12 14 sseqtrrd ⊢ ( 𝜑 → ( 𝐷 ∖ 𝐵 ) ⊆ dom 𝐹 )
16 ssdmres ⊢ ( ( 𝐷 ∖ 𝐵 ) ⊆ dom 𝐹 ↔ dom ( 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) = ( 𝐷 ∖ 𝐵 ) )
17 15 16 sylib ⊢ ( 𝜑 → dom ( 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) = ( 𝐷 ∖ 𝐵 ) )
18 ssidd ⊢ ( 𝜑 → ( 𝐷 ∖ 𝐵 ) ⊆ ( 𝐷 ∖ 𝐵 ) )
19 17 18 eqsstrd ⊢ ( 𝜑 → dom ( 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) ⊆ ( 𝐷 ∖ 𝐵 ) )
20 cores2 ⊢ ( dom ( 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) ⊆ ( 𝐷 ∖ 𝐵 ) → ( ( 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) ∘ ◡ ( ◡ ◡ 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) ) = ( ( 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) ∘ ◡ 𝐹 ) )
21 19 20 syl ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) ∘ ◡ ( ◡ ◡ 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) ) = ( ( 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) ∘ ◡ 𝐹 ) )
22 f1ocnv ⊢ ( 𝐹 : 𝐷 –1-1-onto→ 𝐷 → ◡ 𝐹 : 𝐷 –1-1-onto→ 𝐷 )
23 f1ofun ⊢ ( ◡ 𝐹 : 𝐷 –1-1-onto→ 𝐷 → Fun ◡ 𝐹 )
24 1 22 23 3syl ⊢ ( 𝜑 → Fun ◡ 𝐹 )
25 ssidd ⊢ ( 𝜑 → 𝐷 ⊆ 𝐷 )
26 25 14 sseqtrrd ⊢ ( 𝜑 → 𝐷 ⊆ dom 𝐹 )
27 fores ⊢ ( ( Fun 𝐹 ∧ 𝐷 ⊆ dom 𝐹 ) → ( 𝐹 ↾ 𝐷 ) : 𝐷 –onto→ ( 𝐹 “ 𝐷 ) )
28 4 26 27 syl2anc ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐷 ) : 𝐷 –onto→ ( 𝐹 “ 𝐷 ) )
29 df-ima ⊢ ( 𝐹 “ 𝐷 ) = ran ( 𝐹 ↾ 𝐷 )
30 foeq3 ⊢ ( ( 𝐹 “ 𝐷 ) = ran ( 𝐹 ↾ 𝐷 ) → ( ( 𝐹 ↾ 𝐷 ) : 𝐷 –onto→ ( 𝐹 “ 𝐷 ) ↔ ( 𝐹 ↾ 𝐷 ) : 𝐷 –onto→ ran ( 𝐹 ↾ 𝐷 ) ) )
31 29 30 ax-mp ⊢ ( ( 𝐹 ↾ 𝐷 ) : 𝐷 –onto→ ( 𝐹 “ 𝐷 ) ↔ ( 𝐹 ↾ 𝐷 ) : 𝐷 –onto→ ran ( 𝐹 ↾ 𝐷 ) )
32 28 31 sylib ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐷 ) : 𝐷 –onto→ ran ( 𝐹 ↾ 𝐷 ) )
33 2 14 sseqtrrd ⊢ ( 𝜑 → 𝐵 ⊆ dom 𝐹 )
34 fores ⊢ ( ( Fun 𝐹 ∧ 𝐵 ⊆ dom 𝐹 ) → ( 𝐹 ↾ 𝐵 ) : 𝐵 –onto→ ( 𝐹 “ 𝐵 ) )
35 4 33 34 syl2anc ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) : 𝐵 –onto→ ( 𝐹 “ 𝐵 ) )
36 df-ima ⊢ ( 𝐹 “ 𝐵 ) = ran ( 𝐹 ↾ 𝐵 )
37 foeq3 ⊢ ( ( 𝐹 “ 𝐵 ) = ran ( 𝐹 ↾ 𝐵 ) → ( ( 𝐹 ↾ 𝐵 ) : 𝐵 –onto→ ( 𝐹 “ 𝐵 ) ↔ ( 𝐹 ↾ 𝐵 ) : 𝐵 –onto→ ran ( 𝐹 ↾ 𝐵 ) ) )
38 36 37 ax-mp ⊢ ( ( 𝐹 ↾ 𝐵 ) : 𝐵 –onto→ ( 𝐹 “ 𝐵 ) ↔ ( 𝐹 ↾ 𝐵 ) : 𝐵 –onto→ ran ( 𝐹 ↾ 𝐵 ) )
39 35 38 sylib ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) : 𝐵 –onto→ ran ( 𝐹 ↾ 𝐵 ) )
40 resdif ⊢ ( ( Fun ◡ 𝐹 ∧ ( 𝐹 ↾ 𝐷 ) : 𝐷 –onto→ ran ( 𝐹 ↾ 𝐷 ) ∧ ( 𝐹 ↾ 𝐵 ) : 𝐵 –onto→ ran ( 𝐹 ↾ 𝐵 ) ) → ( 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) : ( 𝐷 ∖ 𝐵 ) –1-1-onto→ ( ran ( 𝐹 ↾ 𝐷 ) ∖ ran ( 𝐹 ↾ 𝐵 ) ) )
41 24 32 39 40 syl3anc ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) : ( 𝐷 ∖ 𝐵 ) –1-1-onto→ ( ran ( 𝐹 ↾ 𝐷 ) ∖ ran ( 𝐹 ↾ 𝐵 ) ) )
42 f1ofn ⊢ ( 𝐹 : 𝐷 –1-1-onto→ 𝐷 → 𝐹 Fn 𝐷 )
43 fnresdm ⊢ ( 𝐹 Fn 𝐷 → ( 𝐹 ↾ 𝐷 ) = 𝐹 )
44 1 42 43 3syl ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐷 ) = 𝐹 )
45 44 rneqd ⊢ ( 𝜑 → ran ( 𝐹 ↾ 𝐷 ) = ran 𝐹 )
46 f1ofo ⊢ ( 𝐹 : 𝐷 –1-1-onto→ 𝐷 → 𝐹 : 𝐷 –onto→ 𝐷 )
47 forn ⊢ ( 𝐹 : 𝐷 –onto→ 𝐷 → ran 𝐹 = 𝐷 )
48 1 46 47 3syl ⊢ ( 𝜑 → ran 𝐹 = 𝐷 )
49 45 48 eqtrd ⊢ ( 𝜑 → ran ( 𝐹 ↾ 𝐷 ) = 𝐷 )
50 49 difeq1d ⊢ ( 𝜑 → ( ran ( 𝐹 ↾ 𝐷 ) ∖ ran ( 𝐹 ↾ 𝐵 ) ) = ( 𝐷 ∖ ran ( 𝐹 ↾ 𝐵 ) ) )
51 50 f1oeq3d ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) : ( 𝐷 ∖ 𝐵 ) –1-1-onto→ ( ran ( 𝐹 ↾ 𝐷 ) ∖ ran ( 𝐹 ↾ 𝐵 ) ) ↔ ( 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) : ( 𝐷 ∖ 𝐵 ) –1-1-onto→ ( 𝐷 ∖ ran ( 𝐹 ↾ 𝐵 ) ) ) )
52 41 51 mpbid ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) : ( 𝐷 ∖ 𝐵 ) –1-1-onto→ ( 𝐷 ∖ ran ( 𝐹 ↾ 𝐵 ) ) )
53 f1ococnv2 ⊢ ( ( 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) : ( 𝐷 ∖ 𝐵 ) –1-1-onto→ ( 𝐷 ∖ ran ( 𝐹 ↾ 𝐵 ) ) → ( ( 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) ∘ ◡ ( 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) ) = ( I ↾ ( 𝐷 ∖ ran ( 𝐹 ↾ 𝐵 ) ) ) )
54 52 53 syl ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) ∘ ◡ ( 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) ) = ( I ↾ ( 𝐷 ∖ ran ( 𝐹 ↾ 𝐵 ) ) ) )
55 11 21 54 3eqtr3d ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐷 ∖ 𝐵 ) ) ∘ ◡ 𝐹 ) = ( I ↾ ( 𝐷 ∖ ran ( 𝐹 ↾ 𝐵 ) ) ) )