MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  symggen Structured version   Visualization version   GIF version
Theorem symggen 19338
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 19268 . . . . . 6 (𝐷 ∈ V β†’ 𝐺 ∈ Grp)
43grpmndd 18832 . . . . 5 (𝐷 ∈ V β†’ 𝐺 ∈ Mnd)
5 symgtrf.b . . . . . 6 𝐡 = (Baseβ€˜πΊ)
65submacs 18708 . . . . 5 (𝐺 ∈ Mnd β†’ (SubMndβ€˜πΊ) ∈ (ACSβ€˜π΅))
7 acsmre 17596 . . . . 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 19337 . . . . 5 𝑇 βŠ† 𝐡
1211a1i 11 . . . 4 (𝐷 ∈ 𝑉 β†’ 𝑇 βŠ† 𝐡)
13 2onn 8641 . . . . . 6 2o ∈ Ο‰
14 nnfi 9167 . . . . . 6 (2o ∈ Ο‰ β†’ 2o ∈ Fin)
1513, 14ax-mp 5 . . . . 5 2o ∈ Fin
16 eqid 2733 . . . . . . . . 9 (pmTrspβ€˜π·) = (pmTrspβ€˜π·)
1716, 10pmtrfb 19333 . . . . . . . 8 (π‘₯ ∈ 𝑇 ↔ (𝐷 ∈ V ∧ π‘₯:𝐷–1-1-onto→𝐷 ∧ dom (π‘₯ βˆ– I ) β‰ˆ 2o))
1817simp3bi 1148 . . . . . . 7 (π‘₯ ∈ 𝑇 β†’ dom (π‘₯ βˆ– I ) β‰ˆ 2o)
19 enfi 9190 . . . . . . 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 4072 . . 3 (𝐷 ∈ 𝑉 β†’ 𝑇 βŠ† {π‘₯ ∈ 𝐡 ∣ dom (π‘₯ βˆ– I ) ∈ Fin})
242, 5symgfisg 19336 . . . 4 (𝐷 ∈ 𝑉 β†’ {π‘₯ ∈ 𝐡 ∣ dom (π‘₯ βˆ– I ) ∈ Fin} ∈ (SubGrpβ€˜πΊ))
25 subgsubm 19028 . . . 4 ({π‘₯ ∈ 𝐡 ∣ dom (π‘₯ βˆ– I ) ∈ Fin} ∈ (SubGrpβ€˜πΊ) β†’ {π‘₯ ∈ 𝐡 ∣ dom (π‘₯ βˆ– I ) ∈ Fin} ∈ (SubMndβ€˜πΊ))
2624, 25syl 17 . . 3 (𝐷 ∈ 𝑉 β†’ {π‘₯ ∈ 𝐡 ∣ dom (π‘₯ βˆ– I ) ∈ Fin} ∈ (SubMndβ€˜πΊ))
27 symggen.k . . . 4 𝐾 = (mrClsβ€˜(SubMndβ€˜πΊ))
2827mrcsscl 17564 . . 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 9943 . . . . . 6 (dom (π‘₯ βˆ– I ) ∈ Fin β†’ dom (π‘₯ βˆ– I ) ∈ dom card)
33 domfi 9192 . . . . . . . 8 ((dom (π‘₯ βˆ– I ) ∈ Fin ∧ dom (𝑦 βˆ– I ) β‰Ό dom (π‘₯ βˆ– I )) β†’ dom (𝑦 βˆ– I ) ∈ Fin)
342, 5symgbasf1o 19242 . . . . . . . . . . . . . . 15 (𝑦 ∈ 𝐡 β†’ 𝑦:𝐷–1-1-onto→𝐷)
3534adantl 483 . . . . . . . . . . . . . 14 ((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) β†’ 𝑦:𝐷–1-1-onto→𝐷)
36 f1ofn 6835 . . . . . . . . . . . . . 14 (𝑦:𝐷–1-1-onto→𝐷 β†’ 𝑦 Fn 𝐷)
37 fnnfpeq0 7176 . . . . . . . . . . . . . 14 (𝑦 Fn 𝐷 β†’ (dom (𝑦 βˆ– I ) = βˆ… ↔ 𝑦 = ( I β†Ύ 𝐷)))
3835, 36, 373syl 18 . . . . . . . . . . . . 13 ((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) β†’ (dom (𝑦 βˆ– I ) = βˆ… ↔ 𝑦 = ( I β†Ύ 𝐷)))
392, 5elbasfv 17150 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ 𝐡 β†’ 𝐷 ∈ V)
4039adantl 483 . . . . . . . . . . . . . . . 16 ((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) β†’ 𝐷 ∈ V)
412symgid 19269 . . . . . . . . . . . . . . . 16 (𝐷 ∈ V β†’ ( I β†Ύ 𝐷) = (0gβ€˜πΊ))
4240, 41syl 17 . . . . . . . . . . . . . . 15 ((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) β†’ ( I β†Ύ 𝐷) = (0gβ€˜πΊ))
4340, 8syl 17 . . . . . . . . . . . . . . . . 17 ((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) β†’ (SubMndβ€˜πΊ) ∈ (Mooreβ€˜π΅))
4427mrccl 17555 . . . . . . . . . . . . . . . . 17 (((SubMndβ€˜πΊ) ∈ (Mooreβ€˜π΅) ∧ 𝑇 βŠ† 𝐡) β†’ (πΎβ€˜π‘‡) ∈ (SubMndβ€˜πΊ))
4543, 11, 44sylancl 587 . . . . . . . . . . . . . . . 16 ((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) β†’ (πΎβ€˜π‘‡) ∈ (SubMndβ€˜πΊ))
46 eqid 2733 . . . . . . . . . . . . . . . . 17 (0gβ€˜πΊ) = (0gβ€˜πΊ)
4746subm0cl 18692 . . . . . . . . . . . . . . . 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 4347 . . . . . . . . . . . 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 19311 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦:𝐷–1-1-onto→𝐷 ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (π‘¦β€˜π‘’) ∈ (dom (𝑦 βˆ– I ) βˆ– {𝑒}))
5835, 57sylan 581 . . . . . . . . . . . . . . . . . . . . . . . 24 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (π‘¦β€˜π‘’) ∈ (dom (𝑦 βˆ– I ) βˆ– {𝑒}))
5958eldifad 3961 . . . . . . . . . . . . . . . . . . . . . . 23 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (π‘¦β€˜π‘’) ∈ dom (𝑦 βˆ– I ))
6056, 59prssd 4826 . . . . . . . . . . . . . . . . . . . . . 22 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ {𝑒, (π‘¦β€˜π‘’)} βŠ† dom (𝑦 βˆ– I ))
61 difss 4132 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 βˆ– I ) βŠ† 𝑦
62 dmss 5903 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 βˆ– I ) βŠ† 𝑦 β†’ dom (𝑦 βˆ– I ) βŠ† dom 𝑦)
6361, 62ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 dom (𝑦 βˆ– I ) βŠ† dom 𝑦
64 f1odm 6838 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦:𝐷–1-1-onto→𝐷 β†’ dom 𝑦 = 𝐷)
6535, 64syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) β†’ dom 𝑦 = 𝐷)
6663, 65sseqtrid 4035 . . . . . . . . . . . . . . . . . . . . . . 23 ((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) β†’ dom (𝑦 βˆ– I ) βŠ† 𝐷)
6766adantr 482 . . . . . . . . . . . . . . . . . . . . . 22 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ dom (𝑦 βˆ– I ) βŠ† 𝐷)
6860, 67sstrd 3993 . . . . . . . . . . . . . . . . . . . . 21 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ {𝑒, (π‘¦β€˜π‘’)} βŠ† 𝐷)
69 vex 3479 . . . . . . . . . . . . . . . . . . . . . 22 𝑒 ∈ V
70 fvex 6905 . . . . . . . . . . . . . . . . . . . . . 22 (π‘¦β€˜π‘’) ∈ V
7135adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ 𝑦:𝐷–1-1-onto→𝐷)
7271, 36syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ 𝑦 Fn 𝐷)
7366sselda 3983 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ 𝑒 ∈ 𝐷)
74 fnelnfp 7175 . . . . . . . . . . . . . . . . . . . . . . . . 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 9997 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑒 ∈ V ∧ (π‘¦β€˜π‘’) ∈ V ∧ 𝑒 β‰  (π‘¦β€˜π‘’)) β†’ {𝑒, (π‘¦β€˜π‘’)} β‰ˆ 2o)
7969, 70, 77, 78mp3an12i 1466 . . . . . . . . . . . . . . . . . . . . 21 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ {𝑒, (π‘¦β€˜π‘’)} β‰ˆ 2o)
8016, 10pmtrrn 19325 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷 ∈ V ∧ {𝑒, (π‘¦β€˜π‘’)} βŠ† 𝐷 ∧ {𝑒, (π‘¦β€˜π‘’)} β‰ˆ 2o) β†’ ((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∈ 𝑇)
8155, 68, 79, 80syl3anc 1372 . . . . . . . . . . . . . . . . . . . 20 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ ((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∈ 𝑇)
8211, 81sselid 3981 . . . . . . . . . . . . . . . . . . 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 19251 . . . . . . . . . . . . . . . . . . 19 ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∈ 𝐡 ∧ 𝑦 ∈ 𝐡) β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) = (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦))
8682, 83, 85syl2anc 585 . . . . . . . . . . . . . . . . . 18 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) = (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦))
8786oveq2d 7425 . . . . . . . . . . . . . . . . 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 18827 . . . . . . . . . . . . . . . . . . . 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 19251 . . . . . . . . . . . . . . . . . 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 6265 . . . . . . . . . . . . . . . . . 18 ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ ((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})) ∘ 𝑦) = (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦))
9616, 10pmtrfinv 19329 . . . . . . . . . . . . . . . . . . . . 21 (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∈ 𝑇 β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ ((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})) = ( I β†Ύ 𝐷))
9781, 96syl 17 . . . . . . . . . . . . . . . . . . . 20 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ ((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})) = ( I β†Ύ 𝐷))
9897coeq1d 5862 . . . . . . . . . . . . . . . . . . 19 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ ((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})) ∘ 𝑦) = (( I β†Ύ 𝐷) ∘ 𝑦))
99 f1of 6834 . . . . . . . . . . . . . . . . . . . 20 (𝑦:𝐷–1-1-onto→𝐷 β†’ 𝑦:𝐷⟢𝐷)
100 fcoi2 6767 . . . . . . . . . . . . . . . . . . . 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 17561 . . . . . . . . . . . . . . . . . . . 20 (((SubMndβ€˜πΊ) ∈ (Mooreβ€˜π΅) ∧ 𝑇 βŠ† 𝐡) β†’ 𝑇 βŠ† (πΎβ€˜π‘‡))
10843, 11, 107sylancl 587 . . . . . . . . . . . . . . . . . . 19 ((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) β†’ 𝑇 βŠ† (πΎβ€˜π‘‡))
109108adantr 482 . . . . . . . . . . . . . . . . . 18 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ 𝑇 βŠ† (πΎβ€˜π‘‡))
110109, 81sseldd 3984 . . . . . . . . . . . . . . . . 17 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ ((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∈ (πΎβ€˜π‘‡))
111110adantlr 714 . . . . . . . . . . . . . . . 16 ((((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ βˆ€π‘§(dom (𝑧 βˆ– I ) β‰Ί dom (𝑦 βˆ– I ) β†’ (𝑧 ∈ 𝐡 β†’ 𝑧 ∈ (πΎβ€˜π‘‡)))) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ ((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∈ (πΎβ€˜π‘‡))
11286difeq1d 4122 . . . . . . . . . . . . . . . . . . . 20 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) βˆ– I ) = ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦) βˆ– I ))
113112dmeqd 5906 . . . . . . . . . . . . . . . . . . 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 19313 . . . . . . . . . . . . . . . . . . . . . 22 dom ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦) βˆ– I ) βŠ† (dom (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) βˆ– I ) βˆͺ dom (𝑦 βˆ– I ))
11616pmtrmvd 19324 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐷 ∈ V ∧ {𝑒, (π‘¦β€˜π‘’)} βŠ† 𝐷 ∧ {𝑒, (π‘¦β€˜π‘’)} β‰ˆ 2o) β†’ dom (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) βˆ– I ) = {𝑒, (π‘¦β€˜π‘’)})
11755, 68, 79, 116syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . 24 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ dom (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) βˆ– I ) = {𝑒, (π‘¦β€˜π‘’)})
118117, 60eqsstrd 4021 . . . . . . . . . . . . . . . . . . . . . . 23 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ dom (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) βˆ– I ) βŠ† dom (𝑦 βˆ– I ))
119 ssidd 4006 . . . . . . . . . . . . . . . . . . . . . . 23 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ dom (𝑦 βˆ– I ) βŠ† dom (𝑦 βˆ– I ))
120118, 119unssd 4187 . . . . . . . . . . . . . . . . . . . . . 22 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (dom (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) βˆ– I ) βˆͺ dom (𝑦 βˆ– I )) βŠ† dom (𝑦 βˆ– I ))
121115, 120sstrid 3994 . . . . . . . . . . . . . . . . . . . . 21 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ dom ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦) βˆ– I ) βŠ† dom (𝑦 βˆ– I ))
122 fvco2 6989 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 Fn 𝐷 ∧ 𝑒 ∈ 𝐷) β†’ ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦)β€˜π‘’) = (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})β€˜(π‘¦β€˜π‘’)))
12372, 73, 122syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . 23 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦)β€˜π‘’) = (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})β€˜(π‘¦β€˜π‘’)))
124 prcom 4737 . . . . . . . . . . . . . . . . . . . . . . . . . 26 {𝑒, (π‘¦β€˜π‘’)} = {(π‘¦β€˜π‘’), 𝑒}
125124fveq2i 6895 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) = ((pmTrspβ€˜π·)β€˜{(π‘¦β€˜π‘’), 𝑒})
126125fveq1i 6893 . . . . . . . . . . . . . . . . . . . . . . . 24 (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})β€˜(π‘¦β€˜π‘’)) = (((pmTrspβ€˜π·)β€˜{(π‘¦β€˜π‘’), 𝑒})β€˜(π‘¦β€˜π‘’))
12767, 59sseldd 3984 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (π‘¦β€˜π‘’) ∈ 𝐷)
12816pmtrprfv 19321 . . . . . . . . . . . . . . . . . . . . . . . . 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 19242 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦) ∈ 𝐡 β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦):𝐷–1-1-onto→𝐷)
133 f1ofn 6835 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦):𝐷–1-1-onto→𝐷 β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦) Fn 𝐷)
13492, 132, 1333syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦) Fn 𝐷)
135 fnelnfp 7175 . . . . . . . . . . . . . . . . . . . . . . . 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 4113 . . . . . . . . . . . . . . . . . . . 20 (((dom (𝑦 βˆ– I ) ∈ Fin ∧ 𝑦 ∈ 𝐡) ∧ 𝑒 ∈ dom (𝑦 βˆ– I )) β†’ dom ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)}) ∘ 𝑦) βˆ– I ) ⊊ dom (𝑦 βˆ– I ))
140 php3 9212 . . . . . . . . . . . . . . . . . . . 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 5171 . . . . . . . . . . . . . . . . . 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 7442 . . . . . . . . . . . . . . . . . . 19 (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) ∈ V
146 difeq1 4116 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) β†’ (𝑧 βˆ– I ) = ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) βˆ– I ))
147146dmeqd 5906 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = (((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) β†’ dom (𝑧 βˆ– I ) = dom ((((pmTrspβ€˜π·)β€˜{𝑒, (π‘¦β€˜π‘’)})(+gβ€˜πΊ)𝑦) βˆ– I ))
148147breq1d 5159 . . . . . . . . . . . . . . . . . . . 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 18693 . . . . . . . . . . . . . . . 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 4116 . . . . . . 7 (𝑦 = 𝑧 β†’ (𝑦 βˆ– I ) = (𝑧 βˆ– I ))
174173dmeqd 5906 . . . . . 6 (𝑦 = 𝑧 β†’ dom (𝑦 βˆ– I ) = dom (𝑧 βˆ– I ))
175 difeq1 4116 . . . . . . 7 (𝑦 = π‘₯ β†’ (𝑦 βˆ– I ) = (π‘₯ βˆ– I ))
176175dmeqd 5906 . . . . . 6 (𝑦 = π‘₯ β†’ dom (𝑦 βˆ– I ) = dom (π‘₯ βˆ– I ))
17731, 32, 166, 169, 172, 174, 176indcardi 10036 . . . . 5 (dom (π‘₯ βˆ– I ) ∈ Fin β†’ (π‘₯ ∈ 𝐡 β†’ π‘₯ ∈ (πΎβ€˜π‘‡)))
178177impcom 409 . . . 4 ((π‘₯ ∈ 𝐡 ∧ dom (π‘₯ βˆ– I ) ∈ Fin) β†’ π‘₯ ∈ (πΎβ€˜π‘‡))
1791783adant1 1131 . . 3 ((𝐷 ∈ 𝑉 ∧ π‘₯ ∈ 𝐡 ∧ dom (π‘₯ βˆ– I ) ∈ Fin) β†’ π‘₯ ∈ (πΎβ€˜π‘‡))
180179rabssdv 4073 . 2 (𝐷 ∈ 𝑉 β†’ {π‘₯ ∈ 𝐡 ∣ dom (π‘₯ βˆ– I ) ∈ Fin} βŠ† (πΎβ€˜π‘‡))
18129, 180eqssd 4000 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 3946   βˆͺ cun 3947   βŠ† wss 3949   ⊊ wpss 3950  βˆ…c0 4323  {csn 4629  {cpr 4631   class class class wbr 5149   I cid 5574  dom cdm 5677  ran crn 5678   β†Ύ cres 5679   ∘ ccom 5681   Fn wfn 6539  βŸΆwf 6540  β€“1-1-ontoβ†’wf1o 6543  β€˜cfv 6544  (class class class)co 7409  Ο‰com 7855  2oc2o 8460   β‰ˆ cen 8936   β‰Ό cdom 8937   β‰Ί csdm 8938  Fincfn 8939  Basecbs 17144  +gcplusg 17197  0gc0g 17385  Moorecmre 17526  mrClscmrc 17527  ACScacs 17529  Mndcmnd 18625  SubMndcsubmnd 18670  Grpcgrp 18819  SubGrpcsubg 19000  SymGrpcsymg 19234  pmTrspcpmtr 19309
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 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187
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 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-2o 8467  df-er 8703  df-map 8822  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-nn 12213  df-2 12275  df-3 12276  df-4 12277  df-5 12278  df-6 12279  df-7 12280  df-8 12281  df-9 12282  df-n0 12473  df-z 12559  df-uz 12823  df-fz 13485  df-struct 17080  df-sets 17097  df-slot 17115  df-ndx 17127  df-base 17145  df-ress 17174  df-plusg 17210  df-tset 17216  df-0g 17387  df-mre 17530  df-mrc 17531  df-acs 17533  df-mgm 18561  df-sgrp 18610  df-mnd 18626  df-submnd 18672  df-efmnd 18750  df-grp 18822  df-minusg 18823  df-subg 19003  df-symg 19235  df-pmtr 19310
This theorem is referenced by:  symggen2  19339  psgneldm2  19372
  Copyright terms: Public domain W3C validator