Metamath Proof Explorer

Theorem pmtrcnel2

Description: Variation on pmtrcnel . (Contributed by Thierry Arnoux, 16-Nov-2023)

Ref Expression
Hypotheses pmtrcnel.s ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
pmtrcnel.t ⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
pmtrcnel.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
pmtrcnel.j ⊢ 𝐽 = ( 𝐹 ‘ 𝐼 )
pmtrcnel.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
pmtrcnel.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
pmtrcnel.i ⊢ ( 𝜑 → 𝐼 ∈ dom ( 𝐹 ∖ I ) )
Assertion pmtrcnel2 ( 𝜑 → ( dom ( 𝐹 ∖ I ) ∖ { 𝐼 , 𝐽 } ) ⊆ dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) )

Proof

Step Hyp Ref Expression
1 pmtrcnel.s ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
2 pmtrcnel.t ⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
3 pmtrcnel.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
4 pmtrcnel.j ⊢ 𝐽 = ( 𝐹 ‘ 𝐼 )
5 pmtrcnel.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
6 pmtrcnel.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
7 pmtrcnel.i ⊢ ( 𝜑 → 𝐼 ∈ dom ( 𝐹 ∖ I ) )
8 mvdco ⊢ dom ( ( ◡ ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ) ∖ I ) ⊆ ( dom ( ◡ ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∖ I ) ∪ dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) )
9 8 a1i ⊢ ( 𝜑 → dom ( ( ◡ ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ) ∖ I ) ⊆ ( dom ( ◡ ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∖ I ) ∪ dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) ) )
10 coass ⊢ ( ( ◡ ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ) ∘ 𝐹 ) = ( ◡ ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) )
11 difss ⊢ ( 𝐹 ∖ I ) ⊆ 𝐹
12 dmss ⊢ ( ( 𝐹 ∖ I ) ⊆ 𝐹 → dom ( 𝐹 ∖ I ) ⊆ dom 𝐹 )
13 11 12 ax-mp ⊢ dom ( 𝐹 ∖ I ) ⊆ dom 𝐹
14 13 7 sselid ⊢ ( 𝜑 → 𝐼 ∈ dom 𝐹 )
15 1 3 symgbasf1o ⊢ ( 𝐹 ∈ 𝐵 → 𝐹 : 𝐷 –1-1-onto→ 𝐷 )
16 f1of ⊢ ( 𝐹 : 𝐷 –1-1-onto→ 𝐷 → 𝐹 : 𝐷 ⟶ 𝐷 )
17 6 15 16 3syl ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ 𝐷 )
18 17 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝐷 )
19 14 18 eleqtrd ⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
20 17 19 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐼 ) ∈ 𝐷 )
21 4 20 eqeltrid ⊢ ( 𝜑 → 𝐽 ∈ 𝐷 )
22 19 21 prssd ⊢ ( 𝜑 → { 𝐼 , 𝐽 } ⊆ 𝐷 )
23 17 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐷 )
24 fnelnfp ⊢ ( ( 𝐹 Fn 𝐷 ∧ 𝐼 ∈ 𝐷 ) → ( 𝐼 ∈ dom ( 𝐹 ∖ I ) ↔ ( 𝐹 ‘ 𝐼 ) ≠ 𝐼 ) )
25 24 biimpa ⊢ ( ( ( 𝐹 Fn 𝐷 ∧ 𝐼 ∈ 𝐷 ) ∧ 𝐼 ∈ dom ( 𝐹 ∖ I ) ) → ( 𝐹 ‘ 𝐼 ) ≠ 𝐼 )
26 23 19 7 25 syl21anc ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐼 ) ≠ 𝐼 )
27 26 necomd ⊢ ( 𝜑 → 𝐼 ≠ ( 𝐹 ‘ 𝐼 ) )
28 4 a1i ⊢ ( 𝜑 → 𝐽 = ( 𝐹 ‘ 𝐼 ) )
29 27 28 neeqtrrd ⊢ ( 𝜑 → 𝐼 ≠ 𝐽 )
30 enpr2 ⊢ ( ( 𝐼 ∈ 𝐷 ∧ 𝐽 ∈ 𝐷 ∧ 𝐼 ≠ 𝐽 ) → { 𝐼 , 𝐽 } ≈ 2o )
31 19 21 29 30 syl3anc ⊢ ( 𝜑 → { 𝐼 , 𝐽 } ≈ 2o )
32 eqid ⊢ ran 𝑇 = ran 𝑇
33 2 32 pmtrrn ⊢ ( ( 𝐷 ∈ 𝑉 ∧ { 𝐼 , 𝐽 } ⊆ 𝐷 ∧ { 𝐼 , 𝐽 } ≈ 2o ) → ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∈ ran 𝑇 )
34 5 22 31 33 syl3anc ⊢ ( 𝜑 → ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∈ ran 𝑇 )
35 2 32 pmtrff1o ⊢ ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∈ ran 𝑇 → ( 𝑇 ‘ { 𝐼 , 𝐽 } ) : 𝐷 –1-1-onto→ 𝐷 )
36 f1ococnv1 ⊢ ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) : 𝐷 –1-1-onto→ 𝐷 → ( ◡ ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ) = ( I ↾ 𝐷 ) )
37 34 35 36 3syl ⊢ ( 𝜑 → ( ◡ ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ) = ( I ↾ 𝐷 ) )
38 37 coeq1d ⊢ ( 𝜑 → ( ( ◡ ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ) ∘ 𝐹 ) = ( ( I ↾ 𝐷 ) ∘ 𝐹 ) )
39 10 38 eqtr3id ⊢ ( 𝜑 → ( ◡ ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ) = ( ( I ↾ 𝐷 ) ∘ 𝐹 ) )
40 fcoi2 ⊢ ( 𝐹 : 𝐷 ⟶ 𝐷 → ( ( I ↾ 𝐷 ) ∘ 𝐹 ) = 𝐹 )
41 17 40 syl ⊢ ( 𝜑 → ( ( I ↾ 𝐷 ) ∘ 𝐹 ) = 𝐹 )
42 39 41 eqtrd ⊢ ( 𝜑 → ( ◡ ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ) = 𝐹 )
43 42 difeq1d ⊢ ( 𝜑 → ( ( ◡ ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ) ∖ I ) = ( 𝐹 ∖ I ) )
44 43 dmeqd ⊢ ( 𝜑 → dom ( ( ◡ ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ) ∖ I ) = dom ( 𝐹 ∖ I ) )
45 2 32 pmtrfcnv ⊢ ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∈ ran 𝑇 → ◡ ( 𝑇 ‘ { 𝐼 , 𝐽 } ) = ( 𝑇 ‘ { 𝐼 , 𝐽 } ) )
46 34 45 syl ⊢ ( 𝜑 → ◡ ( 𝑇 ‘ { 𝐼 , 𝐽 } ) = ( 𝑇 ‘ { 𝐼 , 𝐽 } ) )
47 46 difeq1d ⊢ ( 𝜑 → ( ◡ ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∖ I ) = ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∖ I ) )
48 47 dmeqd ⊢ ( 𝜑 → dom ( ◡ ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∖ I ) = dom ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∖ I ) )
49 2 pmtrmvd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ { 𝐼 , 𝐽 } ⊆ 𝐷 ∧ { 𝐼 , 𝐽 } ≈ 2o ) → dom ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∖ I ) = { 𝐼 , 𝐽 } )
50 5 22 31 49 syl3anc ⊢ ( 𝜑 → dom ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∖ I ) = { 𝐼 , 𝐽 } )
51 48 50 eqtrd ⊢ ( 𝜑 → dom ( ◡ ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∖ I ) = { 𝐼 , 𝐽 } )
52 51 uneq1d ⊢ ( 𝜑 → ( dom ( ◡ ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∖ I ) ∪ dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) ) = ( { 𝐼 , 𝐽 } ∪ dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) ) )
53 uncom ⊢ ( { 𝐼 , 𝐽 } ∪ dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) ) = ( dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) ∪ { 𝐼 , 𝐽 } )
54 52 53 eqtrdi ⊢ ( 𝜑 → ( dom ( ◡ ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∖ I ) ∪ dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) ) = ( dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) ∪ { 𝐼 , 𝐽 } ) )
55 9 44 54 3sstr3d ⊢ ( 𝜑 → dom ( 𝐹 ∖ I ) ⊆ ( dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) ∪ { 𝐼 , 𝐽 } ) )
56 55 ssdifd ⊢ ( 𝜑 → ( dom ( 𝐹 ∖ I ) ∖ { 𝐼 , 𝐽 } ) ⊆ ( ( dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) ∪ { 𝐼 , 𝐽 } ) ∖ { 𝐼 , 𝐽 } ) )
57 difun2 ⊢ ( ( dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) ∪ { 𝐼 , 𝐽 } ) ∖ { 𝐼 , 𝐽 } ) = ( dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) ∖ { 𝐼 , 𝐽 } )
58 difss ⊢ ( dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) ∖ { 𝐼 , 𝐽 } ) ⊆ dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I )
59 57 58 eqsstri ⊢ ( ( dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) ∪ { 𝐼 , 𝐽 } ) ∖ { 𝐼 , 𝐽 } ) ⊆ dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I )
60 56 59 sstrdi ⊢ ( 𝜑 → ( dom ( 𝐹 ∖ I ) ∖ { 𝐼 , 𝐽 } ) ⊆ dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) )