Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  reprpmtf1o Structured version   Visualization version   GIF version

Theorem reprpmtf1o 34127
Description: Transposing 0 and 𝑋 maps representations with a condition on the first index to transpositions with the same condition on the index 𝑋. (Contributed by Thierry Arnoux, 27-Dec-2021.)
Hypotheses
Ref Expression
reprpmtf1o.s (πœ‘ β†’ 𝑆 ∈ β„•)
reprpmtf1o.m (πœ‘ β†’ 𝑀 ∈ β„€)
reprpmtf1o.a (πœ‘ β†’ 𝐴 βŠ† β„•)
reprpmtf1o.x (πœ‘ β†’ 𝑋 ∈ (0..^𝑆))
reprpmtf1o.o 𝑂 = {𝑐 ∈ (𝐴(reprβ€˜π‘†)𝑀) ∣ Β¬ (π‘β€˜0) ∈ 𝐡}
reprpmtf1o.p 𝑃 = {𝑐 ∈ (𝐴(reprβ€˜π‘†)𝑀) ∣ Β¬ (π‘β€˜π‘‹) ∈ 𝐡}
reprpmtf1o.t 𝑇 = if(𝑋 = 0, ( I β†Ύ (0..^𝑆)), ((pmTrspβ€˜(0..^𝑆))β€˜{𝑋, 0}))
reprpmtf1o.f 𝐹 = (𝑐 ∈ 𝑃 ↦ (𝑐 ∘ 𝑇))
Assertion
Ref Expression
reprpmtf1o (πœ‘ β†’ 𝐹:𝑃–1-1-onto→𝑂)
Distinct variable groups:   𝐴,𝑐   𝐡,𝑐   𝑀,𝑐   𝑃,𝑐   𝑆,𝑐   𝑇,𝑐   𝑋,𝑐   πœ‘,𝑐
Allowed substitution hints:   𝐹(𝑐)   𝑂(𝑐)

Proof of Theorem reprpmtf1o
Dummy variables π‘Ž 𝑏 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2724 . . . . 5 (𝐴 ↑m (0..^𝑆)) = (𝐴 ↑m (0..^𝑆))
2 eqid 2724 . . . . 5 (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) = (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇))
3 ovexd 7436 . . . . 5 (πœ‘ β†’ (0..^𝑆) ∈ V)
4 nnex 12215 . . . . . . 7 β„• ∈ V
54a1i 11 . . . . . 6 (πœ‘ β†’ β„• ∈ V)
6 reprpmtf1o.a . . . . . 6 (πœ‘ β†’ 𝐴 βŠ† β„•)
75, 6ssexd 5314 . . . . 5 (πœ‘ β†’ 𝐴 ∈ V)
8 reprpmtf1o.x . . . . . 6 (πœ‘ β†’ 𝑋 ∈ (0..^𝑆))
9 reprpmtf1o.s . . . . . . 7 (πœ‘ β†’ 𝑆 ∈ β„•)
10 lbfzo0 13669 . . . . . . 7 (0 ∈ (0..^𝑆) ↔ 𝑆 ∈ β„•)
119, 10sylibr 233 . . . . . 6 (πœ‘ β†’ 0 ∈ (0..^𝑆))
12 reprpmtf1o.t . . . . . 6 𝑇 = if(𝑋 = 0, ( I β†Ύ (0..^𝑆)), ((pmTrspβ€˜(0..^𝑆))β€˜{𝑋, 0}))
133, 8, 11, 12pmtridf1o 32721 . . . . 5 (πœ‘ β†’ 𝑇:(0..^𝑆)–1-1-ontoβ†’(0..^𝑆))
141, 1, 2, 3, 3, 7, 13fmptco1f1o 32326 . . . 4 (πœ‘ β†’ (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)):(𝐴 ↑m (0..^𝑆))–1-1-ontoβ†’(𝐴 ↑m (0..^𝑆)))
15 f1of1 6822 . . . 4 ((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)):(𝐴 ↑m (0..^𝑆))–1-1-ontoβ†’(𝐴 ↑m (0..^𝑆)) β†’ (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)):(𝐴 ↑m (0..^𝑆))–1-1β†’(𝐴 ↑m (0..^𝑆)))
1614, 15syl 17 . . 3 (πœ‘ β†’ (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)):(𝐴 ↑m (0..^𝑆))–1-1β†’(𝐴 ↑m (0..^𝑆)))
17 ssrab2 4069 . . . . . 6 {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜π‘Ž) = 𝑀} βŠ† (𝐴 ↑m (0..^𝑆))
18 reprpmtf1o.p . . . . . . . . . 10 𝑃 = {𝑐 ∈ (𝐴(reprβ€˜π‘†)𝑀) ∣ Β¬ (π‘β€˜π‘‹) ∈ 𝐡}
1918ssrab3 4072 . . . . . . . . 9 𝑃 βŠ† (𝐴(reprβ€˜π‘†)𝑀)
2019a1i 11 . . . . . . . 8 (πœ‘ β†’ 𝑃 βŠ† (𝐴(reprβ€˜π‘†)𝑀))
21 reprpmtf1o.m . . . . . . . . 9 (πœ‘ β†’ 𝑀 ∈ β„€)
229nnnn0d 12529 . . . . . . . . 9 (πœ‘ β†’ 𝑆 ∈ β„•0)
236, 21, 22reprval 34111 . . . . . . . 8 (πœ‘ β†’ (𝐴(reprβ€˜π‘†)𝑀) = {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜π‘Ž) = 𝑀})
2420, 23sseqtrd 4014 . . . . . . 7 (πœ‘ β†’ 𝑃 βŠ† {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜π‘Ž) = 𝑀})
2524sselda 3974 . . . . . 6 ((πœ‘ ∧ 𝑐 ∈ 𝑃) β†’ 𝑐 ∈ {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜π‘Ž) = 𝑀})
2617, 25sselid 3972 . . . . 5 ((πœ‘ ∧ 𝑐 ∈ 𝑃) β†’ 𝑐 ∈ (𝐴 ↑m (0..^𝑆)))
2726ex 412 . . . 4 (πœ‘ β†’ (𝑐 ∈ 𝑃 β†’ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))))
2827ssrdv 3980 . . 3 (πœ‘ β†’ 𝑃 βŠ† (𝐴 ↑m (0..^𝑆)))
29 f1ores 6837 . . 3 (((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)):(𝐴 ↑m (0..^𝑆))–1-1β†’(𝐴 ↑m (0..^𝑆)) ∧ 𝑃 βŠ† (𝐴 ↑m (0..^𝑆))) β†’ ((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) β†Ύ 𝑃):𝑃–1-1-ontoβ†’((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) β€œ 𝑃))
3016, 28, 29syl2anc 583 . 2 (πœ‘ β†’ ((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) β†Ύ 𝑃):𝑃–1-1-ontoβ†’((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) β€œ 𝑃))
31 resmpt 6027 . . . . 5 (𝑃 βŠ† (𝐴 ↑m (0..^𝑆)) β†’ ((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) β†Ύ 𝑃) = (𝑐 ∈ 𝑃 ↦ (𝑐 ∘ 𝑇)))
3228, 31syl 17 . . . 4 (πœ‘ β†’ ((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) β†Ύ 𝑃) = (𝑐 ∈ 𝑃 ↦ (𝑐 ∘ 𝑇)))
33 reprpmtf1o.f . . . 4 𝐹 = (𝑐 ∈ 𝑃 ↦ (𝑐 ∘ 𝑇))
3432, 33eqtr4di 2782 . . 3 (πœ‘ β†’ ((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) β†Ύ 𝑃) = 𝐹)
35 eqidd 2725 . . 3 (πœ‘ β†’ 𝑃 = 𝑃)
36 vex 3470 . . . . . . . . 9 𝑑 ∈ V
3736a1i 11 . . . . . . . 8 (πœ‘ β†’ 𝑑 ∈ V)
382, 37, 28elimampt 32331 . . . . . . 7 (πœ‘ β†’ (𝑑 ∈ ((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) β€œ 𝑃) ↔ βˆƒπ‘ ∈ 𝑃 𝑑 = (𝑐 ∘ 𝑇)))
39 simpr 484 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) β†’ 𝑑 = (𝑐 ∘ 𝑇))
40 f1of 6823 . . . . . . . . . . . . . . . . 17 ((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)):(𝐴 ↑m (0..^𝑆))–1-1-ontoβ†’(𝐴 ↑m (0..^𝑆)) β†’ (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)):(𝐴 ↑m (0..^𝑆))⟢(𝐴 ↑m (0..^𝑆)))
4114, 40syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)):(𝐴 ↑m (0..^𝑆))⟢(𝐴 ↑m (0..^𝑆)))
4241ad2antrr 723 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) β†’ (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)):(𝐴 ↑m (0..^𝑆))⟢(𝐴 ↑m (0..^𝑆)))
432fmpt 7101 . . . . . . . . . . . . . . 15 (βˆ€π‘ ∈ (𝐴 ↑m (0..^𝑆))(𝑐 ∘ 𝑇) ∈ (𝐴 ↑m (0..^𝑆)) ↔ (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)):(𝐴 ↑m (0..^𝑆))⟢(𝐴 ↑m (0..^𝑆)))
4442, 43sylibr 233 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) β†’ βˆ€π‘ ∈ (𝐴 ↑m (0..^𝑆))(𝑐 ∘ 𝑇) ∈ (𝐴 ↑m (0..^𝑆)))
4526adantr 480 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) β†’ 𝑐 ∈ (𝐴 ↑m (0..^𝑆)))
46 rspa 3237 . . . . . . . . . . . . . 14 ((βˆ€π‘ ∈ (𝐴 ↑m (0..^𝑆))(𝑐 ∘ 𝑇) ∈ (𝐴 ↑m (0..^𝑆)) ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) β†’ (𝑐 ∘ 𝑇) ∈ (𝐴 ↑m (0..^𝑆)))
4744, 45, 46syl2anc 583 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) β†’ (𝑐 ∘ 𝑇) ∈ (𝐴 ↑m (0..^𝑆)))
4839, 47eqeltrd 2825 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) β†’ 𝑑 ∈ (𝐴 ↑m (0..^𝑆)))
4939adantr 480 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ 𝑑 = (𝑐 ∘ 𝑇))
5049fveq1d 6883 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ (π‘‘β€˜π‘Ž) = ((𝑐 ∘ 𝑇)β€˜π‘Ž))
51 f1ofun 6825 . . . . . . . . . . . . . . . . . . 19 (𝑇:(0..^𝑆)–1-1-ontoβ†’(0..^𝑆) β†’ Fun 𝑇)
5213, 51syl 17 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ Fun 𝑇)
5352ad2antrr 723 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ π‘Ž ∈ (0..^𝑆)) β†’ Fun 𝑇)
54 simpr 484 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ π‘Ž ∈ (0..^𝑆)) β†’ π‘Ž ∈ (0..^𝑆))
55 f1odm 6827 . . . . . . . . . . . . . . . . . . . 20 (𝑇:(0..^𝑆)–1-1-ontoβ†’(0..^𝑆) β†’ dom 𝑇 = (0..^𝑆))
5613, 55syl 17 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ dom 𝑇 = (0..^𝑆))
5756ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ π‘Ž ∈ (0..^𝑆)) β†’ dom 𝑇 = (0..^𝑆))
5854, 57eleqtrrd 2828 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ π‘Ž ∈ (0..^𝑆)) β†’ π‘Ž ∈ dom 𝑇)
59 fvco 6979 . . . . . . . . . . . . . . . . 17 ((Fun 𝑇 ∧ π‘Ž ∈ dom 𝑇) β†’ ((𝑐 ∘ 𝑇)β€˜π‘Ž) = (π‘β€˜(π‘‡β€˜π‘Ž)))
6053, 58, 59syl2anc 583 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ π‘Ž ∈ (0..^𝑆)) β†’ ((𝑐 ∘ 𝑇)β€˜π‘Ž) = (π‘β€˜(π‘‡β€˜π‘Ž)))
6160adantlr 712 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ ((𝑐 ∘ 𝑇)β€˜π‘Ž) = (π‘β€˜(π‘‡β€˜π‘Ž)))
6250, 61eqtrd 2764 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ (π‘‘β€˜π‘Ž) = (π‘β€˜(π‘‡β€˜π‘Ž)))
6362sumeq2dv 15646 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) β†’ Ξ£π‘Ž ∈ (0..^𝑆)(π‘‘β€˜π‘Ž) = Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜(π‘‡β€˜π‘Ž)))
64 fveq2 6881 . . . . . . . . . . . . . . 15 (𝑏 = (π‘‡β€˜π‘Ž) β†’ (π‘β€˜π‘) = (π‘β€˜(π‘‡β€˜π‘Ž)))
65 fzofi 13936 . . . . . . . . . . . . . . . 16 (0..^𝑆) ∈ Fin
6665a1i 11 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑐 ∈ 𝑃) β†’ (0..^𝑆) ∈ Fin)
6713adantr 480 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑐 ∈ 𝑃) β†’ 𝑇:(0..^𝑆)–1-1-ontoβ†’(0..^𝑆))
68 eqidd 2725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ π‘Ž ∈ (0..^𝑆)) β†’ (π‘‡β€˜π‘Ž) = (π‘‡β€˜π‘Ž))
696ad2antrr 723 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑏 ∈ (0..^𝑆)) β†’ 𝐴 βŠ† β„•)
706adantr 480 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑐 ∈ 𝑃) β†’ 𝐴 βŠ† β„•)
7121adantr 480 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑐 ∈ 𝑃) β†’ 𝑀 ∈ β„€)
7222adantr 480 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑐 ∈ 𝑃) β†’ 𝑆 ∈ β„•0)
7320sselda 3974 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑐 ∈ 𝑃) β†’ 𝑐 ∈ (𝐴(reprβ€˜π‘†)𝑀))
7470, 71, 72, 73reprf 34113 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑐 ∈ 𝑃) β†’ 𝑐:(0..^𝑆)⟢𝐴)
7574ffvelcdmda 7076 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑏 ∈ (0..^𝑆)) β†’ (π‘β€˜π‘) ∈ 𝐴)
7669, 75sseldd 3975 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑏 ∈ (0..^𝑆)) β†’ (π‘β€˜π‘) ∈ β„•)
7776nncnd 12225 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑏 ∈ (0..^𝑆)) β†’ (π‘β€˜π‘) ∈ β„‚)
7864, 66, 67, 68, 77fsumf1o 15666 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑐 ∈ 𝑃) β†’ Σ𝑏 ∈ (0..^𝑆)(π‘β€˜π‘) = Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜(π‘‡β€˜π‘Ž)))
7978adantr 480 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) β†’ Σ𝑏 ∈ (0..^𝑆)(π‘β€˜π‘) = Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜(π‘‡β€˜π‘Ž)))
8070, 71, 72, 73reprsum 34114 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑐 ∈ 𝑃) β†’ Σ𝑏 ∈ (0..^𝑆)(π‘β€˜π‘) = 𝑀)
8180adantr 480 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) β†’ Σ𝑏 ∈ (0..^𝑆)(π‘β€˜π‘) = 𝑀)
8263, 79, 813eqtr2d 2770 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) β†’ Ξ£π‘Ž ∈ (0..^𝑆)(π‘‘β€˜π‘Ž) = 𝑀)
83 fveq1 6880 . . . . . . . . . . . . . . 15 (𝑐 = 𝑑 β†’ (π‘β€˜π‘Ž) = (π‘‘β€˜π‘Ž))
8483sumeq2sdv 15647 . . . . . . . . . . . . . 14 (𝑐 = 𝑑 β†’ Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜π‘Ž) = Ξ£π‘Ž ∈ (0..^𝑆)(π‘‘β€˜π‘Ž))
8584eqeq1d 2726 . . . . . . . . . . . . 13 (𝑐 = 𝑑 β†’ (Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜π‘Ž) = 𝑀 ↔ Ξ£π‘Ž ∈ (0..^𝑆)(π‘‘β€˜π‘Ž) = 𝑀))
8685elrab 3675 . . . . . . . . . . . 12 (𝑑 ∈ {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜π‘Ž) = 𝑀} ↔ (𝑑 ∈ (𝐴 ↑m (0..^𝑆)) ∧ Ξ£π‘Ž ∈ (0..^𝑆)(π‘‘β€˜π‘Ž) = 𝑀))
8748, 82, 86sylanbrc 582 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) β†’ 𝑑 ∈ {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜π‘Ž) = 𝑀})
8823ad2antrr 723 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) β†’ (𝐴(reprβ€˜π‘†)𝑀) = {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜π‘Ž) = 𝑀})
8987, 88eleqtrrd 2828 . . . . . . . . . 10 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) β†’ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀))
9039fveq1d 6883 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) β†’ (π‘‘β€˜0) = ((𝑐 ∘ 𝑇)β€˜0))
9152ad2antrr 723 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) β†’ Fun 𝑇)
9211, 56eleqtrrd 2828 . . . . . . . . . . . . . 14 (πœ‘ β†’ 0 ∈ dom 𝑇)
9392ad2antrr 723 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) β†’ 0 ∈ dom 𝑇)
94 fvco 6979 . . . . . . . . . . . . 13 ((Fun 𝑇 ∧ 0 ∈ dom 𝑇) β†’ ((𝑐 ∘ 𝑇)β€˜0) = (π‘β€˜(π‘‡β€˜0)))
9591, 93, 94syl2anc 583 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) β†’ ((𝑐 ∘ 𝑇)β€˜0) = (π‘β€˜(π‘‡β€˜0)))
963, 8, 11, 12pmtridfv2 32723 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π‘‡β€˜0) = 𝑋)
9796ad2antrr 723 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) β†’ (π‘‡β€˜0) = 𝑋)
9897fveq2d 6885 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) β†’ (π‘β€˜(π‘‡β€˜0)) = (π‘β€˜π‘‹))
99 simpr 484 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑐 ∈ 𝑃) β†’ 𝑐 ∈ 𝑃)
10099, 18eleqtrdi 2835 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑐 ∈ 𝑃) β†’ 𝑐 ∈ {𝑐 ∈ (𝐴(reprβ€˜π‘†)𝑀) ∣ Β¬ (π‘β€˜π‘‹) ∈ 𝐡})
101 rabid 3444 . . . . . . . . . . . . . . . 16 (𝑐 ∈ {𝑐 ∈ (𝐴(reprβ€˜π‘†)𝑀) ∣ Β¬ (π‘β€˜π‘‹) ∈ 𝐡} ↔ (𝑐 ∈ (𝐴(reprβ€˜π‘†)𝑀) ∧ Β¬ (π‘β€˜π‘‹) ∈ 𝐡))
102100, 101sylib 217 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑐 ∈ 𝑃) β†’ (𝑐 ∈ (𝐴(reprβ€˜π‘†)𝑀) ∧ Β¬ (π‘β€˜π‘‹) ∈ 𝐡))
103102simprd 495 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑐 ∈ 𝑃) β†’ Β¬ (π‘β€˜π‘‹) ∈ 𝐡)
104103adantr 480 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) β†’ Β¬ (π‘β€˜π‘‹) ∈ 𝐡)
10598, 104eqneltrd 2845 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) β†’ Β¬ (π‘β€˜(π‘‡β€˜0)) ∈ 𝐡)
10695, 105eqneltrd 2845 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) β†’ Β¬ ((𝑐 ∘ 𝑇)β€˜0) ∈ 𝐡)
10790, 106eqneltrd 2845 . . . . . . . . . 10 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) β†’ Β¬ (π‘‘β€˜0) ∈ 𝐡)
10889, 107jca 511 . . . . . . . . 9 (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) β†’ (𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡))
109108r19.29an 3150 . . . . . . . 8 ((πœ‘ ∧ βˆƒπ‘ ∈ 𝑃 𝑑 = (𝑐 ∘ 𝑇)) β†’ (𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡))
1106adantr 480 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) β†’ 𝐴 βŠ† β„•)
11121adantr 480 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) β†’ 𝑀 ∈ β„€)
11222adantr 480 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) β†’ 𝑆 ∈ β„•0)
113 simpr 484 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) β†’ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀))
114110, 111, 112, 113reprf 34113 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) β†’ 𝑑:(0..^𝑆)⟢𝐴)
115 f1ocnv 6835 . . . . . . . . . . . . . . . . . . 19 (𝑇:(0..^𝑆)–1-1-ontoβ†’(0..^𝑆) β†’ ◑𝑇:(0..^𝑆)–1-1-ontoβ†’(0..^𝑆))
116 f1of 6823 . . . . . . . . . . . . . . . . . . 19 (◑𝑇:(0..^𝑆)–1-1-ontoβ†’(0..^𝑆) β†’ ◑𝑇:(0..^𝑆)⟢(0..^𝑆))
11713, 115, 1163syl 18 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ ◑𝑇:(0..^𝑆)⟢(0..^𝑆))
118117adantr 480 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) β†’ ◑𝑇:(0..^𝑆)⟢(0..^𝑆))
119 fco 6731 . . . . . . . . . . . . . . . . 17 ((𝑑:(0..^𝑆)⟢𝐴 ∧ ◑𝑇:(0..^𝑆)⟢(0..^𝑆)) β†’ (𝑑 ∘ ◑𝑇):(0..^𝑆)⟢𝐴)
120114, 118, 119syl2anc 583 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) β†’ (𝑑 ∘ ◑𝑇):(0..^𝑆)⟢𝐴)
121 elmapg 8829 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ V ∧ (0..^𝑆) ∈ V) β†’ ((𝑑 ∘ ◑𝑇) ∈ (𝐴 ↑m (0..^𝑆)) ↔ (𝑑 ∘ ◑𝑇):(0..^𝑆)⟢𝐴))
1227, 3, 121syl2anc 583 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((𝑑 ∘ ◑𝑇) ∈ (𝐴 ↑m (0..^𝑆)) ↔ (𝑑 ∘ ◑𝑇):(0..^𝑆)⟢𝐴))
123122adantr 480 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) β†’ ((𝑑 ∘ ◑𝑇) ∈ (𝐴 ↑m (0..^𝑆)) ↔ (𝑑 ∘ ◑𝑇):(0..^𝑆)⟢𝐴))
124120, 123mpbird 257 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) β†’ (𝑑 ∘ ◑𝑇) ∈ (𝐴 ↑m (0..^𝑆)))
125124adantr 480 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡) β†’ (𝑑 ∘ ◑𝑇) ∈ (𝐴 ↑m (0..^𝑆)))
126 f1ofun 6825 . . . . . . . . . . . . . . . . . . . 20 (◑𝑇:(0..^𝑆)–1-1-ontoβ†’(0..^𝑆) β†’ Fun ◑𝑇)
12713, 115, 1263syl 18 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ Fun ◑𝑇)
128127ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ Fun ◑𝑇)
129 simpr 484 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘Ž ∈ (0..^𝑆)) β†’ π‘Ž ∈ (0..^𝑆))
130 f1odm 6827 . . . . . . . . . . . . . . . . . . . . . 22 (◑𝑇:(0..^𝑆)–1-1-ontoβ†’(0..^𝑆) β†’ dom ◑𝑇 = (0..^𝑆))
13113, 115, 1303syl 18 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ dom ◑𝑇 = (0..^𝑆))
132131adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘Ž ∈ (0..^𝑆)) β†’ dom ◑𝑇 = (0..^𝑆))
133129, 132eleqtrrd 2828 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘Ž ∈ (0..^𝑆)) β†’ π‘Ž ∈ dom ◑𝑇)
134133adantlr 712 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ π‘Ž ∈ dom ◑𝑇)
135 fvco 6979 . . . . . . . . . . . . . . . . . 18 ((Fun ◑𝑇 ∧ π‘Ž ∈ dom ◑𝑇) β†’ ((𝑑 ∘ ◑𝑇)β€˜π‘Ž) = (π‘‘β€˜(β—‘π‘‡β€˜π‘Ž)))
136128, 134, 135syl2anc 583 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ ((𝑑 ∘ ◑𝑇)β€˜π‘Ž) = (π‘‘β€˜(β—‘π‘‡β€˜π‘Ž)))
137136sumeq2dv 15646 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) β†’ Ξ£π‘Ž ∈ (0..^𝑆)((𝑑 ∘ ◑𝑇)β€˜π‘Ž) = Ξ£π‘Ž ∈ (0..^𝑆)(π‘‘β€˜(β—‘π‘‡β€˜π‘Ž)))
138 fveq2 6881 . . . . . . . . . . . . . . . . 17 (𝑏 = (β—‘π‘‡β€˜π‘Ž) β†’ (π‘‘β€˜π‘) = (π‘‘β€˜(β—‘π‘‡β€˜π‘Ž)))
13965a1i 11 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) β†’ (0..^𝑆) ∈ Fin)
14013, 115syl 17 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ ◑𝑇:(0..^𝑆)–1-1-ontoβ†’(0..^𝑆))
141140adantr 480 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) β†’ ◑𝑇:(0..^𝑆)–1-1-ontoβ†’(0..^𝑆))
142 eqidd 2725 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ (β—‘π‘‡β€˜π‘Ž) = (β—‘π‘‡β€˜π‘Ž))
143110adantr 480 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) ∧ 𝑏 ∈ (0..^𝑆)) β†’ 𝐴 βŠ† β„•)
144114ffvelcdmda 7076 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) ∧ 𝑏 ∈ (0..^𝑆)) β†’ (π‘‘β€˜π‘) ∈ 𝐴)
145143, 144sseldd 3975 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) ∧ 𝑏 ∈ (0..^𝑆)) β†’ (π‘‘β€˜π‘) ∈ β„•)
146145nncnd 12225 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) ∧ 𝑏 ∈ (0..^𝑆)) β†’ (π‘‘β€˜π‘) ∈ β„‚)
147138, 139, 141, 142, 146fsumf1o 15666 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) β†’ Σ𝑏 ∈ (0..^𝑆)(π‘‘β€˜π‘) = Ξ£π‘Ž ∈ (0..^𝑆)(π‘‘β€˜(β—‘π‘‡β€˜π‘Ž)))
148110, 111, 112, 113reprsum 34114 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) β†’ Σ𝑏 ∈ (0..^𝑆)(π‘‘β€˜π‘) = 𝑀)
149137, 147, 1483eqtr2d 2770 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) β†’ Ξ£π‘Ž ∈ (0..^𝑆)((𝑑 ∘ ◑𝑇)β€˜π‘Ž) = 𝑀)
150149adantr 480 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡) β†’ Ξ£π‘Ž ∈ (0..^𝑆)((𝑑 ∘ ◑𝑇)β€˜π‘Ž) = 𝑀)
151 fveq1 6880 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑑 ∘ ◑𝑇) β†’ (π‘β€˜π‘Ž) = ((𝑑 ∘ ◑𝑇)β€˜π‘Ž))
152151sumeq2sdv 15647 . . . . . . . . . . . . . . . 16 (𝑐 = (𝑑 ∘ ◑𝑇) β†’ Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜π‘Ž) = Ξ£π‘Ž ∈ (0..^𝑆)((𝑑 ∘ ◑𝑇)β€˜π‘Ž))
153152eqeq1d 2726 . . . . . . . . . . . . . . 15 (𝑐 = (𝑑 ∘ ◑𝑇) β†’ (Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜π‘Ž) = 𝑀 ↔ Ξ£π‘Ž ∈ (0..^𝑆)((𝑑 ∘ ◑𝑇)β€˜π‘Ž) = 𝑀))
154153elrab 3675 . . . . . . . . . . . . . 14 ((𝑑 ∘ ◑𝑇) ∈ {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜π‘Ž) = 𝑀} ↔ ((𝑑 ∘ ◑𝑇) ∈ (𝐴 ↑m (0..^𝑆)) ∧ Ξ£π‘Ž ∈ (0..^𝑆)((𝑑 ∘ ◑𝑇)β€˜π‘Ž) = 𝑀))
155125, 150, 154sylanbrc 582 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡) β†’ (𝑑 ∘ ◑𝑇) ∈ {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜π‘Ž) = 𝑀})
15623ad2antrr 723 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡) β†’ (𝐴(reprβ€˜π‘†)𝑀) = {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Ξ£π‘Ž ∈ (0..^𝑆)(π‘β€˜π‘Ž) = 𝑀})
157155, 156eleqtrrd 2828 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡) β†’ (𝑑 ∘ ◑𝑇) ∈ (𝐴(reprβ€˜π‘†)𝑀))
158127ad2antrr 723 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡) β†’ Fun ◑𝑇)
1598, 131eleqtrrd 2828 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑋 ∈ dom ◑𝑇)
160159ad2antrr 723 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡) β†’ 𝑋 ∈ dom ◑𝑇)
161 fvco 6979 . . . . . . . . . . . . . 14 ((Fun ◑𝑇 ∧ 𝑋 ∈ dom ◑𝑇) β†’ ((𝑑 ∘ ◑𝑇)β€˜π‘‹) = (π‘‘β€˜(β—‘π‘‡β€˜π‘‹)))
162158, 160, 161syl2anc 583 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡) β†’ ((𝑑 ∘ ◑𝑇)β€˜π‘‹) = (π‘‘β€˜(β—‘π‘‡β€˜π‘‹)))
163 f1ocnvfv 7268 . . . . . . . . . . . . . . . . . 18 ((𝑇:(0..^𝑆)–1-1-ontoβ†’(0..^𝑆) ∧ 0 ∈ (0..^𝑆)) β†’ ((π‘‡β€˜0) = 𝑋 β†’ (β—‘π‘‡β€˜π‘‹) = 0))
164163imp 406 . . . . . . . . . . . . . . . . 17 (((𝑇:(0..^𝑆)–1-1-ontoβ†’(0..^𝑆) ∧ 0 ∈ (0..^𝑆)) ∧ (π‘‡β€˜0) = 𝑋) β†’ (β—‘π‘‡β€˜π‘‹) = 0)
16513, 11, 96, 164syl21anc 835 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (β—‘π‘‡β€˜π‘‹) = 0)
166165ad2antrr 723 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡) β†’ (β—‘π‘‡β€˜π‘‹) = 0)
167166fveq2d 6885 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡) β†’ (π‘‘β€˜(β—‘π‘‡β€˜π‘‹)) = (π‘‘β€˜0))
168 simpr 484 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡) β†’ Β¬ (π‘‘β€˜0) ∈ 𝐡)
169167, 168eqneltrd 2845 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡) β†’ Β¬ (π‘‘β€˜(β—‘π‘‡β€˜π‘‹)) ∈ 𝐡)
170162, 169eqneltrd 2845 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡) β†’ Β¬ ((𝑑 ∘ ◑𝑇)β€˜π‘‹) ∈ 𝐡)
171 fveq1 6880 . . . . . . . . . . . . . . 15 (𝑐 = (𝑑 ∘ ◑𝑇) β†’ (π‘β€˜π‘‹) = ((𝑑 ∘ ◑𝑇)β€˜π‘‹))
172171eleq1d 2810 . . . . . . . . . . . . . 14 (𝑐 = (𝑑 ∘ ◑𝑇) β†’ ((π‘β€˜π‘‹) ∈ 𝐡 ↔ ((𝑑 ∘ ◑𝑇)β€˜π‘‹) ∈ 𝐡))
173172notbid 318 . . . . . . . . . . . . 13 (𝑐 = (𝑑 ∘ ◑𝑇) β†’ (Β¬ (π‘β€˜π‘‹) ∈ 𝐡 ↔ Β¬ ((𝑑 ∘ ◑𝑇)β€˜π‘‹) ∈ 𝐡))
174173elrab 3675 . . . . . . . . . . . 12 ((𝑑 ∘ ◑𝑇) ∈ {𝑐 ∈ (𝐴(reprβ€˜π‘†)𝑀) ∣ Β¬ (π‘β€˜π‘‹) ∈ 𝐡} ↔ ((𝑑 ∘ ◑𝑇) ∈ (𝐴(reprβ€˜π‘†)𝑀) ∧ Β¬ ((𝑑 ∘ ◑𝑇)β€˜π‘‹) ∈ 𝐡))
175157, 170, 174sylanbrc 582 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡) β†’ (𝑑 ∘ ◑𝑇) ∈ {𝑐 ∈ (𝐴(reprβ€˜π‘†)𝑀) ∣ Β¬ (π‘β€˜π‘‹) ∈ 𝐡})
176175, 18eleqtrrdi 2836 . . . . . . . . . 10 (((πœ‘ ∧ 𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀)) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡) β†’ (𝑑 ∘ ◑𝑇) ∈ 𝑃)
177176anasss 466 . . . . . . . . 9 ((πœ‘ ∧ (𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡)) β†’ (𝑑 ∘ ◑𝑇) ∈ 𝑃)
178 simpr 484 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡)) ∧ 𝑐 = (𝑑 ∘ ◑𝑇)) β†’ 𝑐 = (𝑑 ∘ ◑𝑇))
179178coeq1d 5851 . . . . . . . . . 10 (((πœ‘ ∧ (𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡)) ∧ 𝑐 = (𝑑 ∘ ◑𝑇)) β†’ (𝑐 ∘ 𝑇) = ((𝑑 ∘ ◑𝑇) ∘ 𝑇))
180179eqeq2d 2735 . . . . . . . . 9 (((πœ‘ ∧ (𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡)) ∧ 𝑐 = (𝑑 ∘ ◑𝑇)) β†’ (𝑑 = (𝑐 ∘ 𝑇) ↔ 𝑑 = ((𝑑 ∘ ◑𝑇) ∘ 𝑇)))
181 f1ococnv1 6852 . . . . . . . . . . . . . 14 (𝑇:(0..^𝑆)–1-1-ontoβ†’(0..^𝑆) β†’ (◑𝑇 ∘ 𝑇) = ( I β†Ύ (0..^𝑆)))
18213, 181syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ (◑𝑇 ∘ 𝑇) = ( I β†Ύ (0..^𝑆)))
183182adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡)) β†’ (◑𝑇 ∘ 𝑇) = ( I β†Ύ (0..^𝑆)))
184183coeq2d 5852 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡)) β†’ (𝑑 ∘ (◑𝑇 ∘ 𝑇)) = (𝑑 ∘ ( I β†Ύ (0..^𝑆))))
185114adantrr 714 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡)) β†’ 𝑑:(0..^𝑆)⟢𝐴)
186 fcoi1 6755 . . . . . . . . . . . 12 (𝑑:(0..^𝑆)⟢𝐴 β†’ (𝑑 ∘ ( I β†Ύ (0..^𝑆))) = 𝑑)
187185, 186syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡)) β†’ (𝑑 ∘ ( I β†Ύ (0..^𝑆))) = 𝑑)
188184, 187eqtr2d 2765 . . . . . . . . . 10 ((πœ‘ ∧ (𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡)) β†’ 𝑑 = (𝑑 ∘ (◑𝑇 ∘ 𝑇)))
189 coass 6254 . . . . . . . . . 10 ((𝑑 ∘ ◑𝑇) ∘ 𝑇) = (𝑑 ∘ (◑𝑇 ∘ 𝑇))
190188, 189eqtr4di 2782 . . . . . . . . 9 ((πœ‘ ∧ (𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡)) β†’ 𝑑 = ((𝑑 ∘ ◑𝑇) ∘ 𝑇))
191177, 180, 190rspcedvd 3606 . . . . . . . 8 ((πœ‘ ∧ (𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡)) β†’ βˆƒπ‘ ∈ 𝑃 𝑑 = (𝑐 ∘ 𝑇))
192109, 191impbida 798 . . . . . . 7 (πœ‘ β†’ (βˆƒπ‘ ∈ 𝑃 𝑑 = (𝑐 ∘ 𝑇) ↔ (𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡)))
19338, 192bitrd 279 . . . . . 6 (πœ‘ β†’ (𝑑 ∈ ((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) β€œ 𝑃) ↔ (𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡)))
194 fveq1 6880 . . . . . . . . 9 (𝑐 = 𝑑 β†’ (π‘β€˜0) = (π‘‘β€˜0))
195194eleq1d 2810 . . . . . . . 8 (𝑐 = 𝑑 β†’ ((π‘β€˜0) ∈ 𝐡 ↔ (π‘‘β€˜0) ∈ 𝐡))
196195notbid 318 . . . . . . 7 (𝑐 = 𝑑 β†’ (Β¬ (π‘β€˜0) ∈ 𝐡 ↔ Β¬ (π‘‘β€˜0) ∈ 𝐡))
197196elrab 3675 . . . . . 6 (𝑑 ∈ {𝑐 ∈ (𝐴(reprβ€˜π‘†)𝑀) ∣ Β¬ (π‘β€˜0) ∈ 𝐡} ↔ (𝑑 ∈ (𝐴(reprβ€˜π‘†)𝑀) ∧ Β¬ (π‘‘β€˜0) ∈ 𝐡))
198193, 197bitr4di 289 . . . . 5 (πœ‘ β†’ (𝑑 ∈ ((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) β€œ 𝑃) ↔ 𝑑 ∈ {𝑐 ∈ (𝐴(reprβ€˜π‘†)𝑀) ∣ Β¬ (π‘β€˜0) ∈ 𝐡}))
199198eqrdv 2722 . . . 4 (πœ‘ β†’ ((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) β€œ 𝑃) = {𝑐 ∈ (𝐴(reprβ€˜π‘†)𝑀) ∣ Β¬ (π‘β€˜0) ∈ 𝐡})
200 reprpmtf1o.o . . . 4 𝑂 = {𝑐 ∈ (𝐴(reprβ€˜π‘†)𝑀) ∣ Β¬ (π‘β€˜0) ∈ 𝐡}
201199, 200eqtr4di 2782 . . 3 (πœ‘ β†’ ((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) β€œ 𝑃) = 𝑂)
20234, 35, 201f1oeq123d 6817 . 2 (πœ‘ β†’ (((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) β†Ύ 𝑃):𝑃–1-1-ontoβ†’((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) β€œ 𝑃) ↔ 𝐹:𝑃–1-1-onto→𝑂))
20330, 202mpbid 231 1 (πœ‘ β†’ 𝐹:𝑃–1-1-onto→𝑂)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   = wceq 1533   ∈ wcel 2098  βˆ€wral 3053  βˆƒwrex 3062  {crab 3424  Vcvv 3466   βŠ† wss 3940  ifcif 4520  {cpr 4622   ↦ cmpt 5221   I cid 5563  β—‘ccnv 5665  dom cdm 5666   β†Ύ cres 5668   β€œ cima 5669   ∘ ccom 5670  Fun wfun 6527  βŸΆwf 6529  β€“1-1β†’wf1 6530  β€“1-1-ontoβ†’wf1o 6532  β€˜cfv 6533  (class class class)co 7401   ↑m cmap 8816  Fincfn 8935  0cc0 11106  β„•cn 12209  β„•0cn0 12469  β„€cz 12555  ..^cfzo 13624  Ξ£csu 15629  pmTrspcpmtr 19351  reprcrepr 34109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-om 7849  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-er 8699  df-map 8818  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-sup 9433  df-oi 9501  df-card 9930  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-n0 12470  df-z 12556  df-uz 12820  df-rp 12972  df-fz 13482  df-fzo 13625  df-seq 13964  df-exp 14025  df-hash 14288  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-clim 15429  df-sum 15630  df-pmtr 19352  df-repr 34110
This theorem is referenced by:  hgt750lema  34158
  Copyright terms: Public domain W3C validator