MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  symggen Structured version   Visualization version   GIF version
Theorem symggen 19333
Description: The span of the transpositions is the subgroup that moves finitely many points. (Contributed by Stefan O'Rear, 28-Aug-2015.)
Hypotheses
Ref Expression
symgtrf.t 𝑇 = ran (pmTrspβ€˜π·)
symgtrf.g 𝐺 = (SymGrpβ€˜π·)
symgtrf.b 𝐡 = (Baseβ€˜πΊ)
symggen.k 𝐾 = (mrClsβ€˜(SubMndβ€˜πΊ))
Assertion
Ref Expression
symggen (𝐷 ∈ 𝑉 β†’ (πΎβ€˜π‘‡) = {π‘₯ ∈ 𝐡 ∣ dom (π‘₯ βˆ– I ) ∈ Fin})
Distinct variable groups:   π‘₯,𝐡   π‘₯,𝑇   π‘₯,𝐾   π‘₯,𝐷   π‘₯,𝐺   π‘₯,𝑉
Proof of Theorem symggen
Dummy variables 𝑒 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 3493 . . . 4 (𝐷 ∈ 𝑉 β†’ 𝐷 ∈ V)
2 symgtrf.g . . . . . . 7 𝐺 = (SymGrpβ€˜π·)
32symggrp 19263 . . . . . 6 (𝐷 ∈ V β†’ 𝐺 ∈ Grp)
43grpmndd 18829 . . . . 5 (𝐷 ∈ V β†’ 𝐺 ∈ Mnd)
5 symgtrf.b . . . . . 6 𝐡 = (Baseβ€˜πΊ)
65submacs 18705 . . . . 5 (𝐺 ∈ Mnd β†’ (SubMndβ€˜πΊ) ∈ (ACSβ€˜π΅))
7 acsmre 17593 . . . . 5 ((SubMndβ€˜πΊ) ∈ (ACSβ€˜π΅) β†’ (SubMndβ€˜πΊ) ∈ (Mooreβ€˜π΅))
84, 6, 73syl 18 . . . 4 (𝐷 ∈ V β†’ (SubMndβ€˜πΊ) ∈ (Mooreβ€˜π΅))
91, 8syl 17 . . 3 (𝐷 ∈ 𝑉 β†’ (SubMndβ€˜πΊ) ∈ (Mooreβ€˜π΅))
10 symgtrf.t . . . . . 6 𝑇 = ran (pmTrspβ€˜π·)
1110, 2, 5symgtrf 19332 . . . . 5 𝑇 βŠ† 𝐡
1211a1i 11 . . . 4 (𝐷 ∈ 𝑉 β†’ 𝑇 βŠ† 𝐡)
13 2onn 8638 . . . . . 6 2o ∈ Ο‰
14 nnfi 9164 . . . . . 6 (2o ∈ Ο‰ β†’ 2o ∈ Fin)
1513, 14ax-mp 5 . . . . 5 2o ∈ Fin
16 eqid 2733 . . . . . . . . 9 (pmTrspβ€˜π·) = (pmTrspβ€˜π·)
1716, 10pmtrfb 19328 . . . . . . . 8 (π‘₯ ∈ 𝑇 ↔ (𝐷 ∈ V ∧ π‘₯:𝐷–1-1-onto→𝐷 ∧ dom (π‘₯ βˆ– I ) β‰ˆ 2o))
1817simp3bi 1148 . . . . . . 7 (π‘₯ ∈ 𝑇 β†’ dom (π‘₯ βˆ– I ) β‰ˆ 2o)
19 enfi 9187 . . . . . . 7 (dom (π‘₯ βˆ– I ) β‰ˆ 2o β†’ (dom (π‘₯ βˆ– I ) ∈ Fin ↔ 2o ∈ Fin))
2018, 19syl 17 . . . . . 6 (π‘₯ ∈ 𝑇 β†’ (dom (π‘₯ βˆ– I ) ∈ Fin ↔ 2o ∈ Fin))
2120adantl 483 . . . . 5 ((𝐷 ∈ 𝑉 ∧ π‘₯ ∈ 𝑇) β†’ (dom (π‘₯ βˆ– I ) ∈ Fin ↔ 2o ∈ Fin))
2215, 21mpbiri 258 . . . 4 ((𝐷 ∈ 𝑉 ∧ π‘₯ ∈ 𝑇) β†’ dom (π‘₯ βˆ– I ) ∈ Fin)
2312, 22ssrabdv 4071 . . 3 (𝐷 ∈ 𝑉 β†’ 𝑇 βŠ† {π‘₯ ∈ 𝐡 ∣ dom (π‘₯ βˆ– I ) ∈ Fin})
242, 5symgfisg 19331 . . . 4 (𝐷 ∈ 𝑉 β†’ {π‘₯ ∈ 𝐡 ∣ dom (π‘₯ βˆ– I ) ∈ Fin} ∈ (SubGrpβ€˜πΊ))
25 subgsubm 19023 . . . 4 ({π‘₯ ∈ 𝐡 ∣ dom (π‘₯ βˆ– I ) ∈ Fin} ∈ (SubGrpβ€˜πΊ) β†’ {π‘₯ ∈ 𝐡 ∣ dom (π‘₯ βˆ– I ) ∈ Fin} ∈ (SubMndβ€˜πΊ))
2624, 25syl 17 . . 3 (𝐷 ∈ 𝑉 β†’ {π‘₯ ∈ 𝐡 ∣ dom (π‘₯ βˆ– I ) ∈ Fin} ∈ (SubMndβ€˜πΊ))
27 symggen.k . . . 4 𝐾 = (mrClsβ€˜(SubMndβ€˜πΊ))
2827mrcsscl 17561 . . 3 (((SubMndβ€˜πΊ) ∈ (Mooreβ€˜π΅) ∧ 𝑇 βŠ† {π‘₯ ∈ 𝐡 ∣ dom (π‘₯ βˆ– I ) ∈ Fin} ∧ {π‘₯ ∈ 𝐡 ∣ dom (π‘₯ βˆ– I ) ∈ Fin} ∈ (SubMndβ€˜πΊ)) β†’ (πΎβ€˜π‘‡) βŠ† {π‘₯ ∈ 𝐡 ∣ dom (π‘₯ βˆ– I ) ∈ Fin})
299, 23, 26, 28syl3anc 1372 . 2 (𝐷 ∈ 𝑉 β†’ (πΎβ€˜π‘‡) βŠ† {π‘₯ ∈ 𝐡 ∣ dom (π‘₯ βˆ– I ) ∈ Fin})
30 vex 3479 . . . . . . 7 π‘₯ ∈ V
3130a1i 11 . . . . . 6 (dom (π‘₯ βˆ– I ) ∈ Fin β†’ π‘₯ ∈ V)
32 finnum 9940 . . . . . 6 (dom (π‘₯ βˆ– I ) ∈ Fin β†’ dom (π‘₯ βˆ– I ) ∈ dom card)
33 domfi 9189 . . . . . . . 8 ((dom (π‘₯ βˆ– I ) ∈ Fin ∧ dom (𝑦 βˆ– I ) β‰Ό dom (π‘₯ βˆ– I )) β†’ dom (𝑦 βˆ– I ) ∈ Fin)
342, 5symgbasf1o 19237 . . . . . . . . . . . . . . 15 (𝑦 ∈ 𝐡 β†’ 𝑦:𝐷–1-1-onto→𝐷)
3534adantl 483 . . . . . . . . . . . . . 14 ((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) β†’ 𝑦:𝐷–1-1-onto→𝐷)
36 f1ofn 6832 . . . . . . . . . . . . . 14 (𝑦:𝐷–1-1-onto→𝐷 β†’ 𝑦 Fn 𝐷)
37 fnnfpeq0 7173 . . . . . . . . . . . . . 14 (𝑦 Fn 𝐷 β†’ (dom (𝑦 βˆ– I ) = βˆ… ↔ 𝑦 = ( I β†Ύ 𝐷)))
3835, 36, 373syl 18 . . . . . . . . . . . . 13 ((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) β†’ (dom (𝑦 βˆ– I ) = βˆ… ↔ 𝑦 = ( I β†Ύ 𝐷)))
392, 5elbasfv 17147 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ 𝐡 β†’ 𝐷 ∈ V)
4039adantl 483 . . . . . . . . . . . . . . . 16 ((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) β†’ 𝐷 ∈ V)
412symgid 19264 . . . . . . . . . . . . . . . 16 (𝐷 ∈ V β†’ ( I β†Ύ 𝐷) = (0gβ€˜πΊ))
4240, 41syl 17 . . . . . . . . . . . . . . 15 ((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) β†’ ( I β†Ύ 𝐷) = (0gβ€˜πΊ))
4340, 8syl 17 . . . . . . . . . . . . . . . . 17 ((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) β†’ (SubMndβ€˜πΊ) ∈ (Mooreβ€˜π΅))
4427mrccl 17552 . . . . . . . . . . . . . . . . 17 (((SubMndβ€˜πΊ) ∈ (Mooreβ€˜π΅) ∧ 𝑇 βŠ† 𝐡) β†’ (πΎβ€˜π‘‡) ∈ (SubMndβ€˜πΊ))
4543, 11, 44sylancl 587 . . . . . . . . . . . . . . . 16 ((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) β†’ (πΎβ€˜π‘‡) ∈ (SubMndβ€˜πΊ))
46 eqid 2733 . . . . . . . . . . . . . . . . 17 (0gβ€˜πΊ) = (0gβ€˜πΊ)
4746subm0cl 18689 . . . . . . . . . . . . . . . 16 ((πΎβ€˜π‘‡) ∈ (SubMndβ€˜πΊ) β†’ (0gβ€˜πΊ) ∈ (πΎβ€˜π‘‡))
4845, 47syl 17 . . . . . . . . . . . . . . 15 ((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) β†’ (0gβ€˜πΊ) ∈ (πΎβ€˜π‘‡))
4942, 48eqeltrd 2834 . . . . . . . . . . . . . 14 ((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) β†’ ( I β†Ύ 𝐷) ∈ (πΎβ€˜π‘‡))
50 eleq1a 2829 . . . . . . . . . . . . . 14 (( I β†Ύ 𝐷) ∈ (πΎβ€˜π‘‡) β†’ (𝑦 = ( I β†Ύ 𝐷) β†’ 𝑦 ∈ (πΎβ€˜π‘‡)))
5149, 50syl 17 . . . . . . . . . . . . 13 ((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) β†’ (𝑦 = ( I β†Ύ 𝐷) β†’ 𝑦 ∈ (πΎβ€˜π‘‡)))
5238, 51sylbid 239 . . . . . . . . . . . 12 ((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) β†’ (dom (𝑦 βˆ– I ) = βˆ… β†’ 𝑦 ∈ (πΎβ€˜π‘‡)))
5352adantr 482 . . . . . . . . . . 11 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ βˆ€π‘§(dom (𝑧 βˆ– I ) β‰Ί dom (𝑦 βˆ– I ) β†’ (𝑧 ∈ 𝐡 β†’ 𝑧 ∈ (πΎβ€˜π‘‡)))) β†’ (dom (𝑦 βˆ– I ) = βˆ… β†’ 𝑦 ∈ (πΎβ€˜π‘‡)))
54 n0 4346 . . . . . . . . . . . 12 (dom (𝑦 βˆ– I ) β‰  βˆ… ↔ βˆƒπ‘’ 𝑒 ∈ dom (𝑦 βˆ– I ))
5540adantr 482 . . . . . . . . . . . . . . . . . . . . 21 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ 𝐷 ∈ V)
56 simpr 486 . . . . . . . . . . . . . . . . . . . . . . 23 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ 𝑒 ∈ dom (𝑦 βˆ– I ))
57 f1omvdmvd 19306 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦:𝐷–1-1-onto→𝐷 ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (π‘¦β€˜π‘’) ∈ (dom (𝑦 βˆ– I ) βˆ– {𝑒}))
5835, 57sylan 581 . . . . . . . . . . . . . . . . . . . . . . . 24 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (π‘¦β€˜π‘’) ∈ (dom (𝑦 βˆ– I ) βˆ– {𝑒}))
5958eldifad 3960 . . . . . . . . . . . . . . . . . . . . . . 23 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (π‘¦β€˜π‘’) ∈ dom (𝑦 βˆ– I ))
6056, 59prssd 4825 . . . . . . . . . . . . . . . . . . . . . 22 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ {𝑒, (π‘¦β€˜π‘’)} βŠ† dom (𝑦 βˆ– I ))
61 difss 4131 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 βˆ– I ) βŠ† 𝑦
62 dmss 5901 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 βˆ– I ) βŠ† 𝑦 β†’ dom (𝑦 βˆ– I ) βŠ† dom 𝑦)
6361, 62ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 dom (𝑦 βˆ– I ) βŠ† dom 𝑦
64 f1odm 6835 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦:𝐷–1-1-onto→𝐷 β†’ dom 𝑦 = 𝐷)
6535, 64syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) β†’ dom 𝑦 = 𝐷)
6663, 65sseqtrid 4034 . . . . . . . . . . . . . . . . . . . . . . 23 ((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) β†’ dom (𝑦 βˆ– I ) βŠ† 𝐷)
6766adantr 482 . . . . . . . . . . . . . . . . . . . . . 22 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ dom (𝑦 βˆ– I ) βŠ† 𝐷)
6860, 67sstrd 3992 . . . . . . . . . . . . . . . . . . . . 21 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ {𝑒, (π‘¦β€˜π‘’)} βŠ† 𝐷)
69 vex 3479 . . . . . . . . . . . . . . . . . . . . . 22 𝑒 ∈ V
70 fvex 6902 . . . . . . . . . . . . . . . . . . . . . 22 (π‘¦β€˜π‘’) ∈ V
7135adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ 𝑦:𝐷–1-1-onto→𝐷)
7271, 36syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ 𝑦 Fn 𝐷)
7366sselda 3982 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ 𝑒 ∈ 𝐷)
74 fnelnfp 7172 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 Fn 𝐷 ∧ 𝑒 ∈ 𝐷) β†’ (𝑒 ∈ dom (𝑦 βˆ– I ) ↔ (π‘¦β€˜π‘’) β‰  𝑒))
7572, 73, 74syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . 24 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (𝑒 ∈ dom (𝑦 βˆ– I ) ↔ (π‘¦β€˜π‘’) β‰  𝑒))
7656, 75mpbid 231 . . . . . . . . . . . . . . . . . . . . . . 23 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (π‘¦β€˜π‘’) β‰  𝑒)
7776necomd 2997 . . . . . . . . . . . . . . . . . . . . . 22 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ 𝑒 β‰  (π‘¦β€˜π‘’))
78 enpr2 9994 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑒 ∈ V ∧ (π‘¦β€˜π‘’) ∈ V ∧ 𝑒 β‰  (π‘¦β€˜π‘’)) β†’ {𝑒, (π‘¦β€˜π‘’)} β‰ˆ 2o)
7969, 70, 77, 78mp3an12i 1466 . . . . . . . . . . . . . . . . . . . . 21 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ {𝑒, (π‘¦β€˜π‘’)} β‰ˆ 2o)
8016, 10pmtrrn 19320 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷 ∈ V ∧ {𝑒, (π‘¦β€˜π‘’)} βŠ† 𝐷 ∧ {𝑒, (π‘¦β€˜π‘’)} β‰ˆ 2o) β†’ ((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∈ 𝑇)
8155, 68, 79, 80syl3anc 1372 . . . . . . . . . . . . . . . . . . . 20 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ ((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∈ 𝑇)
8211, 81sselid 3980 . . . . . . . . . . . . . . . . . . 19 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ ((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∈ 𝐡)
83 simplr 768 . . . . . . . . . . . . . . . . . . 19 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ 𝑦 ∈ 𝐡)
84 eqid 2733 . . . . . . . . . . . . . . . . . . . 20 (+gβ€˜πΊ) = (+gβ€˜πΊ)
852, 5, 84symgov 19246 . . . . . . . . . . . . . . . . . . 19 ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) = (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦))
8682, 83, 85syl2anc 585 . . . . . . . . . . . . . . . . . 18 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) = (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦))
8786oveq2d 7422 . . . . . . . . . . . . . . . . 17 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)(((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦)) = (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)(((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦)))
8840, 3syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) β†’ 𝐺 ∈ Grp)
8988adantr 482 . . . . . . . . . . . . . . . . . . . 20 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ 𝐺 ∈ Grp)
905, 84grpcl 18824 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ Grp ∧ ((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) ∈ 𝐡)
9189, 82, 83, 90syl3anc 1372 . . . . . . . . . . . . . . . . . . 19 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) ∈ 𝐡)
9286, 91eqeltrrd 2835 . . . . . . . . . . . . . . . . . 18 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦) ∈ 𝐡)
932, 5, 84symgov 19246 . . . . . . . . . . . . . . . . . 18 ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∈ 𝐡 ∧ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦) ∈ 𝐡) β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)(((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦)) = (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦)))
9482, 92, 93syl2anc 585 . . . . . . . . . . . . . . . . 17 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)(((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦)) = (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦)))
95 coass 6262 . . . . . . . . . . . . . . . . . 18 ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ ((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})) ∘ 𝑦) = (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦))
9616, 10pmtrfinv 19324 . . . . . . . . . . . . . . . . . . . . 21 (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∈ 𝑇 β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ ((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})) = ( I β†Ύ 𝐷))
9781, 96syl 17 . . . . . . . . . . . . . . . . . . . 20 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ ((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})) = ( I β†Ύ 𝐷))
9897coeq1d 5860 . . . . . . . . . . . . . . . . . . 19 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ ((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})) ∘ 𝑦) = (( I β†Ύ 𝐷) ∘ 𝑦))
99 f1of 6831 . . . . . . . . . . . . . . . . . . . 20 (𝑦:𝐷–1-1-onto→𝐷 β†’ 𝑦:𝐷⟢𝐷)
100 fcoi2 6764 . . . . . . . . . . . . . . . . . . . 20 (𝑦:𝐷⟢𝐷 β†’ (( I β†Ύ 𝐷) ∘ 𝑦) = 𝑦)
10171, 99, 1003syl 18 . . . . . . . . . . . . . . . . . . 19 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (( I β†Ύ 𝐷) ∘ 𝑦) = 𝑦)
10298, 101eqtrd 2773 . . . . . . . . . . . . . . . . . 18 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ ((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})) ∘ 𝑦) = 𝑦)
10395, 102eqtr3id 2787 . . . . . . . . . . . . . . . . 17 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦)) = 𝑦)
10487, 94, 1033eqtrd 2777 . . . . . . . . . . . . . . . 16 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)(((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦)) = 𝑦)
105104adantlr 714 . . . . . . . . . . . . . . 15 ((((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ βˆ€π‘§(dom (𝑧 βˆ– I ) β‰Ί dom (𝑦 βˆ– I ) β†’ (𝑧 ∈ 𝐡 β†’ 𝑧 ∈ (πΎβ€˜π‘‡)))) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)(((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦)) = 𝑦)
10645ad2antrr 725 . . . . . . . . . . . . . . . 16 ((((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ βˆ€π‘§(dom (𝑧 βˆ– I ) β‰Ί dom (𝑦 βˆ– I ) β†’ (𝑧 ∈ 𝐡 β†’ 𝑧 ∈ (πΎβ€˜π‘‡)))) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (πΎβ€˜π‘‡) ∈ (SubMndβ€˜πΊ))
10727mrcssid 17558 . . . . . . . . . . . . . . . . . . . 20 (((SubMndβ€˜πΊ) ∈ (Mooreβ€˜π΅) ∧ 𝑇 βŠ† 𝐡) β†’ 𝑇 βŠ† (πΎβ€˜π‘‡))
10843, 11, 107sylancl 587 . . . . . . . . . . . . . . . . . . 19 ((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) β†’ 𝑇 βŠ† (πΎβ€˜π‘‡))
109108adantr 482 . . . . . . . . . . . . . . . . . 18 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ 𝑇 βŠ† (πΎβ€˜π‘‡))
110109, 81sseldd 3983 . . . . . . . . . . . . . . . . 17 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ ((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∈ (πΎβ€˜π‘‡))
111110adantlr 714 . . . . . . . . . . . . . . . 16 ((((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ βˆ€π‘§(dom (𝑧 βˆ– I ) β‰Ί dom (𝑦 βˆ– I ) β†’ (𝑧 ∈ 𝐡 β†’ 𝑧 ∈ (πΎβ€˜π‘‡)))) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ ((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∈ (πΎβ€˜π‘‡))
11286difeq1d 4121 . . . . . . . . . . . . . . . . . . . 20 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) βˆ– I ) = ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦) βˆ– I ))
113112dmeqd 5904 . . . . . . . . . . . . . . . . . . 19 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ dom ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) βˆ– I ) = dom ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦) βˆ– I ))
114 simpll 766 . . . . . . . . . . . . . . . . . . . 20 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ dom (𝑦 βˆ– I ) ∈ Fin)
115 mvdco 19308 . . . . . . . . . . . . . . . . . . . . . 22 dom ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦) βˆ– I ) βŠ† (dom (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) βˆ– I ) βˆͺ dom (𝑦 βˆ– I ))
11616pmtrmvd 19319 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐷 ∈ V ∧ {𝑒, (π‘¦β€˜π‘’)} βŠ† 𝐷 ∧ {𝑒, (π‘¦β€˜π‘’)} β‰ˆ 2o) β†’ dom (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) βˆ– I ) = {𝑒, (π‘¦β€˜π‘’)})
11755, 68, 79, 116syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . 24 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ dom (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) βˆ– I ) = {𝑒, (π‘¦β€˜π‘’)})
118117, 60eqsstrd 4020 . . . . . . . . . . . . . . . . . . . . . . 23 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ dom (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) βˆ– I ) βŠ† dom (𝑦 βˆ– I ))
119 ssidd 4005 . . . . . . . . . . . . . . . . . . . . . . 23 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ dom (𝑦 βˆ– I ) βŠ† dom (𝑦 βˆ– I ))
120118, 119unssd 4186 . . . . . . . . . . . . . . . . . . . . . 22 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (dom (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) βˆ– I ) βˆͺ dom (𝑦 βˆ– I )) βŠ† dom (𝑦 βˆ– I ))
121115, 120sstrid 3993 . . . . . . . . . . . . . . . . . . . . 21 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ dom ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦) βˆ– I ) βŠ† dom (𝑦 βˆ– I ))
122 fvco2 6986 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 Fn 𝐷 ∧ 𝑒 ∈ 𝐷) β†’ ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦)β€˜π‘’) = (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})β€˜(π‘¦β€˜π‘’)))
12372, 73, 122syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . 23 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦)β€˜π‘’) = (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})β€˜(π‘¦β€˜π‘’)))
124 prcom 4736 . . . . . . . . . . . . . . . . . . . . . . . . . 26 {𝑒, (π‘¦β€˜π‘’)} = {(π‘¦β€˜π‘’), 𝑒}
125124fveq2i 6892 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) = ((pmTrspβ€˜π·)β€˜{(π‘¦β€˜π‘’), 𝑒})
126125fveq1i 6890 . . . . . . . . . . . . . . . . . . . . . . . 24 (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})β€˜(π‘¦β€˜π‘’)) = (((pmTrspβ€˜π·)β€˜{(π‘¦β€˜π‘’), 𝑒})β€˜(π‘¦β€˜π‘’))
12767, 59sseldd 3983 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (π‘¦β€˜π‘’) ∈ 𝐷)
12816pmtrprfv 19316 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐷 ∈ V ∧ ((π‘¦β€˜π‘’) ∈ 𝐷 ∧ 𝑒 ∈ 𝐷 ∧ (π‘¦β€˜π‘’) β‰  𝑒)) β†’ (((pmTrspβ€˜π·)β€˜{(π‘¦β€˜π‘’), 𝑒})β€˜(π‘¦β€˜π‘’)) = 𝑒)
12955, 127, 73, 76, 128syl13anc 1373 . . . . . . . . . . . . . . . . . . . . . . . 24 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (((pmTrspβ€˜π·)β€˜{(π‘¦β€˜π‘’), 𝑒})β€˜(π‘¦β€˜π‘’)) = 𝑒)
130126, 129eqtrid 2785 . . . . . . . . . . . . . . . . . . . . . . 23 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})β€˜(π‘¦β€˜π‘’)) = 𝑒)
131123, 130eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . 22 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦)β€˜π‘’) = 𝑒)
1322, 5symgbasf1o 19237 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦) ∈ 𝐡 β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦):𝐷–1-1-onto→𝐷)
133 f1ofn 6832 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦):𝐷–1-1-onto→𝐷 β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦) Fn 𝐷)
13492, 132, 1333syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦) Fn 𝐷)
135 fnelnfp 7172 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦) Fn 𝐷 ∧ 𝑒 ∈ 𝐷) β†’ (𝑒 ∈ dom ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦) βˆ– I ) ↔ ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦)β€˜π‘’) β‰  𝑒))
136135necon2bbid 2985 . . . . . . . . . . . . . . . . . . . . . . 23 (((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦) Fn 𝐷 ∧ 𝑒 ∈ 𝐷) β†’ (((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦)β€˜π‘’) = 𝑒 ↔ Β¬ 𝑒 ∈ dom ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦) βˆ– I )))
137134, 73, 136syl2anc 585 . . . . . . . . . . . . . . . . . . . . . 22 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦)β€˜π‘’) = 𝑒 ↔ Β¬ 𝑒 ∈ dom ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦) βˆ– I )))
138131, 137mpbid 231 . . . . . . . . . . . . . . . . . . . . 21 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ Β¬ 𝑒 ∈ dom ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦) βˆ– I ))
139121, 56, 138ssnelpssd 4112 . . . . . . . . . . . . . . . . . . . 20 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ dom ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦) βˆ– I ) ⊊ dom (𝑦 βˆ– I ))
140 php3 9209 . . . . . . . . . . . . . . . . . . . 20 ((dom (𝑦 βˆ– I ) ∈ Fin ∧ dom ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦) βˆ– I ) ⊊ dom (𝑦 βˆ– I )) β†’ dom ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦) βˆ– I ) β‰Ί dom (𝑦 βˆ– I ))
141114, 139, 140syl2anc 585 . . . . . . . . . . . . . . . . . . 19 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ dom ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦) βˆ– I ) β‰Ί dom (𝑦 βˆ– I ))
142113, 141eqbrtrd 5170 . . . . . . . . . . . . . . . . . 18 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ dom ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) βˆ– I ) β‰Ί dom (𝑦 βˆ– I ))
143142adantlr 714 . . . . . . . . . . . . . . . . 17 ((((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ βˆ€π‘§(dom (𝑧 βˆ– I ) β‰Ί dom (𝑦 βˆ– I ) β†’ (𝑧 ∈ 𝐡 β†’ 𝑧 ∈ (πΎβ€˜π‘‡)))) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ dom ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) βˆ– I ) β‰Ί dom (𝑦 βˆ– I ))
14491adantlr 714 . . . . . . . . . . . . . . . . 17 ((((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ βˆ€π‘§(dom (𝑧 βˆ– I ) β‰Ί dom (𝑦 βˆ– I ) β†’ (𝑧 ∈ 𝐡 β†’ 𝑧 ∈ (πΎβ€˜π‘‡)))) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) ∈ 𝐡)
145 ovex 7439 . . . . . . . . . . . . . . . . . . 19 (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) ∈ V
146 difeq1 4115 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) β†’ (𝑧 βˆ– I ) = ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) βˆ– I ))
147146dmeqd 5904 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) β†’ dom (𝑧 βˆ– I ) = dom ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) βˆ– I ))
148147breq1d 5158 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) β†’ (dom (𝑧 βˆ– I ) β‰Ί dom (𝑦 βˆ– I ) ↔ dom ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) βˆ– I ) β‰Ί dom (𝑦 βˆ– I )))
149 eleq1 2822 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) β†’ (𝑧 ∈ 𝐡 ↔ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) ∈ 𝐡))
150 eleq1 2822 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) β†’ (𝑧 ∈ (πΎβ€˜π‘‡) ↔ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) ∈ (πΎβ€˜π‘‡)))
151149, 150imbi12d 345 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) β†’ ((𝑧 ∈ 𝐡 β†’ 𝑧 ∈ (πΎβ€˜π‘‡)) ↔ ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) ∈ 𝐡 β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) ∈ (πΎβ€˜π‘‡))))
152148, 151imbi12d 345 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) β†’ ((dom (𝑧 βˆ– I ) β‰Ί dom (𝑦 βˆ– I ) β†’ (𝑧 ∈ 𝐡 β†’ 𝑧 ∈ (πΎβ€˜π‘‡))) ↔ (dom ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) βˆ– I ) β‰Ί dom (𝑦 βˆ– I ) β†’ ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) ∈ 𝐡 β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) ∈ (πΎβ€˜π‘‡)))))
153145, 152spcv 3596 . . . . . . . . . . . . . . . . . 18 (βˆ€π‘§(dom (𝑧 βˆ– I ) β‰Ί dom (𝑦 βˆ– I ) β†’ (𝑧 ∈ 𝐡 β†’ 𝑧 ∈ (πΎβ€˜π‘‡))) β†’ (dom ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) βˆ– I ) β‰Ί dom (𝑦 βˆ– I ) β†’ ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) ∈ 𝐡 β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) ∈ (πΎβ€˜π‘‡))))
154153ad2antlr 726 . . . . . . . . . . . . . . . . 17 ((((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ βˆ€π‘§(dom (𝑧 βˆ– I ) β‰Ί dom (𝑦 βˆ– I ) β†’ (𝑧 ∈ 𝐡 β†’ 𝑧 ∈ (πΎβ€˜π‘‡)))) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (dom ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) βˆ– I ) β‰Ί dom (𝑦 βˆ– I ) β†’ ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) ∈ 𝐡 β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) ∈ (πΎβ€˜π‘‡))))
155143, 144, 154mp2d 49 . . . . . . . . . . . . . . . 16 ((((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ βˆ€π‘§(dom (𝑧 βˆ– I ) β‰Ί dom (𝑦 βˆ– I ) β†’ (𝑧 ∈ 𝐡 β†’ 𝑧 ∈ (πΎβ€˜π‘‡)))) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) ∈ (πΎβ€˜π‘‡))
15684submcl 18690 . . . . . . . . . . . . . . . 16 (((πΎβ€˜π‘‡) ∈ (SubMndβ€˜πΊ) ∧ ((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∈ (πΎβ€˜π‘‡) ∧ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) ∈ (πΎβ€˜π‘‡)) β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)(((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦)) ∈ (πΎβ€˜π‘‡))
157106, 111, 155, 156syl3anc 1372 . . . . . . . . . . . . . . 15 ((((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ βˆ€π‘§(dom (𝑧 βˆ– I ) β‰Ί dom (𝑦 βˆ– I ) β†’ (𝑧 ∈ 𝐡 β†’ 𝑧 ∈ (πΎβ€˜π‘‡)))) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)(((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦)) ∈ (πΎβ€˜π‘‡))
158105, 157eqeltrrd 2835 . . . . . . . . . . . . . 14 ((((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ βˆ€π‘§(dom (𝑧 βˆ– I ) β‰Ί dom (𝑦 βˆ– I ) β†’ (𝑧 ∈ 𝐡 β†’ 𝑧 ∈ (πΎβ€˜π‘‡)))) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ 𝑦 ∈ (πΎβ€˜π‘‡))
159158ex 414 . . . . . . . . . . . . 13 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ βˆ€π‘§(dom (𝑧 βˆ– I ) β‰Ί dom (𝑦 βˆ– I ) β†’ (𝑧 ∈ 𝐡 β†’ 𝑧 ∈ (πΎβ€˜π‘‡)))) β†’ (𝑒 ∈ dom (𝑦 βˆ– I ) β†’ 𝑦 ∈ (πΎβ€˜π‘‡)))
160159exlimdv 1937 . . . . . . . . . . . 12 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ βˆ€π‘§(dom (𝑧 βˆ– I ) β‰Ί dom (𝑦 βˆ– I ) β†’ (𝑧 ∈ 𝐡 β†’ 𝑧 ∈ (πΎβ€˜π‘‡)))) β†’ (βˆƒπ‘’ 𝑒 ∈ dom (𝑦 βˆ– I ) β†’ 𝑦 ∈ (πΎβ€˜π‘‡)))
16154, 160biimtrid 241 . . . . . . . . . . 11 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ βˆ€π‘§(dom (𝑧 βˆ– I ) β‰Ί dom (𝑦 βˆ– I ) β†’ (𝑧 ∈ 𝐡 β†’ 𝑧 ∈ (πΎβ€˜π‘‡)))) β†’ (dom (𝑦 βˆ– I ) β‰  βˆ… β†’ 𝑦 ∈ (πΎβ€˜π‘‡)))
16253, 161pm2.61dne 3029 . . . . . . . . . 10 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ βˆ€π‘§(dom (𝑧 βˆ– I ) β‰Ί dom (𝑦 βˆ– I ) β†’ (𝑧 ∈ 𝐡 β†’ 𝑧 ∈ (πΎβ€˜π‘‡)))) β†’ 𝑦 ∈ (πΎβ€˜π‘‡))
163162exp31 421 . . . . . . . . 9 (dom (𝑦 βˆ– I ) ∈ Fin β†’ (𝑦 ∈ 𝐡 β†’ (βˆ€π‘§(dom (𝑧 βˆ– I ) β‰Ί dom (𝑦 βˆ– I ) β†’ (𝑧 ∈ 𝐡 β†’ 𝑧 ∈ (πΎβ€˜π‘‡))) β†’ 𝑦 ∈ (πΎβ€˜π‘‡))))
164163com23 86 . . . . . . . 8 (dom (𝑦 βˆ– I ) ∈ Fin β†’ (βˆ€π‘§(dom (𝑧 βˆ– I ) β‰Ί dom (𝑦 βˆ– I ) β†’ (𝑧 ∈ 𝐡 β†’ 𝑧 ∈ (πΎβ€˜π‘‡))) β†’ (𝑦 ∈ 𝐡 β†’ 𝑦 ∈ (πΎβ€˜π‘‡))))
16533, 164syl 17 . . . . . . 7 ((dom (π‘₯ βˆ– I ) ∈ Fin ∧ dom (𝑦 βˆ– I ) β‰Ό dom (π‘₯ βˆ– I )) β†’ (βˆ€π‘§(dom (𝑧 βˆ– I ) β‰Ί dom (𝑦 βˆ– I ) β†’ (𝑧 ∈ 𝐡 β†’ 𝑧 ∈ (πΎβ€˜π‘‡))) β†’ (𝑦 ∈ 𝐡 β†’ 𝑦 ∈ (πΎβ€˜π‘‡))))
1661653impia 1118 . . . . . 6 ((dom (π‘₯ βˆ– I ) ∈ Fin ∧ dom (𝑦 βˆ– I ) β‰Ό dom (π‘₯ βˆ– I ) ∧ βˆ€π‘§(dom (𝑧 βˆ– I ) β‰Ί dom (𝑦 βˆ– I ) β†’ (𝑧 ∈ 𝐡 β†’ 𝑧 ∈ (πΎβ€˜π‘‡)))) β†’ (𝑦 ∈ 𝐡 β†’ 𝑦 ∈ (πΎβ€˜π‘‡)))
167 eleq1w 2817 . . . . . . 7 (𝑦 = 𝑧 β†’ (𝑦 ∈ 𝐡 ↔ 𝑧 ∈ 𝐡))
168 eleq1w 2817 . . . . . . 7 (𝑦 = 𝑧 β†’ (𝑦 ∈ (πΎβ€˜π‘‡) ↔ 𝑧 ∈ (πΎβ€˜π‘‡)))
169167, 168imbi12d 345 . . . . . 6 (𝑦 = 𝑧 β†’ ((𝑦 ∈ 𝐡 β†’ 𝑦 ∈ (πΎβ€˜π‘‡)) ↔ (𝑧 ∈ 𝐡 β†’ 𝑧 ∈ (πΎβ€˜π‘‡))))
170 eleq1w 2817 . . . . . . 7 (𝑦 = π‘₯ β†’ (𝑦 ∈ 𝐡 ↔ π‘₯ ∈ 𝐡))
171 eleq1w 2817 . . . . . . 7 (𝑦 = π‘₯ β†’ (𝑦 ∈ (πΎβ€˜π‘‡) ↔ π‘₯ ∈ (πΎβ€˜π‘‡)))
172170, 171imbi12d 345 . . . . . 6 (𝑦 = π‘₯ β†’ ((𝑦 ∈ 𝐡 β†’ 𝑦 ∈ (πΎβ€˜π‘‡)) ↔ (π‘₯ ∈ 𝐡 β†’ π‘₯ ∈ (πΎβ€˜π‘‡))))
173 difeq1 4115 . . . . . . 7 (𝑦 = 𝑧 β†’ (𝑦 βˆ– I ) = (𝑧 βˆ– I ))
174173dmeqd 5904 . . . . . 6 (𝑦 = 𝑧 β†’ dom (𝑦 βˆ– I ) = dom (𝑧 βˆ– I ))
175 difeq1 4115 . . . . . . 7 (𝑦 = π‘₯ β†’ (𝑦 βˆ– I ) = (π‘₯ βˆ– I ))
176175dmeqd 5904 . . . . . 6 (𝑦 = π‘₯ β†’ dom (𝑦 βˆ– I ) = dom (π‘₯ βˆ– I ))
17731, 32, 166, 169, 172, 174, 176indcardi 10033 . . . . 5 (dom (π‘₯ βˆ– I ) ∈ Fin β†’ (π‘₯ ∈ 𝐡 β†’ π‘₯ ∈ (πΎβ€˜π‘‡)))
178177impcom 409 . . . 4 ((π‘₯ ∈ 𝐡 ∧ dom (π‘₯ βˆ– I ) ∈ Fin) β†’ π‘₯ ∈ (πΎβ€˜π‘‡))
1791783adant1 1131 . . 3 ((𝐷 ∈ 𝑉 ∧ π‘₯ ∈ 𝐡 ∧ dom (π‘₯ βˆ– I ) ∈ Fin) β†’ π‘₯ ∈ (πΎβ€˜π‘‡))
180179rabssdv 4072 . 2 (𝐷 ∈ 𝑉 β†’ {π‘₯ ∈ 𝐡 ∣ dom (π‘₯ βˆ– I ) ∈ Fin} βŠ† (πΎβ€˜π‘‡))
18129, 180eqssd 3999 1 (𝐷 ∈ 𝑉 β†’ (πΎβ€˜π‘‡) = {π‘₯ ∈ 𝐡 ∣ dom (π‘₯ βˆ– I ) ∈ Fin})
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397  βˆ€wal 1540   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107   β‰  wne 2941  {crab 3433  Vcvv 3475   βˆ– cdif 3945   βˆͺ cun 3946   βŠ† wss 3948   ⊊ wpss 3949  βˆ…c0 4322  {csn 4628  {cpr 4630   class class class wbr 5148   I cid 5573  dom cdm 5676  ran crn 5677   β†Ύ cres 5678   ∘ ccom 5680   Fn wfn 6536  βŸΆwf 6537  β€“1-1-ontoβ†’wf1o 6540  β€˜cfv 6541  (class class class)co 7406  Ο‰com 7852  2oc2o 8457   β‰ˆ cen 8933   β‰Ό cdom 8934   β‰Ί csdm 8935  Fincfn 8936  Basecbs 17141  +gcplusg 17194  0gc0g 17382  Moorecmre 17523  mrClscmrc 17524  ACScacs 17526  Mndcmnd 18622  SubMndcsubmnd 18667  Grpcgrp 18816  SubGrpcsubg 18995  SymGrpcsymg 19229  pmTrspcpmtr 19304
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-isom 6550  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-1st 7972  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-2o 8464  df-er 8700  df-map 8819  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-card 9931  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-5 12275  df-6 12276  df-7 12277  df-8 12278  df-9 12279  df-n0 12470  df-z 12556  df-uz 12820  df-fz 13482  df-struct 17077  df-sets 17094  df-slot 17112  df-ndx 17124  df-base 17142  df-ress 17171  df-plusg 17207  df-tset 17213  df-0g 17384  df-mre 17527  df-mrc 17528  df-acs 17530  df-mgm 18558  df-sgrp 18607  df-mnd 18623  df-submnd 18669  df-efmnd 18747  df-grp 18819  df-minusg 18820  df-subg 18998  df-symg 19230  df-pmtr 19305
This theorem is referenced by:  symggen2  19334  psgneldm2  19367
  Copyright terms: Public domain W3C validator